hyperpolymath · hyperpolymath · May 31, 2026 · May 31, 2026 · May 31, 2026
@@ -21,9 +21,9 @@ Two first-class roles (ADR-004):
      (both compile to WasmGC).  Provides formally verified type layout and ABI
      conventions so cross-language calls require no marshalling layer.
 """
-completion-percentage = 70   # bumped from 55: foundation defensibly engineered; codegen pipeline kickoff complete; CI honest; 545+ test assertions across 11 surfaces; ROADMAP truthful with drift-detection aspect in place
-production-phase = "0"      # see docs/PRODUCTION-PATH.adoc — phase 0 of 6
-production-phase-status = "2 of 3 gates met (gate 1: CI green-or-advisory ✓; gate 2: codegen v0 ✗; gate 3: ROADMAP truthful ✓)"
+completion-percentage = 73   # bumped from 70: codegen v0 landed (in-tree Rust producer crates/typed-wasm-codegen, tw build; PR #134) — Phase 0 gate 2 discharged; CI honest; ROADMAP truthful with drift-detection aspect in place
+production-phase = "0"      # see docs/PRODUCTION-PATH.adoc — phase 0 of 6 (all 3 gates met; Phase 1 open)
+production-phase-status = "3 of 3 gates met (gate 1: CI green-or-advisory ✓; gate 2: codegen v0 ✓ — crates/typed-wasm-codegen tw build, PR #134, host-language ADR-0004 Proposed; gate 3: ROADMAP truthful ✓)"
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
@@ -77,7 +77,6 @@ issues = [
   "Venue-facing paper and benchmark claims still outrun the evidence present in-repo (now caught by tests/aspect/claim-envelope §8 drift detection).",
   "generated/abi/ C header pipeline not yet implemented (milestone at 0%).",
   "HostType F32 = Double in TypedAccess.idr — Idris2 lacks Float32; documented limitation.",
-  "Track A codegen v0 outstanding — gates Phase 0 → Phase 1 transition.",
   "Track B (AffineScript verifier migration) requires a separate Claude session pointed at hyperpolymath/affinescript (cross-repo, locked MCP scope).",
   "Build + E2E job persistently red; likely cause: Idris2 release tarball pins ubuntu-20.04 binary but runners are ubuntu-24.04. Marked non-blocking in PR #59; deeper fix needs idris2-pack or build-from-source.",
   "Validate A2ML / Validate K9 third-party actions persistently failing; non-blocking in PR #59; upstream investigation needed in hyperpolymath/{a2ml,k9}-validate-action repos.",
@@ -92,7 +91,7 @@ actions = [
   "Track A: extend tree-sitter grammar from region-decls v0 to full spec/grammar.ebnf parity.",
   "Track A: Idris2 parser at 188-test parity with the ReScript parser.",
   "Track A: ReScript cut single PR (auto-closes anti-pattern policy red).",
-  "Track A: codegen v0 for examples/01-single-module.twasm end-to-end — closes Phase 0 → Phase 1 gate.",
+  "Track A: extend codegen v0 (crates/typed-wasm-codegen) from examples 01/03 + multi-module to the remaining examples + full grammar + front-end → IR seam (Phase 1, issue #49/#127).",
   "Track B: open AffineScript session, swap lib/{tw_verify,tw_interface}.ml for subprocess call to typed-wasm-verify binary.",
   "Investigate Build+E2E root cause once authenticated log access available; replace idris2 install with idris2-pack or build-from-source.",
   "L11-modal-box: integration test with TypeLL L10 context; QTT semantics review before graduation.",

@@ -68,8 +68,9 @@ For typed-wasm-specific audit posture:
 * `PROOF-NEEDS.md` — outstanding proof obligations
 * `TEST-NEEDS.md` — outstanding test coverage
 * `docs/PRODUCTION-PATH.adoc` — 6-phase plan to production-quality compile
-  target; current state is Phase 0 (foundation stabilisation), 2 of 3 gates
-  met
+  target; current state is Phase 0 (foundation stabilisation), all 3 gates
+  met (gate 2 / codegen v0 discharged by the in-tree Rust producer
+  `crates/typed-wasm-codegen`, PR #134); Phase 1 open
 * `.machine_readable/6a2/STATE.a2ml` — machine-readable project state
 * `tests/aspect/claim-envelope.mjs` (53 assertions) +
   `tests/aspect/security-envelope.mjs` (10 assertions) — automated
@@ -81,8 +82,12 @@ Bots operating on this repository should treat this document as a key root
 audit document and should not make optimistic release or publication claims
 that conflict with it. Specifically:
 
-* Do not claim end-to-end `.twasm → .wasm` compilation works (codegen v0
-  is outstanding — Phase 0 gate 2).
+* Codegen v0 emits valid, verifier-accepted wasm for
+  `examples/01-single-module.twasm` (+ example 03 and a multi-module
+  boundary) via the in-tree Rust producer `crates/typed-wasm-codegen`
+  (`tw build`; Phase 0 gate 2, met by PR #134; host-language ADR-0004 is
+  *Proposed*, pending ratification). Do NOT claim full `.twasm → .wasm`
+  compilation across all examples/levels works — that is Phase 1 (#49).
 * Do not claim "fully verified soundness discipline" without the qualifier
   that producer-side enforcement only; runtime enforcement is Phase 3 work.
 * Do not claim production-readiness — production hardening is Phase 6.

@@ -58,16 +58,24 @@ The plan below targets reading (1).
 
 What is *not* yet in place:
 
-* A `.twasm` -> `.wasm` codegen. The parser parses, the verifier verifies
-  someone else's wasm, but nothing in this repository emits wasm from a
-  `.twasm` source.
+* A `.twasm` -> `.wasm` codegen *beyond v0*. As of 2026-05-30 the in-tree
+  Rust producer `crates/typed-wasm-codegen` (`tw build`, PR #134) emits
+  verifier-accepted wasm for `examples/01-single-module.twasm` (plus
+  example 03 and a multi-module boundary); codegen for the remaining
+  examples, the full grammar, and the front-end -> IR seam is Phase 1
+  (issue #49 / #127). (At the start of Phase 0, nothing in this repository
+  emitted wasm from a `.twasm` source.)
 * Tree-sitter grammar, LSP, Linguist registration.
 * A producer specification document for third-party compilers.
 * Runtime-side enforcement of L7-L10.
 * Frozen 1.0 spec, conformance suite, third-party verifier implementation.
 
-Honest framing: today typed-wasm is a *verifier + spec*, not a *compiler*.
-That distinction is the spine of every phase that follows.
+Honest framing: at the start of Phase 0 typed-wasm was a *verifier + spec*,
+not a *compiler*. Codegen v0 (gate 2, met 2026-05-30 via
+`crates/typed-wasm-codegen`) makes it a *minimal compiler* for the
+example-01 schema (plus example 03 and a multi-module boundary); the full
+producer story is Phase 1. That distinction is the spine of every phase
+that follows.
 
 == The six phases
 
@@ -118,7 +126,10 @@ What advancing to Phase 1 requires:
   removed from the merge requirement set, with reason recorded in this
   document).
 . Codegen v0 emits valid wasm for `examples/01-single-module.twasm`,
-  verifiable end-to-end by `typed-wasm-verify`.
+  verifiable end-to-end by `typed-wasm-verify`. **MET 2026-05-30** —
+  in-tree Rust producer `crates/typed-wasm-codegen` (`tw build`, PR #134;
+  host-language ADR-0004 *Proposed*); round-trip gated by that crate's
+  `tests/roundtrip.rs`.
 . ROADMAP.adoc reflects reality — claims that an artifact is DONE only
   when the artifact exists and is reachable from a green CI run.
 

@@ -1,14 +1,16 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+
 # Phase 0 Status
 
-**Foundation defensibly engineered as of 2026-05-25. Gates 1 + 3 met; gate 2 (codegen v0) remains as the Phase-1-handoff item.**
+**Foundation defensibly engineered. All 3 Phase 0 gates met as of 2026-05-30 — gate 2 (codegen v0) discharged by the in-tree Rust producer `crates/typed-wasm-codegen` (PR #134). Phase 1 ([#49](https://github.com/hyperpolymath/typed-wasm/issues/49)) is open.**
 
 Phase 0 closes the engineering-surface fragility around the proofs so all subsequent phases have a load-bearing foundation. See [Production-Path](Production-Path) §Phase 0 for the full statement and [#48](https://github.com/hyperpolymath/typed-wasm/issues/48) for live tracking.
 
 ## Headline numbers
 
 - **11 PRs landed** across two sessions
 - **545+ test assertions** across 11 surfaces (up from ~430)
-- **2 of 3 Phase 0 gates met** (gate 2 needs Idris2 parser + codegen v0)
+- **3 of 3 Phase 0 gates met** (gate 2 / codegen v0 discharged 2026-05-30 — Rust crate `crates/typed-wasm-codegen` `tw build`, PR #134)
 - **8 deletions** of worthless / template-residue files
 - **4 new RSR-aligned taxonomy stubs** (`AUDIT.adoc`, `docs/onboarding/`, `docs/status/`, `docs/proposals/`)
 - **2 real bugs caught and fixed** by drift-detection aspects (`.well-known/security.txt` template residue, missing SPDX headers)
@@ -24,7 +26,7 @@ Phase 0 closes the engineering-surface fragility around the proofs so all subseq
 | Extend tree-sitter to remaining `spec/grammar.ebnf` productions (imports, L11–L16, match, proof) | 🟡 Next | — |
 | Idris2 parser at 188-test parity with ReScript | ⬜ Not started | — |
 | ReScript cut (single PR) | ⬜ Blocked on parser parity | — |
-| Codegen v0 for `examples/01-single-module.twasm` | ⬜ Blocked on parser | — |
+| Codegen v0 for `examples/01-single-module.twasm` | ✅ Shipped — Rust crate `crates/typed-wasm-codegen` (`tw build`), verifier-accepted; + example 03 (L7–10) + multi-module boundary | [#134](https://github.com/hyperpolymath/typed-wasm/pull/134) |
 
 ### Track B — AffineScript verifier migration
 
@@ -79,10 +81,10 @@ Per the production-path definition, Phase 0 advances to Phase 1 when:
 
 Status against those gates:
 - **Gate 1**: ✅ Met via #59 — all CI is now either green or explicitly advisory with documented removal preconditions.
-- **Gate 2**: ⬜ Not yet — needs codegen v0 from Track A (multi-PR work).
+- **Gate 2**: ✅ Met 2026-05-30 — in-tree Rust producer `crates/typed-wasm-codegen` (`tw build`, PR #134) emits valid wasm for `examples/01-single-module.twasm`, verified end-to-end by `typed-wasm-verify` (round-trip gated by the crate's `tests/roundtrip.rs`). Host-language ADR-0004 is *Proposed* (pending ratification).
 - **Gate 3**: ✅ Met via #60 — every documented claim verified, drift-detection aspect in place.
 
-**So Phase 0 is 2/3 of the way to its gate**. The blocker is codegen v0, which is the terminal deliverable of Track A's multi-PR sequence.
+**So Phase 0 has met all 3 gates and is closed; Phase 1 is open.** Codegen v0 — the terminal gate-2 deliverable — landed as the Rust crate `crates/typed-wasm-codegen` (PRs #134/#139/#141), covering example 01 (L1–6), example 03 (L7–10), and a multi-module linear boundary.
 
 ## Test surface summary
 
@@ -109,7 +111,7 @@ None of D1–D6 from [Production-Path](Production-Path) have ADRs yet. D2 (produ
 
 ## What unblocks Phase 1
 
-Track A's codegen v0 PR. Track B can land in parallel without blocking the gate.
+Codegen v0 landed (`crates/typed-wasm-codegen`, PR #134) — Phase 1 ([#49](https://github.com/hyperpolymath/typed-wasm/issues/49)) is now open: remaining examples + full `spec/grammar.ebnf`, the front-end → IR seam (#127), source → line maps (#129), and the ECHIDNA round-trip corpus (#130). Track B (verifier migration) can still land in parallel in `hyperpolymath/affinescript`.
 
 ## 2026-05-27 — Post-Phase-0 proof-debt closure pass
 
@@ -124,4 +126,28 @@ Independent of the Phase 0 / Phase 1 gate transition, a 2026-05-27 sweep closed
 **Test surface 545 → 627+ assertions** (proof regression 25 → 107 from +33 #79 + +49 #80).
 **Zero new `believe_me` / `assert_total` / `postulate` / `sorry` / `assert_smaller`; `%default total` preserved.**
 
+## 2026-05-30 — Gate 2 closed: codegen v0 (Rust)
+
+The terminal Phase 0 blocker is resolved. `crates/typed-wasm-codegen` adds
+the first in-tree `.twasm → .wasm` **producer** (`tw build`), a Rust
+workspace sibling of `typed-wasm-verify` that emits wasm via `wasm-encoder`
+and round-trips through `verify_from_module` in-process — the tightest
+soundness net. Host language fixed by [ADR-0004](../decisions/0004-codegen-host-language.adoc)
+(*Proposed*, pending ratification).
+
+| PR | What it lands |
+|---|---|
+| [#134](https://github.com/hyperpolymath/typed-wasm/pull/134) | codegen v0 + `tw build` for `examples/01-single-module.twasm` (`typedwasm.regions` + `typedwasm.access-sites`), verifier-accepted; **discharges gate 2**; WAT emission (`--emit wasm\|wat\|both`) |
+| [#139](https://github.com/hyperpolymath/typed-wasm/pull/139) | multi-module codegen at parity with `verify_cross_module` (Linear export/import boundary, L10) |
+| [#141](https://github.com/hyperpolymath/typed-wasm/pull/141) | `examples/03-ownership-linearity` (L7–10 via `typedwasm.ownership`) + wasm `name` section for debugger symbols |
+| #126 | human-readable error translation layer + `tw build` self-verification |
+
+A standalone `tw-verify <module.wasm>` CLI (for verifying wasm from any
+producer, not just `tw build`) is proposed separately in
+[#143](https://github.com/hyperpolymath/typed-wasm/pull/143).
+
+Deferred to Phase 1 (#49): front-end → IR seam (#127), remaining examples,
+source → line maps (#129), region-imports / L13-positive (#140), ECHIDNA
+round-trip corpus (#130).
+
 These PRs are independent of the Phase 0 → Phase 1 gate (which is still blocked on codegen v0). They close debt items that would otherwise haunt the v1.0 audit.