ed25519-base-prime

(in-package "PRIMES")

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

(defprime ed25519-base-prime
  57896044618658097711785492504343953926634992332820282019728792003956564819949
  (2 (2 3
      65147
      74058212732561358302231226437062788676166966415465897661863160754340907)
    (2 1 1 1)
    (nil nil
      nil
      (2 (2 3
          353
          57467
          132049
          1923133
          31757755568855353
          75445702479781427272750846543864801)
        (1 1 1 1 1 1 1 1)
        (nil nil
          nil
          nil
          nil
          (2 (2 3 43 3727) (2 1 1 1) (nil nil nil nil))
          (10 (2 3 31 107 223 4153 430751)
            (3 1 1 1 1 1 1)
            (nil nil nil nil nil nil nil))
          (7 (2 3 5 75707 72106336199 1919519569386763)
            (5 2 2 1 1 1)
            (nil nil
              nil
              nil
              (7 (2 13 2773320623)
                (1 1 1)
                (nil nil (5 (2 2437 569003) (1 1 1) (nil nil nil))))
              (2 (2 3 7 19 47 127 8574133)
                (1 1 1 1 2 1 1)
                (nil nil
                  nil
                  nil
                  nil
                  nil
                  (2 (2 3 7 103 991) (2 1 1 1 1) (nil nil nil nil nil))))))))))
  :parents (primes)
  :short "The Ed25519 base field prime."
  :long (topstring (p "The Ed25519 base field prime is the size of the finite field
     over which the Edwards curve Ed25519 is defined. This prime is used for
     all field arithmetic operations in the curve.")
    (p "The prime is computed as:")
    (codeblock "2^255 - 19")
    (p "See also "
      (ahref "https://tools.ietf.org/rfc/rfc8032.txt"
        "RFC 8032")
      " and "
      (ahref "https://tools.ietf.org/rfc/rfc7748.txt"
        "RFC 7748"))))

(assert-event (equal (integer-length (ed25519-base-prime)) 255))

(assert-event (equal (ed25519-base-prime)
    57896044618658097711785492504343953926634992332820282019728792003956564819949))

(assert-event (equal (ed25519-base-prime) (- (expt 2 255) 19)))