Claude/adoring volta l cd cj

.github/workflows/e2e.yml

@@ -46,12 +46,24 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Set up Node.js
-        uses: actions/setup-node@v6
+        uses: actions/setup-node@2028fbc5c25fe9cf00d9f06a71cc4710d4507903 # v6.0.0
         with:
-          node-version: '22'
+          node-version: '25'
+
+      - name: Install npm deps (rescript build prerequisite)
+        run: npm install --no-audit --no-fund --silent
+
+      - name: Build ReScript parser
+        run: node_modules/.bin/rescript build
 
       - name: Run smoke test
-        run: node tests/e2e/e2e-smoke.mjs
+        run: node tests/smoke/e2e-smoke.mjs
+
+      - name: Run aspect test (claim envelope)
+        run: node tests/aspect/claim-envelope.mjs
+
+      - name: Run parser benchmark (smoke; full run is local)
+        run: BENCH_ITERS=20 node benchmarks/parser-bench.mjs
 
   # --------------------------------------------------------------------------
   # Job 3: Full Idris2 + Zig build then E2E
@@ -65,12 +77,15 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       # ---- Idris2 ----
+      # 0.8.0 is the version the src/abi/ proofs are written against
+      # (Proofs.idr:629 "verified with Idris2 0.8.0"; Layout.idr / Types.idr
+      # carry 0.8-specific workarounds for reduction + interface resolution).
+      # Older versions will fail the standalone build.
       - name: Install Idris2
         run: |
           sudo apt-get update -qq
           sudo apt-get install -y libgmp-dev
-          # Install Idris2 from binary release
-          IDRIS2_VERSION="0.7.0"
+          IDRIS2_VERSION="0.8.0"
           curl -fsSL \
             "https://github.com/idris-lang/Idris2/releases/download/v${IDRIS2_VERSION}/idris2-${IDRIS2_VERSION}-ubuntu-20.04.tar.gz" \
             -o /tmp/idris2.tar.gz || true
@@ -79,9 +94,13 @@ jobs:
           fi
 
       # ---- Zig ----
+      # 0.15.1 is the version ffi/zig/build.zig is written against (header
+      # comment "Updated for Zig 0.15+ API (addLibrary / createModule
+      # pattern)"). 0.12 lacks `b.addLibrary` and the `.root_module` field
+      # and will not parse the build script.
       - name: Install Zig
         run: |
-          ZIG_VERSION="0.12.0"
+          ZIG_VERSION="0.15.1"
           curl -fsSL \
             "https://ziglang.org/download/${ZIG_VERSION}/zig-linux-x86_64-${ZIG_VERSION}.tar.xz" \
             -o /tmp/zig.tar.xz
@@ -90,9 +109,9 @@ jobs:
 
       # ---- Node (for smoke test within E2E script) ----
       - name: Set up Node.js
-        uses: actions/setup-node@v6
+        uses: actions/setup-node@2028fbc5c25fe9cf00d9f06a71cc4710d4507903 # v6.0.0
         with:
-          node-version: '22'
+          node-version: '25'
 
       # ---- Full E2E ----
       - name: Run full E2E (with build checks)

.gitignore

