zkdefi · notes

#curves

2026-07-06

The deferred half, done four times — point-level ed25519 verification lands on every fork

The four ed25519 verification pyramids each ended their first post with an honest asterisk — the signature apex was proven at the byte level, and lifting it to the point level was deferred. That deferral is now closed, on all four forks: decompress is extracted and proven, the modular square root is proven, compress is canonical, and the acceptance criterion now reads as a real curve-point equation.

2026-07-02

A proof pyramid over the real curve25519-dalek

Machine-checked correctness for the ed25519 implementation everyone actually ships — field, group law, scalar arithmetic, and the EdDSA acceptance criterion itself — proven in Lean 4 about the Aeneas-transpiled Rust, not about a flattering re-model.

2026-07-02

No bridge axioms this time — Pallas field arithmetic, proven properly

Verification of the Pallas field layer in zcash/pasta_curves — Montgomery-form 4×64-limb arithmetic, with the 255-bit modulus's primality machine-checked via a Lucas/Pratt certificate. A do-over of an earlier attempt that axiomatized exactly the statements that needed proving.