diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index c922eec..d9c4152 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,5 +1,5 @@ e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c AUDIT-MANIFEST.txt -9118c39009196247655c3517626bba5447a59cf16484b1bb296ef6bc143fab13 check.sh +91ab3fce14a03fc6fd12b3cdbb52cd0f0e379ae2cd564ec7b61d339d4616fd32 check.sh 070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885 fidelity/lean_defs.py 5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2 fidelity/run_fidelity.py 503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf gen/LTLAcc/HashExternal.lean diff --git a/verification/check.sh b/verification/check.sh index 9abd3ee..f52784c 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -117,6 +117,24 @@ for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do fi done echo " all sources valid" + +# ── Phase 0a: build hygiene ───────────────────────────────────────────────── +# P0-a was applied to the four ed25519 repositories on 2026-07-30 and never +# here — found on 2026-07-31 by the control repo's capability matrix, which +# asks the property rather than looking for a phase by name. +# +# The finding that made it matter there applies verbatim: a verification that +# never cleans up cannot distinguish "these proofs check" from "these proofs +# check GIVEN WHATEVER IS LYING AROUND". Compiled artifacts are gitignored, so +# no `git status` can show a reader that a verdict rested on an object from an +# earlier run of a different script. Purge, and compile from source. +# +# This repository has no --audit-only mode, so there is no case in which the +# artifacts must be kept: the purge is unconditional. +echo "=== Phase 0a: build hygiene ===" +find "$HERE" -name '*.olean' -delete 2>/dev/null || true +find "$HERE" -name '*.ilean' -delete 2>/dev/null || true +echo " purged every compiled artifact — this run compiles from source" # Recursive: no compiled artifact anywhere in the tree may lack its source # (review round 2, GPT M1 — previously scanned Proofs/*.olean only). while IFS= read -r -d '' o; do