Proof: WebAssembly backend semantic preservation (source ⇓ v ⟹ wasm ⇓ encode(v)) #520

Parent: #513

Statement

Prove semantic preservation for the WebAssembly backend in lib/codegen.ml:

For every closed AffineScript program e that evaluates to value v under the source operational semantics, the compiled WASM module compile(e) evaluates to a WASM value v' that is the WASM encoding of v.

⟨ e, σ ⟩ ⇓_{AS} v   ⟹   ⟨ compile(e), σ' ⟩ ⇓_{WASM} encode(v)

Mechanisation

Why3 (existing WASM proof literature uses Why3) or Coq (WasmCert-Coq has primitives we can pull from). Target: formal/Codegen/Wasm/{Lowering.v, Preservation.v}.

Subgoals (do these first, in order)

1. Match compilation soundness: emitted block/br_if discriminator sequence agrees with source match arm semantics (codegen: integer / lowers to floating-point division on the JS-family backends #478 issue ci: Bump actions/setup-node from 4.0.2 to 6.3.0 #1).
2. Struct-layout invariant: field offsets populated globally + propagated to params/returns/lets (codegen: integer / lowers to floating-point division on the JS-family backends #478 issue ci: Bump dtolnay/rust-toolchain from f7ccc83f9ed1e5b9c81d8a67d7ad1a747e22a561 to efa25f7f19611383d5b0ccf2d1c8914531636bf9 #2).
3. Indirect call ABI: call_indirect's type signature matches the source-level function type at the call site.
4. Linear-memory mutation: writes to compiled mut cells do not violate the borrow-graph soundness lemma (proven in Proof: borrow-graph soundness (no use-after-move + no conflict + BorrowOutlivesOwner) #515).

Reference

• WasmCert-Isabelle for the WASM operational semantics (#typed-wasm work has been adjacent — see PRs Cross-module imports: TopConst not threaded by gen_imports / flatten_imports #107/feat(codegen): thread imported TopConst across module boundaries (closes #107) #109/docs(coc): route conduct reports to OU address #115/Codegen: --vscode-extension flag to inline extraImports wiring #116/affine-vscode: align docs with --vscode-extension + npm publish manifest #117).
• Typed-WASM L7 (aliasing) / L10 (linearity) / L13 (module isolation) custom-section encoding — proven separately under the typed-wasm umbrella; this issue is the semantic preservation, not the isolation-fact encoding.

Size

XL. Estimate: 6+ weeks. The largest single proof on this list. Recommend splitting into the 4 subgoals above and shipping them as separate PRs.

Status

NOT STARTED.

🤖 Generated with Claude Code