From 2f182afd64016936b82f88bea3a001a67538613e Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 28 Jul 2026 17:31:54 +0200 Subject: [PATCH] check.sh: delete the compiled audit artifact, not just its source MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase 3 and 3b mktemp an audit file, compile it, then removed only the .lean — leaving the .olean behind on every run. check-scalar.sh:38 has always done this correctly (`rm -f "$AUD" "${AUD%.lean}.olean"`); the main script was the odd one out. Estate-wide that had accumulated 101 orphan compiled modules with no sibling source (dalek 44, anza/risc0/betrusted 19 each), invisible to git because *.olean is gitignored. All swept. The litter was inert — the names are not valid Lean identifiers, so nothing could import them. It matters as a pattern: an audit whose verdict can depend on untracked build state is the class of defect that took eight review rounds to close in the sibling SLH-DSA repository (there: an orphan .olean with its source deleted satisfied an import and the button went green). A build-hygiene phase that purges compiled artifacts and bans stray files is the proper fix and is queued as part of the protocol port; this commit stops the bleeding. Co-Authored-By: Claude Opus 4.8 --- verification/check.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/verification/check.sh b/verification/check.sh index 2ebeaec..bd02889 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -197,7 +197,7 @@ lake env bash -c " } > \"\$AUD\" OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) echo \"\$OUT\" - rm -f \"\$AUD\" + rm -f \"\$AUD\" \"\${AUD%.lean}.olean\" N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true) if [ \"\$N_CLEAN\" -ne ${#CERTS[@]} ]; then echo \"AXIOM AUDIT FAILED: \$N_CLEAN/${#CERTS[@]} certificates clean\" @@ -220,7 +220,7 @@ lake env bash -c " { echo 'import Proofs.SigApexSpec'; echo 'import Proofs.PointLiftSpec'; echo 'import Proofs.PointEqSpec'; echo 'import Proofs.DecompressMain'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point_eq'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_decompress'; } > \"\$AUD\" OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) echo \"\$OUT\" - rm -f \"\$AUD\" + rm -f \"\$AUD\" \"\${AUD%.lean}.olean\" FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ') if echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff' depends on axioms: \$ALLOWED\" \ && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ALLOWED\" \