From 78c8acec0f8f497135e30f49e9845faf4feec3c6 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 4 Jul 2026 22:49:18 +0200 Subject: [PATCH] extract.sh: reproducible CurveSig glue stanza (sha512_hash3 recipe) The [3/4]+[4/4] steps that produced the shipped gen/CurveSig, verified byte-exact by re-running them and diffing Types.lean/Funs.lean against the installed model. Deltas from dalek's recipe for the sha2-0.10 stack: `--opaque crate::verifying::sha512_hash3` (single-call oracle) instead of the three stateful wrappers, `--opaque block_buffer --opaque crypto_common`, `--exclude generic_array` (mixed recursion with typenum), and `-- --no-default-features` (no-std error path, no boxed dyn-Error). Co-Authored-By: Claude Fable 5 --- verification/extract.sh | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/verification/extract.sh b/verification/extract.sh index e9b8d36..9f6c2ea 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -61,8 +61,30 @@ charon cargo --preset=aeneas \ --dest-file "$HERE/CurveField.llbc" \ -- --no-default-features -echo "[2/2] aeneas: LLBC -> Lean (split files, CurveField.* modules)" +echo "[2/4] aeneas: LLBC -> Lean (split files, CurveField.* modules)" cd "$HERE" aeneas -backend lean -split-files -subdir CurveField -dest gen CurveField.llbc +echo "[3/4] charon: ed25519-dalek verify glue -> LLBC (sha512_hash3 opaque)" +SIGCRATE="$(dirname "$CRATE")/ed25519-dalek" +cd "$SIGCRATE" +charon cargo --preset=aeneas \ + --start-from 'crate::verifying::verify_sha512' \ + --start-from 'crate::verifying::recompute_r_sha512' \ + --opaque 'crate::verifying::sha512_hash3' \ + --opaque 'crate::signature::compressed_from_bytes' \ + --opaque 'curve25519_dalek' \ + --opaque 'sha2' --opaque 'digest' --opaque 'ed25519' \ + --opaque 'signature' --opaque 'subtle' --opaque 'zeroize' \ + --opaque 'block_buffer' --opaque 'crypto_common' \ + --exclude 'generic_array' --exclude 'typenum' \ + --hide-marker-traits \ + --dest-file "$HERE/CurveSig.llbc" \ + -- --no-default-features + +echo "[4/4] aeneas: LLBC -> Lean (CurveSig.* modules; hand-maintained" +echo " TypesExternal.lean / FunsExternal.lean are NOT overwritten)" +cd "$HERE" +aeneas -backend lean -split-files -subdir CurveSig -dest gen CurveSig.llbc + echo "Done. Now run ./check.sh to type-check the regenerated model."