Machine-checked primality of the Ed25519 group order ℓ #
Nat.Prime ed25519Llit for ℓ = 2^252 + 27742317777372353535851937790883648493
from an inline Pratt certificate tree checked by kernel reduction
(PrattCertificate.pratt_prime). The same ℓ is the order of Curve25519's
prime-order subgroup. Nested nodes certify the prime factors of ℓ - 1 above
2^20; the factors below 2^20 are leaves checked by trial division.
The Ed25519 group order ℓ, as a literal (definitionally equal to
2^252 + 27742317777372353535851937790883648493).
Equations
- CatCrypt.Crypto.Util.Ed25519LPrimeCert.ed25519Llit = 7237005577332262213973186563042994240857116359379907606001950938285454250989
Instances For
Nat.Prime ed25519Llit, by a Pratt certificate with root witness 2.