From 3d25fb68510a95de5e36c65ea9cdcf096752ba0f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 8 Sep 2026 08:29:47 +0100 Subject: [PATCH 1/3] docs(#176): restore the DOC-04 status banner and fix 3 dead ledger links 3661d98 removed the DOC-04 banner from README's "Status" section, which tools/check-doc-truthing.sh requires. That failure has held the `build` job red on main since 2026-06-28. Also repoints three references to `SOUNDNESS-LEDGER.adoc` -- a file that does not exist -- at docs/SOUNDNESS.adoc. tools/check-doc-truthing.sh now exits 0. Co-Authored-By: Claude Opus 5 (1M context) --- README.adoc | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/README.adoc b/README.adoc index e2177c5a..d7896df8 100644 --- a/README.adoc +++ b/README.adoc @@ -23,11 +23,21 @@ delivery mechanism. They _are_ the product. == Status +[IMPORTANT] +==== +Authoritative per-feature status lives in +link:docs/CAPABILITY-MATRIX.adoc[docs/CAPABILITY-MATRIX.adoc]; soundness-hole +status lives in link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc]. Where this +README and those documents disagree, *they win* -- +`.machine_readable/descriptiles/STATE.a2ml` mirrors the matrix and does not +lead it. +==== + Early and experimental. This is *v0.2*: the architecture is settled, the implementation and the metatheory are partial and still moving. It is suitable for experimentation, teaching, and small sound components -- not yet for production. What is proven, what is implemented, and what is still prose are -stated plainly below and tracked in `SOUNDNESS-LEDGER.adoc`. +stated plainly below and tracked in link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc]. == What you get @@ -142,7 +152,7 @@ risk here, and it is not yet solved. Soundness is *partially mechanised, and honestly tracked.* An initial, axiom-free, machine-checked result for code-generation preservation exists (Coq/Rocq). A number of residuals remain open; they are recorded -- not hidden --- in `SOUNDNESS-LEDGER.adoc`, which states for each claim whether it is +-- in link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc], which states for each claim whether it is mechanised or still argued in prose. The ledger is the source of truth for what currently holds. This README @@ -192,7 +202,7 @@ totality cut, and a WebAssembly target -- rather than any one ingredient. == Documentation // TODO: link the design notes and the examples directory once locations are stable. -* Soundness status: `SOUNDNESS-LEDGER.adoc` +* Soundness status: link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc] == License From 5c0366aacdfac155360858deaa26ca6bcb889429 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 8 Sep 2026 08:29:47 +0100 Subject: [PATCH 2/3] ci: stop one red gate from disarming every gate below it GitHub Actions skips all later steps in a job once one fails, so the doc-truthing failure silently disarmed the soundness-ledger gate, the capability-anchor gate and the formatting check. Those report `skipped`, not `failure` -- worse than red, because `skipped` reads as absence of news rather than as a gate that never ran. `if: ${{ !cancelled() }}` makes the four gates independent: each reports its own verdict regardless of the others, while a cancelled run still stops. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1598f961..e174c1f0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -100,6 +100,7 @@ jobs: # rationale + recovery instructions. run: ./tools/check-no-extension-ts.sh - name: Issue #176 — doc-truthing re-drift guard (DOC-01..09) + if: ${{ !cancelled() }} # Single toolchain-free gate enforcing both halves of the doc-truthing # MONITOR: the presence invariants (DOC-04/05 — banner pointers, matrix # primacy + anti-over-claim section, STATE.a2ml mirror keys) AND the @@ -108,6 +109,7 @@ jobs: # See tools/check-doc-truthing.sh. run: ./tools/check-doc-truthing.sh - name: Soundness-ledger anti-staleness gate + if: ${{ !cancelled() }} # 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 @@ -116,6 +118,7 @@ jobs: # See tools/check-soundness-ledger.sh. run: ./tools/check-soundness-ledger.sh - name: Capability-matrix test-anchor gate + if: ${{ !cancelled() }} # docs/CAPABILITY-MATRIX.adoc anchors each feature-readiness claim to an # executable test ("== Test anchors"). This gate fails if that section # disappears or if any test it names goes missing — so a "works" status @@ -123,6 +126,7 @@ jobs: # See tools/check-capability-anchors.sh. run: ./tools/check-capability-anchors.sh - name: Check formatting + if: ${{ !cancelled() }} run: opam exec -- dune build @fmt lint: runs-on: ubuntu-latest From f3a70ae7e64262a231152ee0e8a4e9d98a31e095 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 8 Sep 2026 08:29:47 +0100 Subject: [PATCH 3/3] docs: restore SOUNDNESS.adoc content reverted by the 2026-08-18 stale merge 152d959 merged origin/claude/capability-test-anchors, a branch whose copy of docs/SOUNDNESS.adoc predated three fixes that had already landed on the main line. The merge took the branch's whole file, reverting all three (27 insertions, 51 deletions, none of them new content): 1. The #555 row was re-pointed at `test_resume_nontail_known_shallow`, a name that was only ever planned and has never existed in the tree. The pin that does exist -- `test_resume_nontail_xfail`, test/xfail/test_xfail_pins.ml:56, over the same fixture and the same behaviour -- is what the seal hashes. 2. The "Pinned-residual discipline" section was deleted -- the section naming the XPASS hand-off as the one place the anti-drift machinery relies on a human. 3. Two claims regressed to being false. #624 was restated as "flagged but not yet fenced" although f020a6f fenced it, and the mechanisation paragraph was rolled back to "#620/#621", dropping P-2, P-3, F-3 and F-4. The row also reverted to `|*residual (pinned)*` markup, which the gate's row parser cannot see at all, so property 5 reported "no pinned/open rows found (fail closed)". This is a revert of that revert: docs/SOUNDNESS.adoc is restored to 808e859, the main-line parent of the merge. Nothing has touched the file since, so no later work is lost. The seal is unchanged and was never wrong -- the ledger was the side that drifted -- so tools/soundness-anchors.sha256 is NOT resealed. tools/check-soundness-ledger.sh now exits 0 on all five properties. Co-Authored-By: Claude Opus 5 (1M context) --- docs/SOUNDNESS.adoc | 78 +++++++++++++++++++++++++++++---------------- 1 file changed, 51 insertions(+), 27 deletions(-) diff --git a/docs/SOUNDNESS.adoc b/docs/SOUNDNESS.adoc index 9669f833..c46cc21f 100644 --- a/docs/SOUNDNESS.adoc +++ b/docs/SOUNDNESS.adoc @@ -145,16 +145,17 @@ without reified continuations, and previously returned a silently-wrong value). | `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). Tracked: #623. -|*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) +| #555 (interp, non-tail single-shot) / #623 +| `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, #623). +| `residual (pinned)` +| `test/e2e/fixtures/handle_resume_nontail.affine` + `test_resume_nontail_xfail` +(xfail: asserts the correct `105`; currently fails-as-expected; flips to an +unexpected pass the day delimited continuations land). See _Pinned-residual +discipline_. | #556 | Async CPS table-miss fails loud instead of silently lowering synchronously. @@ -218,26 +219,49 @@ The implementation holes marked `fixed` / `loud-fail` / `removed` above are closed. Honesty requires naming what is *not* a guarantee. Each item here is a row in the table above, restated for the hurried reader — not a separate list: -* *Interpreter non-tail resume* (#555 residual, pinned; tracked as #623) — 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 (tracked as #624). Treat all - non-reference backends as experimental (see `docs/CAPABILITY-MATRIX.adoc`). -* *Generic-subsumption coherence* (#559 follow-up) — see the ledger row. +* *Interpreter non-tail resume* (#555 / #623, `residual (pinned)`) — the +`5`-not-`105` shape. Silent on the interpreter path; pinned by +`test_resume_nontail_xfail`. +(Stub backends dropping `return` (#555-stub / #624) is now `loud-fail` — Lean and +Why3 reject an early `return` instead of silently dropping it — so it is no longer +a "still open" residual. Treat all non-reference backends as experimental anyway, +see `docs/CAPABILITY-MATRIX.adoc`.) + +If you are deciding whether AffineScript is "sound enough" for a use, the +interpreter non-tail resume row above is the one remaining residual, and the +metatheory caveat below applies to it. + +=== Pinned-residual discipline + +A `residual (pinned)` / `open (tracked)` row carries an *xfail* test that asserts +the *desired* behaviour and currently fails because the hole is present. The +xfail harness (`test/xfail/test_xfail_pins.ml`) tolerates that expected failure +and reports `XFAIL-OK`; if the assertion ever *passes*, the harness reports +`XPASS`, exits non-zero, and the gate surfaces a distinct "pin for #N is passing +— is the hole fixed? update the row" message. + +That second job is a *social* guarantee wearing a mechanical costume. The harness +mechanically catches the flip; but it relies on the engineer reading `XPASS` as +"good — now advance the ledger row to `fixed`" rather than "annoying — silence +it". The gate cannot tell those apart. So: *when an `*_xfail` pin reports `XPASS`, +the correct first move is to open this ledger, not to silence the test.* This is +the one place the anti-drift machinery hands off to a human, and it is named here +so the hand-off is deliberate. == 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* — an -axiom-free Coq/Rocq `formal/` track (codegen-preservation: K-1 -`K1_CodegenPreservation.v`, K-1-with-`let` `K1Let_CodegenPreservation.v`, and -the F-1 transformer-preservation composition; #620/#621) — 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: +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 +`Soundness.idr` progress / preservation are still `?todo`. Mechanisation has +*grown substantially* — the axiom-free Coq/Rocq `formal/` track now covers the +Wave-0 codegen-preservation seed (K-1 `K1_CodegenPreservation.v`, K-1-with-`let` +`K1Let_CodegenPreservation.v`), the F-1 transformer-preservation composition, and +the four Wave-0 siblings P-2 (progress), P-3 (borrow-graph, with loan edges + +move-locality), F-3 and F-4 (#620–#627). These target core/fragment metatheory; +*none yet covers a hole in this ledger* — they are not the full AffineScript +borrow checker / interpreter / backends. The obligations, their rigour tiers, and +their exact status are catalogued in `docs/PROOF-NEEDS.adoc` (umbrella #513). The one distinction to carry away, stated so the polish of *this ledger* is not mistaken for the rigour of the *metatheory*: