proof-progress(typed-wasm): spec tracker stale — TW1 partial work landed, TW4 effectively discharged, TW3 ReScript doc-drift

[hyperpolymath]

Routine proof-progress check — 2026-05-21

Baseline: 2026-04-30, all six theorems [ ] Pending.

---

Status Tracker delta

#	Theorem	Spec says	Actual state	Change?
TW1	L1-L10 progressive type safety	[ ] Pending	Partial progress — §A9 attestLN_Sound family (15 levels) added in commit 987da5c (2026-05-19); witness→certificate-claims-level bridge now exists. Stronger "attestation entails semantic property" remains future work. Spec tracker not updated.	Yes — spec is stale
TW2	Region immutability post-declaration	[ ] Pending	Still blocked — RegionImmut.idr does not exist.	No change
TW3	Multi-module schema agreement	[ ] Pending	Still blocked — SchemaAgree.idr does not exist. Plus doc-drift (see below).	No change (+ doc-drift)
TW4	No escape hatches in L1-L10	[ ] Pending	Effectively discharged — comprehensive re-grep of all 21 .idr files finds ZERO believe_me / assert_total / assert_impossible (only "NO believe_me" banner comments). Confirmed by clean Idris2 0.8.0 build (typed-wasm.ipkg rc=0, 21/21 TTC). Spec tracker not updated, verification/proofs/idris2/NoEscape.idr not yet written.	Yes — spec is stale
TW5	Linear handle consumption (L10)	[ ] Pending	Still blocked — no new proof content in Linear.idr.	No change
TW6	Lifetime resource cleanup (L9)	[ ] Pending	Still blocked — no new proof content in Lifetime.idr.	No change

---

TW3 doc-drift (stale language reference)

docs/proofs/spec-templates/T2-high/typed-wasm.md line 67 still reads:

Statement: Rust and ReScript modules importing same region must see identical definition.

ReScript is banned as of 2026-04-30 (CLAUDE.md language policy; estate migration is RS/TS/JS → AffineScript → typed-wasm). The estate language default is now AffineScript.

Proposed corrected wording:

Statement: Rust and AffineScript modules importing same region must see identical definition.

Note: commit eb9966b in typed-wasm (2026-05-18) already retired ReScript guidance text in EXPLAINME.adoc and PROOF-NEEDS.md, but the standards spec-template was not updated as part of that sweep.

---

TW4 escape-hatch grep results (for the record)

Grep over Region.idr, Levels.idr, TypedAccess.idr, Effects.idr, Linear.idr, Lifetime.idr, Proofs.idr for believe_me, assert_total, assert_impossible:

ZERO matches (excluding "NO believe_me" banner comments)

TW4 obligation (§ "Scan L1-L10 modules / Document zero matches") is factually satisfied. The formal NoEscape.idr proof file (verification/proofs/idris2/NoEscape.idr) still needs to be created to close the checkbox.

---

Recommended actions

1. Update spec tracker in docs/proofs/spec-templates/T2-high/typed-wasm.md:

   • TW1: mark as [ ] In-progress (§A9 bridge landed; stronger claim pending)
   • TW4: mark as [x] Verified once NoEscape.idr is written and committed

2. Fix TW3 doc-drift: replace "ReScript" → "AffineScript" in the TW3 statement (line 67).

3. Write NoEscape.idr at verification/proofs/idris2/NoEscape.idr to formally close TW4's checkbox obligation.

---

Environment note

idris2 was not available in the check environment; build-clean status taken from commit 987da5c message ("verified with Idris2 0.8.0 via typed-wasm.ipkg: rc=0, 0 errors, 21/21 TTC").

Refs typed-wasm commit 987da5c (proof(abi): discharge witness-discarding attestations + reconcile #130)
Refs typed-wasm commit eb9966b (chore: retire ReScript guidance text → AffineScript, Estate Item 9)

[hyperpolymath]

Status delta — 2026-05-30 (proof-progress check):

TW1 (L1-L10 progressive type safety) — Materially advanced. typed-wasm A10/A11/A12/A13 all CLOSED (typed-wasm#72/#79/#80); L2/L3-L6/L15 carrier-backed verifier coverage SHIPPED via typed-wasm proposals 0001+0002 (now ADR-0002 + ADR-0003; PRs #107/#109/#115/#116). Spec tracker still likely understates progress.

TW3 (Multi-module schema agreement) — Still blocked: SchemaAgree.idr does not exist. L13 cross-module is a remaining gap, gated on producer codegen (proposals 0003+0004 are still [draft]).

TW4 (No escape hatches in L1-L10) — Still effectively discharged. Worth a spec-tracker [x] Discharged flip.

Long-tail remaining: WasmCert-Isabelle tie-back, .wasm byte-equality (blocked on emitter), Idris2 parser round-trip (Phase 0 Track A).

Suggest: refresh the tracker rows for TW1/TW4 to current reality, leave TW2/TW3 pending, then close this status-snapshot issue.

[hyperpolymath]

Closing this snapshot per today's status-delta comment. Spec-tracker rows for TW1 (materially advanced — A10/A11/A12/A13 closed + proposals 0001+0002 accepted) and TW4 (effectively discharged) should be refreshed in a separate spec-edit PR. TW2 + TW3 remain genuinely pending (gated on RegionImmut.idr + SchemaAgree.idr not existing yet; proposals 0003+0004 still [draft]).