Phase 1 / D2: round-trip soundness corpus — verify(codegen(parse(src))) == OK, ECHIDNA-enforced

[hyperpolymath]

Deliverable 2 of #49. A property-test corpus: for every valid .twasm source, verify(codegen(parse(src))) returns OK. This is the codegen regression net.

Scope

• Extend tests/echidna/echidna-harness.mjs (and/or tests/property/property_test.mjs) to drive parse → codegen → verify over the example corpus plus generated variants.
• Wire into CI so a codegen regression turns the corpus red.
• Differential fixtures (producer-emitted bytes) land in crates/typed-wasm-verify/tests/fixtures/c5_real/, exercised by cargo test -p typed-wasm-verify.

Acceptance

• The property holds across all six examples (and generated cases) in CI.
• A deliberately-broken codegen makes the corpus fail (negative control).

Dependencies

• Blocked by D1 (codegen across examples); ideally also D7 for the multi-module cases.

Deliverable: Phase 1 / deliverable 2 (docs/PRODUCTION-PATH.adoc §Phase 1). Part of #49.

[hyperpolymath]

The IR-level round-trip property corpus landed in #147 (merged b8ab31f): 512 deterministically-generated well-formed modules each satisfy verify(emit(m)) == OK — structural validation + verify_from_module (L7/L10) + verify_access_sites (L2) — and negative controls (double-free, &mut aliasing, leak) are rejected (crates/typed-wasm-codegen/tests/corpus.rs, no new deps).

Keeping this open for the source-level form the title implies — verify(codegen(parse(src))) over real .twasm sources — which awaits the front-end → IR parser seam (#127). Once that lands, the corpus generator can be fed parsed sources (and/or wired into the JS ECHIDNA harness driving tw build → tw-verify).

---

Generated by Claude Code