docs: make soundness status a single, test-anchored source of truth

The known soundness holes (#554/#555/#556/#558/#559) were fixed, fenced, or
removed across 2026-05/2026-06, but their status was duplicated across ~6 docs
that drifted independently. A reader who opened the stale one (the
CAPABILITY-MATRIX rows, the CLAUDE.md survey block, a STATE snapshot) got a
stale "is it sound?" answer — and in the dangerous direction.

Structural fix, not just prose:

- Add docs/SOUNDNESS.adoc: the single source of truth for soundness-hole
  status, test-anchored (every row names the fixture/test that proves it),
  with a freshness stamp (SHA + date). Ground-truthed against a green
  `dune build` / `dune runtest` at 85e3f0d on 2026-06-21.
- Add tools/check-soundness-ledger.sh, wired into `just guard` + CI: fails the
  build if the ledger loses its primacy declaration or freshness stamp, if any
  anchor fixture it cites goes missing, or if a status surface stops linking
  back to it. This binds prose to executable truth so the ledger cannot rot
  silently (verified: the gate fails on a missing anchor).
- Correct every live status surface to ground-truth and point at the ledger:
  README, CAPABILITY-MATRIX (borrow / effects / refinement / traits rows + the
  anti-over-claim bullet + See-also), PROOF-NEEDS (holes block + P-9/P-10),
  NAVIGATION, reference/COMPILER-CAPABILITIES, TECH-DEBT (CORE-04/CORE-05),
  the wiki (README + traits + dependent-types), STATE.a2ml, agent debt, and
  the CLAUDE.md survey (converted to a deferral; no header/license change).
- Cap the dated STATE-2026-06-11 snapshot with a superseded banner rather than
  rewriting history.

Ground-truth recorded: #554 fixed (use-after-move via a callee-returned borrow
rejected), #555 fenced loud on every compiled backend (one pinned interpreter
non-tail-resume residual), #556 fixed, #558 removed, #559 fixed for concrete
overlaps, #553 Polonius M1-M3 but test-only/unwired. Closing these
implementation holes is not the same as proving soundness; the metatheory
remains prose (PROOF-NEEDS).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa

Author: claude

.claude/CLAUDE.md

@@ -9,7 +9,7 @@
 | File extension | `.affine` (plus face dialects) | `.eph` |
 | Build | `dune-project` at root | `Cargo.toml` at root |
 | Type checker | `lib/borrow.ml` (OCaml) | `ephapax-linear/src/{linear,affine}.rs` (Rust) |
