diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml index 28899b9..19a7f80 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -31,7 +31,7 @@ projects = [ [integration-points] systems = [ { system = "Idris2 proof build", direction = "inbound", protocol = "idris2 --build" }, - { system = "ReScript parser toolchain", direction = "inbound", protocol = "rescript build" }, + { system = "AffineScript parser toolchain", direction = "inbound", protocol = "affinescript build (post-2026-05-25 ReScript -> AffineScript migration)" }, { system = "Zig FFI and oracle tests", direction = "inbound", protocol = "zig build" }, { system = "ECHIDNA property testing", direction = "inbound", protocol = "node harness + oracle tests" }, ] diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 935f4b5..5e2bb2c 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -10,7 +10,7 @@ last-updated = "2026-03-30" [project-info] type = "library" -languages = ["idris2", "rescript", "zig", "javascript", "ebnf", "latex", "asciidoc"] +languages = ["idris2", "affinescript", "zig", "javascript", "ebnf", "latex", "asciidoc"] license = "MPL-2.0" author = "Jonathan D.A. Jewell (hyperpolymath)" diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 01fbd86..488532b 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,9 +6,9 @@ [metadata] project = "typed-wasm" version = "0.1.0" -last-updated = "2026-05-24" +last-updated = "2026-05-25" status = "active" # active | paused | archived -session = "2026-05-24 — Phase 0 closure pass. 7 PRs landed (#46 CI triage, #47 PRODUCTION-PATH doc, #55 cargo-audit CI, #57 Track C complete +64 assertions, #58 tree-sitter scaffold, #59 CI hardening non-blocking, #60 ROADMAP truthfulness audit + drift-detection aspect §8). Phase 0 gates 1 + 3 met; gate 2 (codegen v0) outstanding." +session = "2026-05-24/25 — Phase 0 closure pass. 11 PRs landed (#46 CI triage, #47 PRODUCTION-PATH doc, #55 cargo-audit CI, #57 Track C complete +64 assertions and 2 real bugs fixed, #58 tree-sitter scaffold, #59 CI hardening non-blocking, #60 ROADMAP truthfulness audit + drift-detection aspect §8, #61 wiki source-of-truth + STATE.a2ml comprehensive, #62 tree-sitter v1 parses example 01 end-to-end with 0 ERROR, #63 repo tidy RSR-aligned + smoke fix + duplication scrub). Phase 0 gates 1 + 3 met; gate 2 (codegen v0) is the terminal Phase-1-handoff item." [project-context] name = "typed-wasm" @@ -43,9 +43,14 @@ milestones = [ { name = "L11-L12 checked integration", completion = 0 }, { name = "Preprint published on Zenodo (12-level)", completion = 100 }, { name = "Production-path canonical plan (6-phase) + tracking issues", completion = 100 }, # added 2026-05-24 (PR #47) - { name = "Tree-sitter grammar scaffold (Track A kickoff)", completion = 20 }, # added 2026-05-24 (PR #58); region-decls only, full EBNF parity pending - { name = "CI persistent-reds hardening (non-blocking + documented)", completion = 100 }, # added 2026-05-24 (PR #59) - { name = "ROADMAP truthfulness audit + drift-detection aspect", completion = 100 }, # added 2026-05-24 (PR #60) + { name = "Tree-sitter grammar v0 scaffold (Track A kickoff)", completion = 100 }, # 2026-05-24 (PR #58) + { name = "Tree-sitter grammar v1 — parses example 01 end-to-end (0 ERROR)", completion = 100 }, # 2026-05-25 (PR #62) + { name = "Tree-sitter grammar at full spec/grammar.ebnf parity", completion = 35 }, # ~60-70% by production count at v1; imports/L11-L16/match/proof/lifetime/striated still ahead + { name = "CI persistent-reds hardening (non-blocking + documented)", completion = 100 }, # 2026-05-24 (PR #59) + { name = "ROADMAP truthfulness audit + drift-detection aspect", completion = 100 }, # 2026-05-24 (PR #60) + { name = "Wiki source-of-truth at docs/wiki/", completion = 100 }, # 2026-05-25 (PR #61) + { name = "RSR-template taxonomy alignment (AUDIT.adoc + onboarding/status/proposals stubs)", completion = 100 }, # 2026-05-25 (PR #63) + { name = "Parser migration ReScript -> AffineScript -> Idris2", completion = 50 }, # ReScript->AffineScript landed; AffineScript->Idris2 still ahead ] [blockers-and-issues] @@ -75,7 +80,7 @@ actions = [ ] [maintenance-status] -last-run-utc = "2026-05-24T20:00:00Z" +last-run-utc = "2026-05-25T20:00:00Z" last-report = "docs/PRODUCTION-PATH.adoc" # the canonical strategic doc supersedes one-off audit reports last-result = "pass" # unknown | pass | warn | fail open-warnings = 4 # Build+E2E + A2ML + K9 non-blocking advisories (PR #59) + anti-pattern policy (fixed by Track A's ReScript cut) diff --git a/CHANGELOG.md b/CHANGELOG.md index 20c00d6..4647415 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,33 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Phase 0 closure pass (2026-05-24 / 2026-05-25) + +Two sessions of focused engineering-surface stabilisation, closing the +foundation gates of `docs/PRODUCTION-PATH.adoc` §Phase 0. Gates 1 +(CI green-or-advisory) and 3 (ROADMAP truthful + drift-detected) met; +gate 2 (codegen v0 round-trips through verifier) remains as the +terminal Phase-1-handoff item. + +**11 PRs landed**: + +- **#46** — CI triage round 1 (3 of 6 reds fixed: cargo install, structural E2E, hypatia exemption) +- **#47** — `docs/PRODUCTION-PATH.adoc` canonical 6-phase plan + ROADMAP version↔phase mapping + README pointer +- **#55** — `cargo audit` workflow (RustSec advisories, weekly cron) +- **#57** — Track C complete: `tests/property/property_test.mjs` (29 assertions), `tests/aspect/security-envelope.mjs` (10), `tests/proof/regression.mjs` (25 + optional idris2 layer). Caught + fixed 2 real bugs (`.well-known/security.txt` template residue, missing SPDX on `ffi/zig/src/main.zig` and `.machine_readable/scripts/forge/git-cleanup.sh`). +- **#58** — `tools/tree-sitter-twasm/` scaffold (Track A kickoff): region-decls grammar v0 +- **#59** — A2ML / K9 / Build+E2E persistent-red jobs marked non-blocking with documented removal preconditions +- **#60** — ROADMAP truthfulness audit (3 real path drifts fixed: `spec/10-levels-for-wasm.adoc` rename → `type-safety-levels-for-wasm.adoc` in 5 callers; EXPLAINME.adoc pre-restructure file table; stray `src/abi/Foreign.idr` reference) + `claim-envelope.mjs` §8 drift-detection aspect +- **#61** — Wiki source-of-truth at `docs/wiki/` (`Home.md`, `Production-Path.md`, `Phase-0-Status.md`, `Comparison.md`, sync workflow) + comprehensive `.machine_readable/6a2/STATE.a2ml` update +- **#62** — tree-sitter v1 grammar — parses `examples/01-single-module.twasm` end-to-end with 0 ERROR nodes (~270 lines covering memory decls, functions, parameters, statements, expressions, nested field paths) +- **#63** — Repo tidy: RSR-template taxonomy alignment (added `AUDIT.adoc`, `docs/onboarding/`, `docs/status/`, `docs/proposals/`, `docs/architecture/ABI-PIPELINE.adoc`); deleted 8 worthless files (3 template-residue QUICKSTARTs, 2 heuristic `.invariants.md` artefacts, empty `docs/wikis/`, stray `generated/abi/README.adoc`); README Quick Tour rebuilt; smoke job made graceful for the in-flight parser migration; `claim-envelope.mjs` §4 tolerates build outputs whose source exists; stale ReScript references scrubbed from `.hypatia-ignore`, `README.adoc`, `AUDIT.adoc` + +**Test surface after Phase 0 pass**: 545+ assertions across 11 surfaces (88 parser + 53 verify + 56 per-level + 53+10 aspect + 29 property + 25 proof + 40 smoke + 53 structural + 14 integration + 124 ECHIDNA). Up from ~430 pre-session. + +**Out of scope for this pass** (multi-week / cross-repo): Track A's full `spec/grammar.ebnf` parity + Idris2 parser at 188-test parity + codegen v0; Track B's cross-repo AffineScript verifier migration (requires separate session pointed at `hyperpolymath/affinescript`). + +**Tracking**: GitHub issue #48 carries the live ledger; phases 1–6 at #49–#54. + ### Added - **typed-wasm-verify** Rust crate (`crates/typed-wasm-verify/`) — post-codegen verifier for L7 (aliasing) + L10 (linearity) on emitted wasm modules. Rust port of `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml`. 50/50 tests pass (40 unit + 10 cross-compat integration). Replaces the AffineScript verifier path which is on its way out. - C1 (#19) — Scaffold: crate skeleton, public types (`OwnershipKind`, `OwnershipError`, `CrossError`, `FuncInterface`, `VerifyError`), `OWNERSHIP_SECTION_NAME` constant, stubbed entry points. diff --git a/docs/reports/maintenance/2026-05-25-phase-0-closure.adoc b/docs/reports/maintenance/2026-05-25-phase-0-closure.adoc new file mode 100644 index 0000000..51c55a0 --- /dev/null +++ b/docs/reports/maintenance/2026-05-25-phase-0-closure.adoc @@ -0,0 +1,197 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += 2026-05-24/25 — Phase 0 Closure Pass +:author: Jonathan D.A. Jewell +:revdate: 2026-05-25 +:toc: + +== Purpose + +Canonical written record of the two-day Phase 0 closure pass. +Companion to `CHANGELOG.md` (which lists what shipped per release) +and `docs/wiki/Phase-0-Status.md` (the live ledger). This document +exists so a reader six months from now can reconstruct what +happened, why, and where to look next. + +== Summary + +11 PRs landed across two sessions of focused engineering-surface +stabilisation. Phase 0 §"What advancing to Phase 1 requires" gates: + +* **Gate 1** — every commit on main exits CI green (or explicitly + advisory): **met** via PR #59 +* **Gate 2** — codegen v0 emits valid wasm for example 01, + verifiable end-to-end: **not yet** — terminal blocker; needs + Idris2 parser + codegen implementation (weeks of work) +* **Gate 3** — `ROADMAP.adoc` reflects reality: **met** via PR #60 + and the drift-detection aspect that prevents recurrence + +State at end of pass: the project is *defensibly engineered* — a +research prototype that builds, tests, ships without hand-holding, +with honest CI status and a complete documentation surface for +humans and machines. Not yet a working compile target; that's +Phase 1. + +== PRs that landed (chronological) + +[cols="1,4",options="header"] +|=== +| PR | What + +| #46 | CI triage round 1 — three of six persistent red jobs fixed + (cargo install, structural E2E, hypatia exemption) + +| #47 | `docs/PRODUCTION-PATH.adoc` canonical 6-phase plan; version + axis ↔ phase axis mapping in `ROADMAP.adoc`; README pointer + +| #55 | `cargo audit` workflow — RustSec advisories on every PR and + weekly cron + +| #57 | Track C audit-floor cleanup complete: real + `tests/property/property_test.mjs` (29 assertions), + `tests/aspect/security-envelope.mjs` (10), + `tests/proof/regression.mjs` (25 + optional idris2 layer). + The new security-envelope caught two real bugs the moment it + ran: `.well-known/security.txt` still had template placeholders + (`{{SECURITY_EMAIL}}`, `{{PGP_KEY_URL}}`, `{{FORGE}}`, + `{{WEBSITE}}`), and `ffi/zig/src/main.zig` plus + `.machine_readable/scripts/forge/git-cleanup.sh` were missing + SPDX headers. Fixed in the same commit. + +| #58 | `tools/tree-sitter-twasm/` scaffold (Track A kickoff) — + region-decls grammar v0 + +| #59 | A2ML / K9 / Build+E2E persistent-red jobs marked + non-blocking via `continue-on-error: true` with explicit + Phase 0 NOTE comments documenting the removal precondition + for each + +| #60 | ROADMAP truthfulness audit — three real path drifts fixed + (the `spec/10-levels-for-wasm.adoc` → `type-safety-levels-for-wasm.adoc` + rename had five stale callers; EXPLAINME.adoc described a + pre-restructure Idris2 ABI architecture; stray + `src/abi/Foreign.idr` reference). Added `claim-envelope.mjs` + §8 — path-reference drift detection that catches this class + automatically going forward. + +| #61 | Wiki source-of-truth at `docs/wiki/` + (`Home.md`, `Production-Path.md`, `Phase-0-Status.md`, + `Comparison.md`, sync workflow) — the GitHub wiki had stale + PMPL license and pre-restructure proof paths. + Comprehensive `.machine_readable/6a2/STATE.a2ml` update: + completion 55 → 70, new `production-phase` keys, + `[test-surface]` enumeration of 545+ assertions across 11 + surfaces, `[tracking-issues]` mapping each phase to its + GitHub issue, removed ReScript from `depends-on`, added + `ships-to` for AffineScript + Ephapax + +| #62 | tree-sitter v1 grammar — parses + `examples/01-single-module.twasm` end-to-end with 0 ERROR + nodes. Extended from ~80-line scaffold to ~270 lines + covering memory declarations, function declarations + (parameters, return types, effects), and all statement and + expression forms used in example 01 (`region.get`, + `region.set`, `region.scan`, `let [mut]`, assignment, + `if/else`, `return`, binary operators with full precedence + chain, `unary`, `is_null`, nested field paths) + +| #63 | Repo tidy for humans and machines: + *RSR-template taxonomy alignment* — added `AUDIT.adoc` at + root, `docs/onboarding/README.adoc`, `docs/status/README.adoc`, + `docs/proposals/README.adoc`, `docs/architecture/ABI-PIPELINE.adoc`. + *Eight deletions* — three template-residue QUICKSTARTs (still + contained `{{BUILD_CMD}}`, `{{LANG_STACK}}` placeholders and + "Typed Wasm — See README.adoc for details." body text), two + heuristic `.invariants.md` artefacts, empty `docs/wikis/` + placeholder, stray `generated/abi/README.adoc`. + *README Quick Tour rebuilt* with current paths + (`src/abi/TypedWasm/ABI/*.idr`, tree-sitter grammar, verifier + crate, status documents, AUDIT.adoc, onboarding index). + *Smoke job made graceful* for the in-flight ReScript → + AffineScript parser migration (build step tries AffineScript + first, ReScript as fallback, skips cleanly with CI warning if + neither compiler is available; downstream invocations guard + on `[ -f src/parser/Parser.mjs ]`). + *`claim-envelope.mjs` §4 patch* — tolerates `tests/parser/*.mjs` + build outputs whose `.affine` (or `.res`) source exists. + *Duplication scrub* — stale ReScript references cleared from + `.hypatia-ignore`, `README.adoc`, `AUDIT.adoc`. +|=== + +== What changed in numbers + +[cols="2,1,1",options="header"] +|=== +| Surface | Before pass | After pass + +| Test assertions across all surfaces | ~430 | 545+ +| CI jobs gating merge | unknown red+green mix; PRs merged with 8 red | all gating jobs green or explicitly advisory with documented removal precondition +| Phase 0 gates met | 0 of 3 | 2 of 3 +| Phase 0 issue ledger | placeholder TODO links | live cross-linked PR ledger +| Documentation surface | template-residue + drift-prone | RSR-aligned + drift-checked +| Wiki | 1 stale page (PMPL license, pre-restructure paths) | 5 current pages tracked in `docs/wiki/` with sync workflow +| `.machine_readable/6a2/STATE.a2ml` | anchored to 2026-04-12, completion 55% | anchored to 2026-05-25, completion 70%, new `production-phase` and `[test-surface]` sections +| Tree-sitter grammar | 0 lines | ~270 lines; parses example 01 with 0 ERROR +| Stale `.res` references | 6 in `.hypatia-ignore` + others scattered | 0 in human-facing docs +| Template-residue files at root | 3 QUICKSTARTs + 2 invariants.md | 0 +|=== + +== What is *not* done (Phase 0 outstanding work) + +These three items together close Phase 0 → Phase 1: + +. **Idris2 parser at 188-test parity** with the AffineScript parser + (currently at `src/parser/*.affine`). Multi-week implementation. +. **Codegen v0** for `examples/01-single-module.twasm` end-to-end — + the terminal gate-2 deliverable. Multi-week implementation. +. **Track B AffineScript verifier migration** — swap + `hyperpolymath/affinescript/lib/{tw_verify,tw_interface}.ml` for + subprocess call to `typed-wasm-verify` binary; retire ~491 LOC of + OCaml. Requires a separate Claude session pointed at the + `affinescript` repo (cross-repo, MCP scope locked here to typed-wasm). + +== Process notes / lessons + +* **Drift-detection aspects pay for themselves immediately.** The + security-envelope test introduced in PR #57 caught two real bugs + before its first commit shipped — neither would have surfaced for + months otherwise. Same pattern with claim-envelope §8 in PR #60. + Whenever the project adds a new documentation surface or claims + invariant, a corresponding aspect should land in the same PR. + +* **"Persistent red" CI is an honesty problem before it is a + technical one.** PRs were merging with 8 red checks before this + pass; the cargo-verify job intended to catch wasmparser breaks + was *itself silently broken on every PR*. The fix wasn't to + make the checks green by lowering the bar — it was to repair the + checks that should be green and mark the ones that genuinely + can't be (third-party action failures, in-flight migrations) + as advisory with explicit removal preconditions in the workflow + YAML. + +* **In-flight migrations need to land complete or be self-skipping.** + The ReScript → AffineScript parser migration partially landed in + one session (sources renamed) without updating the build + wiring (`package.json` empty, workflow still ran `rescript build`) + or the test scripts (`tests/e2e.sh` still asserted `.res`). + Result: every subsequent PR's CI showed misleading red. Fixed by + making the workflow + scripts gracefully detect and skip when + the migration is mid-way, with CI annotations surfacing the + actual gap. + +* **Bot signal-to-noise matters.** The Hypatia security scan posts + 100+ findings on every PR; most are false positives matching its + own banlist tokens inside Idris2 anti-pattern banner comments + (e.g. `-- NO believe_me`). Documented in `AUDIT.adoc` and queued + for upstream filing at `hyperpolymath/hypatia`. Skipping these as + duplicates is correct; sinking time into each one would drown the + PR loop. + +== Where to look next + +* `docs/PRODUCTION-PATH.adoc` — the 6-phase strategic plan +* `docs/wiki/Phase-0-Status.md` — the live closure ledger +* GitHub issue [#48](https://github.com/hyperpolymath/typed-wasm/issues/48) — Phase 0 tracking +* GitHub issue [#49](https://github.com/hyperpolymath/typed-wasm/issues/49) — Phase 1 (next) +* `.machine_readable/6a2/STATE.a2ml` — machine-readable state +* `AUDIT.adoc` — hard rules and audit posture diff --git a/docs/wiki/Phase-0-Status.md b/docs/wiki/Phase-0-Status.md index c0ef5d3..34b48fb 100644 --- a/docs/wiki/Phase-0-Status.md +++ b/docs/wiki/Phase-0-Status.md @@ -1,9 +1,18 @@ # Phase 0 Status -**Foundation defensibly engineered as of 2026-05-24.** +**Foundation defensibly engineered as of 2026-05-25. Gates 1 + 3 met; gate 2 (codegen v0) remains as the Phase-1-handoff item.** 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) +- **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) + ## Sub-tracks ### Track A — Codegen pipeline @@ -58,7 +67,7 @@ Phase 0 closes the engineering-surface fragility around the proofs so all subseq | ROADMAP truthfulness audit (3 real drifts fixed) | ✅ Shipped | [#60](https://github.com/hyperpolymath/typed-wasm/pull/60) | | claim-envelope §8 drift-detection (catches rename + missing-file drift) | ✅ Shipped | #60 | | Wiki source-of-truth at `docs/wiki/` + comprehensive STATE.a2ml update | ✅ Shipped | [#61](https://github.com/hyperpolymath/typed-wasm/pull/61) | -| Repo taxonomy tidy: RSR-aligned (AUDIT.adoc, docs/status/, docs/onboarding/, docs/proposals/); deletions (3 template-residue QUICKSTARTs, 2 .invariants.md heuristic artefacts, empty docs/wikis/, stray generated/abi/README); ABI-PIPELINE doc move | 🟡 In flight | This PR | +| Repo taxonomy tidy: RSR-aligned (AUDIT.adoc, docs/status/, docs/onboarding/, docs/proposals/); deletions (3 template-residue QUICKSTARTs, 2 .invariants.md heuristic artefacts, empty docs/wikis/, stray generated/abi/README); ABI-PIPELINE doc move; smoke job graceful for in-flight parser migration; duplication scrub (stale ReScript references) | ✅ Shipped | [#63](https://github.com/hyperpolymath/typed-wasm/pull/63) | ## When does Phase 0 "close"?