Skip to content

[P2.36] run_proof discards why it produced no results, so callers have to guess #1138

Description

@frankbria

Split out of #1118 / PR #1137, after four review rounds each catching the CLI asserting a wrong reason. Priority P2.36 — severity low, category observability.

Problem

run_proof returns dict[req_id, list[(gate, outcome)]] and nothing else. When that dict is empty, the caller cannot tell why, because the reasons are computed inside the runner and then discarded:

cause where it happens reported?
ledger empty _requirements_for_run[] no
all requirements excluded by status (SATISFIED on a scoped run, WAIVED always) runner.py:261-263 no
scope filter excluded every requirement runner.py:339-342, collected into scope_skipped computed, then only logged (runner.py:435)
--gate excluded every obligation runner.py:355-356 no
enabled_gates config excluded them runner.py:359-360 no
requirement has no obligations no

scope_skipped is the closest: the runner builds the list and hands it to _report_scope_skipped for logging, but never returns it.

Why it matters

#1118 made cf proof run distinguish "nothing to verify" from "verified and passed". Doing that well needs the reason, and the CLI can only guess at it. Four consecutive review rounds on #1137 caught a guess that was confidently wrong:

  • claiming scope when the ledger was empty
  • claiming scope in --full mode, where scope is never evaluated
  • claiming scope when the requirements were all WAIVED, so run_proof short-circuited before scope was computed
  • claiming scope when --gate unit had excluded every obligation of an in-scope requirement

The CLI now stops asserting a cause and lists the candidates. That is honest but worse for the user than naming the actual reason.

Acceptance criteria

  • run_proof reports why it produced no results — a structured reason alongside the results, not a log line
  • At minimum it distinguishes: no requirements, excluded by status, excluded by scope, excluded by gate filter/config, no obligations defined
  • cf proof run names the actual reason instead of listing candidates
  • _report_scope_skipped keeps working, or its logging is subsumed
  • A test per reason

Notes

There are ~24 call sites of run_proof, so widening the return type is the main cost. An additive approach (a second return value, or an out-parameter object) avoids touching all of them.

Metadata

Metadata

Assignees

No one assigned

    Labels

    type:bugSomething is broken and needs fixing

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions