ci: drop the hardcoded STATUS.md test count so it can't redden CI

STATUS.md pinned a unit-test total ("903 host unit tests", "Total: **903**")
that only `cargo test --lib` can derive. Every time the suite grew, the prose
went stale and check-status-freshness --full --strict failed CI until someone
hand-edited the number — most recently 892 -> 903, the drift the preceding
unblock commit had to repair. The number's own prose already said "numbers
live in code, not prose"; this makes the file honor that instead of pinning a
copy that drifts.

What:
  - STATUS.md: remove the two hardcoded test totals. "At a glance" and the
    Test-coverage section now point at `make stats` / `cargo test --lib` for
    the live count and state explicitly that it is not pinned in prose.
  - tools/check-status-freshness.py: remove the unit-test number-drift check
    entirely — the TEST_COUNT_RES/MAKE_STATS_TESTS_RE regexes, the intra-prose
    consistency check, the `--full`/`make stats` live-compare path, and the
    `subprocess` import. The two checks that remain are the date heuristic
    (advisory) and the Kani-harness total (cheap, no compile). `--strict` now
    fails only on Kani-harness drift. Docstring + `--full` flag removed.
  - .github/workflows/ci.yml: the freshness gate no longer needs a built test
    binary, so it moves out of the `test` job (where it ran `--full --strict`
    after `cargo test`) into the pure-python `lints` job as a plain `--strict`
    step. The STATS_TEST_TARGET env it needed is gone with it.
  - Makefile: drop the now-dead `check-status-freshness-full` target.

Why: a derived number does not belong hardcoded in prose. With nothing pinned,
there is nothing to drift, and the compile-gated `--full` path that existed
only to re-verify that number has no remaining purpose. The Kani-harness total
stays pinned-and-checked because it is derivable without a compile.

