diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 79b4749..659af84 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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.", diff --git a/AUDIT.adoc b/AUDIT.adoc index b0273a9..0dd0dac 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -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. diff --git a/docs/PRODUCTION-PATH.adoc b/docs/PRODUCTION-PATH.adoc index 04d0ba1..3e8c553 100644 --- a/docs/PRODUCTION-PATH.adoc +++ b/docs/PRODUCTION-PATH.adoc @@ -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. diff --git a/docs/wiki/Phase-0-Status.md b/docs/wiki/Phase-0-Status.md index 36a82b3..c6d0696 100644 --- a/docs/wiki/Phase-0-Status.md +++ b/docs/wiki/Phase-0-Status.md @@ -1,6 +1,8 @@ + + # 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. @@ -8,7 +10,7 @@ Phase 0 closes the engineering-surface fragility around the proofs so all subseq - **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 ` 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.