fix(proof): an empty ledger is not a pass (#1118) - #1137
Conversation
`cf proof run` is the quickstart's PROVE step, on the product's stated differentiator. On a fresh workspace it printed "No applicable obligations found." in green and exited 0 — which reads as "PROOF9 quality gates passed" when nothing had been checked. Every new workspace is in that state, and it held even after an agent run had written code and tests. Exit 2, not 1. An empty ledger is not a failure, but it cannot be 0 either or CI stays green on it. A third code lets a script tell "the gate failed" from "the gate had nothing to check" — different problems needing different responses. --allow-empty opts back into 0 where that is genuinely expected, and still prints the explanation. The message now says nothing was verified, that this is not a pass, and how to capture a first requirement. `cf proof status` says the same rather than the neutral "No proof requirements". For the #731 merge gate: it now reports an empty ledger instead of passing in silence, but still allows the merge. Blocking every merge in a workspace with no requirements is far beyond this issue and would immediately block this repo's own PRs; #731's gate is about *open* requirements. The consistency AC #4 asks for is that both surfaces say "nothing was verified", which they now do. docs/QUICKSTART.md already said "exits 0 — ... which is not the same as passing". The doc had the right model and the behaviour did not match it; it now describes the real exit codes. test_run_no_requirements_exits_zero pinned the old contract and is rewritten, with a companion for --allow-empty. 10 new tests. The #614 harness records this step as FAIL / exit 2 now, which is the honest record of the state it exists to surface. It does not abort (set -uo pipefail, no -e). Full suite: 6390 passed, 49 skipped.
|
Claude finished @frankbria's task in 3m 56s —— View job GLM bug-hunting review — #1118Scoped to concrete defects only (logic, contract, security, data loss). Style, naming, architecture, and test coverage are covered by the general review.
1 finding.
Why it's real: Reviewed and cleared (no defect):
|
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Review: #1137 — an empty ledger is not a passOverall this is a well-scoped, well-tested change to Bug:
|
Review finding, and a regression I was introducing rather than one I inherited.
run_proof returning {} is ambiguous: the ledger may be empty, or it may hold
requirements none of which intersect the changed scope. My first version treated
both as the vacuous-pass case, so a workspace with three requirements scoped to
src/** and a doc-only PR would have been told "there are no proof obligations in
this workspace ... capture your first requirement" and exited 2 — failing CI
because the scope filter did exactly its job.
The two states now report separately:
empty ledger -> "no obligations in this workspace", exit 2
nothing in scope -> "N requirement(s) exist, but none apply to the
changed files", points at --full, exit 0
Both still say "nothing was verified", which is true either way; only the first
is the silent-green this issue is about. A ledger that cannot be read falls
through to the unverified case rather than claiming scope filtering.
The tests patch run_proof rather than staging changes through git: with no
working-tree changes the scope detector fails closed and runs everything, so the
real filter cannot produce this state in a fixture. The ambiguity under test is
in how the CLI reports an empty result.
Full suite: 6394 passed, 49 skipped.
|
Claude finished @frankbria's task in 4m 46s —— View job GLM bug-hunting review — #1137 (re-review after fix push)Scoped to concrete defects only (logic, contract, security, data loss). Style, naming, architecture, and test coverage are covered by the general review.
The conflation bug from the first pass is fixed correctly: the empty- 1 finding.
Reviewed and cleared (no defect):
Note (not a defect in this diff, pre-existing in untouched |
Review: #1137 (update) — an empty ledger is not a passThe second commit ( New finding: the scope-skip message conflates scope with status, and ignores
|
Second review finding. The "requirements exist but nothing ran" branch
hard-coded the scope-filter explanation, but it is reachable in --full mode too —
where runner.py skips the scope check entirely. An all-waived ledger lands there:
_requirements_for_run excludes WAIVED from both modes, so the runnable set is
empty while list_requirements() is not.
The result was a message that was confidently wrong ("none apply to the changed
files" when scope was never consulted) followed by circular advice ("run --full"
to someone who just did).
Now branched on the mode:
scoped -> "none apply to the changed files", points at --full
--full -> "none are runnable (N waived)", points at cf proof status and
notes a waiver is an accepted risk that no run re-checks
Exit code was already correct (0) in both; only the explanation was wrong.
Full suite: 6396 passed, 49 skipped.
|
Claude finished @frankbria's task in 4m 31s —— View job GLM bug-hunting review — #1137 (re-review after latest synchronize)Scoped to concrete defects only (logic, contract, security, data loss). Style, naming, architecture, and test coverage are covered by the general review.
The 1 finding.
Reviewed and cleared (no defect):
Note (pre-existing, outside this PR's files): |
Review: #1137 (update after 9cafa2f) — an empty ledger is not a passThe third commit fixes the second finding cleanly: One more instance of the same conflation (minor)
Both land in the Same shape as the two prior findings, so flagging for consistency; not blocking given the milder impact (exit code still correct at 0, and the fallback advice still works). Still open: merge-gate print has no testNoted in both previous reviews — still true after this commit. The "PROOF9: the ledger is empty" print added to Everything elseExit-code scheme (0/1/2), |
Third review finding of the same shape, so this stops patching branches and changes the approach. The CLI was inferring the reason for an empty result from the --full flag. That is wrong because run_proof short-circuits when the runnable set is empty, *before* scope is ever computed — so an all-SATISFIED scoped ledger, or an all-WAIVED one in either mode, was reported as "none apply to the changed files" when scope had not been consulted at all. The root cause is two places independently deciding what "runnable" means. The CLI now calls the runner's own _requirements_for_run, so it cannot drift. Four causes, four accurate messages: ledger empty "no obligations in this workspace" exit 2 nothing runnable "none are runnable (1 waived)" exit 0 nothing in scope (scoped) "none apply to the changed files" exit 0 runnable, no results states only what is known exit 0 The scope branch is now guarded on `not full`, since --full never evaluates scope; the remaining --full case says what is known rather than inventing a fourth reason. Test hygiene: assertions were matching against Rich's hard-wrapped output, so "changed files" failed to match text that was present. Added a whitespace flattener — otherwise those tests fail cosmetically and get "fixed" by being weakened. Full suite: 6398 passed, 49 skipped.
|
Claude finished @frankbria's task in 3m 50s —— View job GLM bug-hunting review — #1137 (re-review after latest synchronize)Scoped to concrete defects only (logic, contract, security, data loss). Style, naming, architecture, and test coverage are covered by the general review.
The status-vs-scope / waived-vs- 1 finding.
Reviewed and cleared (no defect):
Note (pre-existing, outside this PR's files): |
Review: #1137 (final pass, at
|
Fourth review round on the same message, and the answer is to stop guessing.
run_proof computes the reasons and discards them: it builds scope_skipped
(runner.py:334), hands it to a logger (runner.py:435), and returns only results.
So an empty dict has at least six causes — empty ledger, excluded by status,
excluded by scope, excluded by --gate, disabled in proof_config.json, or no
obligations defined — and the caller has no way to tell them apart. Each of my
previous fixes was a better guess at unknowable information, and each was wrong
somewhere else:
round 1: claimed scope when the ledger was empty
round 2: claimed scope in --full mode, where scope is never evaluated
round 3: claimed scope for an all-WAIVED ledger, where run_proof
short-circuits before scope is computed
round 4: claimed scope when --gate excluded every obligation of an
in-scope requirement
The eligible-requirements branch now states what is known and lists the
candidates, naming the actual --gate value when one was passed. The one case
that IS knowable — runnable set empty while the ledger is not — keeps its
precise message ("none are runnable (1 waived)").
#1138 tracks having run_proof report its reason, which would let this be exact.
That is a core change across ~24 call sites and outside what #1118 asked for.
Full suite: 6399 passed, 49 skipped.
|
Claude finished @frankbria's task in 4m 10s —— View job GLM bug-hunting review — #1137 (re-review after latest synchronize)Scoped to concrete defects only (logic, contract, security, data loss). Style, naming, architecture, and test coverage are covered by the general review.
The 1 finding.
Reviewed and cleared (no defect):
Note (pre-existing, outside this PR's files): |
Review: #1137 (final pass, at
|
Fifth review round. The candidate list always included "none of them cover the changed files", but --full never consults scope (runner.py:339), so the honest enumeration itself contained an impossible cause. Candidates are now filtered to the invocation: scoped, no gate scope, config, no obligations scoped + --gate scope, --gate <value>, config, no obligations --full + --gate --gate <value>, config, no obligations Two tests pin both omissions: scope absent under --full, and the --gate candidate absent when no gate was passed. Full suite: 6401 passed, 49 skipped.
|
Claude finished @frankbria's task in 2m 40s —— View job GLM bug-hunting review — #1137 (re-review after latest synchronize)Scoped to concrete defects only (logic, contract, security, data loss). Style, naming, architecture, and test coverage are covered by the general review.
The I re-derived the candidate list against the actual causes of
These four are exhaustive for an empty ✅ GLM review: no defects found. Reviewed and cleared (no defect):
Note (pre-existing, outside this PR's files, tracked as #1138): |
Review: #1137 (at
|
`run_proof` returned only `dict[req_id, [(gate, outcome)]]`, and an empty dict has six causes. The runner computed them and threw them away — `scope_skipped` got as far as a log line — so `cf proof run` had to infer the reason from the flags. Four consecutive review rounds on #1137 caught it inferring wrong, each time about a different cause. `run_proof_with_diagnostics` returns `(results, ProofRunDiagnostics)`. `run_proof` stays as a one-line wrapper, so the ~60 call sites that only want the dict are untouched — the additive approach the issue asks for. `EmptyReason` distinguishes: no requirements, excluded by status, excluded by scope, excluded by the --gate filter, excluded by enabled_gates, excluded by the two filters jointly, no obligations defined, and MIXED. Diagnostics carries the per-bucket requirement ids, not just a verdict: with three requirements dropped for three reasons, any single reason is wrong, so `reason` collapses only when the collapse is honest and `describe()` enumerates otherwise. The CLI now names the cause and gives the matching remedy instead of printing a candidate list. `_report_scope_skipped` is unchanged (#922's warning still fires); the empty-ledger exit-2 behaviour from #1118 is unchanged. The joint-filter case came from review and is worth spelling out: with obligations {unit, sec}, `--gate unit` and `enabled_gates: ["sec"]`, NEITHER filter excludes everything on its own, so both `all(...)` checks were false and the requirement fell into no bucket — surfacing as an unclassified MIXED with no hint at all. Each filter is now tested for sufficiency separately, and the joint case has its own reason and its own remedy. Updating tests/cli/test_proof_empty_ledger_1118.py was not optional: it patched `runner.run_proof`, which the CLI no longer calls, so the patch quietly stopped applying and the tests began asserting against a live run. That failed loudly here, but it is the same class of thing as #1077 — a guard patching a function nothing calls. Most of those cases are now driven for real instead: a waived ledger, a --gate that matches no obligation, and a requirement with no obligations are all reachable states. Only the scope filter still needs a patch, because with no working-tree changes the detector fails closed.
1 participant
Closes #1118.
Before / after
Why exit 2, not 1
An empty ledger is not a failure — but it cannot be
0either, or CI staysgreen on it, which is the whole complaint. A third code lets a script tell "the
gate failed" from "the gate had nothing to check"; those need different
responses.
--allow-emptyopts back into0where that is genuinely expected — and stillprints the explanation, so opting into the exit code does not silence the reason.
cf proof statussays the same thingIt previously said the neutral "No proof requirements." Both surfaces now
frame an empty ledger as nothing is being verified, so they cannot disagree
about what it means.
The docs already said this
docs/QUICKSTART.md, verbatim before this change:The documentation had the right model; the behaviour did not match it. It now
describes the real exit codes.
AC #4 — the merge gate, and where I drew the line
The #731 gate now reports an empty ledger instead of passing in silence, but
still allows the merge.
Making an empty ledger a merge blocker would be a much larger change than this
issue asks for, and it would immediately block this repository's own PRs — this
repo has no proof requirements. #731's gate is specifically about open
requirements. I read AC #4's "consistently" as both surfaces must stop implying
verification happened, which they now do. Say the word if you meant the
stronger reading and I will make it blocking.
Acceptance criteria
--allow-emptydefaulting to the safe behaviour10 new tests.
ruffclean. Full suite: 6390 passed, 49 skipped.Note on the #614 harness
scripts/quickstart-cleanroom/walkthrough.shwill now record5-proof-runasFAIL / exit 2. That is the honest record of the state the harness exists tosurface, and it does not abort the walkthrough (
set -uo pipefail, no-e).Contract change
test_run_no_requirements_exits_zeroasserted the old behaviour and isrewritten, with a companion covering
--allow-empty. Anything scripted againstcf proof runreturning 0 on an empty ledger needs--allow-empty— which isthe intended migration, since that is precisely the silent green this removes.