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

[hyperpolymath]

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:

$ 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 tracking: general effect-handler dispatch (post-CORE-02 residual) — silent arm-drop on 3 backends; DECISION: back-port loud failure now? #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: tracking: Lean and Why3 (experimental) backends drop return control flow — early returns silently mis-emitted #624 restated as "flagged but not yet fenced" although f020a6f fenced it, and the mechanisation paragraph rolled back to "feat(formal): stand up Coq formal/ track + mechanize the K-1 Wave-0 seed #620/feat(formal): F-1 preservation + grow K-1 (let/vars) + state P-2/P-3/F-3/F-4 #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

[coderabbitai]

Warning

Review limit reached

Next included review available in 2 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: e745d694-0efb-4578-840f-d8ad053b6e61

📥 Commits

Reviewing files that changed from the base of the PR and between 8abeaaa and f3a70ae.

📒 Files selected for processing (3)

• .github/workflows/ci.yml
• README.adoc
• docs/SOUNDNESS.adoc

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud