From b84f6fb7fa02af3b5b7869131f1fe2d4c93cd14a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 11:55:16 +0000 Subject: [PATCH] docs: make soundness status a single, test-anchored source of truth MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa --- .claude/CLAUDE.md | 33 ++- .github/workflows/ci.yml | 8 + .machine_readable/6a2/STATE.a2ml | 6 +- .../agent_instructions/debt.a2ml | 2 +- README.adoc | 24 +- docs/CAPABILITY-MATRIX.adoc | 64 ++--- docs/NAVIGATION.adoc | 5 +- docs/PROOF-NEEDS.adoc | 36 +-- docs/SOUNDNESS.adoc | 222 ++++++++++++++++++ docs/STATE-2026-06-11.adoc | 10 + docs/TECH-DEBT.adoc | 8 +- docs/reference/COMPILER-CAPABILITIES.adoc | 5 +- justfile | 1 + tools/check-soundness-ledger.sh | 116 +++++++++ wiki/README.md | 17 +- wiki/language-reference/dependent-types.md | 19 +- wiki/language-reference/traits.md | 18 +- 17 files changed, 494 insertions(+), 100 deletions(-) create mode 100644 docs/SOUNDNESS.adoc create mode 100755 tools/check-soundness-ledger.sh diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 20a4b0b0..fe9902fc 100644 --- a/.claude/CLAUDE.md +++ b/.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 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4991030d..41163b47 100644 --- a/.github/workflows/ci.yml +++ b/.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: diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index a2299169..018b1f70 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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" diff --git a/.machine_readable/agent_instructions/debt.a2ml b/.machine_readable/agent_instructions/debt.a2ml index 89dfb75e..d64167a1 100644 --- a/.machine_readable/agent_instructions/debt.a2ml +++ b/.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" diff --git a/README.adoc b/README.adoc index fc7d7f88..23ba43c5 100644 --- a/README.adoc +++ b/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 diff --git a/docs/CAPABILITY-MATRIX.adoc b/docs/CAPABILITY-MATRIX.adoc index ca1ed792..d8bcd215 100644 --- a/docs/CAPABILITY-MATRIX.adoc +++ b/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. diff --git a/docs/NAVIGATION.adoc b/docs/NAVIGATION.adoc index 00b0ed34..0382e874 100644 --- a/docs/NAVIGATION.adoc +++ b/docs/NAVIGATION.adoc @@ -72,7 +72,9 @@ This guide helps you navigate the AffineScript repository structure. **Guides:** -* link:CAPABILITY-MATRIX.adoc[Capability Matrix] - **Live** per-component readiness (authoritative) +* link:CAPABILITY-MATRIX.adoc[Capability Matrix] - **Live** per-component readiness (authoritative for feature readiness) +* link:SOUNDNESS.adoc[Soundness Ledger] - **Live** test-anchored soundness-hole status (authoritative for "is it sound?"; the matrix links here). *Start here for soundness questions.* +* link:PROOF-NEEDS.adoc[Proof-Needs Inventory] - what must be *proven* (mostly unmechanised); distinct from the soundness ledger above * link:guides/TESTING-REPORT.adoc[Testing Report] - *RETIRED* (redirects to standards/TESTING.adoc + CAPABILITY-MATRIX.adoc) == Build System @@ -187,6 +189,7 @@ affinescript/ │ ├── TECH-DEBT.adoc # Coordination ledger (CORE/STDLIB/INT/DOC) │ ├── ECOSYSTEM.adoc # Spine + AS↔typed-wasm contract │ ├── KNOWN-ISSUES.md # Tracked issues backlog +│ ├── SOUNDNESS.adoc # Soundness-hole status — test-anchored SSOT (start here) │ ├── PROOF-NEEDS.adoc # Proof obligations inventory (P-/F-/K- series) │ ├── EXPLAINME.adoc # Receipts backing README claims │ ├── architecture/ # Compiler / backend internals diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index 3682bed4..a11bb885 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -84,14 +84,18 @@ defect but **none has a stated proof obligation** whose discharge would have caught it or would prevent regression — that linkage is itself a gap (see <>). -* **#554** — borrow checker *accepts* use-after-move through a callee-returned - borrow (`let r = pick(a); consume(a); *r` typechecks). Polonius residual: #553 - (ADR-022, 0% implemented). CORE-01/#177 closed 2026-05-30 did **not** close this. -* **#555** — `handle` is mis-lowered on core-WASM / JS-text / Deno-ESM (effect - arms dropped); interpreter dispatch is shallow single-shot tail-resume only. -* **#556** — async CPS table-miss silently lowers synchronously. -* **#558** — refinement-type predicates parse but are silently *not enforced*. -* **#559** — trait coherence is *not checked*. +These were the execution-verified *implementation* holes. As of 2026-06 their +implementation status is closed and now tracked, test-anchored, in +link:SOUNDNESS.adoc[docs/SOUNDNESS.adoc] — #554 *fixed* (UAM via callee-returned +borrow rejected), #555 *fenced loud* on every compiled backend (one pinned +interpreter residual), #556 *fixed*, #558 *removed* (refinements withdrawn, not +left unenforced), #559 *fixed* for concrete overlaps, #553 Polonius M1–M3 but +test-only/unwired. **That does not discharge the proof obligations below.** +Closing a hole means the implementation no longer exhibits the counterexample; +it does *not* mean the property is mechanically proven. The obligations these +holes motivate — most pointedly that the borrow proof must now be *stated to +reject the (now-fixed) #554 program* as a negative test — remain `prose` or +`absent`. Implementation truth: SOUNDNESS.adoc. Proof truth: this file. v1 readiness ledger: #563. Proof programme umbrella: #513. ==== @@ -157,15 +161,19 @@ obligations. They are the "we might have missed" half of the brief. | #513 must-have 8 | P-9 -| **Refinement enforcement = proof obligation.** #558 is simultaneously a bug - *and* the missing obligation "refinement predicates are checked." Drawing that - equivalence is itself the catalogue gap. -| L | `absent` +| **Refinement enforcement = proof obligation.** #558 was simultaneously a bug + *and* the missing obligation "refinement predicates are checked." *Withdrawn:* + the refinement/dependent surface was *removed* in v1, so there is no unenforced + predicate left to prove about (see link:SOUNDNESS.adoc[SOUNDNESS.adoc]). + Retained for history; reopen only if refinements return. +| L | `absent` (withdrawn) | #558 | P-10 -| **Trait coherence.** At most one instance resolves per (trait, type); #559 is - the open counterexample. +| **Trait coherence.** At most one instance resolves per (trait, type). The + *implementation* now rejects concrete overlaps (#559, see + link:SOUNDNESS.adoc[SOUNDNESS.adoc]); generic-subsumption overlap is the open + follow-up. The *proof* that resolution is unique remains unwritten. | L | `absent` | #559; #513 high-priority |=== diff --git a/docs/SOUNDNESS.adoc b/docs/SOUNDNESS.adoc new file mode 100644 index 00000000..61b6811a --- /dev/null +++ b/docs/SOUNDNESS.adoc @@ -0,0 +1,222 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2024-2026 hyperpolymath (Jonathan D.A. Jewell ) += AffineScript Soundness Ledger +:toc: macro +:toclevels: 3 +:icons: font +// Freshness stamp — update both when you re-ground-truth (see "Keeping this honest"). +:ground-truth-sha: d55e22c +:ground-truth-date: 2026-06-21 + +[IMPORTANT] +==== +*This document is the single source of truth for the status of AffineScript's +known soundness holes.* If any other document — `README.adoc`, +`docs/CAPABILITY-MATRIX.adoc`, `docs/PROOF-NEEDS.adoc`, `.claude/CLAUDE.md`, a +dated `STATE-*.adoc` snapshot, the wiki — disagrees with this ledger about +whether a hole is open, fixed, fenced, or removed, *this ledger wins* and the +other document is drift to be corrected. + +It is *test-anchored*: every row names the fixture or test that proves its +claim, and `tools/check-soundness-ledger.sh` (wired into `just check` + CI) +fails the build if any named fixture goes missing or if a status surface stops +pointing here. That binding is what stops this ledger going stale silently: +you cannot change a soundness behaviour without changing a test this ledger is +nailed to. +==== + +Ground-truthed at `{ground-truth-sha}` on {ground-truth-date} by source +inspection at the cited `file:line` anchors, with `dune build` and +`dune runtest` green. The status words below are deliberate; read them +precisely. + +toc::[] + +== Why this file exists + +Soundness status used to live in ~6 places that drifted independently — the +capability matrix, a survey block in `.claude/CLAUDE.md`, dated `STATE-*` +snapshots, session handoffs, the wiki. A reader (human or agent) who happened +to open the stale one got a stale answer, in the *dangerous* direction: +"this hole is still open" long after it was fixed, or — worse in principle — +the reverse. This file is the structural fix: + +. *One surface.* Soundness-hole status is stated here and nowhere else. Other + docs may *summarise* and then link here; they may not maintain a competing + per-issue ledger. The gate enforces the back-link. +. *Anchored to tests.* Each claim cites the executable artefact that proves it. + Prose detached from tests is what rots; prose nailed to a fixture cannot + drift without the fixture (and the gate) noticing. +. *Stamped.* The freshness attributes above record the commit and date this was + last reconciled against the running compiler. + +== Status vocabulary + +[cols="1,4"] +|=== +|Term |Meaning + +|*fixed* +|The previously-unsound behaviour is gone. The program that used to be wrongly + accepted is now rejected, or the wrong result is now the right one. + +|*loud-fail* +|The construct is not implementable on this path, but it *errors at + compile-time or run-time* — it never silently emits a plausible-wrong value. + "Fail loud, never silent" is the governing rule. + +|*removed* +|The feature whose surface could not be honestly enforced was withdrawn from + the language, so there is no unenforced surface left to mislead anyone. + +|*residual (pinned)* +|A known-incorrect behaviour still exists, but an executable test pins it, so + it cannot regress unnoticed and *will* alarm (the test flips to failing) the + day it is fixed. + +|*open (tracked)* +|A known gap with no fix yet, tracked by an issue. Stated here so it cannot be + mistaken for a guarantee. + +|*partial* +|Implemented and load-bearing for common cases; the named residual is the gap. +|=== + +== The ledger + +[cols="1,3,1,2",options="header"] +|=== +|Issue |Soundness claim (current behaviour) |Status |Proven in code + +|*#554* / #177 +|Use-after-move through a *callee-returned borrow* is rejected. + `let r = pick(a); consume(a); *r` no longer type-checks — it is reported as + `MoveWhileBorrowed`. CORE-01 (#177) closed; this was its last execution-verified + hole. +|*fixed* +|`test/e2e/fixtures/borrow_callee_returned_borrow_uam.affine` (+ the + `borrow_callee_returned_borrow_{aggregate,interproc,match_arm,return_stmt}.affine` + hardening variants and `borrow_callee_value_return_ok.affine` anti-over-rejection) + +|*#555* (codegen) +|`handle` / `resume` on *every compiled backend* (core-WASM, WasmGC, Deno-ESM, + JS-text, C) fails loud with `UnsupportedFeature` instead of silently dropping + handler arms. The old failure — compile the body, drop the arms, lower + `resume` as a pass-through (42 in the interpreter vs 41 in wasm) — is gone. +|*loud-fail* +|`test/e2e/fixtures/handle_return_arm.affine`; `lib/codegen.ml` `ExprHandle` / + `ExprResume` arms; `lib/codegen_deno.ml` + +|*#555* (interp, multi-shot) +|Calling `resume` more than once in a handler fails loud (it cannot be + expressed without reified continuations, and previously returned a + silently-wrong value). +|*loud-fail* +|`test/e2e/fixtures/handle_resume_multishot.affine`; `lib/interp.ml` resume + invocation counter + +|*#555* (interp, non-tail single-shot) +|`let x = op(); x + 100` resuming to `5` returns `5`, not `105`: the shallow + tree-walking continuation has already unwound the bind chain. This is the one + genuinely-still-silent shape, on the *interpreter* path only. It needs a CPS + rewrite of `eval` (blocked: OCaml 4.14 has no native effect handlers and the + interpreter must stay `js_of_ocaml`-compatible — owner-steer item). +|*residual (pinned)* +|`test/e2e/fixtures/handle_resume_nontail.affine` + + `test_resume_nontail_known_shallow` (asserts the wrong-but-known value; flips + to failing the day delimited continuations land) + +|*#556* +|Async CPS table-miss fails loud instead of silently lowering synchronously. +|*loud-fail* +|`test/e2e/fixtures/async_sync_fallback.affine` (+ `async_no_boundary.affine`, + `async_passthrough_thenable.affine`) + +|*#558* +|Refinement / dependent types were *removed* in v1 (2026-04-10). There is no + `TRefined` node for the checker to silently ignore; `assume(...)` is rejected + at parse and `T where (P)` is a parse error. You cannot write an unenforced + predicate. +|*removed* +|`test/e2e/fixtures/assume_rejected.affine` + `test_parse_assume_rejected` + +|*#559* +|Overlapping trait impls whose self types unify are rejected as a coherence + violation, before the check pass, so an ambiguous instance base is reported up + front. +|*fixed* +|`lib/typecheck.ml` `check_all_coherence` call; `lib/trait.ml` + `check_coherence` / `check_all_coherence`; the Trait-Coherence suite in + `test/test_e2e.ml` + +|*#559* (generic subsumption) +|Generic-subsumption overlap — `impl[T] Greet for Box[T]` overlapping + `impl Greet for Box[Int]` — is *not yet* detected; generic-impl registration + must be fixed first. Concrete overlaps (above) are caught. +|*open (tracked)* +|Documented in the coherence test block in `test/test_e2e.ml` + +|*#553* (Polonius) +|The Polonius extractor (ADR-022) is implemented through M3 but is + *TEST-ONLY / unwired* — it gates no production verdict. The lexical + `lib/borrow.ml` is the production checker; the extractor is diffed against it + over the fixture corpus with a shrinking allowlist (7 known divergences). +|*partial* +|`test/test_borrow_polonius.ml` (parallel-run diff gate + `known_divergences`) +|=== + +== Still open — read before claiming "sound" + +The implementation holes above are closed, but honesty requires naming what is +*not* a guarantee: + +* *Interpreter non-tail resume* (#555 residual, pinned) — see the ledger row. +* *Stub backends drop `return`.* The Lean and Why3 *experimental* code + generators drop `return` statements wholesale — a broader codegen-honesty gap + than #555, flagged but not yet fenced. Treat all non-reference backends as + experimental (see `docs/CAPABILITY-MATRIX.adoc`). +* *Generic-subsumption coherence* (#559 follow-up) — see the ledger row. + +== Closed holes are not proofs + +Closing an *implementation* hole is not the same as having *metatheory*. The +soundness *arguments* for the holes above (`docs/academic/proofs/*.adoc`, the +comments in `lib/borrow.ml`) remain `prose`, and the `Solo` core fragment's +`progress` / `preservation` are still `?todo`. Mechanisation has *started* — a +Wave-0 codegen-preservation seed (`formal/K1_CodegenPreservation.v`, axiom-free +Coq/Rocq, minimal nat/bool fragment) landed via #620 — but it does not yet cover +any hole in this ledger. The proof obligations, their rigour tiers, and their +(mostly `prose` / `absent`) status are catalogued in `docs/PROOF-NEEDS.adoc` +(umbrella issue #513). The one-line distinction: + +[quote] +The compiler now fails loud on these shapes and the residuals are pinned by +tests — but the soundness arguments are still paper proofs, not machine-checked. + +The v1 release-readiness ledger is issue #563. + +== Keeping this honest (how to update) + +. *Ground-truth by running the tool.* Reproduce the behaviour against the + built compiler (`dune build && dune runtest`, `dune exec affinescript -- …`). + Never edit a status here from another doc — that is how drift starts. +. *Change the row, change the anchor.* If you fix or break a hole, update the + status word *and* its anchoring fixture/test in the same change. The gate + (`tools/check-soundness-ledger.sh`) fails if a named + `test/e2e/fixtures/*.affine` anchor no longer exists. +. *Bump the stamp.* Update `:ground-truth-sha:` and `:ground-truth-date:` above + to the commit you verified against. +. *Do not fork the ledger.* If another doc needs to mention soundness status, + it links here; it does not copy the table. The gate checks the back-links + from `README.adoc`, `docs/CAPABILITY-MATRIX.adoc`, `docs/PROOF-NEEDS.adoc`, + `docs/NAVIGATION.adoc`, and `.claude/CLAUDE.md`. + +== See also + +* link:CAPABILITY-MATRIX.adoc[CAPABILITY-MATRIX.adoc] — authoritative *feature + readiness* (this ledger owns *soundness-hole* status; the matrix links here). +* link:PROOF-NEEDS.adoc[PROOF-NEEDS.adoc] — what must be *proven*, at what + rigour, with what (mostly unmechanised) status. +* link:reports/HANDOFF-2026-06-17-soundness.adoc[reports/HANDOFF-2026-06-17-soundness.adoc], + link:reports/TIDY-UP-LEDGER-2026-06-16.adoc[reports/TIDY-UP-LEDGER-2026-06-16.adoc] + — the dated session reports this ledger consolidates (historical inputs). diff --git a/docs/STATE-2026-06-11.adoc b/docs/STATE-2026-06-11.adoc index ab90d567..f8ca3c6e 100644 --- a/docs/STATE-2026-06-11.adoc +++ b/docs/STATE-2026-06-11.adoc @@ -12,6 +12,16 @@ feature readiness; TECH-DEBT is the ledger; this document is narrative. Trigger for this re-emit: stage-status change (CORE-01 closed) + the 2026-06-11 whole-picture survey findings. +[IMPORTANT] +==== +*Dated snapshot — do not read soundness status from here.* This is a narrative +record as of 2026-06-11. Its soundness-hole claims (#554/#555/#556/#558/#559) +described that day's state and are now *superseded*: #554 fixed, #555 fenced +loud, #556 fixed, #558 removed, #559 fixed (concrete overlaps). The live, +test-anchored single source of truth is link:SOUNDNESS.adoc[docs/SOUNDNESS.adoc]. +Dated snapshots are capped, not rewritten. +==== + == What changed since 2026-05-26 * *CORE-01 (#177) CLOSED 2026-05-30* via PR #473 after the full slice diff --git a/docs/TECH-DEBT.adoc b/docs/TECH-DEBT.adoc index e50b1575..1aee1704 100644 --- a/docs/TECH-DEBT.adoc +++ b/docs/TECH-DEBT.adoc @@ -259,9 +259,11 @@ merged (#241). Post-#228 estate re-audit DONE — true #229 scope is authoritative ledger + language-grounded canonical map + ESC-01..03 escalations: link:RESCRIPT-ELIMINATION.adoc[RESCRIPT-ELIMINATION.adoc] |CORE-04 |Traits: associated-type substitution, where-clause supertraits, -coherence checking. |S2 |partial -|CORE-05 |Dependent/refinement types: predicate reduction / SMT. |S3 -|parse-only +generic-subsumption overlap. (Concrete-overlap coherence DONE — #559, see +link:SOUNDNESS.adoc[SOUNDNESS.adoc].) |S2 |partial +|CORE-05 |Dependent/refinement types: *removed in v1* (#558) — withdrawn, not +shipped unenforced. See link:SOUNDNESS.adoc[SOUNDNESS.adoc]. |S3 +|removed |=== == Section C — STDLIB diff --git a/docs/reference/COMPILER-CAPABILITIES.adoc b/docs/reference/COMPILER-CAPABILITIES.adoc index f30a3728..f8252607 100644 --- a/docs/reference/COMPILER-CAPABILITIES.adoc +++ b/docs/reference/COMPILER-CAPABILITIES.adoc @@ -150,8 +150,9 @@ form `@erased/@linear/@unrestricted` accepted) (`Quantity.check++_++program++_++quantities` runs in standard CLI pipeline) * ⚠️ *Borrow Checker:* Live gate with ongoing Phase 3 work -* ⚠️ *Dependent / Refinement Types:* parse-only — `TRefined` AST node -exists but predicates do not reduce +* ❌ *Dependent / Refinement Types:* removed in v1 (#558) — withdrawn rather +than shipped unenforced; `assume(...)` is rejected at parse. See +link:../SOUNDNESS.adoc[docs/SOUNDNESS.adoc] * ✅ *WASM Codegen:* Primary backend (feature gaps remain for advanced effect-handler lowering) * ✅ *Julia Codegen:* Phase 1 (basic types) diff --git a/justfile b/justfile index 0e5b9955..7806d3e8 100644 --- a/justfile +++ b/justfile @@ -98,6 +98,7 @@ check: lint test guard guard: ./tools/check-no-extension-ts.sh ./tools/check-doc-truthing.sh + ./tools/check-soundness-ledger.sh # Re-baseline the doc-truthing over-claim ledger after a deliberate, legitimate # change (e.g. a new dated roadmap milestone). Commit the .allow diff. diff --git a/tools/check-soundness-ledger.sh b/tools/check-soundness-ledger.sh new file mode 100755 index 00000000..69407ffa --- /dev/null +++ b/tools/check-soundness-ledger.sh @@ -0,0 +1,116 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# Anti-staleness gate for the soundness ledger (docs/SOUNDNESS.adoc). +# +# Soundness-hole status used to live in ~6 documents that drifted +# independently, so whoever opened the stale one got a stale answer. The fix is +# structural: docs/SOUNDNESS.adoc is the single source of truth, it is +# *test-anchored*, and every other status surface must point back at it. This +# gate enforces that contract in-repo, toolchain-free, mirroring the sibling +# guard tools/check-doc-truthing.sh (which does the same job for the feature +# matrix). +# +# It checks four invariants: +# +# 1. The ledger exists and self-declares primacy ("single source of truth"). +# 2. It carries a freshness stamp (:ground-truth-sha:) so readers know when it +# was last reconciled against the running compiler. +# 3. Every test fixture the ledger names as an *anchor* actually exists. This +# is the binding that stops drift: you cannot delete the behaviour a row +# claims is proven without this gate (and the test suite) noticing. +# 4. Every status surface that summarises soundness still links to the ledger, +# so no competing per-issue ledger can re-grow elsewhere. +# +# Usage: ./tools/check-soundness-ledger.sh +# Wired into: just check (via the `guard` recipe) and CI (.github/workflows/ci.yml). +# Run from anywhere; it cd's to the repo root itself. + +set -euo pipefail + +cd "$(dirname "$0")/.." + +LEDGER="docs/SOUNDNESS.adoc" + +# Status surfaces that must point back at the ledger (single-source invariant). +# A doc may summarise soundness, but it must link here rather than maintain a +# rival per-issue table — that rivalry is exactly what went stale. +POINTER_DOCS=( + "README.adoc" + "docs/CAPABILITY-MATRIX.adoc" + "docs/PROOF-NEEDS.adoc" + "docs/NAVIGATION.adoc" + ".claude/CLAUDE.md" +) + +fail=0 +note() { printf '%s\n' "$*" >&2; } + +# --- 1. The ledger exists and asserts its own primacy ----------------------- +if [ ! -f "$LEDGER" ]; then + note "ERROR: the soundness ledger is missing: $LEDGER" + note " It is the single source of truth for soundness-hole status." + note " Restore it or amend this guard." + exit 1 +fi +if ! grep -q "single source of truth" "$LEDGER"; then + note "ERROR: $LEDGER no longer self-declares primacy." + note " Expected the phrase 'single source of truth'." + fail=1 +fi + +# --- 2. Freshness stamp is present ------------------------------------------ +if ! grep -q ":ground-truth-sha:" "$LEDGER"; then + note "ERROR: $LEDGER lost its freshness stamp (:ground-truth-sha:)." + note " Readers rely on it to know when the ledger was last reconciled" + note " against the running compiler. Restore and bump it." + fail=1 +fi + +# --- 3. Every anchored fixture the ledger names actually exists ------------- +# The ledger pins each claim to a test/e2e/fixtures/*.affine file. If one is +# renamed or deleted without updating the ledger, the claim is unmoored — fail. +missing_anchor=0 +while IFS= read -r anchor; do + [ -z "$anchor" ] && continue + if [ ! -f "$anchor" ]; then + if [ "$missing_anchor" -eq 0 ]; then + note "ERROR: $LEDGER cites anchor fixtures that no longer exist:" + missing_anchor=1 + fail=1 + fi + note " - $anchor" + fi +done < <(grep -oE 'test/e2e/fixtures/[A-Za-z0-9_]+\.affine' "$LEDGER" | LC_ALL=C sort -u) +if [ "$missing_anchor" -eq 1 ]; then + note " Either restore the fixture or update the ledger row to its new" + note " anchor in the same change (see $LEDGER, 'Keeping this honest')." +fi + +# --- 4. Every status surface still links to the ledger ---------------------- +for doc in "${POINTER_DOCS[@]}"; do + if [ ! -f "$doc" ]; then + note "ERROR: expected status surface is missing: $doc" + note " If it was intentionally removed, drop it from POINTER_DOCS in" + note " this guard. Otherwise restore it." + fail=1 + continue + fi + if ! grep -q "SOUNDNESS.adoc" "$doc"; then + note "ERROR: $doc no longer points at the soundness ledger ($LEDGER)." + note " Every doc that summarises soundness status must link to the" + note " single source of truth so a rival ledger cannot re-grow and" + note " go stale. Add a reference to docs/SOUNDNESS.adoc." + fail=1 + fi +done + +if [ "$fail" -ne 0 ]; then + note "" + note "Soundness-ledger guard failed. The single-source contract for soundness" + note "status is drifting. See docs/SOUNDNESS.adoc (authoritative)." + exit 1 +fi + +echo "OK: soundness ledger intact — primacy + freshness stamp + anchors exist + back-links present." diff --git a/wiki/README.md b/wiki/README.md index 2c831664..346ba090 100644 --- a/wiki/README.md +++ b/wiki/README.md @@ -12,11 +12,14 @@ algebraic effects, and a typed-WebAssembly compilation target. > [`docs/CAPABILITY-MATRIX.adoc`](../docs/CAPABILITY-MATRIX.adoc) for live > per-feature readiness and [`docs/TECH-DEBT.adoc`](../docs/TECH-DEBT.adoc) > for the coordination ledger. AffineScript is **alpha** today: CORE-01 -> (#177) closed 2026-05-30, but one known borrow-checker soundness hole -> remains (#554; Polonius residual #553) and effect handlers are silently -> mis-lowered outside the interpreter (#555) — `handle`/`resume` examples -> in these pages run correctly **only** under `--interp` (single-shot -> tail-resume) until #555 lands. Dated narrative: +> (#177) closed 2026-05-30, and 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, and effect handlers (#555) now +> **fail loud** on every compiled backend rather than dropping arms. `handle`/ +> `resume` examples in these pages still execute only under `--interp` +> (single-shot tail-resume); the compiled backends reject them loudly. The +> single source of truth for soundness-hole status is the test-anchored +> [`docs/SOUNDNESS.adoc`](../docs/SOUNDNESS.adoc). Dated narrative: > [`docs/STATE-2026-06-11.adoc`](../docs/STATE-2026-06-11.adoc) · > v1 release-readiness ledger: #563. @@ -46,7 +49,7 @@ or `parse-only` today.** - [Effects](language-reference/effects.md) — Algebraic effect system - [Traits](language-reference/traits.md) — Type classes *(currently `partial`)* - [Modules](language-reference/modules.md) — Module system -- [Dependent Types](language-reference/dependent-types.md) — Indexed and refined types *(currently `parse-only`)* +- [Dependent Types](language-reference/dependent-types.md) — Indexed and refined types *(REMOVED in v1 — #558; page is historical)* - [Row Polymorphism](language-reference/rows.md) — Extensible records ### Compiler @@ -157,7 +160,7 @@ greet({name: "Bob", role: "Admin", active: true}) Records + effect rows in typecheck/unify. Not fully exercised end-to-end yet. -### Dependent Types *(parse-only — not enforced)* +### Dependent Types *(REMOVED in v1 — historical; see #558 / [`docs/SOUNDNESS.adoc`](../docs/SOUNDNESS.adoc))* ```affine // Length-indexed vectors — SYNTAX PARSES, but predicates do not diff --git a/wiki/language-reference/dependent-types.md b/wiki/language-reference/dependent-types.md index b446d1aa..f8df77d8 100644 --- a/wiki/language-reference/dependent-types.md +++ b/wiki/language-reference/dependent-types.md @@ -1,14 +1,15 @@ # Dependent Types -> **⚠️ Current state: `parse-only`.** -> The surface syntax described in this page parses, but the typechecker -> **does not reduce predicates** and there is **no SMT / decision -> procedure** wired in today. `TRefined` constructors exist in the AST. -> Predicates and refinements are not enforced at runtime. -> Authoritative source: [`docs/CAPABILITY-MATRIX.adoc`](../../docs/CAPABILITY-MATRIX.adoc) -> row "Dependent / refinement types". The ledger entry CORE-05 in -> [`docs/TECH-DEBT.adoc`](../../docs/TECH-DEBT.adoc) tracks the work -> needed to lift this from parse-only to enforced. +> **⚠️ Removed in v1 (2026-04-10).** +> Refinement / dependent types were **withdrawn** from the language rather +> than shipped parse-only-and-unenforced (issue #558): there is no `TRefined` +> node, `assume(...)` is **rejected at parse**, and `T where (P)` is a parse +> error. This page is retained for historical / design context only — the +> syntax below does **not** compile today. +> Authoritative status: the test-anchored soundness ledger +> [`docs/SOUNDNESS.adoc`](../../docs/SOUNDNESS.adoc) (#558 row) and +> [`docs/CAPABILITY-MATRIX.adoc`](../../docs/CAPABILITY-MATRIX.adoc) +> row "Dependent / refinement types". Dependent types allow types to depend on values, enabling compile-time verification of invariants. diff --git a/wiki/language-reference/traits.md b/wiki/language-reference/traits.md index e691e800..4a757b39 100644 --- a/wiki/language-reference/traits.md +++ b/wiki/language-reference/traits.md @@ -1,15 +1,17 @@ # Traits > **⚠️ Current state: `partial`.** -> Registry, `TopTrait`/`TopImpl`, unification-based `find_impl`, and -> impl-satisfies-trait are wired into the typechecker. **Missing today:** -> associated-type substitution in method bodies, where-clause -> supertraits, coherence checking. The surface and runtime guarantees -> described below may overstate current enforcement — cross-check with +> Registry, `TopTrait`/`TopImpl`, unification-based `find_impl`, +> impl-satisfies-trait, and **coherence checking** (issue #559 — overlapping +> impls whose self types unify are rejected) are wired into the typechecker. +> **Missing today:** associated-type substitution in method bodies, +> where-clause supertraits, and generic-subsumption overlap (#559 follow-up). +> The surface and runtime guarantees described below may overstate current +> enforcement — cross-check with > [`docs/CAPABILITY-MATRIX.adoc`](../../docs/CAPABILITY-MATRIX.adoc) -> row "Traits", and see CORE-04 in -> [`docs/TECH-DEBT.adoc`](../../docs/TECH-DEBT.adoc) for the remaining -> work. +> row "Traits", the soundness ledger +> [`docs/SOUNDNESS.adoc`](../../docs/SOUNDNESS.adoc) (#559 row), and CORE-04 in +> [`docs/TECH-DEBT.adoc`](../../docs/TECH-DEBT.adoc) for the remaining work. Traits define shared behavior that types can implement. They enable polymorphism and code reuse.