Run original assertions during symbolic verification and validate generated harnesses

[KryptosAI]

Failed Foundry tests previously led to generated symbolic assertions that could lose the original setup and property. Run the original compiled tests under Halmos, retain exact test identities and counterexamples, and preserve a concrete fuzz violation even when symbolic execution disagrees or remains incomplete. Empty results, skipped tests, malformed path counts, timeouts and bounded loops cannot become successful verification.

Echidna and CVL exports now resolve concrete contract storage, report unsupported properties, and avoid tautological unsigned nonnegativity assertions. The Echidna regression executes the generated harness against correct and deliberately corrupt accounting. CI requires real Forge/Halmos integration and separately compiles the generated CVL with Certora without submitting a remote proof.

Both Forge and Halmos use native contract creation rather than Foundry 1.8's dynamic test linking, whose injected deployment cheatcode is unsupported by Halmos 0.3.3. Inconclusive bytecode checks retain their per-test status and diagnostic transcript.

Validation on this remote-main-based branch:

• Existing 35 end-to-end tests plus 9 new regressions pass, including real Forge/Halmos and generated Solidity execution; zero skipped integration tests.
• All 16 benchmark cases, 9 bytecode expectations and 28 leaderboard expectations pass.
• npm run test:cvl passes with Certora CLI 8.19.1 and Solidity 0.8.24.
• All six GitHub CI jobs pass at af7cf07, including the Node 18/20/22 matrix, mandatory real integration and bytecode checks, generated CVL compilation, and action smoke.

Halmos results remain bounded by its configured exploration limits. Stateful invariant sequence replay is explicitly unsupported. Exported coverage can be partial; the example CVL covers solvency, and remote Certora proof is still pending service access.