Skip to content

Commit 18ba057

Browse files
authored
fix(proof): close four PROOF9 evidence-integrity holes (#952) (#1080)
* fix(proof): close four evidence-integrity holes (#952) Waiver expiry: compared local-date isoformat with <=, so a waiver expiring today was already expired and spuriously blocked the #731 merge gate on its last valid day. Now UTC, compared as dates, and < — the expiry date is the last VALID day. run_id: str(uuid4())[:8] is 32 bits, so runs collide around 600 by the birthday bound and a passing run can absorb a failing run's artifacts. Both generation sites now use a shared _new_run_id() returning a full UUID. Checksums: computed and stored but never verified on read, so the integrity claim was unenforced. Added verify_evidence + EvidenceTamperError, called from check_obligation_satisfied so a tampered artifact cannot satisfy a gate. Per the issue's design note the digest binds run id, gate and canonical path — not bytes alone — so a genuinely passing artifact cannot be transplanted into another run. Verification also accepts the pre-#952 bytes-only digest so existing evidence does not all become 'tampered' at once; new writes are always bound, so that path drains. Stubs: title/description were interpolated raw. A newline escaped whatever line context held them and the next line landed as code; an apostrophe broke the E2E test('...') literal open. Now collapsed to one line with docstring delimiters neutralized, and the JS literal built with json.dumps. 30 tests, RED first: a waiver expiring today, two runs' evidence staying separable, a mutated/deleted/transplanted artifact, and a title carrying a quote and a newline through every gate's template (Python stubs must still ast.parse). * fix(proof): enforce checksum verification on the path that gates merges (#952) codex review P1, and correct: the first cut wired verify_evidence into check_obligation_satisfied, which has NO production callers. The #731 merge gate asks only for OPEN requirements, so a requirement already recorded SATISFIED kept that status after its artifact was edited or deleted, and the merge went through until someone happened to run a full proof again. Added evidence.list_blocking_requirements: OPEN requirements plus SATISFIED ones whose evidence fails verification. Both merge gates (API pr_v2 and CLI pr_commands) now use it instead of the raw status query, with a test asserting neither goes back. A SATISFIED requirement with no evidence rows deliberately does not block — that is a pre-existing state in older ledgers, not a tamper signal, and treating it as one would wedge every workspace that has it. 339 proof/PR tests pass. * fix(proof): judge the merge gate on the latest evidence per gate (#952) codex review P2, and a worse failure than the one it guards: blocking on any historical evidence row meant deleting last month's superseded artifacts — routine housekeeping — would wedge the merge gate permanently. list_blocking_requirements now takes the newest passing row per gate (list_evidence returns newest first) and verifies only those. Judged per gate, so a stale-but-intact UNIT artifact cannot mask a tampered SEC one. Three tests: cleanup of a superseded artifact does not block, tampering with the current one still does, and a tampered SEC artifact blocks even when UNIT is fine. * fix(proof): handle text ending at a docstring delimiter, and say why a req blocks (#952) CI review on #1080. A description ending in a single quote is not a """ run, so _inline did not touch it — and six templates butt {description} straight against their own closing delimiter. Four quotes in a row: Python closes the docstring on the first three and the fourth opens an unterminated literal, i.e. a SyntaxError in the generated stub, the exact failure AC4 exists to prevent. A trailing backslash escapes the delimiter's first quote for the same result. Both now get one separating space. Reproduced before fixing; 24 new parametrized cases across the six affected gates, for title as well as description. Also: both merge gates kept saying 'N open requirement(s) block this merge' after switching to list_blocking_requirements, which now also returns requirements recorded SATISFIED whose evidence fails verification — so a user blocked by a tampered artifact saw a status that did not match the ledger. Renamed the variable and reworded both messages to name either cause. * fix(proof): verify evidence on the public read paths too (#952) codex review, and AC3 says reads specifically. Verification reached the merge gate but not GET /api/v2/proof/requirements/{id}/evidence or /runs/{id}/evidence — both serialized satisfied straight from the ledger and served the artifact's CURRENT bytes beside it. Editing a file after a passing run therefore showed a pass in the UI next to forged text. EvidenceResponse gains verified + tamper_detail, computed per record in both endpoints. When a record fails verification its artifact_text is withheld rather than rendered: the bytes on disk are not the ones the record attests to, so showing them is the forgery. Reported per record rather than raised, so one bad artifact does not 404 a whole run's evidence list — pinned by a test where one gate is tampered and the other still reads clean. 6 new tests; tests/ -k 'proof or pr_v2 or pr_commands': 357 passed. * fix(proof): stop serving tampered evidence as a pass, and surface it in the UI (#952) codex review, and the sharpest finding of the set: adding verified:false beside an unchanged satisfied:true fixed nothing a user sees. Every existing client renders green from satisfied/status and knows nothing about the new fields, so tampered evidence still displayed as passing proof — just without its text. Backend: a record failing verification now serializes satisfied=false and status='unverifiable' — the existing vocabulary for 'this obligation could not be checked', which every client already renders as not-green — while verified/tamper_detail carry the precise reason for clients that look. So even an un-updated client can no longer show it as proof. Web UI: ProofEvidence gains verified/tamper_detail; GateEvidencePanel shows a distinct red 'tampered' badge (not the amber 'cannot verify', which means something else) and, when expanded, explains that the contents are withheld because the artifact no longer matches its checksum. Backend: 360 proof/PR tests pass. Web UI: 1103 tests pass, production build succeeds. The 25 pre-existing tsc errors are all in unrelated test files. * fix(proof): treat an unreadable artifact as tamper, not a crash (#952) codex review. FileNotFoundError is only one kind of OSError. An artifact replaced by a directory, or chmodded unreadable, still exists — read_bytes then raises IsADirectoryError/PermissionError, which escaped verify_evidence. That 500'd the evidence endpoints and took down the merge gate before it could block the specific requirement or honor an override. Catching OSError covers all three (FileNotFoundError is a subclass), and an artifact we cannot read is exactly an artifact we cannot verify. Three tests: directory-in-place-of-file, an unreadable file (skipped where the environment ignores mode), and the merge gate naming the requirement rather than raising. * fix(proof): escape backslashes in stub text instead of padding them (#952) CI caught what my local run did not: appending a space after a trailing backslash produced '\ ' inside a non-raw docstring — an invalid escape sequence, which this repo's pytest config escalates from SyntaxWarning to an error. My fix for an escaping bug introduced a different escaping bug. Padding a dangerous character is not escaping it. _inline now escapes every backslash ('\\' renders identically when the docstring is read), which also covers Windows paths and regexes anywhere in the text, not just at the delimiter boundary. The trailing-quote case keeps its separating space, which is safe. The tests were too weak to catch it: ast.parse succeeds on source that merely warns. They now assert under warnings.simplefilter('error') and cover 'C:\\path', 're: \\d+' and '\\n' as well as the boundary tails. Also records the lesson, including: run the CI invocation locally, not a single-file subset — warning behaviour differs. * fix(proof): apply stub escaping per context, exactly once (#952) CI review, and a precise catch: my backslash-doubling commit made _js_string run on _inline's already-doubled output, so json.dumps escaped those doubles again. A title of '\d+' reached the .ts source as four backslashes and read back as '\\d+'. The markdown templates had the same problem in reverse — they got Python-docstring escaping they have no use for. Split the escaping: _collapse is the context-neutral half (one line, no docstring-closing sequence), and each context applies its own escaper to that, once. Python templates get _inline (backslash-doubled, trailing quote padded), the E2E literal gets _js_string(raw), markdown gets _collapse. Tests assert round-trip fidelity rather than absence of a bad character: the E2E literal must json.loads back to exactly the original title, the Python docstring must ast.get_docstring back to exactly the original description, and markdown must contain the original verbatim. * fix(proof): E2E comments are not Python either (#952) CI review follow-up. The E2E template's {title}/{description} sit in '//' comments, but they were still getting _inline's backslash-doubling — which a JS comment shows verbatim. My own docstring said 'per context, applied once', and that was the one context still getting the wrong escaper. _MARKDOWN_GATES becomes _NON_PYTHON_GATES and includes E2E. Only the Python templates need doubling; {title_js} stays on _js_string, being the one field that really is a string literal.
1 parent 6663367 commit 18ba057

12 files changed

Lines changed: 1291 additions & 59 deletions

File tree

codeframe/cli/pr_commands.py

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -432,8 +432,6 @@ def _check_merge_gate(
432432
override is pending so the caller can persist the audit record after the
433433
merge actually succeeds, or None when nothing was bypassed.
434434
"""
435-
from codeframe.core.proof import ledger as proof_ledger
436-
from codeframe.core.proof.models import ReqStatus
437435
from codeframe.core.workspace import find_workspace_root, get_workspace
438436

439437
reason = (override_reason or "").strip()
@@ -455,27 +453,35 @@ def _check_merge_gate(
455453
return None
456454

457455
try:
458-
open_reqs = proof_ledger.list_requirements(workspace, status=ReqStatus.OPEN)
456+
# Blocking, not merely open: a requirement recorded SATISFIED whose
457+
# evidence no longer verifies must stop the merge too (#952).
458+
from codeframe.core.proof.evidence import list_blocking_requirements
459+
460+
blocking_reqs = list_blocking_requirements(workspace)
459461
except Exception as e:
460462
# Fail closed, like the API path: a broken ledger blocks the merge.
461463
console.print(f"[red]PROOF9 gate check failed:[/red] {e} — merge blocked")
462464
raise typer.Exit(1)
463-
if not open_reqs:
465+
if not blocking_reqs:
464466
return None
465467

466468
if not override:
467469
console.print(
468-
f"[red]PROOF9 merge gate:[/red] {len(open_reqs)} open requirement(s) block this merge:"
470+
f"[red]PROOF9 merge gate:[/red] {len(blocking_reqs)} requirement(s) block this merge:"
469471
)
470-
for r in open_reqs[:10]:
472+
for r in blocking_reqs[:10]:
471473
console.print(f" - {r.id}: {r.title}")
472-
console.print('Satisfy or waive them, or pass --override --reason "...".')
474+
console.print(
475+
"Each is either unproven, or recorded satisfied with evidence that "
476+
"no longer matches its checksum."
477+
)
478+
console.print('Satisfy, waive or re-prove them, or pass --override --reason "...".')
473479
raise typer.Exit(1)
474480

475481
console.print(
476-
f"[yellow]PROOF9 merge gate overridden[/yellow] ({len(open_reqs)} open requirement(s) bypassed — audited)"
482+
f"[yellow]PROOF9 merge gate overridden[/yellow] ({len(blocking_reqs)} requirement(s) bypassed — audited)"
477483
)
478-
return workspace, [{"id": r.id, "title": r.title} for r in open_reqs]
484+
return workspace, [{"id": r.id, "title": r.title} for r in blocking_reqs]
479485

480486

481487
@pr_app.command("merge")

codeframe/core/proof/evidence.py

Lines changed: 147 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,16 +5,32 @@
55
"""
66

77
import hashlib
8+
import logging
89
from datetime import datetime, timezone
910
from pathlib import Path
1011

1112
from codeframe.core.proof import ledger
1213
from codeframe.core.proof.models import Evidence, Gate, GateOutcome, Requirement
1314
from codeframe.core.workspace import Workspace
1415

16+
logger = logging.getLogger(__name__)
17+
18+
19+
class EvidenceTamperError(Exception):
20+
"""A stored artifact no longer matches the checksum recorded with it.
21+
22+
A hard state, never a warning: the whole point of the ledger is that a
23+
recorded pass is attributable. Raised on a mutated artifact, a missing one,
24+
and on one transplanted from a different run or gate.
25+
"""
26+
1527

1628
def _sha256(file_path: str) -> str:
17-
"""Compute SHA-256 checksum of a file. Raises if file missing."""
29+
"""Compute SHA-256 checksum of a file's bytes. Raises if file missing.
30+
31+
The pre-#952 digest. Kept because evidence written before that change is
32+
stored in this form — see ``verify_evidence``.
33+
"""
1834
path = Path(file_path)
1935
if not path.exists():
2036
raise FileNotFoundError(f"Artifact not found: {file_path}")
@@ -23,6 +39,70 @@ def _sha256(file_path: str) -> str:
2339
return h.hexdigest()
2440

2541

42+
def _bound_digest(run_id: str, gate: Gate, artifact_path: str) -> str:
43+
"""Checksum binding the artifact's bytes to *where it came from* (#952).
44+
45+
Hashing bytes alone proves only that a file is unmodified — it says nothing
46+
about which run produced it, so a genuinely passing artifact could be
47+
transplanted into another run's evidence and still verify. The digest
48+
therefore covers a canonical header (run id, gate, resolved path) as well
49+
as the content.
50+
51+
The header is length-prefixed so no two different tuples can produce the
52+
same byte stream (``run="a|b", gate="c"`` vs ``run="a", gate="b|c"``).
53+
"""
54+
path = Path(artifact_path)
55+
if not path.exists():
56+
raise FileNotFoundError(f"Artifact not found: {artifact_path}")
57+
h = hashlib.sha256()
58+
for part in ("codeframe-proof-evidence-v1", run_id, gate.value, str(path.resolve())):
59+
raw = part.encode("utf-8")
60+
h.update(len(raw).to_bytes(4, "big"))
61+
h.update(raw)
62+
h.update(path.read_bytes())
63+
return h.hexdigest()
64+
65+
66+
def verify_evidence(evidence: Evidence) -> None:
67+
"""Re-derive an artifact's checksum and raise if it does not match.
68+
69+
Checksums were computed and stored but never checked on read, so the
70+
integrity claim was unenforced (#952). This is the check.
71+
72+
Accepts the legacy bytes-only digest as well as the bound one, so evidence
73+
recorded before #952 does not all become 'tampered' at once. Legacy rows
74+
still detect modification of the artifact; they just cannot detect a
75+
transplant. New evidence is always written in the bound form, so the
76+
legacy path drains as runs happen.
77+
"""
78+
try:
79+
if _bound_digest(evidence.run_id, evidence.gate, evidence.artifact_path) == evidence.artifact_checksum:
80+
return
81+
if _sha256(evidence.artifact_path) == evidence.artifact_checksum:
82+
logger.debug(
83+
"Evidence for %s/%s verified via the pre-#952 bytes-only digest",
84+
evidence.req_id, evidence.gate.value,
85+
)
86+
return
87+
# OSError, not just FileNotFoundError: an artifact replaced by a directory
88+
# or made unreadable still exists, so read_bytes raises IsADirectoryError /
89+
# PermissionError instead. Those escaped, 500ing the evidence endpoints and
90+
# taking down the merge gate before it could block the specific requirement
91+
# or honor an override (codex review on #1080). An artifact we cannot read
92+
# is an artifact we cannot verify, which is the tamper state.
93+
except OSError as exc:
94+
raise EvidenceTamperError(
95+
f"Evidence artifact for {evidence.req_id}/{evidence.gate.value} "
96+
f"cannot be read: {evidence.artifact_path} ({exc.__class__.__name__})"
97+
) from exc
98+
99+
raise EvidenceTamperError(
100+
f"Evidence artifact for {evidence.req_id}/{evidence.gate.value} does not "
101+
f"match its recorded checksum: {evidence.artifact_path} "
102+
f"(run {evidence.run_id})"
103+
)
104+
105+
26106
def attach_evidence(
27107
workspace: Workspace,
28108
req_id: str,
@@ -41,7 +121,7 @@ def attach_evidence(
41121
gate=gate,
42122
satisfied=(outcome == GateOutcome.PASSED),
43123
artifact_path=artifact_path,
44-
artifact_checksum=_sha256(artifact_path),
124+
artifact_checksum=_bound_digest(run_id, gate, artifact_path),
45125
timestamp=datetime.now(timezone.utc),
46126
run_id=run_id,
47127
status=outcome.value,
@@ -53,9 +133,71 @@ def attach_evidence(
53133
def check_obligation_satisfied(
54134
workspace: Workspace, req: Requirement, gate: Gate
55135
) -> bool:
56-
"""Check if a gate obligation has passing evidence."""
136+
"""Check if a gate obligation has passing evidence.
137+
138+
Evidence whose artifact no longer matches its checksum does not count. The
139+
verification has to happen here, before a gate accepts the artifact, or the
140+
stored checksum buys nothing (#952). A tampered record is skipped and
141+
logged rather than raised: one corrupted artifact must not take down the
142+
whole proof run, and the obligation correctly reports unsatisfied.
143+
"""
57144
evidence_list = ledger.list_evidence(workspace, req.id)
58145
for ev in evidence_list:
59-
if ev.gate == gate and ev.satisfied:
60-
return True
146+
if ev.gate != gate or not ev.satisfied:
147+
continue
148+
try:
149+
verify_evidence(ev)
150+
except EvidenceTamperError as exc:
151+
logger.warning("Rejecting evidence for %s: %s", req.id, exc)
152+
continue
153+
return True
61154
return False
155+
156+
157+
def list_blocking_requirements(workspace: Workspace) -> list[Requirement]:
158+
"""Requirements that must stop a merge (#731 gate, #952 verification).
159+
160+
Two reasons a requirement blocks:
161+
162+
* It is still OPEN — never proven.
163+
* It is recorded SATISFIED but its evidence no longer verifies. Checksum
164+
verification is worthless if the only path that runs it is a fresh proof
165+
run: a requirement marked satisfied yesterday keeps that status forever,
166+
so editing its artifact afterwards left the merge gate waving the change
167+
through (codex review on #952).
168+
169+
Only the **latest** passing evidence per gate is checked, not every row
170+
ever recorded. Runs accumulate evidence, and deleting last month's
171+
artifacts is routine housekeeping — blocking on any historical row would
172+
make that cleanup wedge the gate permanently, which is a worse failure than
173+
the hole this closes (codex review). Each gate is judged separately, so a
174+
stale-but-intact UNIT artifact cannot mask a tampered SEC one.
175+
176+
A SATISFIED requirement with *no* evidence rows does not block. That is a
177+
pre-existing state in older ledgers, not a tamper signal, and treating it
178+
as one would wedge every workspace that has it. Only evidence that is
179+
present and fails to verify counts.
180+
"""
181+
from codeframe.core.proof.models import ReqStatus
182+
183+
blocking = list(ledger.list_requirements(workspace, status=ReqStatus.OPEN))
184+
185+
for req in ledger.list_requirements(workspace, status=ReqStatus.SATISFIED):
186+
# list_evidence returns newest first, so the first passing row for a
187+
# gate is that gate's current proof.
188+
latest: dict[Gate, Evidence] = {}
189+
for ev in ledger.list_evidence(workspace, req.id):
190+
if ev.satisfied:
191+
latest.setdefault(ev.gate, ev)
192+
193+
for ev in latest.values():
194+
try:
195+
verify_evidence(ev)
196+
except EvidenceTamperError as exc:
197+
logger.warning(
198+
"Requirement %s blocks the merge gate: %s", req.id, exc
199+
)
200+
blocking.append(req)
201+
break
202+
203+
return blocking

codeframe/core/proof/ledger.py

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -703,7 +703,9 @@ def get_run_evidence(workspace: Workspace, run_id: str) -> list[Evidence]:
703703
def check_expired_waivers(workspace: Workspace) -> list[Requirement]:
704704
"""Find and revert expired waivers to open status."""
705705
_ensure_tables(workspace)
706-
today = date.today().isoformat()
706+
# UTC, not the machine's local date: the ledger's timestamps are UTC, so a
707+
# local date makes expiry depend on the operator's timezone (#952).
708+
today = datetime.now(timezone.utc).date()
707709
conn = get_db_connection(workspace)
708710
cursor = conn.cursor()
709711

@@ -720,7 +722,12 @@ def check_expired_waivers(workspace: Workspace) -> list[Requirement]:
720722

721723
for row in rows:
722724
req = _row_to_requirement(row)
723-
if req.waiver and req.waiver.expires and req.waiver.expires.isoformat() <= today:
725+
# `<` not `<=`: the expiry date is the waiver's LAST VALID day, so a
726+
# waiver expiring today must survive today. `<=` expired it a day early
727+
# and spuriously blocked the #731 merge gate (#952). Compared as dates,
728+
# not isoformat strings, so the comparison cannot silently go
729+
# lexicographic on a malformed value.
730+
if req.waiver and req.waiver.expires and req.waiver.expires < today:
724731
cursor.execute(
725732
"UPDATE proof_requirements SET status = 'open', waiver = NULL WHERE id = ?",
726733
(req.id,),

codeframe/core/proof/runner.py

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,19 @@
2727
logger = logging.getLogger(__name__)
2828

2929

30+
def _new_run_id() -> str:
31+
"""A fresh proof-run identifier.
32+
33+
A full UUID, never a truncated one. ``str(uuid4())[:8]`` gives 32 bits, so
34+
two runs in a workspace collide around 600 runs by the birthday bound — and
35+
a collision merges evidence across runs, letting a passing run absorb a
36+
failing run's artifacts (#952). Callers that need the id before the run
37+
starts (the v2 router, so its response matches the evidence rows) use this
38+
too, so there is one definition.
39+
"""
40+
return str(uuid.uuid4())
41+
42+
3043
def _load_proof_config(workspace: Workspace) -> tuple[Optional[set[Gate]], str]:
3144
"""Load (enabled_gates, strictness) from .codeframe/proof_config.json.
3245
@@ -270,7 +283,7 @@ def run_proof(
270283
Dict mapping req_id → list of (Gate, GateOutcome) tuples
271284
"""
272285
if not run_id:
273-
run_id = str(uuid.uuid4())[:8]
286+
run_id = _new_run_id()
274287

275288
started_at = datetime.now(timezone.utc)
276289

0 commit comments

Comments
 (0)