The deferred half, done four times — point-level ed25519 verification lands on every fork
When I wrote up the ed25519 proof pyramids a few days ago — upstream curve25519-dalek and its Solana, RISC-Zero, and Betrusted forks — each post ended on the same honest note. The signature apex was proven, but only at the byte level: the extracted verifier returns Ok(()) iff the recomputed compressed point compress([s]B − [k]A) equals the signature's R, byte for byte. Lifting that to the point level — proving [s]B − [k]A = decompress R as an equation about actual curve points — was marked Phase 2, deferred, because it needs two things the byte-level proof could sidestep: that compress is canonical, and that decompress is itself verified.
I don't like deferrals that sit. This post is to record that the deferral is closed — and closed on all four forks, not just the flagship.
What "point level" actually demanded
The gap between the two statements is exactly the gap where an implementation can lie to you. Byte-level says the bytes match; point-level says the math holds. To cross it, the extracted code had to be proven correct at every step that turns 32 bytes back into a curve point:
decompress, extracted for real — not modeled, not assumed. The Aeneas
transpilation of the actual Rust decompression path, with its theorems stated about the extracted function.
- The square-root walk — decompression recovers the x coordinate by a
modular square root (pow_p58, the 2²⁵²−3 exponentiation chain, then the ±√−1 correction). That chain is proven to compute what it claims, with the constant-time equality (ct_eq) semantics kernel-audited.
- The byte parser —
from_bytes_spec: that parsing the wire format yields
exactly the field element and sign bit the bytes encode, or rejects.
compresscanonicity —ed_compress_specandto_bytescanonicity:
that compression is injective on the represented points, so the byte equality the Phase-1 apex proved actually implies the point equality. Without this, matching bytes wouldn't guarantee matching points.
With those in hand, the apex certificate becomes verify_accepts_iff_point_eq: the verifier accepts iff [s]B − [k]A decompresses-equal to R, as points on the twisted Edwards curve, with k the scalar the (still opaque) SHA-512 oracle produces. The half-lift landed first (verify_accepts_iff_point, button-enforced), then the full lift closed it.
Four forks, and why that's the whole point
The same campaign ran independently against each fork's own extraction: upstream dalek, Solana's solana-ed25519, RISC-Zero's guest fork, Betrusted's Precursor fork. "PHASE 2 COMPLETE ON DALEK / ANZA / RISC0 / BETRUSTED" are four separate apexes over four separate codebases, because — as the fork posts argued — a theorem about one does not transfer to another. The interesting finding is the same as before, sharpened: the proofs went through on every fork, which is the strongest available evidence that none of the four guest/validator/loader patches disturbed the curve arithmetic on the path that actually decides acceptance. Where a proof needed fork-specific adjustment, the adjustment is a precise map of the fork's real divergence.
Each apex still carries — and the build still audits down to — exactly the three Lean foundations plus the documented SHA-512/wire-format boundary. Zero curve, scalar, or backend axioms. A verification/check.sh phase fails the build if the axiom cone grows by so much as one name.
The book kept pace
The teaching text was brought to the same four-tier apex state in the same window — and roughly doubled, from 53 to 106 pages, with pen-and-paper worked examples at the real constants and in-book solution pathways, plus an honesty ledger recording the kernel axiom audit of every solution certificate. The proofs and the pedagogy advanced together, which is the only way I know to keep a curriculum from drifting off the code it claims to teach.
Companion track: the Pallas field layer reached its own proven-and-green foundation state alongside this — Montgomery arithmetic and the Lucas/Pratt primality certificate for the 255-bit modulus, no bridge axioms. Different curve, different limb discipline, same rule: the status table changes only when the kernel says it may.