saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-08 21:00:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

scalar: add ScalarLoop to the check manifest

Browse source 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-02 21:56:40 +02:00
parent 24a9fb653a
commit 5eeaaad74a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
verification/check-scalar.sh
View file

@ -7,7 +7,7 @@ source ~/aeneas-toolchain/env.sh
HERE="$(cd "$(dirname "$0")" && pwd)" HERE="$(cd "$(dirname "$0")" && pwd)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean" AENEAS_LEAN="$AENEAS_HOME/backends/lean"
GEN=(CurveScalar/TypesExternal CurveScalar/Types CurveScalar/FunsExternal CurveScalar/Funs) GEN=(CurveScalar/TypesExternal CurveScalar/Types CurveScalar/FunsExternal CurveScalar/Funs)
PROOFS=(ScalarDenote) PROOFS=(ScalarDenote ScalarLoop)
echo "=== stub/axiom audit ===" echo "=== stub/axiom audit ==="
grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; } grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }