feat(proof): report why a proof run produced no results (#1138)

[frankbria]

Closes #1138.

What

run_proof returned only dict[req_id, [(gate, outcome)]], and an empty dict has six causes. The runner computed every one of 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. It ended up printing a candidate list: honest, and useless.

run_proof_with_diagnostics(...) → (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.

The reasons

EmptyReason	Cause
NO_REQUIREMENTS	the ledger is empty
EXCLUDED_BY_STATUS	all WAIVED, or SATISFIED on a scoped run
EXCLUDED_BY_SCOPE	none intersect the changed files
EXCLUDED_BY_GATE_FILTER	--gate excluded every obligation
EXCLUDED_BY_CONFIG	enabled_gates did
EXCLUDED_BY_FILTER_COMBINATION	neither alone did, but their intersection is empty
NO_OBLIGATIONS	in-scope requirements define none
MIXED	more than one applies, so naming one would be a lie

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 names the cause and gives the matching remedy. _report_scope_skipped is unchanged (#922's warning still fires) and #1118's empty-ledger exit-2 is unchanged.

Review finding, worth spelling out

codex review caught a real gap in the first version:

With obligations {unit, sec}, --gate unit and enabled_gates: ["sec"], no obligation runs but neither all(...) check is true. The requirement is left out of every diagnostics bucket.

Correct. It surfaced as an unclassified MIXED with no hint at all — the exact failure this PR exists to remove, in a case I had not thought of. Each filter is now tested for sufficiency separately, and the joint case gets its own reason and its own remedy ("drop --gate, or add that gate to enabled_gates — each filter alone leaves work to do, but they do not overlap"). Three tests cover it, including one asserting the joint bucket does not swallow the simple single-filter cases.

A test file that had stopped testing

tests/cli/test_proof_empty_ledger_1118.py patched runner.run_proof, which the CLI no longer calls. The patch quietly stopped applying and those tests began asserting against a live run. It failed loudly here, but it is the same class as #1077 — a guard patching a function nothing calls.

Most of them are now driven for real rather than patched: 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 and evaluates everything.

Testing

• tests/core/test_proof_run_diagnostics_1138.py — one test per reason, as the AC asks, plus the joint-filter case, the mixed case, and the back-compat wrapper
• tests/cli/test_proof_empty_ledger_1118.py — rewritten for the new contract; 34 tests pass across both files
• Full backend suite + ruff reported in a comment

Known limitation

The v2 proof router still returns results only. It does not currently explain an empty run to the web UI either, but that is a separate surface with its own response model and no acceptance criterion here — the issue's ask is run_proof and cf proof run. The diagnostics object is what a follow-up would serialise.

[github-actions]

Claude finished @frankbria's task in 6m 28s —— View job

---

Bug-hunting review complete

• Gather PR diff and context
• Read changed files and surrounding code/callers
• Analyze for concrete defects (logic errors, null derefs, data loss, contract breaks)
• Post summary

Scope: concrete defects only (logic errors, crashes, data loss, contract breaks, security). Style/coverage/architecture is covered by the general review.

Method: read the full diff, then opened codeframe/core/proof/runner.py, codeframe/cli/proof_commands.py, codeframe/ui/routers/proof_v2.py, codeframe/core/proof/scope.py, codeframe/core/proof/obligations.py, and codeframe/core/proof/ledger.py to verify each suspicious hunk against real context.

Areas scrutinized and cleared:

• ProofRunDiagnostics.reason (runner.py:84–107) — the collapse logic is sound: evaluated → total → considered ordering correctly distinguishes NOT_EMPTY / NO_REQUIREMENTS / EXCLUDED_BY_STATUS; the len(non_empty)==1 → single, >=2 → MIXED, 0 → defensive MIXED fallback is correct. The fallback is unreachable in practice (every considered-but-unevaluated requirement lands in exactly one bucket), but harmless.
• Filter attribution (runner.py:545–566) — proven correct: the block is entered iff survives_gate ∩ survives_config is empty, and the if not survives_gate / elif not survives_config / else partition is exhaustive and matches the loop's filters exactly. The joint case gets its own bucket and does not swallow the single-filter cases.
• Bucket mutual exclusivity — a no-obligation requirement is added only to no_obligations (the filter block requires req.obligations truthy); out-of-scope requirements continue before any other bucket. No requirement is double-counted.
• _REASON_TEXT (runner.py:136–164) covers all 9 enum values, so describe() cannot KeyError.
• run_proof wrapper (runner.py:404–419) preserves the exact signature and returns [0] (the dict), so the v2 router (run_in_threadpool(run_proof, …) at proof_v2.py:444) and the other ~60 dict-consuming call sites are unbroken.
• Early-return path (runner.py:462–476) returns {}, diagnostics with evaluated=0/buckets defaulted — reason/describe() still resolve correctly there.
• CLI exit codes (proof_commands.py:189–254) — only NO_REQUIREMENTS exits 2 (gated by --allow-empty); all other empty reasons exit 0. This matches the prior behavior exactly; no regression.

✅ GLM review: no defects found.

[claude]

Review: feat(proof): report why a proof run produced no results (#1138)

Read through codeframe/core/proof/runner.py, codeframe/cli/proof_commands.py, and both test files (checked out the merge commit locally rather than relying on the diff alone). This is a well-scoped, well-tested PR — no prior human/AI review comments on this PR to reconcile with, just the still-in-progress automated placeholder.

Correctness

Traced the classification logic in ProofRunDiagnostics end-to-end:

• No double-counting. A requirement lands in exactly one bucket: scope-skip continues before the no_obligations/filter checks even run, and the post-loop filter-attribution block (runner.py:545) is gated on req.obligations being non-empty, so a no_obligations requirement can never also land in gate_filtered/config_filtered/filter_combination.
• The joint-filter fix is right. survives_gate/survives_config are each computed independently against the full obligation list, so a requirement excluded only by the intersection of --gate and enabled_gates correctly lands in EXCLUDED_BY_FILTER_COMBINATION rather than being silently dropped (the exact gap codex review caught, per the PR description) or misattributed to whichever filter happened to be checked first.
• reason collapse is honest. Verified the MIXED fallback at the bottom of the property is currently unreachable dead code (every considered-but-not-evaluated requirement is provably captured by one of the five buckets), so it's a safe defensive branch rather than a sign something's missing.
• CLI exit codes are unchanged from the old behavior: only NO_REQUIREMENTS exits 2 (or 0 with --allow-empty); every other reason (EXCLUDED_BY_STATUS, EXCLUDED_BY_SCOPE, filter-related, NO_OBLIGATIONS, MIXED) falls through to a plain return, i.e. exit 0 — matching the pre-PR behavior for those cases. Good backward compat.
• Confirmed codeframe/ui/routers/proof_v2.py still imports the plain run_proof, so the "known limitation" called out in the PR description (v2 router doesn't explain empty runs yet) is accurate and this change doesn't silently break that surface.
• core/ stays headless — no FastAPI/UI imports introduced, consistent with the architecture rule in CLAUDE.md.

Minor nits (non-blocking)

1. "six causes" is an undercount. The EmptyReason docstring, the CLI comment, and the new test file's module docstring all say "an empty dict has six different causes," but there are 7 non-meta reasons enumerated (NO_REQUIREMENTS, EXCLUDED_BY_STATUS, EXCLUDED_BY_SCOPE, EXCLUDED_BY_GATE_FILTER, EXCLUDED_BY_CONFIG, EXCLUDED_BY_FILTER_COMBINATION, NO_OBLIGATIONS) — 8 counting MIXED. Given this PR's entire thesis is "stop stating things imprecisely," it's a bit ironic to carry over a stale count from an earlier iteration (fix(proof): an empty ledger is not a pass (#1118) #1137 apparently started at "three"). Worth a quick find-and-fix pass.
2. Extra DB round trip. run_proof_with_diagnostics now calls ledger.list_requirements(workspace) (unfiltered) in addition to _requirements_for_run's own filtered queries, purely to get total_requirements for the NO_REQUIREMENTS vs EXCLUDED_BY_STATUS distinction. Fine for a single CLI invocation; flagging only because if this diagnostics path ever gets adopted by the v2 router (the stated follow-up), it's one more query per request worth being aware of.
3. Readability nit in ProofRunDiagnostics.reason: non_empty = [name for name, ids in buckets.items() if ids] — name is actually the EmptyReason enum member (used as a dict key), not a string name. A rename to reason/cause would avoid the momentary "wait, that's not a string" double-take.

Test coverage

Solid — one test per EmptyReason value, the joint-filter case, a dedicated mixed-cause test, the run_proof back-compat wrapper, and _report_scope_skipped still firing (#922 regression guard). The rewrite of test_proof_empty_ledger_1118.py to patch run_proof_with_diagnostics instead of the now-dead run_proof patch target is the right fix — nice catch calling out that the old patch was silently no-op-ing (same class as #1077).

Nothing here blocks merge; the nits above are polish, not correctness issues.

[frankbria]

Demo — each reason named, on a real workspace

Not asserted from tests: cf driven against a fresh cf init workspace, one requirement captured for real.

1. Empty ledger — unchanged #1118 behaviour, exit 2:

Nothing was verified.
There are no proof obligations in this workspace, so this run checked nothing — it is not a pass.
Capture your first requirement with:
  cf proof capture

2. Out of scope — the requirement is scoped to src/auth/login.py, which this repo does not contain. No patch, no mock — the real scope filter:

Nothing was verified. all 1 open requirement(s) are out of scope for the current
changes — re-run with --full to include them.
cf proof run --full ignores scope entirely.

Before this PR that same state printed Possible reasons: none of them cover the changed files; their obligations are disabled in proof_config.json; they have no obligations defined.

3. --gate perf, against a requirement whose obligations are unit and contract:

Nothing was verified. the --gate filter excluded every obligation of all 1
in-scope requirement(s).
Drop --gate to run every obligation.

4. All waived — scope is never evaluated here, because the runner short-circuits before it. Naming scope was one of the four wrong guesses:

Nothing was verified. all 1 requirement(s) are waived, or satisfied on a scoped
run — re-run with --full to include satisfied ones.
A waiver is an accepted risk that no run re-checks; cf proof run --full also re-verifies satisfied ones.

Each output names one cause and one remedy. No candidate lists.

Acceptance criteria

AC	Evidence
run_proof reports why, structured, not a log line	run_proof_with_diagnostics → (results, ProofRunDiagnostics)
Distinguishes no-requirements / status / scope / gate-filter / config / no-obligations	EmptyReason, 8 members — the AC's five plus FILTER_COMBINATION (from review) and NOT_EMPTY/MIXED
cf proof run names the actual reason	the four transcripts above
_report_scope_skipped keeps working	unchanged; a test asserts the #922 warning still fires
A test per reason	tests/core/test_proof_run_diagnostics_1138.py

Checks

• Full backend suite: 6478 passed, 49 skipped, 606s
• uv run ruff check . — clean
• All 14 CI checks green
• codex review — one P2, fixed (the joint-filter case), detailed in the PR body