mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
Extraction widened to backend::serial::curve_models + edwards (v4 Aeneas, 183 defs, own gen/). Reference Ed* suite adapted: namespace + v4 SharedA/SharedB instance renames. All 20 proofs compile under lean-guard (ReduceSpec needs an 8GB cap against the widened gen — contained by the guard, documented). Both certificates axiom-clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| gen/CurveField | ||
| Proofs | ||
| check.sh | ||
| CurveField.llbc | ||
| extract.sh | ||
| lean-guard | ||