Skip to content

Commit 8a98e63

Browse files
authored
fix(proof): explicit UNVERIFIABLE state for gates without runners (#728) (#801)
* fix(proof): explicit UNVERIFIABLE state for gates without runners (#728) The 6 PROOF9 gates with no automated runner (e2e, visual, a11y, perf, demo, manual) previously collapsed to hard FAIL, so most captured glitches could never be SATISFIED and every run failed perpetually. - core: new GateOutcome enum (passed/failed/unverifiable); _run_gate returns the tri-state and its stale docstring is corrected; run_proof maps obligations three-way, keeps requirements OPEN (waivable) on unverifiable, and excludes unverifiable from overall_passed - evidence/ledger: Evidence.status persists the outcome; nullable status column added with a PRAGMA-guarded ALTER TABLE migration so legacy DBs keep working (old rows read back status=None) - api: run results carry {gate, satisfied, status}; EvidenceResponse gains optional status; passed aggregation mirrors the runner rule - cli: yellow UNVERIFIABLE cell, waive hint, exit 0 when nothing failed - tui: distinct ❓ icon for unverifiable obligations - web-ui: 'unverifiable' GateRunStatus + amber badge/banner/pills on /proof and /proof/[req_id] (incl. evidence history filter + sort); gate.run.failed notifications no longer fire for unverifiable gates * fix(web-ui): tidy Gate Results help copy on /proof * fix(proof): harden evidence-status migration + review polish - ledger: try/finally around the migration connection, tolerate the concurrent-first-run duplicate-column race, and memoize per workspace so the PRAGMA doesn't run on every DB access (CodeRabbit + claude-review) - web-ui: compute evidenceResult once per row; give the unverifiable badge distinct styling from in-progress so live runs visibly flip
1 parent 62586b4 commit 8a98e63

25 files changed

Lines changed: 871 additions & 91 deletions

codeframe/cli/proof_commands.py

Lines changed: 37 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ def run(
144144
codeframe proof run --gate unit
145145
"""
146146
from codeframe.core.workspace import get_workspace
147-
from codeframe.core.proof.models import Gate
147+
from codeframe.core.proof.models import Gate, GateOutcome
148148
from codeframe.core.proof.runner import run_proof
149149

150150
workspace_path = repo_path or Path.cwd()
@@ -178,21 +178,41 @@ def run(
178178
table.add_column("Gate", style="blue")
179179
table.add_column("Result", style="bold")
180180

181-
all_pass = True
181+
_CELL = {
182+
GateOutcome.PASSED: "[green]PASS[/green]",
183+
GateOutcome.FAILED: "[red]FAIL[/red]",
184+
GateOutcome.UNVERIFIABLE: "[yellow]UNVERIFIABLE[/yellow]",
185+
}
186+
any_failed = False
187+
unverifiable_gates: set[str] = set()
182188
for req_id, gate_results in results.items():
183-
for g, passed in gate_results:
184-
status = "[green]PASS[/green]" if passed else "[red]FAIL[/red]"
185-
if not passed:
186-
all_pass = False
187-
table.add_row(req_id, g.value, status)
189+
for g, outcome in gate_results:
190+
if outcome == GateOutcome.FAILED:
191+
any_failed = True
192+
elif outcome == GateOutcome.UNVERIFIABLE:
193+
unverifiable_gates.add(g.value)
194+
table.add_row(req_id, g.value, _CELL[outcome])
188195

189196
console.print(table)
190197

191-
if all_pass:
192-
console.print("\n[green]All obligations satisfied.[/green]")
193-
else:
198+
if unverifiable_gates:
199+
gates = ", ".join(sorted(unverifiable_gates))
200+
console.print(
201+
f"\n[yellow]Could not verify {len(unverifiable_gates)} gate(s):[/yellow] "
202+
f"{gates} — no automated runner. "
203+
"Waive with 'cf proof waive <REQ> --reason \"...\"'."
204+
)
205+
206+
if any_failed:
194207
console.print("\n[red]Some obligations failed.[/red] Fix issues and re-run.")
195208
raise typer.Exit(1)
209+
elif unverifiable_gates:
210+
console.print(
211+
"\n[green]No obligations failed[/green] "
212+
"[dim](some gates could not be verified).[/dim]"
213+
)
214+
else:
215+
console.print("\n[green]All obligations satisfied.[/green]")
196216

197217

198218
@proof_app.command("list")
@@ -319,7 +339,13 @@ def show(
319339
if evidence_list:
320340
console.print(f"\n[bold]Evidence ({len(evidence_list)}):[/bold]")
321341
for ev in evidence_list[:10]:
322-
status = "[green]PASS[/green]" if ev.satisfied else "[red]FAIL[/red]"
342+
if ev.status == "unverifiable":
343+
status = "[yellow]UNVERIFIABLE[/yellow]"
344+
elif ev.satisfied:
345+
status = "[green]PASS[/green]"
346+
else:
347+
# Legacy rows (status=None) fall back to the satisfied bool.
348+
status = "[red]FAIL[/red]"
323349
console.print(f" {ev.gate.value} {status}{ev.artifact_path}")
324350

325351

codeframe/core/proof/evidence.py

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
from pathlib import Path
1010

1111
from codeframe.core.proof import ledger
12-
from codeframe.core.proof.models import Evidence, Gate, Requirement
12+
from codeframe.core.proof.models import Evidence, Gate, GateOutcome, Requirement
1313
from codeframe.core.workspace import Workspace
1414

1515

@@ -28,18 +28,23 @@ def attach_evidence(
2828
req_id: str,
2929
gate: Gate,
3030
artifact_path: str,
31-
satisfied: bool,
31+
outcome: GateOutcome,
3232
run_id: str,
3333
) -> Evidence:
34-
"""Create and persist an evidence record with artifact checksum."""
34+
"""Create and persist an evidence record with artifact checksum.
35+
36+
`satisfied` is True only when the gate PASSED; UNVERIFIABLE and FAILED both
37+
record satisfied=False. The tri-state `outcome` is preserved in `status`.
38+
"""
3539
evidence = Evidence(
3640
req_id=req_id,
3741
gate=gate,
38-
satisfied=satisfied,
42+
satisfied=(outcome == GateOutcome.PASSED),
3943
artifact_path=artifact_path,
4044
artifact_checksum=_sha256(artifact_path),
4145
timestamp=datetime.now(timezone.utc),
4246
run_id=run_id,
47+
status=outcome.value,
4348
)
4449
ledger.save_evidence(workspace, evidence)
4550
return evidence

codeframe/core/proof/ledger.py

Lines changed: 41 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
"""
66

77
import json
8+
import sqlite3
89
from datetime import date, datetime, timezone
910
from typing import Optional
1011

@@ -67,6 +68,7 @@ def init_proof_tables(workspace: Workspace) -> None:
6768
timestamp TEXT NOT NULL,
6869
run_id TEXT NOT NULL,
6970
workspace_id TEXT NOT NULL,
71+
status TEXT,
7072
FOREIGN KEY (req_id) REFERENCES proof_requirements(id)
7173
)
7274
""")
@@ -121,6 +123,38 @@ def _ensure_tables(workspace: Workspace) -> None:
121123
conn.close()
122124
if missing:
123125
init_proof_tables(workspace)
126+
_migrate_evidence_status_column(workspace)
127+
128+
129+
# Workspaces already checked for the #728 status column this process —
130+
# skips the per-call PRAGMA once the migration is known to have run.
131+
_status_migrated_workspaces: set[str] = set()
132+
133+
134+
def _migrate_evidence_status_column(workspace: Workspace) -> None:
135+
"""Add proof_evidence.status to pre-existing DBs that predate #728.
136+
137+
The column is nullable; old rows read back status=None. No-op once present.
138+
"""
139+
if workspace.id in _status_migrated_workspaces:
140+
return
141+
conn = get_db_connection(workspace)
142+
try:
143+
cursor = conn.cursor()
144+
cursor.execute("PRAGMA table_info(proof_evidence)")
145+
columns = {row[1] for row in cursor.fetchall()}
146+
if columns and "status" not in columns:
147+
try:
148+
cursor.execute("ALTER TABLE proof_evidence ADD COLUMN status TEXT")
149+
conn.commit()
150+
except sqlite3.OperationalError as exc:
151+
# Concurrent first-run: another worker added the column
152+
# between our check and the ALTER.
153+
if "duplicate column" not in str(exc).lower():
154+
raise
155+
_status_migrated_workspaces.add(workspace.id)
156+
finally:
157+
conn.close()
124158

125159

126160
# --- Serialization helpers ---
@@ -315,12 +349,13 @@ def save_evidence(workspace: Workspace, evidence: Evidence) -> None:
315349
cursor.execute(
316350
"""INSERT INTO proof_evidence
317351
(req_id, gate, satisfied, artifact_path, artifact_checksum,
318-
timestamp, run_id, workspace_id)
319-
VALUES (?, ?, ?, ?, ?, ?, ?, ?)""",
352+
timestamp, run_id, workspace_id, status)
353+
VALUES (?, ?, ?, ?, ?, ?, ?, ?, ?)""",
320354
(
321355
evidence.req_id, evidence.gate.value, int(evidence.satisfied),
322356
evidence.artifact_path, evidence.artifact_checksum,
323357
evidence.timestamp.isoformat(), evidence.run_id, workspace.id,
358+
evidence.status,
324359
),
325360
)
326361
conn.commit()
@@ -334,7 +369,7 @@ def list_evidence(workspace: Workspace, req_id: str) -> list[Evidence]:
334369
cursor = conn.cursor()
335370
cursor.execute(
336371
"""SELECT req_id, gate, satisfied, artifact_path, artifact_checksum,
337-
timestamp, run_id
372+
timestamp, run_id, status
338373
FROM proof_evidence WHERE req_id = ? AND workspace_id = ?
339374
ORDER BY timestamp DESC""",
340375
(req_id, workspace.id),
@@ -346,6 +381,7 @@ def list_evidence(workspace: Workspace, req_id: str) -> list[Evidence]:
346381
req_id=r[0], gate=Gate(r[1]), satisfied=bool(r[2]),
347382
artifact_path=r[3], artifact_checksum=r[4],
348383
timestamp=datetime.fromisoformat(r[5]), run_id=r[6],
384+
status=r[7],
349385
)
350386
for r in rows
351387
]
@@ -460,7 +496,7 @@ def get_run_evidence(workspace: Workspace, run_id: str) -> list[Evidence]:
460496
cursor = conn.cursor()
461497
cursor.execute(
462498
"""SELECT req_id, gate, satisfied, artifact_path, artifact_checksum,
463-
timestamp, run_id
499+
timestamp, run_id, status
464500
FROM proof_evidence WHERE run_id = ? AND workspace_id = ?
465501
ORDER BY timestamp ASC""",
466502
(run_id, workspace.id),
@@ -472,6 +508,7 @@ def get_run_evidence(workspace: Workspace, run_id: str) -> list[Evidence]:
472508
req_id=r[0], gate=Gate(r[1]), satisfied=bool(r[2]),
473509
artifact_path=r[3], artifact_checksum=r[4],
474510
timestamp=datetime.fromisoformat(r[5]), run_id=r[6],
511+
status=r[7],
475512
)
476513
for r in rows
477514
]

