ed25519-group-prime

(in-package "PRIMES")

(include-book "kestrel/number-theory/defprime" :dir :system)

(defprime ed25519-group-prime
  7237005577332262213973186563042994240857116359379907606001950938285454250989
  (2 (2 3
      11
      198211423230930754013084525763697
      276602624281642239937218680557139826668747)
    (2 1 1 1 1)
    (nil nil
      nil
      (5 (2 3 23 58964693 3044861653679985063343)
        (4 1 1 1 1)
        (nil nil
          nil
          (2 (2 14741173)
            (2 1)
            (nil (2 (2 3 409477) (2 2 1) (nil nil nil))))
          (5 (2 3 11 30703 82163 132667 137849)
            (1 1 1 1 1 1 1)
            (nil nil nil nil nil nil nil))))
      (2 (2 7 19757330305831588566944191468367130476339)
        (1 1 1)
        (nil nil
          (2 (2 269 213441916511 172054593956031949258510691)
            (1 1 1 1)
            (nil nil
              (13 (2 5 73 292386187)
                (1 1 1 1)
                (nil nil nil (2 (2 3 307 5879) (1 4 1 1) (nil nil nil nil))))
              (2 (2 5 1361 2851 4434155615661930479)
                (1 1 1 1 1)
                (nil nil
                  nil
                  nil
                  (17 (2 41 43 1257559732178653)
                    (1 1 1 1)
                    (nil nil
                      nil
                      (2 (2 3 7 23 531581 1224481)
                        (2 1 1 1 1 1)
                        (nil nil
                          nil
                          nil
                          nil
                          (13 (2 3 5 2551) (5 1 1 1) (nil nil nil nil))))))))))))))
  :parents (primes)
  :short "The Ed25519 group order prime."
  :long (topstring (p "The Ed25519 group order prime is the order of the largest prime subgroup
     of the Edwards curve Ed25519. This prime is used as the scalar field
     for EdDSA signature operations.")
    (p (ahref "https://tools.ietf.org/rfc/rfc8032.txt"
        "RFC 8032")
      " states that the group order (called @($L$)) is equal to "
      (codeblock "2^252 + 27742317777372353535851937790883648493"))))

(assert-event (equal (integer-length (ed25519-group-prime)) 253))

(assert-event (equal (ed25519-group-prime)
    7237005577332262213973186563042994240857116359379907606001950938285454250989))

(assert-event (equal (ed25519-group-prime)
    (+ (expt 2 252) 27742317777372353535851937790883648493)))