mirror of
https://github.com/saymrwulf/anza-ed25519-verified.git
synced 2026-09-04 20:24:06 +00:00
THE HALF-LIFT IS NOW PROVEN ON ALL FOUR PYRAMIDS. anza's shape: the hash oracle is one sha512_hash3 bind, -A is the STORED minus_A field (no negation call), and the scalar arrives already parsed - so the recompute inversion is five flat bind_ok_inv steps (two anonymous slice reads, the oracle, the reduction, the dsm) and the assembly takes ExtValid/OnCurveExt of self.minus_A directly. Files 1-4 are dalek's verbatim modulo the curve25519 namespace; every proof compiled FIRST TRY. verify_accepts_iff_point: accept IFF the signature's R bytes are the canonical encoding of the recomputed [k]*minus_A + [s]*B (valid, on-curve, certified model). Five new standard certificates; Phase 3b enforces anza's tight boundary (SHA-512 oracle + foreign Signature type + its two accessors) on BOTH apex and half-lift. Full button green fresh. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| gen/CurveField | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| extract.sh | ||
| lean-guard | ||