mrwulf e4034e0880 group-law layer: complete twisted Edwards addition law proven ... Extraction widened to backend::serial::curve_models + edwards (v4 Aeneas). Ed* proof suite shared with the risc0 twin EXCEPT proj_double_spec: upstream reordered ProjectivePoint::double's instructions between v4.1.2 (this fork) and v4.1.3 (risc0), so the step sequence was resequenced to match THIS fork's generated body — the proofs track each fork's actual code, not a template. All 20 proofs pass under lean-guard; both certificates axiom-clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>		2026-07-02 17:11:28 +02:00
..
gen/CurveField	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
Proofs	group-law layer: complete twisted Edwards addition law proven	2026-07-02 17:11:28 +02:00
check.sh	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
CurveField.llbc	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
extract.sh	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
lean-guard	group-law layer: complete twisted Edwards addition law proven	2026-07-02 17:11:28 +02:00