A proof pyramid over the real curve25519-dalek
Most "verified cryptography" proves theorems about a model somebody wrote by hand while looking at the code. The model is clean, the proofs go through, and the distance between the model and the code is exactly where the bugs live. This project takes the other route: the Rust of curve25519-dalek v5.0.0-rc.1 is transpiled to Lean 4 through the Charon/Aeneas pipeline, and every theorem is stated about that — the extracted functions, radix-2⁵¹ limbs, wrapping arithmetic, the lot. If the extraction is honest, the theorems are about the code everyone ships.
The result is a pyramid, and the layers are the point:
- Field 𝔽ₚ, p = 2²⁵⁵ − 19 —
FieldElement51add, sub, mul, square,
negate correct mod p, at the real limb weights, including the ×19 fold and the 16p subtraction constant.
- Group law — the extracted point operations implement the complete
twisted-Edwards addition law. Complete means no special cases, which is the entire reason Edwards coordinates won.
- Scalar arithmetic mod ℓ —
Scalar52add, sub, mul correct modulo
the group order.
- Signature apex — the EdDSA acceptance criterion itself: for a
signature that parses, the extracted verifier returns Ok(()) iff compress([s]B − [k]A) equals the signature's R, byte for byte.
The apex is the part I care about most, because it's where honesty gets audited mechanically. The recomputation resolves entirely through proven definitions — every curve and scalar call lands on a theorem, not an assumption. Only SHA-512 and the wire-format types stay opaque, and the build script has a dedicated phase that fails unless the apex certificate's axiom cone is exactly the three Lean foundations plus that documented boundary. Not "roughly" — exactly, by name. A proof that quietly grew a convenient axiom doesn't build.
That discipline runs through the whole repo: the status table is updated only when verification/check.sh passes for the layer, files that don't compile aren't in the repository, and every certificate ships with its #print axioms output. Phase 2 — lifting the byte-level equation to the point level, which needs compress canonicity and a verified decompress — is deferred and says so out loud. A verification project that won't tell you what it hasn't proven isn't a verification project; it's marketing.
This is the upstream anchor of a four-target family: the same pyramid is built independently for the Solana, RISC Zero, and Betrusted forks of dalek, each against its own extraction of its own patched source. Same theorems, four codebases — because "the fork didn't break the math" is precisely the claim nobody ever checks.