Machine-checked primality of the Curve25519 base-field prime #
Nat.Prime p25519lit for p25519lit = 2^255 - 19 from an inline Pratt
certificate tree checked by kernel reduction (PrattCertificate.pratt_prime).
Nested nodes certify the prime factors of p - 1 above 2^20; the factors below
2^20 are leaves checked by trial division.
The certified prime 57896044618658097711785492504343953926634992332820282019728792003956564819949
(255-bit), the Curve25519 base-field modulus 2^255 - 19.
N - 1 = 2^2 · 3 · 65147 · 74058212732561358302231226437062788676166966415465897661863160754340907.
Equations
- CatCrypt.Crypto.Util.P25519PrimeCert.p25519lit = 57896044618658097711785492504343953926634992332820282019728792003956564819949