fix(proof): an empty ledger is not a pass (#1118)

codeframe/cli/pr_commands.py

@@ -463,6 +463,22 @@ def _check_merge_gate(
         console.print(f"[red]PROOF9 gate check failed:[/red] {e} — merge blocked")
         raise typer.Exit(1)
     if not blocking_reqs:
+        # Consistent with `cf proof run` (#1118): say so when the ledger is
+        # empty, rather than letting silence read as "PROOF9 verified this".
+        # The merge is still allowed — blocking every merge in a workspace with
+        # no requirements would be a far larger change than this issue asks for,
+        # and #731's gate is about *open* requirements.
+        try:
+            from codeframe.core.proof import ledger as _ledger
+
+            if not _ledger.list_requirements(workspace):
+                console.print(
+                    "[yellow]PROOF9:[/yellow] the ledger is empty — this merge "
+                    "was not verified against any requirement."
+                )
+        except Exception:
+            # Reporting only; never let it affect the merge decision.
+            pass
         return None
 
     if not override:

codeframe/cli/proof_commands.py

@@ -135,12 +135,25 @@ def run(
     gate: Optional[str] = typer.Option(
         None, "--gate", help="Run only this gate (e.g., unit, e2e)",
     ),
+    allow_empty: bool = typer.Option(
+        False,
+        "--allow-empty",
+        help=(
+            "Exit 0 when there are no applicable obligations. Off by default: "
+            "a run that verified nothing is not a pass (#1118)."
+        ),
+    ),
 ) -> None:
     """Run proof obligations for current changes.
 
     Determines which requirements apply to changed files,
     runs their obligations, and collects evidence.
 
+    Exit codes:
+        0  obligations ran and none failed
+        1  an obligation failed
+        2  nothing was verified — no applicable obligations (see --allow-empty)
+
     Example:
         codeframe proof run
         codeframe proof run --full
@@ -172,8 +185,112 @@ def run(
     results = run_proof(workspace, full=full, gate_filter=gate_filter)
 
     if not results:
-        console.print("[green]No applicable obligations found.[/green]")
-        return
+        # `run_proof` returning {} has three causes and they need different
+        # answers. Two review rounds went by patching one branch at a time and
+        # getting the reason wrong each time, so this asks the runner's own
+        # selector instead of inferring it from the mode:
+        #
+        #   ledger empty        -> nothing to verify at all (the #1118 case)
+        #   nothing runnable    -> requirements exist but all SATISFIED/WAIVED
+        #                          for this mode; scope was never consulted,
+        #                          because run_proof short-circuits first
+        #   nothing in scope    -> runnable requirements existed and the scope
+        #                          filter excluded every one
+        from codeframe.core.proof import ledger as _ledger
+        from codeframe.core.proof.models import ReqStatus
+        from codeframe.core.proof.runner import _requirements_for_run
+
+        try:
+            all_reqs = _ledger.list_requirements(workspace)
+            # Same selector the runner uses, so this cannot drift from it.
+            runnable = _requirements_for_run(workspace, full=full)
+        except Exception:
+            # A ledger we cannot read is not evidence of an empty one; fall
+            # through to the unverified case rather than inventing a reason.
+            all_reqs, runnable = [], []
+
+        if runnable:
+            # Four review rounds went by asserting a specific reason here and
+            # being wrong each time. The CLI genuinely cannot tell them apart:
+            # run_proof returns only results, and discards the scope_skipped
+            # list it computes internally (runner.py:334/435). With a non-empty
+            # runnable set an empty result can mean the scope filter excluded
+            # everything, --gate excluded every obligation, enabled_gates config
+            # did, or a requirement simply has none.
+            #
+            # So state what is known and list the candidates, rather than
+            # asserting one and sending the user somewhere useless. #1138 tracks
+            # having the runner report the reason so this can be precise.
+            console.print(
+                f"[yellow]Nothing was verified.[/yellow] "
+                f"{len(runnable)} requirement(s) were eligible for this run, "
+                f"but no obligations ran."
+            )
+            reasons = []
+            if not full:
+                # --full provably ignores scope (runner.py:339), so listing it
+                # there would put an impossible cause in the candidate list.
+                reasons.append("none of them cover the changed files")
+            if gate_filter is not None:
+                reasons.append(f"--gate {gate_filter.value} excluded their obligations")
+            reasons.append("their obligations are disabled in proof_config.json")
+            reasons.append("they have no obligations defined")
+            console.print("Possible reasons: " + "; ".join(reasons) + ".")
+            if not full:
+                console.print(
+                    "Try [bold]cf proof run --full[/bold] to ignore scope, or "
+                    "[bold]cf proof status[/bold] for the ledger."
+                )
+            else:
+                console.print("See [bold]cf proof status[/bold] for the ledger.")
+            return
+
+        if all_reqs:
+            # This one IS knowable: the runnable set is empty while the ledger
+            # is not, so every requirement was excluded by its status. WAIVED is
+            # excluded from both modes; SATISFIED only from a scoped run.
+            satisfied = sum(1 for r in all_reqs if r.status == ReqStatus.SATISFIED)
+            waived = sum(1 for r in all_reqs if r.status == ReqStatus.WAIVED)
+            detail = ", ".join(
+                part
+                for part in (
+                    f"{satisfied} satisfied" if satisfied else "",
+                    f"{waived} waived" if waived else "",
+                )
+                if part
+            )
+            console.print(
+                f"[yellow]Nothing was verified.[/yellow] "
+                f"{len(all_reqs)} requirement(s) exist, but none are runnable"
+                + (f" ({detail})." if detail else ".")
+            )
+            console.print(
+                "A waiver is an accepted risk that no run re-checks; "
+                "[bold]cf proof run --full[/bold] also re-verifies satisfied "
+                "ones. See [bold]cf proof status[/bold] for the ledger."
+            )
+            return
+
+        # An empty ledger is not a pass (#1118). Exiting 0 here is what let the
+        # quickstart's PROVE step read as "PROOF9 gates passed" when nothing had
+        # been checked — and every new workspace is in exactly this state.
+        #
+        # Exit 2 rather than 1: this is not a failure either, and a script needs
+        # to tell "the gate failed" from "the gate had nothing to check". CI
+        # treats any non-zero as a stop, which is the point.
+        console.print("[yellow]Nothing was verified.[/yellow]")
+        console.print(
+            "There are no proof obligations in this workspace, so this run "
+            "checked nothing — it is not a pass."
+        )
+        console.print(
+            "\nCapture your first requirement with:\n"
+            "  [bold]cf proof capture[/bold]"
+        )
+        if allow_empty:
+            console.print("\n[dim]--allow-empty: exiting 0 anyway.[/dim]")
+            return
+        raise typer.Exit(2)
 
     # Display results
     table = Table(title="Proof Results")
@@ -427,7 +544,13 @@ def status_cmd(
 
     reqs = ledger.list_requirements(workspace)
     if not reqs:
-        console.print("No proof requirements. Use 'cf proof capture' to add one.")
+        # Same framing as `cf proof run` (#1118): an empty ledger means nothing
+        # is being verified, which is a state to act on, not a clean bill.
+        console.print(
+            "[yellow]No proof requirements — nothing in this workspace is "
+            "being verified.[/yellow]"
+        )
+        console.print("Capture your first one with: [bold]cf proof capture[/bold]")
         return
 
     counts = {"open": 0, "satisfied": 0, "waived": 0}

docs/QUICKSTART.md

@@ -240,8 +240,12 @@ Then run the PROOF9 quality gates:
 codeframe proof run
 ```
 
-> On a brand-new workspace this reports `No applicable obligations found` and
-> exits 0 — there is nothing to verify yet, which is **not** the same as passing.
+> On a brand-new workspace this reports that **nothing was verified** and exits
+> **2** — there is nothing to check yet, which is not the same as passing, so it
+> is not reported as one (#1118). Exit codes: `0` obligations ran and none
+> failed, `1` an obligation failed, `2` nothing was verified. Pass
+> `--allow-empty` to exit 0 on an empty ledger where that is expected.
+>
 > Obligations accumulate as you capture glitches with `codeframe proof capture`;
 > each one becomes a permanent check. See `codeframe proof status` for the ledger.
 

tests/cli/test_proof_commands.py

@@ -247,12 +247,25 @@ def _outcome(_ws, gate, _rules=()):
         assert result.exit_code == 1, result.output
         assert "FAIL" in result.output
 
-    def test_run_no_requirements_exits_zero(self, ws):
-        """run on an empty workspace should exit 0 and say no obligations."""
+    def test_run_no_requirements_does_not_exit_zero(self, ws):
+        """run on an empty workspace reports that nothing was verified (#1118).
+
+        This asserted exit 0 and "No applicable obligations found", which is the
+        vacuous pass #1118 removes: a green exit on an empty ledger reads as
+        "PROOF9 gates passed" when nothing was checked. Exit 2 is distinct from
+        both pass (0) and failure (1); --allow-empty opts back into 0.
+        """
         _, workspace_path = ws
         result = runner.invoke(app, ["proof", "run", "-w", str(workspace_path), "--full"])
+        assert result.exit_code == 2, result.output
+        assert "Nothing was verified" in result.output
+
+    def test_run_no_requirements_with_allow_empty_exits_zero(self, ws):
+        _, workspace_path = ws
+        result = runner.invoke(app, [
+            "proof", "run", "-w", str(workspace_path), "--full", "--allow-empty",
+        ])
         assert result.exit_code == 0, result.output
-        assert "No applicable obligations found" in result.output
 
     def test_run_invalid_gate_exits_nonzero(self, ws):
         """run with an unrecognised --gate should exit non-zero and print error."""