feat(tg-6): differential rung — execute generated wasm and check semantics

TG-6 differential rung. compiler/tangle-wasm/tests/differential.rs adds wasmi
(a pure-Rust wasm interpreter) as a DEV-dependency and executes the generated
wasm modules, supplying reference host primitives (tangle_rt.alloc_strands
initialises the identity strand array; tangle_rt.swap_strands swaps two cells).
It then checks the executed strand permutation equals an independent in-Rust
reference model over: the trefoil; non-commuting pairs (s1 s2 != s2 s1);
braid-relation pairs (s1 s2 s1 == s2 s1 s2); and a 5-strand weave.

This validates the wasm codegen against the braid permutation semantics --
catching wrong crossing indices, wrong generator call order, miscounted
strands, or a non-instantiable module. Honest scope: it is NOT a cross-binary
diff against compiler/lib/eval.ml, and the Markov-move helpers are not yet
exercised; a full source<->wasm bisimulation (WasmCert) remains research-grade.

The shipped backend keeps no runtime dependency (wasmi is dev-only). cargo test
green (10 existing unit tests + 2 differential). Docs: PROOF-NEEDS (TG-6 rung
landed), CHANGELOG, STATE.a2ml.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -38,7 +38,7 @@ milestones = [
   "DONE (TG-5): compositional PD-lowering preserves structural invariants + verbatim echo residue — compiler/test/tg5/tg5_invariants.ml (189 assertions in dune runtest)",
   "BLOCKED (TG-8): dialects are README-only — need one dialect implemented (AST+parser+HasType/Step+eval) before conservativity is even stateable",
   "RUNG-DONE (TG-7): out-of-band braid_equiv (Dehornoy handle reduction) in compiler/lib/braid_equiv.ml — decides braid-group equivalence WITHOUT changing == (compiler/test/tg7, 2220 assertions). Routing == through it stays an owner decision; Lean correctness research-grade.",
-  "BLOCKED (TG-6): no wasm runtime wired in — add wasmtime/wasmer dev-dep + exec harness before differential testing; full bisimulation research-grade",
+  "RUNG-DONE (TG-6): wasm differential — compiler/tangle-wasm/tests/differential.rs executes generated wasm via wasmi (dev-dep) and checks strand permutation == reference model (trefoil, non-commuting, braid-relation, 5-strand). Codegen-vs-semantics; not a cross-binary eval.ml diff; full bisimulation research-grade.",
 ]
 
 [blockers-and-issues]
@@ -48,11 +48,11 @@ issues = []
 actions = [
   "TG-7 OWNER DECISION (rung done): out-of-band braid_equiv now exists (compiler/lib/braid_equiv.ml). Decide whether to route `==`/Step.eqBraids through it (semantics change to eval.ml + Lean + proofs) or keep them list-equality and use braid_equiv only as a tool.",
   "TG-8 prerequisite: implement one dialect end-to-end (virtual-knot suggested) as the conservativity template; dialects are currently README-only.",
-  "TG-6 prerequisite: wire a wasm runtime (wasmtime/wasmer dev-dep) + exec harness to enable differential testing.",
+  "TG-6 (rung done): optional next rungs = cross-binary differential vs eval.ml; Markov-helper coverage; Lean/WasmCert bisimulation (research-grade).",
   "TangleIR Julia: implement EchoClosed node in KRLAdapter.jl per contract (quandledb session)",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-14T16:00:00Z"
+last-run-utc = "2026-06-14T17:00:00Z"
 last-result = "pass"               # unknown | pass | warn | fail
-notes = "dune build + dune test GREEN (incl. tg3 1008 + tg5 189 + tg7 2220 assertions); lean Tangle.lean 0 errors; proofs/check-tg3-differential.sh GREEN (496 obligations); TG-1+TG-2+TG-3+TG-5+TG-9+TG-10 LANDED; TG-7 non-semantic rung LANDED (braid_equiv, == unchanged); remaining: TG-8 blocked (dialects README-only), TG-6 blocked (no wasm runtime), TG-7 semantics change owner-gated; echo-types f7a965f grade semiring experimental (firewalled)"
+notes = "dune build + dune test GREEN (tg3 1008 + tg5 189 + tg7 2220); cargo test tangle-wasm GREEN (10 unit + 2 differential via wasmi); lean Tangle.lean 0 errors; proofs/check-tg3-differential.sh GREEN (496); LANDED: TG-1/2/3/5/9/10 + TG-6 differential rung + TG-7 non-semantic rung; remaining: TG-8 blocked (dialects README-only), TG-7 semantics change owner-gated, full WASM bisimulation research-grade; echo-types f7a965f grade semiring experimental (firewalled)"

CHANGELOG.md

@@ -13,6 +13,23 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### TG-6 (differential rung): execute generated wasm and check it preserves semantics
+
+- **`compiler/tangle-wasm/tests/differential.rs`** adds `wasmi` (a pure-Rust wasm
+  interpreter) as a dev-dependency and EXECUTES the generated wasm modules,
+  supplying reference host primitives (`tangle_rt.alloc_strands` initialises the
+  identity strand array; `tangle_rt.swap_strands` swaps two cells). It then
+  checks the executed strand permutation equals an independent in-Rust reference
+  model — over the trefoil, non-commuting pairs (`s1 s2` ≠ `s2 s1`),
+  braid-relation pairs (`s1 s2 s1` = `s2 s1 s2`), and a 5-strand weave. Run via
+  `cargo test` in `compiler/tangle-wasm`.
+- This validates the wasm **codegen** against the braid permutation semantics
+  (catches wrong crossing indices, call order, strand counts, or a
+  non-instantiable module). It is not a cross-binary diff against `eval.ml`, and
+  the Markov-move helpers are not yet exercised; full source↔wasm bisimulation
+  remains research-grade (PROOF-NEEDS.md TG-6). The shipped backend keeps no
+  runtime dependency (`wasmi` is dev-only).
+
 ### TG-7 (non-semantic rung): out-of-band braid-group equivalence
 
 - **`compiler/lib/braid_equiv.ml`** decides braid-GROUP equivalence via Dehornoy

PROOF-NEEDS.md

@@ -58,7 +58,7 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli
 | TG-3 | OCaml `typecheck.ml` refines the Lean `HasType` spec | TP | Lean 4 + translation validation | P1 | — | **LANDED** (translation-validation level — [`proofs/TG3-REFINEMENT.md`](proofs/TG3-REFINEMENT.md)). Reduced via TG-2 (`infer ≡ HasType`) to "OCaml `infer_expr` ≡ Lean `infer` on the core fragment", then discharged by: (a) a closure proof (core fragment never yields `TTangle`, strengthened tree-IH); (b) 496 Lean kernel-checked obligations in [`proofs/TG3Differential.lean`](proofs/TG3Differential.lean) generated from `infer_expr` by `compiler/test/tg3/tg3_emit.ml` (`by decide`; run `proofs/check-tg3-differential.sh`); (c) 1008 OCaml `--check` assertions (`dune runtest`). Complete divergence catalogue: **D1** `close` (OCaml `Tangle[I,I]` vs Lean `word 0` — sole boundary gateway, + downstream D1b/c/d) and **D2** `bool==bool` (OCaml accepts, Lean rejects). Extra-core feature list (model-later / declare-non-core) in TG3-REFINEMENT §3. Not claimed: a universal Lean proof over all OCaml runs (would require reflecting `typecheck.ml`); refinement is OCaml→Lean only |
 | TG-4 | Pretty-print/parse round-trip on closed values | INV | OCaml property test (cheap) | P2 | 4h | **LANDED** (PR #46 — OCaml property test in `compiler/test/test_roundtrip.ml`, 26-entry corpus including 8 echo/product constructors; 52 round-trip runs) |
 | TG-5 | `compositional.ml` (418 LoC) rewriter preserves types | TP | OCaml property test | P2 | — | **LANDED** (`compiler/test/tg5/tg5_invariants.ml`, 189 assertions in `dune runtest`). compositional is below the Ty layer, so "preserves types" = preserves the PD-lowering structural invariants + echo residue-recovery: `OpenWord`/`ClosedDiagram`/`EchoClosed` each pinned (closedness, `\|crossings\|`=unit-length, source unit-expanded, **verbatim residue** for `EchoClose` with `expand(residue)=diagram word` and echo-diagram pdv1-identical to plain `close`), error paths, count pins. Lean IR model = optional later rung |
-| TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | Lean 4 bisimulation | P1 | 3w (research-grade) | NOT STARTED |
+| TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | differential + Lean bisimulation | P1 | — | **RUNG LANDED (differential)**: `compiler/tangle-wasm/tests/differential.rs` EXECUTES the generated wasm with the `wasmi` interpreter (dev-dep) and checks the braid strand-permutation equals an independent reference model (trefoil, non-commuting pairs, braid-relation pairs, 5-strand weave). Validates codegen vs the permutation semantics; not a cross-binary diff against `eval.ml`, and Markov helpers untested. Full source↔wasm bisimulation (WasmCert) remains research-grade |
 | TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **RUNG LANDED (non-semantic)**: `compiler/lib/braid_equiv.ml` decides braid-group equivalence via Dehornoy handle reduction, out-of-band (leaves `==`/`Step.eqBraids` as list equality). Tested (`compiler/test/tg7`, 2220 assertions: defining relations + 400 constructed-equivalent pairs + invariant-distinguished negatives). **Still OWNER-GATED**: whether to route `==` through it (a semantics change to eval.ml + Lean Step + proofs) is a language-design decision; Lean correctness (Garside/Dehornoy) remains research-grade |
 | TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | Lean 4 per-dialect | P3 | 1w each | NOT STARTED |
 | TG-9 | LSP diagnostics are a subset of `HasType` failures (no LSP-only diagnostics) | INV | Audit + refactor | P2 | — | **LANDED** (`tangle-lsp` delegates all diagnostics to `tanglec --check` ⇒ `compiler/lib/check.ml`; hand-rolled LSP-only false positives removed. Subset holds by construction. Tests: `test_check.ml` + tangle-lsp unit/delegation tests) |
@@ -70,11 +70,12 @@ assumptions each rests on, see PROOF-NARRATIVE.md.
 ## Scoping of the remaining obligations (2026-06-14)
 
 Concrete approach, effort, risk, and dependencies for what is left after
-TG-0/1/2/3/4/5/9/10 landed. The three that remain are each **blocked on a
-prerequisite, not on effort** (parallel readiness assessment, 2026-06-14):
-TG-8 needs a dialect to actually exist as code; TG-7 needs an owner decision on
-braid-equality semantics; TG-6 needs a wasm runtime stood up. **No further
-auto-landing without those prerequisites.**
+TG-0/1/2/3/4/5/9/10 landed. **Landable rungs of TG-6 and TG-7 also landed**
+(2026-06-14): TG-6 now has a `wasmi` differential test executing the generated
+wasm; TG-7 has an out-of-band `braid_equiv` checker. What genuinely remains is
+**prerequisite-gated, not effort-gated**: TG-8 needs a dialect to exist as code;
+TG-7's *semantics change* needs an owner decision; TG-6's *full bisimulation*
+and TG-7's *Lean correctness proof* are research-grade.
 
 ### TG-3 — OCaml `typecheck.ml` refines Lean `HasType` — ✅ **LANDED 2026-06-14**
 - **Key lever (used):** TG-2 proves Lean `infer ≡ HasType`, so refinement
@@ -142,16 +143,21 @@ auto-landing without those prerequisites.**
   test (core typed-in-core iff typed-in-dialect) mirroring the tg3/tg5 harness.
   Only then can conservativity be proven; replicate per dialect (~1w each).
 
-### TG-6 — WASM compilation preserves semantics — ⛔ **BLOCKED (no wasm runtime)**
-- `compiler/tangle-wasm` compiles Tangle→wasm but there is **no wasm runtime**
-  (no wasmtime/wasmer dependency) to execute the output, and no FFI bridge to
-  call it from the OCaml test harness. Differential testing has nothing to run.
-- **Prerequisite (smallest rung):** add `wasmtime` (or `wasmer`) as a
-  dev-dependency in `compiler/tangle-wasm/Cargo.toml`; stand up a harness that
-  compiles an expr→wasm, instantiates it with the runtime, executes, reads the
-  result from linear memory, and diffs against `eval.ml` on the same input
-  (isolated test subdir, mirroring tg3/tg5). Full bisimulation (WasmCert /
-  Wasm-spec) remains a multi-week research project on top of that.
+### TG-6 — WASM compilation preserves semantics — 🟡 **RUNG LANDED (differential)**
+- ✅ **Differential rung landed 2026-06-14**: `compiler/tangle-wasm/tests/differential.rs`
+  adds `wasmi` (pure-Rust interpreter) as a dev-dependency, EXECUTES the
+  generated wasm modules with reference host primitives (`alloc_strands` =
+  identity init, `swap_strands` = cell swap), and checks the resulting strand
+  permutation equals an independent in-Rust reference model — over trefoil,
+  non-commuting pairs (`s1s2` ≠ `s2s1`), braid-relation pairs (`s1s2s1` =
+  `s2s1s2`), and a 5-strand weave. Runs via `cargo test`.
+- **Honest scope:** validates the *codegen* against the permutation semantics
+  (catches wrong crossing indices / call order / strand count / non-instantiable
+  modules); it is NOT a cross-binary diff against `compiler/lib/eval.ml`, and the
+  Markov-move helpers are not yet exercised.
+- **Remaining (research-grade):** a full source↔wasm bisimulation proof
+  (WasmCert / Wasm-spec); and, if desired, a true cross-binary differential that
+  drives `eval.ml` and the wasm over a shared corpus.
 
 ## Proof categories
 

compiler/tangle-wasm/Cargo.toml

@@ -15,3 +15,7 @@ wasm-encoder = "0.225"
 thiserror = "2"
 
 [dev-dependencies]
+# TG-6 differential rung: a pure-Rust wasm interpreter to EXECUTE the generated
+# modules and check they preserve the braid strand-permutation semantics.
+# Test-only; the shipped backend keeps no runtime dependency.
+wasmi = "0.51"