Un-break CI: restore the DOC-04 banner, re-arm the disarmed gates, revert a stale merge's silent ledger regression (#744)

The `build` job has been red on `main` since **2026-06-28**. Three
separable causes, one commit each.

## 1. The red itself (`3d25fb6`)

`3661d98` removed the DOC-04 status banner from `README.adoc`, which
`tools/check-doc-truthing.sh` requires. Restored, plus three references
to `SOUNDNESS-LEDGER.adoc` — a file that does not exist — repointed at
`docs/SOUNDNESS.adoc`.

## 2. Why nothing else reported (`5c0366a`)

GitHub Actions skips every later step in a job once one fails. The
doc-truthing failure therefore disarmed the soundness-ledger gate, the
capability-anchor gate and the formatting check for ten weeks. They
reported `skipped`, not `failure` — **worse than red, because `skipped`
reads as absence of news rather than as a gate that never ran.**

`if: ${{ !cancelled() }}` on all four makes each report its own verdict.

## 3. What the disarmed gate was hiding (`f3a70ae`)

With the gates re-armed, the soundness-ledger gate failed on three of
its five properties. The cause is not a soundness regression:

`152d959` (2026-08-18) merged `origin/claude/capability-test-anchors`, a
branch whose copy of `docs/SOUNDNESS.adoc` predated three fixes already
on the main line. **It raised a real conflict, and the conflict was
resolved by deleting main's side.** Replaying the merge shows this
directly:

```console
$ git merge-tree --write-tree 808e859 fb27a7f
CONFLICT (content): Merge conflict in docs/SOUNDNESS.adoc     # exit 1, two hunks
```

Git's own auto-merge output still contained both of main's fixes next to
the conflict markers. Diffing that replayed tree against what was
committed gives **60 deletions, 0 insertions** — the six marker lines
plus 54 lines of main's side, nothing added: the signature of a pure
"take theirs" resolution. Against its first parent the merge is 27
insertions / 51 deletions with **no new content**, reverting all three:

1. The #555 row was re-pointed at `test_resume_nontail_known_shallow`, a
name that was only ever *planned* (in the 2026-06-17 handoff) and has
never existed in the tree. The pin that does exist,
`test_resume_nontail_xfail` (`test/xfail/test_xfail_pins.ml:56`), covers
the same fixture and the same behaviour and 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 restated as "flagged but
not yet fenced" although `f020a6f` fenced it, and the mechanisation
paragraph rolled back to "#620/#621", dropping P-2, P-3, F-3 and F-4.

This commit restores the file to `808e859`, the main-line parent of that
merge. Nothing has touched it since, so no later work is lost.

### The seal was never wrong — and was NOT resealed

Property 3 fails with a message offering `--reseal (if intentional)`.
Taking that offer would have hashed a test that does not exist: the
computed digest was `e3b0c442…` — the SHA-256 of the empty string.
**`tools/soundness-anchors.sha256` is unchanged.** The ledger was the
side that drifted, and it is the side that was fixed.

## Verification

All three gates run locally from a clean tree:

```
check-doc-truthing      OK  exit 0
check-soundness-ledger  OK  exit 0   all 5 properties (anchors + back-links + content-bound + stamp-fresh + pins live)
check-capability-anchors OK exit 0
```

Property 5 exercises the xfail harness, so its pass is a live
confirmation that `test_resume_nontail_xfail` still fails-as-expected —
the #555 hole is still pinned, not silently closed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.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,13 +118,15 @@ 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
         # row cannot outlive the test that backs it.
         # 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

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
 

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