From bb21b8ab0feb9823d8914cc5f7003cc65d4898f1 Mon Sep 17 00:00:00 2001 From: saymrwulf Date: Fri, 3 Jul 2026 12:54:49 +0200 Subject: [PATCH] coherence pass 2: institutionalize the kernel axiom audit check.sh gains Phase 3: P_prime, sub_spec, INV_spec must each report exactly [propext, Classical.choice, Quot.sound], via lean-guard, audit file inside the workspace. Previously the audits had been run live (pass 1) but no shipped button enforced them. Validated green in the pass-2 sweep (formal-verification-control/COHERENCE-PASS-2.md). Co-Authored-By: Claude Fable 5 --- verification/check.sh | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/verification/check.sh b/verification/check.sh index b5a1b4f..172ded7 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -33,5 +33,27 @@ lake env bash -c " LEAN_TIMEOUT=400 LEAN_MEM_MB=8192 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1 done " || { echo FAIL; exit 1; } +echo "=== Phase 3: axiom audit (kernel-level) ===" +cd "$AENEAS_LEAN" +lake env bash -c " + set -uo pipefail + export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\" + cd '$HERE' + AUD=\$(mktemp '$HERE/.audit-pasta-XXXX.lean') + { echo 'import Proofs.Denote' + echo 'import Proofs.SubNegSpec' + echo 'import Proofs.ConstSpecs' + echo '#print axioms PastaProofs.P_prime' + echo '#print axioms PastaProofs.sub_spec' + echo '#print axioms PastaProofs.INV_spec' + } > \"\$AUD\" + OUT=\$(LEAN_TIMEOUT=180 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) + echo \"\$OUT\" + rm -f \"\$AUD\" \"\${AUD%.lean}.olean\" + N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true) + [ \"\$N\" -eq 3 ] || { echo \"AXIOM AUDIT FAILED: \$N/3 clean\"; exit 1; } +" || { echo FAIL; exit 1; } +echo " 3/3 certificates axiom-clean" + echo "" echo "PASTA FOUNDATION: ALL PROOFS PASS (primality, denotation, adc/sbb/mac, sub/neg, constants)."