feat(#4789): per-case det-sweep coverage ledger; CICS spec status page bot-generated

.claude/skills/blocker-slice/SKILL.md

@@ -52,9 +52,11 @@ $PY tests/tools/proof_blockers.py SURVEY_DIR --label LABEL [--sweep SWEEP_DIR]
 - **Crucible logs are never derived from the spec** (nor from a runtime or a port). The gen script is traced by
   hand from IBM's documentation; `crucible_case.py check-hand-derived` fails if it imports anything but the stdlib
   and `crucible_events`.
-- `python tests/tools/cics_spec_status.py render` regenerates `docs/language_status/cics_spec_status.md` (a test
-  fails on a stale page); after a slice, `refresh --census --crucible DIR` first. A spec PR adds its row to
-  `SPEC_PRS_DONE` there.
+- `docs/language_status/cics_spec_status.md` is generated on main by the evidence-refresh bot (#4789): do NOT commit
+  it in a PR (`cics_spec_status.py render` only to look). After a slice, commit `refresh --census --crucible DIR`'s
+  `cics_spec_status.json`. A spec PR adds its row to `SPEC_PRS_DONE` there.
+- The det-sweep coverage ledger is one file per case, `tests/equivalence/det_sweep_coverage/<case>.json` (#4789):
+  `det_coverage_ledger.py update <sweep DIR>` rewrites only the files of the cases that sweep ran.
 - Then the `cics-command-slice` checklist: both runtimes, the hand-traced crucible case, proofs, X-register entry.
 
 ## 3. Honest refusals (the patterns that made programs whole without guessing)

.claude/skills/cics-command-slice/SKILL.md

@@ -42,8 +42,8 @@ Traps `--check` exists for:
       leave refused and why.
 - [ ] **Spec entry first** (`gitgalaxy/standards/cics`): promote the command's name-only entry to a full one
       (options, refusals with reasons and register, groups, outcomes with RESP2, facts); `det/cics.py` and the stub
-      read it. The runtimes stay hand-written, and no crucible log is derived from the spec. Then
-      `cics_spec_status.py render`.
+      read it. The runtimes stay hand-written, and no crucible log is derived from the spec. Do not commit
+      `cics_spec_status.md` (#4789: the evidence-refresh bot renders it on main).
 - [ ] **Before survey** (now, on the unchanged branch): `$PY tests/tools/cics_census.py survey --out $SCRATCH/s
       --label before --verb VERB` (det_survey.py, translation only; ~minutes per estate; background it with
       `tests/tools/box/heavy-run.sh`).

.github/workflows/evidence-refresh.yml

@@ -21,6 +21,10 @@ name: Evidence Refresh
 # Earlier bot PRs failed twice: #4640 was opened against a feature branch (the base is now pinned to main) and #4649
 # went dirty while parallel PRs kept conflicting on the report (those PRs no longer commit it).
 #
+# #4789: the same for the CICS spec status page (docs/language_status/cics_spec_status.md): rendered here, never in a PR.
+# The det-sweep coverage ledger is one file per case (tests/equivalence/det_sweep_coverage/<CASE>.json), so a case PR and
+# this bot (or two case PRs) touch only the files of the cases they swept.
+#
 # Auto-merge happens only when every proof step succeeded. A run where a proof or the sweep failed still opens the PR,
 # but leaves it for a person (and the job fails). Approvals are never touched (only `evidence.py approve`, run by a
 # person at a terminal, writes one).
@@ -771,6 +775,15 @@ jobs:
           # once its inputs move: #4730), so no sweep is passed here.
           python tests/tools/evidence_report.py --refresh --live
 
+      - name: Re-render the CICS spec status page (#4789)
+        # Derived output like the report above: PRs no longer commit docs/language_status/cics_spec_status.md (parallel
+        # slices conflicted on it); it is rendered here from main's spec, translator, stub and cics_spec_status.json.
+        if: always()
+        continue-on-error: true  # a page that fails to render stays as main has it; it never holds back the records
+        run: |
+          cd gitgalaxy
+          python tests/tools/cics_spec_status.py render
+
       - name: Summary
         if: always()
         run: |
@@ -818,12 +831,15 @@ jobs:
             Automated re-proof of the evidence records (#4048) that a harness, oracle or generator change made stale.
             Each record's proof was run again on the committed port and case; the records and
             docs/language_status/evidence/ are rewritten from those runs. A proof that now fails is recorded as
-            not proven. The evidence reports (docs/language_status/evidence_report/) are re-rendered from them (#4703).
+            not proven. The evidence reports (docs/language_status/evidence_report/) are re-rendered from them (#4703),
+            the det-sweep coverage ledger (tests/equivalence/det_sweep_coverage/, one file per case: #4789) from the
+            sweep, and the CICS spec status page (docs/language_status/cics_spec_status.md, #4789) from main.
             Approvals are never written by this job. Auto-merge (squash) is enabled when every proof succeeded.
           branch: auto/evidence-refresh${{ github.event_name != 'push' && '-full' || '' }}  # a lane's own branch (#4743)
           delete-branch: true
           add-paths: |
-            tests/equivalence/det_sweep_coverage.json
+            tests/equivalence/det_sweep_coverage/*.json
+            docs/language_status/cics_spec_status.md
             tests/equivalence/*/evidence.json
             tests/cics_crucible/ports/*/*/evidence.json
             docs/language_status/evidence/*.md

.github/workflows/smoke-test.yml

@@ -154,3 +154,14 @@ jobs:
         if: always()
         continue-on-error: true
         run: python tests/tools/evidence_report.py --deltas --live >> "$GITHUB_STEP_SUMMARY"
+
+      - name: CICS spec status page (advisory, #4789)
+        if: always()
+        continue-on-error: true
+        run: |
+          {
+            echo "## CICS spec status page (advisory)"
+            if python tests/tools/cics_spec_status.py render --check 2>&1; then :; else
+              echo "The evidence-refresh bot re-renders docs/language_status/cics_spec_status.md on main after merge; do not commit it here."
+            fi
+          } >> "$GITHUB_STEP_SUMMARY"

.gitignore

@@ -168,7 +168,7 @@ museum_2/
 !tests/equivalence/*/evidence.json
 !tests/equivalence/facade_baseline.json
 !tests/equivalence/det_sweep_baseline.json
-!tests/equivalence/det_sweep_coverage.json
+!tests/equivalence/det_sweep_coverage/*.json
 !tests/equivalence/infeasible_outcomes.json
 !tests/cics_crucible/ports/*/*/evidence.json
 !tests/cics_crucible/fixture/**/*.json

docs/language_status/evidence_records.md

@@ -94,7 +94,7 @@ tree and compares it with the record's. It returns a status and every reason for
   the re-rendered evidence report; the PR auto-merges (squash) when every proof succeeded.
 
 **Stale levels in the evidence report** (owner decision, 2026-10-08, #4730): the det-sweep coverage ledger
-(`tests/equivalence/det_sweep_coverage.json`) is fingerprinted like a record, and the same split applies to the
+(`tests/equivalence/det_sweep_coverage/<case>.json`) is fingerprinted like a record, and the same split applies to the
 levels the [evidence report](evidence_report/README.md) derives from it. Stale on a **scheduled** input (harness,
 oracle) means "measured against the previous harness, not yet re-checked", not "regressed": the report keeps the
 program's last measured level and marks it (`L3*`), with `stale since <commit>` (the commit the ledger entry was

tests/cobol_mainframe/test_det_sweep_fast.py

@@ -84,6 +84,14 @@ def test_a_change_inside_one_case_proves_that_case_only():
     assert (p["mode"], p["cases"]) == ("narrow", ["delta"])
 
 
+def test_a_cases_coverage_ledger_file_proves_that_case():
+    """#4789: a case PR's own ledger file (tests/equivalence/det_sweep_coverage/<case>.json) keeps the sweep narrow: the
+    sweep of that case is what checks the entry."""
+    p = plan.plan(["tests/equivalence/delta/case.json", "tests/equivalence/det_sweep_coverage/delta.json",
+                   "tests/equivalence/det_sweep_coverage/alpha.json"], "pull_request", CASES)  # fmt: skip
+    assert (p["mode"], p["cases"]) == ("narrow", ["alpha", "beta", "delta", "gamma"])
+
+
 def test_dependents_of_a_changed_port_are_proven_too():
     p = plan.plan(["tests/equivalence/alpha/port/A.java"], "pull_request", CASES)
     assert p["cases"] == ["alpha", "beta", "gamma"]  # port_from, then uses_ports of that (transitively)
@@ -98,6 +106,8 @@ def test_dependents_of_a_changed_port_are_proven_too():
         "tests/equivalence/gnucobol.Dockerfile",  # the oracle
         "tests/equivalence/faults/ggfault.c",  # a shared stub
         "tests/equivalence/newcase/case.json",  # a case that does not exist yet / removed
+        "tests/equivalence/det_sweep_coverage/newcase.json",  # #4789: the ledger file of no such case
+        "tests/equivalence/det_sweep_coverage.json",  # the retired single-file ledger
         "tests/cobol_mainframe/corpora.json",
         ".github/workflows/det-sweep.yml",
         "README.md",