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 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 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*: