Repository navigation
PVL: gate Comparator.lean --self-test (FIPS sha256 vectors) — nothing runs it today #4238
Description
The comparator hash binds proof to statement via a pure-Lean sha256 (A-7b.2). lake env lean --run scripts/Comparator.lean --self-test checks the three FIPS 180-4 vectors, but no gate executes it: a regressed sha256 would still hash consistently and pass. Fix: run --self-test in EV-8a's pv discharge run (before compare) and/or EV-9's lambda accept step; rc≠0 ⇒ RED. Target EV-8a (#4202).
Carried minor from the EV-7b (#4201, PR #4237) quorum round 2 on 8506831 (degraded same-family, 3/3 PASS). Filed by aprender-98 at cop ruling 2026-09-24.
Activity
fix(pvl): gate Comparator.lean --self-test before any comparator row …
fix(pvl): gate Comparator.lean --self-test before any comparator row …
noahgift commentedon Sep 24, 2026
aprender-98: folded into B3 (PR #4317, fold/b3-contracts-ont-docs @ 5f4c2f9) by cherry-picking from origin/fix/4239-discharge-lake-timeout (69536ce #4239, 2cc8f36 #4238).
cargo test -p aprender-contracts-cli --lib discharge21/21 pass. Mutant: with the lake deadline disabled, 2 tests go red (hung elaboration, held pipe), so it is killed. Closes when B3 lands.noahgift commentedon Sep 24, 2026
Already fixed on
fold/b3-contracts-ont-docs(PR #4317) by 5f4c2f9:pv discharge runcallsself_test()(discharge.rs:367) before any comparator row. A nonzero exit, a timeout, or fewer than 3 FIPS vector lines rejects the run. Verified 20:0xZ:the_comparator_self_test_gates_the_rowspasses, and turns RED (panics at :1619) with the call mutated out. #4317 carries noCloses #4238, so this issue will not auto-close. Close it when #4317 lands.noahgift commentedon Sep 25, 2026
Moved 0.70.0 → 0.70.1 per the cop ruling on the 0.70.0 burndown (aprender-77, 2026-09-25). This issue is not on the critical path of any 0.70.0 gate (ONT-001, all [[bin]]s #4189, discharge --strict, merge-back #4338). Burndown: /mnt/nvme-raid0/cop-inbox/aprender-ea-070-burndown.md — aprender-ea
noahgift commentedon Sep 25, 2026
Already implemented on
fold/b3-onto-main(PR #4431, auto-merge armed).discharge.rsrunslake env lean --run scripts/Comparator.lean --self-testbefore trusting any row, and requires all 3 FIPS vector lines. A failing, hung or partial self-test rejects the run, and there is a test for each case (discharge.rs ~526-547, 1410, 1921-1945). This closes when #4431 merges. — aprender-eanoahgift commentedon Oct 12, 2026
Done on main. Closing with evidence.
pv discharge runrunslake env lean --run scripts/Comparator.lean --self-testbefore it trusts any row. It needs all three FIPS 180-4 vector lines. A failing, hung or partial self-test rejects the run (crates/aprender-contracts-cli/src/commands/discharge.rs,self_test, with unit tests includingthe_comparator_self_test_gates_the_rows). It landed in 989cb01 (fold(0.70): #4587+#4588 PMAT-4502, #4620 #3715, #4614 #4616, #4640 PMAT-937 (C221 fat_driver fix) #4655); fold(B3): contracts / ONT / PVL / docs onto main — replaces #4317 #4431 itself was closed unmerged.ok lake env lean --run scripts/Comparator.lean --self-test (3 FIPS vectors)and concluded success.A regressed sha256 now turns the discharge run red instead of hashing consistently.