saymrwulf/pasta-pallas-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/pasta-pallas-verified.git synced 2026-09-05 20:10:31 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

coherence pass 2: institutionalize the kernel axiom audit

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
saymrwulf 2026-07-03 12:54:49 +02:00
parent 3719156140
commit bb21b8ab0f
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
verification/check.sh
View file

@ -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)."