mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
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> |
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveScalar.llbc | ||
| CurveSig.llbc | ||
| extract-scalar.sh | ||
| extract.sh | ||
| lean-guard | ||