codeframe/core/proof/models.py

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,19 @@ class Gate(str, Enum):
3333
PROOF9_GATE_ORDER: tuple[str, ...] = tuple(g.value for g in Gate)
3434

3535

36+
class GateOutcome(str, Enum):
37+
"""Outcome of running a single proof obligation's gate.
38+
39+
UNVERIFIABLE is distinct from FAILED: the gate has no automated runner
40+
(e.g. e2e, visual, a11y, perf, demo, manual), so the obligation could not
41+
be checked at all. It never satisfies a requirement and never fails a run.
42+
"""
43+
44+
PASSED = "passed"
45+
FAILED = "failed"
46+
UNVERIFIABLE = "unverifiable"
47+
48+
3649
class GlitchType(str, Enum):
3750
"""Classification of the glitch that produced a requirement."""
3851

@@ -88,7 +101,7 @@ class Obligation:
88101
"""A single proof obligation attached to a requirement."""
89102

90103
gate: Gate
91-
status: str = "pending" # pending, satisfied, failed
104+
status: str = "pending" # pending, satisfied, failed, unverifiable
92105

93106

94107
@dataclass
@@ -121,6 +134,7 @@ class Evidence:
121134
artifact_checksum: str
122135
timestamp: datetime
123136
run_id: str
137+
status: Optional[str] = None # passed, failed, unverifiable (None for legacy rows)
124138

125139

126140
@dataclass

codeframe/core/proof/runner.py

Lines changed: 42 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
from codeframe.core.proof.models import (
1717
PROOF_CONFIG_FILENAME,
1818
Gate,
19+
GateOutcome,
1920
ProofRun,
2021
ReqStatus,
2122
)
@@ -71,27 +72,39 @@ def _load_proof_config(workspace: Workspace) -> tuple[Optional[set[Gate]], str]:
7172
Gate.SEC: "ruff",
7273
}
7374

75+
# Map a gate outcome to the persisted obligation status string.
76+
_OUTCOME_TO_OBLIGATION_STATUS: dict[GateOutcome, str] = {
77+
GateOutcome.PASSED: "satisfied",
78+
GateOutcome.FAILED: "failed",
79+
GateOutcome.UNVERIFIABLE: "unverifiable",
80+
}
81+
7482

75-
def _run_gate(workspace: Workspace, gate: Gate) -> tuple[bool, str]:
76-
"""Execute a single gate and return (passed, output).
83+
def _run_gate(workspace: Workspace, gate: Gate) -> tuple[GateOutcome, str]:
84+
"""Execute a single gate and return (outcome, output).
7785
78-
Uses core/gates.py for gates that have direct tool support.
79-
Returns (True, "") for gates without automated tooling yet.
86+
Uses core/gates.py for gates that have direct tool support. Gates without
87+
an automated runner return UNVERIFIABLE — the obligation could not be
88+
checked, which is distinct from running and failing.
8089
"""
8190
core_gate_name = _GATE_TO_CORE.get(gate)
8291
if not core_gate_name:
83-
return False, f"Gate {gate.value} has no automated runner — cannot verify"
92+
return (
93+
GateOutcome.UNVERIFIABLE,
94+
f"Gate {gate.value} has no automated runner — cannot verify",
95+
)
8496

8597
try:
8698
from codeframe.core.gates import run as run_gates
8799
result = run_gates(workspace, gates=[core_gate_name], verbose=False)
88100
output_parts = [
89101
f"{check.name}: {check.status.value}" for check in result.checks
90102
]
91-
return result.passed, "\n".join(output_parts)
103+
outcome = GateOutcome.PASSED if result.passed else GateOutcome.FAILED
104+
return outcome, "\n".join(output_parts)
92105
except Exception as exc:
93106
logger.warning("Gate %s failed to run: %s", gate.value, exc)
94-
return False, str(exc)
107+
return GateOutcome.FAILED, str(exc)
95108

96109

97110
def run_proof(
@@ -100,7 +113,7 @@ def run_proof(
100113
full: bool = False,
101114
gate_filter: Optional[Gate] = None,
102115
run_id: Optional[str] = None,
103-
) -> dict[str, list[tuple[Gate, bool]]]:
116+
) -> dict[str, list[tuple[Gate, GateOutcome]]]:
104117
"""Execute proof obligations and collect evidence.
105118
106119
Args:
@@ -110,7 +123,7 @@ def run_proof(
110123
run_id: Unique run identifier (auto-generated if not provided)
111124
112125
Returns:
113-
Dict mapping req_id → list of (Gate, satisfied) tuples
126+
Dict mapping req_id → list of (Gate, GateOutcome) tuples
114127
"""
115128
if not run_id:
116129
run_id = str(uuid.uuid4())[:8]
@@ -157,7 +170,7 @@ def run_proof(
157170
if not full:
158171
changed_scope = get_changed_scope(workspace)
159172

160-
results: dict[str, list[tuple[Gate, bool]]] = {}
173+
results: dict[str, list[tuple[Gate, GateOutcome]]] = {}
161174
artifact_dir = workspace.state_dir / "proof_artifacts"
162175
artifact_dir.mkdir(exist_ok=True)
163176

@@ -168,7 +181,7 @@ def run_proof(
168181
if not intersects(req.scope, changed_scope):
169182
continue
170183

171-
req_results: list[tuple[Gate, bool]] = []
184+
req_results: list[tuple[Gate, GateOutcome]] = []
172185

173186
for obl in req.obligations:
174187
# Apply gate filter
@@ -180,7 +193,7 @@ def run_proof(
180193
continue
181194

182195
# Run the gate
183-
passed, output = _run_gate(workspace, obl.gate)
196+
outcome, output = _run_gate(workspace, obl.gate)
184197

185198
# Write artifact
186199
artifact_path = artifact_dir / f"{req.id}_{obl.gate.value}_{run_id}.txt"
@@ -189,25 +202,35 @@ def run_proof(
189202
# Attach evidence
190203
attach_evidence(
191204
workspace, req.id, obl.gate,
192-
str(artifact_path), passed, run_id,
205+
str(artifact_path), outcome, run_id,
193206
)
194207

195208
# Update obligation status
196-
obl.status = "satisfied" if passed else "failed"
197-
req_results.append((obl.gate, passed))
209+
obl.status = _OUTCOME_TO_OBLIGATION_STATUS[outcome]
210+
req_results.append((obl.gate, outcome))
198211

199212
if req_results:
200213
results[req.id] = req_results
201214

202-
# Always persist obligation status updates
203-
all_satisfied = all(passed for _, passed in req_results)
204-
if all_satisfied and len(req_results) == len(req.obligations):
215+
# Always persist obligation status updates. A requirement is only
216+
# SATISFIED when every obligation PASSED and all obligations ran —
217+
# an unverifiable obligation leaves it OPEN (and waivable).
218+
all_passed = all(o == GateOutcome.PASSED for _, o in req_results)
219+
if all_passed and len(req_results) == len(req.obligations):
205220
req.status = ReqStatus.SATISFIED
206221
ledger.save_requirement(workspace, req)
207222

208223
completed_at = datetime.now(timezone.utc)
209224
duration_ms = int((completed_at - started_at).total_seconds() * 1000)
210-
executed = [passed for gate_results in results.values() for _, passed in gate_results]
225+
# Only gates that actually ran (passed or failed) count toward the tally;
226+
# unverifiable gates neither pass nor fail, so a run with only unverifiable
227+
# outcomes passes.
228+
executed = [
229+
outcome == GateOutcome.PASSED
230+
for gate_results in results.values()
231+
for _, outcome in gate_results
232+
if outcome != GateOutcome.UNVERIFIABLE
233+
]
211234
all_passed = all(executed) if executed else True
212235
if not all_passed and strictness == "warn":
213236
logger.warning(

0 commit comments

Comments
 (0)