docs: record typed-wasm-verify Rust port (C1-C5) in repo-level docs

0-AI-MANIFEST.a2ml

@@ -15,13 +15,14 @@ id = "typed-wasm-root-manifest"
 level = 0
 
 [canonical_locations]
-state      = ".machine_readable/6a2/STATE.a2ml"
-meta       = ".machine_readable/6a2/META.a2ml"
-ecosystem  = ".machine_readable/6a2/ECOSYSTEM.a2ml"
-grammar    = "spec/grammar.ebnf"
-abi_proofs = "src/abi/"
-zig_ffi    = "ffi/zig/"
-examples   = "examples/"
+state         = ".machine_readable/6a2/STATE.a2ml"
+meta          = ".machine_readable/6a2/META.a2ml"
+ecosystem     = ".machine_readable/6a2/ECOSYSTEM.a2ml"
+grammar       = "spec/grammar.ebnf"
+abi_proofs    = "src/abi/"
+zig_ffi       = "ffi/zig/"
+verify_rust   = "crates/typed-wasm-verify/"
+examples      = "examples/"
 
 [echidna_invocation]
 # All ECHIDNA calls go through the echidna-llm-mcp BoJ cartridge. Never call ECHIDNA directly.

CHANGELOG.md

@@ -11,7 +11,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### 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 ReScript 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.
+  - C2 (#20) — `affinescript.ownership` custom-section codec (parse + encode), 11 unit tests covering wire-format round-trip and OCaml-parity leniency.
+  - C3 (#21) — Per-path `(min, max)` use-range analysis with a control-flow frame stack over wasmparser's operator stream. `verify_function` + `verify_from_module` implement the intra-fn L7+L10 rules. 9 algorithmic + 9 end-to-end tests.
+  - C4 (#22) — Cross-module boundary verifier (`extract_exports`, `verify_cross_module`). 3 + 8 tests. Reuses C3's frame stack via a `CallOf(import_idx)` counter.
+  - C5 (#23) — Cross-compat integration suite (`tests/cross_compat.rs`), 10 fixtures modelling realistic affinescript-shaped modules. Each fixture documents the conceptual AffineScript source and the expected OCaml verdict — divergence on either side is a parity bug.
 - ECHIDNA prover oracle JS harness (tests/echidna/echidna-harness.mjs) — random .twasm generator, 4 property tests, optional ECHIDNA submission
 - arXiv-ready LaTeX paper (docs/arxiv/typed-wasm.tex) — ACM sigplan format, 851 lines
 - BibTeX bibliography (docs/arxiv/typed-wasm.bib) — 15 references
 - TypedQLiser plugin exists at typedqliser/src/plugins/wasm.rs (541 lines, 9 tests)
+
+### Changed
+- Repo is now polyglot Idris2 + Zig + Rust (added a Cargo workspace at the root, `crates/typed-wasm-verify/` is its first member). ReScript files in `src/parser/*.res` remain in tree as the v1.1 surface parser, but the post-codegen verifier no longer depends on them.

LEVEL-STATUS.md

@@ -101,3 +101,39 @@ toolchain remains future work.
 | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
+
+## Post-codegen verifier (Rust)
+
+The Idris2 proofs above establish that **the type discipline is sound** —
+L1-L10 (and L13-L16) are mechanically verified at the spec level. They
+say nothing about whether a particular wasm module out of a particular
+codegen actually obeys the discipline.
+
+`crates/typed-wasm-verify/` (added 2026-05-15) closes that loop on the
+**post-codegen** side. Given a wasm module plus an
+`affinescript.ownership` custom section, the crate runs a per-path
+`(min, max)` use-range analysis over every function body and reports
+L7 (aliasing) + L10 (linearity) violations. It's a second line of
+defence: the source-level checker enforces the rules during compilation;
+this crate re-checks them on the emitted IR to catch codegen bugs.
+
+| Layer | What it proves | Where |
+|-------|----------------|-------|
+| Idris2 proofs | Type discipline is sound (spec-level) | `src/abi/TypedWasm/ABI/*.idr` |
+| Source checker | Source program respects discipline | `hyperpolymath/affinescript:lib/codegen.ml` (QTT pass), upcoming `.twasm` parser/checker |
+| **Post-codegen verifier** | **Emitted wasm respects discipline** | **`crates/typed-wasm-verify/` (Rust)** + `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml` (OCaml, reference impl) |
+
+The Rust crate is a faithful port of the OCaml reference; the OCaml
+files remain the spec of record until the cross-compat suite at
+`crates/typed-wasm-verify/tests/cross_compat.rs` is supplemented with
+real affinescript-emitted fixtures (deferred work, "C5.1").
+
+**Coverage:** L7 (ExclBorrow) + L10 (Linear) only.
+L1-L6, L13-L16 enforcement on emitted wasm is future work.
+
+**Consumers** (live as of 2026-05-15):
+
+- `hyperpolymath/ephapax:src/ephapax-wasm/` — emits the
+  `affinescript.ownership` section on every compile
+- `hyperpolymath/ephapax:src/ephapax-cli/` — exposes the verifier via
+  `ephapax compile --verify-ownership`

ROADMAP.adoc

@@ -62,6 +62,7 @@ Known audit constraints:
 * [x] TypedQLiser plugin (WASM as a "query target") — typedqliser/src/plugins/wasm.rs (541 lines)
 * [ ] VCL-total sibling integration (same levels, different domain)
 * [ ] GraalVM/Truffle target (multi-language shared state type safety)
+* [x] `typed-wasm-verify` Rust crate (`crates/typed-wasm-verify/`) — post-codegen L7+L10 verifier. Consumed by `hyperpolymath/ephapax` as of 2026-05-15 (`compile --verify-ownership`); `hyperpolymath/affinescript` migration from its in-tree OCaml verifier deferred to v1.0.
 
 == v1.0.0 -- Stable Release
 
@@ -71,6 +72,8 @@ Known audit constraints:
 * [ ] CI/CD with proof validation
 * [ ] De-template release/build/container surfaces
 * [ ] Real benchmark and aspect-test evidence
+* [x] Post-codegen verifier in Rust (`crates/typed-wasm-verify/`) — partial v1.0 deliverable, the verifier side of the pipeline. Parser/checker for `.twasm` source remains the open work.
+* [ ] Cross-compat parity proof against `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml` — real OCaml-emitted .wasm fixtures alongside the existing synthetic ones (deferred to "C5.1").
 
 == Language Identity & Linguist Classification