TG-6: WASM compilation preserves semantics (compiler-correctness theorem) #27

Source: PROOF-NARRATIVE.md §3 TG-6.

Claim

For every closed well-typed e, the source-level evaluation of e and the WASM execution of compile_to_wasm(e) agree on the observable result.

Why valuable

This is the compiler-correctness theorem for the WASM backend. Without it, the structural reasoning Tangle claims means "something" on the runtime is unverified. Currently a trust-us claim.

Aligns with the broader estate typed-wasm proof-debt arc (project_typed_wasm_proof_debt_post_a10) and the WasmCert-Isabelle tie-back referenced there.

Assumptions

• [[A-TG-6.1]] Standard WASM small-step semantics is well-defined (wasm-spec / WasmCert-Isabelle).
• [[A-TG-6.2]] Source semantics has no floating-point non-determinism (Tangle has only Int currently).

Acceptance criteria (research-grade; expect multiple PRs)

• Mechanise (in Lean) a small-step semantics for the WASM subset emitted by compile_to_wasm — or reuse WasmCert if it can be imported.
• State the bisimulation invariant: R(e, w) holds iff WASM state w represents source expression e.
• Prove forward bisimulation: R(e, w) ∧ e ⟶ e' ⟹ ∃ w'. w ⟶* w' ∧ R(e', w').
• Prove backward bisimulation: R(e, w) ∧ w ⟶ w' ⟹ ∃ e'. e ⟶* e' ∧ R(e', w').
• Corollary: observable equality.
• No new axiom/sorry/postulate.

Effort

3+ weeks (research-grade). Comparable to CompCert's WASM backend work. Should be staged:

1. State of the art audit (1w): see WasmCert-Isabelle, typed-wasm a13+ proofs.
2. Subset selection (1w): which WASM subset is actually emitted; restrict bisimulation accordingly.
3. Mechanisation (2-3w per phase).

Suggested phasing

• Phase A: Pure arithmetic (no braids). Prove that Add and Eq lower correctly.
• Phase B: BraidLit lowering. Bytewise equality between source AST and the WASM-emitted braid representation.
• Phase C: Compose and Tensor lowering. Algebraic equivalence using T-WidthAppend and T-WidthShift.
• Phase D: Close. The semantic move from word n to word 0.

Relationship to other obligations

• Depends on TG-2 (decidability of type checking) for the source-side termination of evaluation.
• Independent of TG-1 (let-binding) but the lowering should be extended in lockstep.

Out of scope

• WASM cross-platform determinism (covered by the WASM spec itself).
• Linking-level correctness (this is a single-module property).