-| Proofs | None mechanized (programme filed: #513–#521, unstarted); soundness arguments live in `lib/borrow.ml` + `docs/CAPABILITY-MATRIX.adoc`. CORE-01/#177 CLOSED 2026-05-30; known hole #554; Polonius residual #553 | `formal/Semantics.v` (Coq), `src/abi/Ephapax/…` (Idris2) |
+| Proofs | None mechanized (programme filed: #513–#521, unstarted); soundness arguments live in `lib/borrow.ml` + `docs/CAPABILITY-MATRIX.adoc`; soundness-hole status is the test-anchored `docs/SOUNDNESS.adoc` (CORE-01/#177 CLOSED 2026-05-30; #554 FIXED; Polonius #553 test-only/unwired) | `formal/Semantics.v` (Coq), `src/abi/Ephapax/…` (Idris2) |
 
 **The trap.** Ephapax is internally dyadic — it contains `ephapax-linear` and `ephapax-affine` *sublanguages* inside one Rust crate. **The `ephapax-affine` sublanguage is NOT AffineScript.** The word `affine` is shared because both type systems happen to be substructural-logic-family — that's a logic-family fact, not a project relationship.
 
@@ -208,22 +208,21 @@ Action (gitbot): Never use GitHub's "close issue" API directly; only close via P
 Practical guidance for agents (Claude / other) operating in this repo,
 captured from parallel-bot session experience. Read once; saves turns.
 
-### Known soundness items (2026-06-11 survey — read before claiming soundness)
-
-Execution-verified, open, and load-bearing for any "is this sound?" answer:
-
-* **#554** — the borrow checker ACCEPTS use-after-move through a
-  callee-returned borrow (`let r = pick(a); consume(a); *r` passes).
-  Do not state "the soundness gap closed with CORE-01" — #177 closed,
-  this hole remains. Polonius residual: #553 (ADR-022, 0% implemented).
-* **#555** — `handle` is silently mis-lowered on core-WASM / JS-text /
-  Deno-ESM (arms dropped; interpreter 42 vs wasm 41 on an effects-free
-  return-arm program). Interpreter handler dispatch is shallow
-  single-shot tail-resume only. Zero runtime handler tests exist.
-* **#556** — Async CPS table-miss silently lowers synchronously.
-* **#558** — refinement-type predicates parse but are silently not
-  enforced. **#559** — trait coherence not checked.
-* v1 release-readiness ledger (tiers + estate cross-refs): **#563**.
+### Known soundness items — canonical in docs/SOUNDNESS.adoc
+
+Soundness-hole status lives in *one* test-anchored place, `docs/SOUNDNESS.adoc`,
+and is enforced by `tools/check-soundness-ledger.sh`. **Do not restate per-issue
+status here** — a dated survey block in this file is exactly what went stale (it
+listed #554/#555/#556/#558/#559 as open long after they were fixed/fenced/removed,
+which produced a stale "is it sound?" answer). Ground-truth from
+`docs/SOUNDNESS.adoc` and the running compiler before claiming anything.
+
+Convenience snapshot (may lag — `docs/SOUNDNESS.adoc` wins): as of 2026-06,
+#554 fixed, #555 fenced loud on every compiled backend (one pinned interpreter
+non-tail-resume residual), #556 fixed, #558 removed, #559 fixed for concrete
+overlaps, #553 Polonius test-only/unwired. Closing these implementation holes is
+not the same as proving soundness (metatheory still prose — `docs/PROOF-NEEDS.adoc`).
+v1 release-readiness ledger: **#563**.
 
 ### CI signal reliability
 

.github/workflows/ci.yml

@@ -89,6 +89,14 @@ jobs:
         # "production-ready" / stdlib-% phrase beyond tools/doc-overclaims.allow).
         # See tools/check-doc-truthing.sh.
         run: ./tools/check-doc-truthing.sh
+      - name: Soundness-ledger anti-staleness gate
+        # docs/SOUNDNESS.adoc is the single source of truth for soundness-hole
+        # status. This gate fails if the ledger loses its primacy declaration or
+        # freshness stamp, if any test fixture it names as an anchor goes
+        # missing, or if a status surface (README / CAPABILITY-MATRIX /
+        # PROOF-NEEDS / NAVIGATION / CLAUDE.md) stops linking back to it.
+        # See tools/check-soundness-ledger.sh.
+        run: ./tools/check-soundness-ledger.sh
       - name: Check formatting
         run: opam exec -- dune build @fmt
   lint:

.machine_readable/6a2/STATE.a2ml

@@ -79,9 +79,9 @@ affine-types = "wired-and-reachable (Track A Manhattan plan complete 2026-04-10.
 linear-arrows = "enforced (2026-04-11): Three-part fix landed. (1) typecheck.ml lambda synth: |@linear x: T| e now synthesises T -[1]-> U (was always QOmega). (2) typecheck.ml lambda check mode: explicit param quantity annotation validated against expected TArrow quantity; unannotated params inherit context quantity. (3) quantity.ml ExprLambda: added env.errors accumulator; annotated lambda params declared via env_declare so env_use tracks them; usage verified with check_quantity after body walk; violations pushed to env.errors and drained at end of check_function_quantities (step 4). Saved/restored env.quantities entries to prevent scope leakage. Two E2E fixtures + 2 passing tests. 75 tests total, 0 regressions. Commit d2f9b7b pushed."
 borrow-checker = "phase-3-parts-1-3-Slices-A-B-C-light-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted, shared-XOR-exclusive enforced at use sites, ownership from param type TyOwn/TyRef/TyMut, call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape + &mut e parser surface. pt3 Slice A (PR #335) NLL last-use expiry: compute_last_use_index pre-pass; check_block expires in-block ref-bindings once their binder is dead. pt3 Slice B (effectively #354/#355/#356 after #351 procedural close) flow-sensitive escape via re-assignment: `outer = &y` in StmtAssign pre-releases the held borrow and re-binds the ref-graph entry to the freshly-created borrow. pt3 Slice C-light (this PR) CFG-join semantics for non-match join constructs: ExprHandle handler arms and ExprTry catch arms are now isolated via snapshot-restore-merge (factored merge_arm_results helper, mirroring ExprMatch's inlined logic) — moves/borrows from arm i no longer pollute arm i+1. 2 hermetic tests (positive: independent catch-arm moves OK; anti-regression: body-side move persists past the try). Residual (Slices C-full, C', D): true Polonius origin/region variables on TyRef/TyMut with subset constraints + datalog-style solver (architectural; ADR-gated); loop soundness via 2-iter check (coupled to StmtAssign clear-on-rewrite fix); reborrow through indirection (ref-to-ref binding); quantity-checker tightening for captured linears. Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT-alt.adoc CORE-01."
 row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
-effects = "interpreter-complete (handler dispatch, PerformEffect propagation, ExprResume, multi-arg ops all wired in interp.ml 2026-04-11). WasmGC: ops registered as unreachable stubs; ExprHandle/ExprResume reject with UnsupportedFeature — full WASM dispatch needs EH proposal or CPS transform."
-dependent-types = "parse-only (TRefined AST node exists and refinement predicates parse, but predicates do not reduce; no SMT/decision procedure wired in)"
-traits = "90% (2026-04-11, commit 1ca143e): trait_registry added to typecheck context; TopTrait/TopImpl processed in forward pass; ExprField falls back to Trait.find_method_for_type on record-field failure; find_impl/find_impls_for_type use unification-based matching via fresh_impl_self_ty + Unify.unify instead of name string comparison; TopImpl bodies type-checked via check_fn_decl with Self bound; check_impl_satisfies_trait verifies required methods present. Two E2E fixtures + 2 tests. 80 total, 0 regressions. Remaining: associated type substitution in method bodies, where-clause supertrait enforcement, coherence checking.)"
+effects = "interpreter-complete (handler dispatch, PerformEffect propagation, ExprResume, multi-arg ops all wired in interp.ml 2026-04-11). WasmGC: ops registered as unreachable stubs; ExprHandle/ExprResume reject with UnsupportedFeature. Every compiled backend (core-WASM, WasmGC, Deno-ESM, JS-text, C) now fails loud on handle/resume (#555 fenced); interp multi-shot fails loud; one non-tail single-shot residual is pinned by a test. Authoritative: docs/SOUNDNESS.adoc."
+dependent-types = "removed-v1 (refinement/dependent surface withdrawn 2026-04-10 per #558; no TRefined node remains; assume(...) rejected at parse; T where (P) is a parse error — no unenforced predicate is expressible). Authoritative: docs/SOUNDNESS.adoc + docs/CAPABILITY-MATRIX.adoc"
+traits = "90% (2026-04-11, commit 1ca143e): trait_registry added to typecheck context; TopTrait/TopImpl processed in forward pass; ExprField falls back to Trait.find_method_for_type on record-field failure; find_impl/find_impls_for_type use unification-based matching via fresh_impl_self_ty + Unify.unify instead of name string comparison; TopImpl bodies type-checked via check_fn_decl with Self bound; check_impl_satisfies_trait verifies required methods present. Two E2E fixtures + 2 tests. 80 total, 0 regressions. Coherence checking now wired (#559, concrete overlaps whose self types unify are rejected; typecheck.ml check_all_coherence). Remaining: associated type substitution in method bodies, where-clause supertrait enforcement, generic-subsumption overlap (#559 follow-up). Authoritative: docs/SOUNDNESS.adoc.)"
 
 [track-a-manhattan]
 owner = "primary"

.machine_readable/agent_instructions/debt.a2ml

@@ -53,7 +53,7 @@ discovered = "2026-04-11"
 
 [[debt.could]]
 component = "lib/typecheck.ml"
-issue = "Associated type substitution in method bodies and where-clause supertrait enforcement not yet implemented in traits. Coherence checking absent."
+issue = "Associated type substitution in method bodies and where-clause supertrait enforcement not yet implemented in traits. Concrete-overlap coherence checking DONE (#559, typecheck.ml check_all_coherence); generic-subsumption overlap is the follow-up. Authoritative: docs/SOUNDNESS.adoc."
 effort = "hard"
 impact = "medium"
 discovered = "2026-04-11"

README.adoc

@@ -31,13 +31,21 @@ link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambigu
 
 [IMPORTANT]
 ====
-*Authoritative status lives in link:docs/CAPABILITY-MATRIX.adoc[docs/CAPABILITY-MATRIX.adoc].*
-Where this README's prose implies broader maturity than that matrix states,
-the matrix wins. AffineScript is *alpha*: CORE-01 (#177) closed
-2026-05-30, but one known base-language soundness hole remains
-(use-after-move via a callee-returned borrow, issue #554; Polonius
-residual #553) and effect handlers are silently mis-lowered on three
-backends (#555). The v1 release-readiness ledger is issue #563.
+*Authoritative status lives in link:docs/CAPABILITY-MATRIX.adoc[docs/CAPABILITY-MATRIX.adoc]
+(feature readiness) and link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc]
+(soundness-hole status — test-anchored, the single source of truth for what is
+fixed / fenced / removed / residual).* Where this README's prose implies
+broader maturity than those state, they win. AffineScript is *alpha*: CORE-01
+(#177) closed 2026-05-30, and the base-language soundness holes tracked through
+2026-06 are now fixed, fenced, or removed — use-after-move via a callee-returned
+borrow (#554) is rejected, effect handlers (#555) fail loud on every compiled
+backend rather than silently dropping arms, the async sync-fallback (#556) fails
+loud, and refinement predicates (#558) were removed rather than left unenforced.
+One pinned interpreter residual remains; see
+link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc] for the per-issue ledger. Closing
+these *implementation* holes is not the same as *proving* soundness — the
+metatheory is still prose (link:docs/PROOF-NEEDS.adoc[docs/PROOF-NEEDS.adoc]).
+The v1 release-readiness ledger is issue #563.
 typed-wasm is a *separate*
 language-agnostic target (`hyperpolymath/typed-wasm`), not an AffineScript
 subsystem — see link:docs/ECOSYSTEM.adoc[docs/ECOSYSTEM.adoc].
@@ -50,7 +58,7 @@ Write software where the compiler helps enforce resource lifecycles, protocol st
 
 [NOTE]
 ====
-Honest status sync (2026-04-12): affine/QTT and borrow checking are wired into the standard CLI paths today (`check`, `compile`, `eval`) and gate user programs. Dependent/refinement features are still parse-first in places, and some backend features remain incomplete, especially around effect-handler lowering in Wasm targets. See link:docs/CAPABILITY-MATRIX.adoc[docs/CAPABILITY-MATRIX.adoc] for the authoritative per-feature status (`.machine_readable/6a2/STATE.a2ml` mirrors that matrix; it does not lead).
+Honest status sync (2026-06-21): affine/QTT and borrow checking are wired into the standard CLI paths today (`check`, `compile`, `eval`) and gate user programs. Refinement/dependent-type surface was *removed* in v1 rather than left parse-only-and-unenforced (#558); effect-handler lowering on the compiled backends now *fails loud* rather than silently dropping arms (#555). See link:docs/CAPABILITY-MATRIX.adoc[docs/CAPABILITY-MATRIX.adoc] for authoritative per-feature status and link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc] for soundness-hole status (`.machine_readable/6a2/STATE.a2ml` mirrors the matrix; it does not lead).
 ====
 
 == What AffineScript Is

docs/CAPABILITY-MATRIX.adoc

@@ -82,18 +82,17 @@ estate re-audit + ReScript residue (#229) follow separately.
 `Never`/bottom, block divergence. Enforced on every check/compile/eval path.
 
 |Effect system |partial |Pure/impure separation + effect polymorphism
-enforced. Handlers: interpreter dispatch is *shallow single-shot
-tail-resume only* (`resume(v)` returns `v` as the whole handle result,
-discarding post-perform code — in-code admission at `interp.ml:248-263`);
-WasmGC dispatch is `UnsupportedFeature` (loud); core-WASM, JS-text and
-Deno-ESM *silently drop handler arms* — execution-verified divergence on
-an effects-free return-arm program, tracked as #555 (decision: back-port
-the WasmGC loud failure). The #225 CPS line closed the *async slice*
-only; its table-miss fallback silently lowers synchronously (#556).
+enforced. Handlers: *every compiled backend* (core-WASM, WasmGC, Deno-ESM,
+JS-text, C) now *fails loud* (`UnsupportedFeature`) instead of silently
+dropping handler arms — the execution-verified return-arm divergence (#555)
+is closed. Interpreter dispatch is shallow single-shot tail-resume; multi-shot
+now fails loud; the one non-tail single-shot residual is pinned by a test. The
+#225 CPS async table-miss *fails loud*, not silently synchronous (#556 closed).
+Full status + test anchors: link:SOUNDNESS.adoc[SOUNDNESS.adoc].
 
 |Borrow checker |*partial — full CORE-01 slice stack landed, #177
-CLOSED 2026-05-30; one known soundness hole (#554); Polonius residual
-(#553)* |
+CLOSED 2026-05-30; the #554 soundness hole is now FIXED; Polonius
+residual (#553) is M1–M3, test-only/unwired — see link:SOUNDNESS.adoc[SOUNDNESS.adoc]* |
 Place/borrow/move infra + use-after-move, conflicting-borrow,
 move-while-borrowed, lambda-capture. *CORE-01 part 1* (PR #240, Refs #177,
 gate 263/263): borrow-graph validation wired — `BorrowOutlivesOwner` now
@@ -129,13 +128,12 @@ true Polonius origin/region variables on `TyRef`/`TyMut` with subset
 constraints + datalog-style loan-live-at-point solver — ADR-022,
 tracked as #553 (design ratified in-thread, 0% implemented; M1 sketch
 at branch `core-01/polonius-m1-sketch`); quantity-checker tightening
-for captured linears. *Known soundness hole (execution-verified):*
-use-after-move through a *callee-returned borrow* passes the full
-pipeline (#554) — call-arg borrows are released at call end and call
-results never register as borrow sources, so `let r = pick(a);
-consume(a); *r` is accepted. This is the loan-propagation class
-Polonius (#553) resolves; until then the checker is unsound on this
-shape, not merely imprecise.
+for captured linears. *Former soundness hole (#554) — now FIXED:*
+use-after-move through a *callee-returned borrow* (`let r = pick(a);
+consume(a); *r`) is now rejected as `MoveWhileBorrowed`, with hardening +
+anti-over-rejection fixtures. The per-issue, test-anchored status (and the
+Polonius #553 extractor's test-only standing) lives in
+link:SOUNDNESS.adoc[SOUNDNESS.adoc].
 
 |Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
 invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`
@@ -146,11 +144,16 @@ Linear arrows enforced.
 `resume`. `let mut` mutation path has known baseline gaps.
 
 |Traits |partial |Registry, `TopTrait`/`TopImpl`, unification-based
-`find_impl`, impl-satisfies-trait. Missing: associated-type substitution in
-method bodies, where-clause supertraits, coherence checking.
+`find_impl`, impl-satisfies-trait, and *coherence checking* (#559 — overlapping
+impls whose self types unify are rejected; wired in `typecheck.ml`
+`check_all_coherence`). Missing: associated-type substitution in method bodies,
+where-clause supertraits, generic-subsumption overlap (#559 follow-up). See
+link:SOUNDNESS.adoc[SOUNDNESS.adoc].
 
-|Dependent / refinement types |parse-only |`TRefined` parses; predicates do
-not reduce; no SMT/decision procedure.
+|Dependent / refinement types |*removed (v1)* |Withdrawn 2026-04-10 rather than
+shipped parse-only-and-unenforced (#558): no `TRefined` node remains,
+`assume(...)` is rejected at parse, `T where (P)` is a parse error — you cannot
+write an unenforced predicate. See link:SOUNDNESS.adoc[SOUNDNESS.adoc].
 
 |Row polymorphism |partial |Records + effect rows in typecheck/unify; not
 fully exercised end-to-end.
@@ -224,12 +227,16 @@ A few primitives remain `extern` builtins.
 
 == What AffineScript is NOT (anti-over-claim)
 
-* Not "production-ready". Alpha. CORE-01 (#177) closed 2026-05-30, but the
-  borrow checker has one known, execution-verified soundness hole —
-  use-after-move through a callee-returned borrow (#554; Polonius residual
-  #553) — and effect handlers are silently mis-lowered on three backends
-  (#555) with a silently-synchronous async fallback (#556). The v1
-  release-readiness ledger is #563.
+* Not "production-ready". Alpha. CORE-01 (#177) closed 2026-05-30. The
+  base-language soundness holes tracked through 2026-06 are now fixed, fenced,
+  or removed — #554 (use-after-move via a callee-returned borrow) is rejected,
+  #555 (effect handlers) fail loud on every compiled backend, #556 (async
+  fallback) fails loud, #558 (refinements) were removed — with one pinned
+  interpreter residual. The per-issue, test-anchored ledger is
+  link:SOUNDNESS.adoc[SOUNDNESS.adoc]. Closing these *implementation* holes is
+  not the same as *proving* soundness: the metatheory remains prose
+  (link:PROOF-NEEDS.adoc[PROOF-NEEDS.adoc]). The v1 release-readiness ledger
+  is #563.
 * Not "N production backends". One reference target (WASM), two solid JS-host
   targets (Deno-ESM, Node-CJS), the rest experimental.
 * typed-wasm is *not* an AffineScript subsystem. It is a separate,
@@ -252,6 +259,9 @@ any capability change; `STATE.a2ml` mirrors, it does not lead.
 
 == See also
 
+* link:SOUNDNESS.adoc[SOUNDNESS.adoc] — the single source of truth for
+  soundness-hole status (test-anchored). This matrix owns *feature readiness*;
+  the ledger owns *soundness holes*.
 * link:ECOSYSTEM.adoc[ECOSYSTEM.adoc] — the spine, the real AS↔typed-wasm
   contract, the satellite registry, the Stage A–E definitions, INT-01..12.
 * link:TECH-DEBT.adoc[TECH-DEBT.adoc] — the coordination ledger.