saymrwulf/risc0-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/risc0-ed25519-verified.git synced 2026-09-03 19:53:45 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

extract.sh: reproducible CurveSig glue stanza (sha512_hash3 recipe)

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-04 22:49:18 +02:00
parent f544b64e95
commit 78c8acec0f
1 changed files with 23 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
verification/extract.sh
View file

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