feat(guard): a sorry cannot exempt itself by writing a comment (#385)

[avrabe]

REQ-GUARD-GATE-EVIDENCE-002 (f) — v0.36.0 bug-fix track. Written during the GitHub Actions outage, so CI here will be red for infrastructure reasons until the incident clears; see #395 for the same situation.

The defect

Fail on sorry (post-build gate) is part of the required Lean proof typecheck (lake build) context. It permitted every sorry in the tree while printing:

No sorrys in proofs/Proofs/ — gate green.

It excluded any sorry with a same-line -- TODO, and all twelve are sorry -- TODO(v1.0.0). Twelve in, zero out, the if never fires. The gate was satisfied by exactly the thing it exists to prevent.

How it drifted — the part worth keeping

The step's own comment said:

"The five tracked sorrys do NOT carry a same-line comment; the TODO sits on the prior line, so this gate flags all five."

That was true when written. The exclusion was a deliberate no-op against a form nobody used. The sorries then grew 5 → 12 and moved their TODO onto the same line — and the no-op silently became universal. Nobody edited the guard; the code drifted out from under its comment.

So the defect isn't a careless filter. It's that a self-exemption keyed on a pattern the exempted code itself controls cannot hold — the proof author writes both the sorry and the -- TODO that excuses it, in one commit, and no review step sees the exemption grow.

The replacement

A ratchet, same shape as the mutants gate. No comment-based exemption at all — a -- TODO is a note to humans, not a permit — and the floor lives in proofs.yml, not in the proofs.

condition	behaviour
count > floor	FAIL — new sorries cannot be admitted by writing a comment
count < floor	PASS, loudly saying to lower the floor. Improving must never fail, or the ratchet gets walked back instead of tightened
empty scan	exit 2 — zero sorries because no .lean was read is the error-path-yields-ideal-reading shape this requirement names

Count plus per-file, per-line breakdown prints on every path including success, so "12 permitted" is visible rather than inferred from silence.

Measured

On ae27ff1: 11 .lean files scanned, 12 sorries (MinPlus.lean 4, MinPlusPwa.lean 8). Floor set to 12 — green and honest rather than green and blind. Verified it can go red: at --max-sorries 11 it exits 1 naming the breach.

8-case self-test runs before the gate judges anything. The discriminating pair is the regression itself: sorry -- TODO counts and breaches a floor of 0, and the same file passes at a floor of 1 — the comment is signal for neither verdict. A checker still honouring the exemption passes the first case and cannot fail it. Also pinned: sorryAx and "sorry" in prose are not bare sorries.

Not claimed

That the 12 remaining sorries are acceptable. The floor records how many exist, not that they're fine — discharging them is REQ-PROOF-NC-MINPLUS-001 (v0.38.0). This only stops the number rising unnoticed, which is exactly what it did between 5 and 12.

Refs #385

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!