From 5eeaaad74a0753d096c7a279fc06659233c55cce Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 2 Jul 2026 21:56:40 +0200 Subject: [PATCH] scalar: add ScalarLoop to the check manifest Co-Authored-By: Claude Fable 5 --- verification/check-scalar.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verification/check-scalar.sh b/verification/check-scalar.sh index dc49996..5641b72 100755 --- a/verification/check-scalar.sh +++ b/verification/check-scalar.sh @@ -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; }