Out of scope: the per-area breakdown table in the Test-coverage section keeps
its approximate counts (already labelled "breakdown drifts faster than the
total"); only the authoritative total is dropped. STATUS.md's stale
last_synced_to_code date is a separate advisory and is not touched here.

Verification:
  - python3 tools/check-status-freshness.py: exit 0 (date advisory only).
  - python3 tools/check-status-freshness.py --strict: exit 0 (no Kani drift;
    this is the exact CI invocation).
  - python3 -m py_compile tools/check-status-freshness.py: OK; grep confirms
    no remaining TEST_COUNT_RES / MAKE_STATS_TESTS_RE / subprocess / args.full.
  - make check-status-freshness: exit 0 (Makefile wrapper still resolves).
  - make check-deferrals / check-assumptions / check-index-isolation: all exit
    0; neither baseline tracks the edited files, so no line-drift resync.
  - grep: no orphan references to check-status-freshness-full remain.

Staged files:
  .github/workflows/ci.yml
  Makefile
  STATUS.md
  tools/check-status-freshness.py

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: riccajason

.github/workflows/ci.yml

@@ -90,15 +90,6 @@ jobs:
         env:
           RUST_MIN_STACK: "8388608"
         run: cargo test --lib --target x86_64-unknown-linux-gnu
-      # STATUS.md number-drift gate. The test binary is now built, so
-      # `make stats` enumerates --lib tests cheaply (retargeted to the Linux
-      # host via STATS_TEST_TARGET). --strict makes objective count drift
-      # (prose vs build, Kani harnesses vs source) FAIL CI; the date heuristic
-      # stays advisory and is not checked here.
-      - name: check-status-freshness (counts vs build, --full --strict)
-        env:
-          STATS_TEST_TARGET: x86_64-unknown-linux-gnu
-        run: python3 tools/check-status-freshness.py --full --strict
 
   # ---------------------------------------------------------------------------
   # clippy — enforces missing_safety_doc = "deny" (Cargo.toml [lints.clippy],
@@ -130,9 +121,10 @@ jobs:
   # Commit-boundary / provenance gates are excluded on purpose: they read the
   # staged diff or session state and are no-ops or meaningless in CI —
   # check-index-isolation, check-lockfile (advisory), claude-preflight.
-  # (check-status-freshness's number-drift check runs in the `test` job with
-  # --full --strict, where a built test binary makes the counts verifiable; its
-  # date heuristic stays local/advisory and is not run in CI.)
+  # check-status-freshness runs here too (Kani-harness drift, --strict): it is
+  # compile-free now that STATUS.md no longer pins a unit-test total, so it
+  # belongs with the other pure-python gates. Its date heuristic stays
+  # local/advisory and is not run in CI.
   #
   # Note: check-adrs regenerates docs/adr/INDEX.md as a side effect (exit 0 when
   # cross-refs are valid). CI does not commit, so a stale committed INDEX.md is
@@ -155,3 +147,5 @@ jobs:
         run: make check-banned-paths
       - name: check-unsafe-coverage (Convention 1 SAFETY comments)
         run: make check-unsafe-coverage
+      - name: check-status-freshness (Kani-harness drift, --strict)
+        run: python3 tools/check-status-freshness.py --strict

Makefile

@@ -1310,13 +1310,6 @@ check-lockfile:
 check-status-freshness:
 	@python3 tools/check-status-freshness.py
 
-# Full variant: also re-derives the unit-test count via `make stats`
-# (compiles). For CI / manual runs — NOT the pre-commit hook, which must
-# stay compile-free. The cheap Kani-harness + prose-consistency checks
-# run in both; only the live test-count compare is gated behind --full.
-check-status-freshness-full:
-	@python3 tools/check-status-freshness.py --full
-
 # Pre-edit audit for a file. Run before the first Edit on any file per
 # session — especially under parallel-thread development. Surfaces
 # uncommitted changes (HEAD commit, status, full diff) so the caller

STATUS.md

@@ -19,7 +19,7 @@ belongs in the linked ADR, not here.
 ## At a glance
 
 - **Tri-arch first-class**: clean release build on `x86_64`, `aarch64`, `riscv64gc`; all three boot in QEMU to an `cambios>` shell prompt. `make check-all` is the permanent regression gate.
-- **903 host unit tests passing** on `x86_64-apple-darwin`. Run `make stats` for current counts — numbers live in code, not prose.
+- **Host unit tests passing** on `x86_64-apple-darwin`. Run `make stats` for the current count — numbers live in code, not prose.
 - **Security model live end-to-end**: cryptographic identity, signed-ELF verification, capability-gated IPC, content-addressed ObjectStore, audit ring, kernel identity gate, userspace `recv_verified`.
 - **GUI stack live on x86_64 + aarch64**: scanout-virtio-gpu drives QEMU virtio-gpu-pci; compositor composites; virtio-input forwards HID keyboard/pointer events into the focused window; first-party app `pong` (continuous-motion 1-player vs AI) runs as the default GUI boot module on x86_64, and `worm` renders on aarch64 via `make run-aarch64-gui` now that the kernel has an ECAM-based PCI enumerator. `tree` (Minesweeper) stays buildable for regression.
 - **Persistent storage live**: virtio-blk + disk-backed ObjectStore + `arcobj` shell CLI; objects survive reboot.
@@ -204,7 +204,7 @@ Parity-target with x86_64 / AArch64. All phases landed as of 2026-04-19. Source:
 
 ## Test coverage
 
-Total: **903** on `x86_64-apple-darwin`. Run `RUST_MIN_STACK=8388608 cargo test --lib --target x86_64-apple-darwin`, or `make stats` for the current number.
+Run `RUST_MIN_STACK=8388608 cargo test --lib --target x86_64-apple-darwin`, or `make stats`, for the current total on `x86_64-apple-darwin`. The number is not pinned in prose — it lives in code, and a hardcoded copy only drifts CI red as the suite grows.
 
 Major categories (approximate; breakdown drifts faster than the total):
 

tools/check-status-freshness.py

@@ -4,43 +4,38 @@
 """
 Pre-commit advisory: surface STATUS.md drift before it compounds.
 
-Two independent advisory checks, both exit-0 (warn-but-pass), in the
-same don't-grow-the-baseline family as the other tools/check-*.py gates.
+Two independent advisory checks, both exit-0 (warn-but-pass) by default, in
+the same don't-grow-the-baseline family as the other tools/check-*.py gates.
 
 1. DATE drift — `last_synced_to_code:` more than THRESHOLD_DAYS old.
-   (Original behavior, unchanged. Rationale: the 2026-04-22 -> 2026-05-04
-   12-day drift window that had to be recovered in one large catch-up sync.)
-
-2. NUMBER drift — STATUS.md's prose counts no longer match the source.
-   This is the gap that let the file sit at "561 host unit tests /
-   47 harnesses" while the code was already at 892 / 48: a sync bumped
-   the *date* but never re-derived the *numbers*, and a date-only check
-   passed silently. The date moving is not evidence the counts moved.
-
-   - Kani harness count is derived CHEAPLY (count active `#[kani::proof]`
-     under verification/, no compile) and compared to every *total*
-     stated in STATUS.md prose. Safe to run on every commit.
-   - The unit-test count cannot be derived without compiling, so by
-     default this only checks that the stated test numbers agree with
-     EACH OTHER (catches a partial update — one mention fixed, another
-     missed). With `--full` it runs `make stats` and compares against the
-     live count; that path compiles, so it is for CI / manual runs, NOT
-     the pre-commit hook.
-
-Posture unchanged: advisory, exit 0. Only config-level errors (STATUS.md
-missing, unparseable date) exit 1. Tighten to a hard block by flipping
-the relevant return once the warn cycle proves it changes behavior.
+   Rationale: the 2026-04-22 -> 2026-05-04 12-day drift window that had to
+   be recovered in one large catch-up sync. The date moving is not, on its
+   own, evidence the content moved.
+
+2. KANI-HARNESS number drift — STATUS.md's stated harness totals no longer
+   match the source. Derived CHEAPLY (count active `#[kani::proof]` under
+   verification/, no compile) and compared to every *total* stated in the
+   prose. Safe to run on every commit.
+
+   The unit-test COUNT is deliberately NOT checked. STATUS.md no longer pins
+   a test total in prose — it points at `make stats` instead — because that
+   number can only be derived by compiling, and a hardcoded copy drifted CI
+   red every time the suite grew (892 -> 903 was the last instance). With no
+   pinned number there is nothing to compare and nothing to drift, so the
+   `--full`/`make stats` path that used to verify it is gone entirely.
+
+Posture: advisory, exit 0. `--strict` makes objective Kani-harness drift
+exit 1 (for CI); the date heuristic always stays advisory. Only config-level
+errors (STATUS.md missing, unparseable date) exit 1 unconditionally.
 
 Usage:
-  python3 tools/check-status-freshness.py          # date + cheap number checks (pre-commit)
-  python3 tools/check-status-freshness.py --full    # also re-derive the test count via `make stats`
-  make check-status-freshness                       # no-arg form
-  make check-status-freshness-full                  # --full form
+  python3 tools/check-status-freshness.py            # date + Kani-harness checks
+  python3 tools/check-status-freshness.py --strict   # Kani-harness drift FAILs (CI)
+  make check-status-freshness                         # no-arg form
 """
 import argparse
 import datetime
 import re
-import subprocess
 import sys
 from pathlib import Path
 
@@ -59,11 +54,6 @@
     re.compile(r"(\d+)\s+harnesses across \d+ proof crates"),
     re.compile(r"(\d+)\s+passing harnesses"),
 )
-TEST_COUNT_RES = (
-    re.compile(r"(\d+)\s+host unit tests"),
-    re.compile(r"Total:\s*\*\*(\d+)\*\*"),
-)
-MAKE_STATS_TESTS_RE = re.compile(r"Tests \(lib\):\s*(\d+)")
 
 _WARNINGS = 0
 
@@ -131,10 +121,10 @@ def stated_counts(text: str, patterns) -> list:
     return found
 
 
-def check_numbers(text: str, full: bool) -> int:
-    """Advisory number-drift checks. Returns the count of genuine drift
-    mismatches (operational warnings — missing dir, unparseable `make stats`
-    — do not count, so they never trip --strict / CI)."""
+def check_numbers(text: str) -> int:
+    """Advisory number-drift check (Kani harnesses). Returns the count of
+    genuine drift mismatches; operational warnings (missing verification/ dir)
+    do not count, so they never trip --strict / CI."""
     drift = 0
 
     # --- Kani harnesses: cheap, every run ---
@@ -153,52 +143,19 @@ def check_numbers(text: str, full: bool) -> int:
                 f"{', '.join(map(str, bad))}. Update the harness totals."
             )
 
-    # --- Unit tests: intra-prose consistency always; live compare on --full ---
-    stated_t = stated_counts(text, TEST_COUNT_RES)
-    if stated_t and len(set(stated_t)) > 1:
-        drift += 1
-        warn(
-            "STATUS.md states inconsistent unit-test counts "
-            f"({', '.join(map(str, sorted(set(stated_t))))}) — the prose "
-            "disagrees with itself, a partial update."
-        )
-    if full and stated_t:
-        try:
-            out = subprocess.run(
-                ["make", "stats"], capture_output=True, text=True,
-                timeout=900, check=False,
-            ).stdout
-        except (OSError, subprocess.SubprocessError) as exc:
-            warn(f"--full: could not run `make stats` ({exc}).")
-            return drift
-        match = MAKE_STATS_TESTS_RE.search(out)
-        if not match:
-            warn("--full: could not parse Tests(lib) from `make stats`.")
-            return drift
-        live = int(match.group(1))
-        bad = sorted({n for n in stated_t if n != live})
-        if bad:
-            drift += 1
-            warn(
-                f"Unit-test drift: `make stats` reports {live} lib tests, "
-                f"STATUS.md states {', '.join(map(str, bad))}. Update the "
-                "test totals."
-            )
+    # The unit-test count is intentionally NOT checked. STATUS.md no longer
+    # pins a total in prose (it points at `make stats`), so there is nothing
+    # to drift against and nothing that would need a compile to verify.
     return drift
 
 
 def main() -> int:
     parser = argparse.ArgumentParser(
-        description="STATUS.md freshness advisory (date + number drift)."
-    )
-    parser.add_argument(
-        "--full", action="store_true",
-        help="also re-derive the unit-test count via `make stats` "
-             "(compiles; for CI / manual use, not the pre-commit hook)",
+        description="STATUS.md freshness advisory (date + Kani-harness drift)."
     )
     parser.add_argument(
         "--strict", action="store_true",
-        help="exit 1 on objective number drift (Kani/test count mismatch). "
+        help="exit 1 on objective Kani-harness drift (source vs prose). "
              "The date heuristic stays advisory. For CI enforcement.",
     )
     args = parser.parse_args()
@@ -215,7 +172,7 @@ def main() -> int:
     rc = check_date(text)
     if rc != 0:
         return rc
-    drift = check_numbers(text, full=args.full)
+    drift = check_numbers(text)
 
     if args.strict and drift:
         print(