@@ -52,6 +52,8 @@ erl_crash.dump
 !tests/e2e/*.mjs
 !tests/contracts/*.mjs
 !tests/levels/*.mjs
+!tests/aspect/*.mjs
+!benchmarks/*.mjs
 *.cmi
 *.cmj
 *.cmt

Justfile

@@ -146,7 +146,8 @@ test-contract:
 test-e2e:
     @echo "Running end-to-end tests..."
     rescript build
-    node tests/e2e/e2e-smoke.mjs
+    node tests/smoke/e2e-smoke.mjs
+    node tests/e2e/e2e-driver.mjs
 
 # Aspect tests for cross-surface claim coherence
 test-aspect:

LEVEL-STATUS.md

@@ -75,10 +75,14 @@ time; they are not needed at runtime.
 
 ## What "draft" means
 
-Levels 11-12 currently have draft Idris2 files and example syntax, but they are
-not part of `typed-wasm.ipkg` and, as of 2026-03-30, both standalone checks
-fail. Zero dangerous patterns is not enough here: a file that does not
-type-check is not a claimable proof artefact. Wiring these levels into the
+Levels 11-12 are draft for surface semantics, not for ipkg membership.
+As of 2026-04-18 (commit A1) both `Tropical.idr` and `Epistemic.idr` are
+in `typed-wasm.ipkg` and build clean under Idris2 0.8.0 — see the
+2026-05-18 reconciliation in `PROOF-NEEDS.md`. The "draft" label
+applies to the level semantics themselves (Tropical cost-tracking and
+Epistemic freshness propagation under concurrent writes remain
+research-grade): theorems live, but the surface language and Zig FFI
+do not yet expose them. Wiring these levels through the rest of the
 toolchain remains future work.
 
 ## Proof inventory

README.adoc

@@ -79,9 +79,10 @@ WASM instructions with zero overhead.
 | 10 | Linearity | Linear resource usage
 |===
 
-L11-L12 research files exist in the repository, but they are not part of the
-default checked Idris2 package and are not currently claimed as integrated or
-machine-checked proof surface.
+L11-L12 (Tropical, Epistemic) are in `typed-wasm.ipkg` and build clean under
+Idris2 0.8.0 as of 2026-04-18 (see `PROOF-NEEDS.md` reconciliation). Their
+surface semantics remain research-grade — the parser, Zig FFI and downstream
+tooling do not yet expose L11/L12 features.
 
 == The Killer Feature: Multi-Module Type Safety
 

ROADMAP.adoc

@@ -26,7 +26,10 @@ Key capabilities delivered:
 
 Known audit constraints:
 
-* L11-L12 draft files are not part of `typed-wasm.ipkg` and currently fail standalone type-checking
+* L11 (Tropical) and L12 (Epistemic) are in `typed-wasm.ipkg` since 2026-04-18
+  (commit A1) and build clean under Idris2 0.8.0 (PROOF-NEEDS.md reconciliation
+  2026-05-18). Treat them as research/draft for surface semantics, not for
+  ipkg membership.
 * Release/build/container metadata still contains template residue
 * Benchmark and venue-facing paper claims require evidence cleanup before submission
 

TEST-NEEDS.md

@@ -6,41 +6,63 @@
 
 | Category | Count | Details |
 |----------|-------|---------|
-| **Source modules** | 21 | 11 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic), 3 ReScript parser (Ast, Parser, Lexer), 3 Idris2 interface ABI, 2 Zig FFI + cache |
-| **Unit tests** | 1 file | ParserTests.res (~82 assertions) |
-| **Integration tests** | 0 | None |
-| **E2E tests** | 1 | e2e-smoke.mjs (~43 assertions) |
-| **Property-based tests** | 1 | property_test.mjs (10 properties, ~40+ assertions) |
-| **Benchmarks** | 0 | None |
-| **ECHIDNA harness** | 1 | echidna-harness.mjs (7 assertions) |
+| **Source modules** | 21 | 11 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic), 4 ReScript parser (Ast, Parser, Lexer, Checker), 3 Idris2 interface ABI, 2 Zig FFI + cache, 1 Rust verifier crate (typed-wasm-verify, ~1.6k LOC + 53 tests) |
+| **Unit tests** | 2 files | ParserTests.res (88 assertions), crates/typed-wasm-verify (43 unit + 10 cross-compat) |
+| **Integration tests** | 1 | tests/contracts/airborne-step-state-contract.mjs (14 assertions) |
+| **E2E tests** | 2 | tests/smoke/e2e-smoke.mjs (40 assertions), tests/e2e/e2e-driver.mjs (corpus driver) |
+| **Per-level tests** | 10 | tests/levels/L1.mjs .. L10.mjs (56 assertions total) |
+| **Aspect tests** | 1 | tests/aspect/claim-envelope.mjs (49 assertions — added 2026-05 to catch cross-doc claim drift after deep audit found 5 such drifts) |
+| **Property-based tests** | 0 | tests/property/property_test.mjs claimed DONE 2026-04-04 but file is absent — stale entry being scrubbed |
+| **Benchmarks** | 1 | benchmarks/parser-bench.mjs (per-example wallclock; median/p95/min/throughput; JSON summary on stderr; added 2026-05) |
+| **ECHIDNA harness** | 1 | tests/echidna/echidna-harness.mjs (659 LOC, 124 local assertions, remote prover-wars submission) |
 
 ## What's Missing
 
 ### P2P Tests
-- [x] **DONE 2026-04-04**: Property-based tests added (`tests/property/property_test.mjs`, 10 properties, ~40+ assertions)
+- [ ] **REVOKED 2026-05**: prior "DONE 2026-04-04 property tests" entry was
+      false — `tests/property/property_test.mjs` was never committed.
+      Aspect test now catches this drift class automatically.
 - [ ] No tests for Idris2 ABI type checking with Zig FFI
 - [ ] No tests for ReScript parser feeding into Idris2 type checker
 
 ### E2E Tests
-- [ ] e2e-smoke exists but only 43 assertions for a type system with 10 safety levels
-- [ ] No WASM module compilation and execution test
-- [ ] No multi-module linking test (MultiModule.idr untested)
+- [x] **DONE 2026-05**: `tests/e2e/e2e-driver.mjs` exercises every
+      example through parse + check with skip/expect-clean/expect-diagnostic
+      pragmas. Smoke test still narrow (40 assertions) but now augmented
+      by the per-level suite (56 more) and the aspect test (49 more).
+- [ ] No WASM module compilation and execution test (blocked on codegen)
+- [ ] No multi-module linking test (MultiModule.idr untested at runtime)
 
 ### Aspect Tests
-- [ ] **Security**: No memory safety violation detection tests (this IS the product's purpose)
-- [ ] **Performance**: No benchmarks for type checking overhead vs raw WASM
+- [x] **DONE 2026-05**: `tests/aspect/claim-envelope.mjs` — 49 checks that
+      cross-document claims (README/ROADMAP/LEVEL-STATUS/EXPLAINME) stay
+      consistent with actual artefacts (ipkg, Rust constants, CI pins,
+      example corpus, RSR surface). Built in response to a deep audit
+      finding five drifts the test now catches.
+- [ ] **Security**: No memory safety violation detection tests (this IS the
+      product's purpose)
+- [ ] **Performance**: see Benchmarks below
 - [ ] **Concurrency**: No concurrent WASM module compilation tests
-- [ ] **Error handling**: No tests for invalid type annotations, malformed WASM
+- [ ] **Error handling**: 10/10 per-level test suites (`tests/levels/L*.mjs`)
+      include negative cases — partial coverage
 
 ### Build & Execution
 - [ ] 11 Idris2 modules with 0 Idris2-level tests -- are proofs checked?
+      (PROOF-NEEDS.md 2026-05-18 reconciliation: ipkg builds clean, but
+      no Idris2 *test* layer beyond compile-time totality / type-checking)
 - [ ] Zig FFI integration_test.zig likely a template placeholder
 
-### Benchmarks Needed (CRITICAL)
-- [ ] Type checking overhead per WASM instruction
-- [ ] Memory region tracking performance
-- [ ] Lifetime analysis scaling with module size
+### Benchmarks
+- [x] **DONE 2026-05**: `benchmarks/parser-bench.mjs` — per-example parse +
+      check wallclock with median / p95 / min / throughput and JSON summary
+      for trend tracking. Only the parser is end-to-end today, so that's
+      where benchmark evidence has to start.
+- [ ] Type-checking overhead per WASM instruction (blocked on codegen +
+      Zig FFI runtime path)
+- [ ] Memory region tracking performance (blocked on codegen)
+- [ ] Lifetime analysis scaling with module size (blocked on codegen)
 - [ ] Comparison: typed-wasm overhead vs raw WASM execution
+      (blocked on codegen)
 
 ### Self-Tests
 - [ ] No type system self-consistency check