saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +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 5630fb2a3f
commit 7207bbed62
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)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
GEN=(CurveScalar/TypesExternal CurveScalar/Types CurveScalar/FunsExternal CurveScalar/Funs)
PROOFS=(ScalarDenote)
PROOFS=(ScalarDenote ScalarLoop)
echo "=== stub/axiom audit ==="
grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }