nist-p-256-base-prime

(in-package "PRIMES")

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

(defprime nist-p-256-base-prime
  115792089210356248762697446949407573530086143415290314195533631308867097853951
  (6 (2 3
      5
      17
      257
      641
      1531
      65537
      490463
      6700417
      835945042244614951780389953367877943453916927241)
    (1 1 2 1 1 1 1 1 1 1 1)
    (nil nil
      nil
      nil
      nil
      nil
      nil
      nil
      nil
      nil
      (11 (2 3 5 774023187263532362759620327192479577272145303)
        (3 3 1 1)
        (nil nil
          nil
          (3 (2 3 2411 34282281433 11290956913871 46076956964474543)
            (1 2 1 1 1 1)
            (nil nil
              nil
              (17 (2 3 7 204061199)
                (3 1 1 1)
                (nil nil
                  nil
                  (11 (2 11 23 107 3769) (1 1 1 1 1) (nil nil nil nil nil))))
              (13 (2 5 17 66417393611)
                (1 1 1 1)
                (nil nil
                  nil
                  (6 (2 5 53 173 197 3677)
                    (1 1 1 1 1 1)
                    (nil nil nil nil nil nil))))
              (5 (2 23 18169 78283 704251)
                (1 1 1 1 1)
                (nil nil nil nil nil))))))))
  :parents (primes)
  :short "The NIST P-256 base field prime."
  :long (topstring (p "The NIST P-256 base field prime is the characteristic of the finite field
     over which the Weierstrass elliptic curve @('NIST P-256') is defined. This prime
     is used for all field arithmetic operations in the curve.")
    (p "The curve @('NIST P-256') is also called @('secp256r1').")
    (p "The prime is computed as:")
    (codeblock "2^256 - 2^224 + 2^192 + 2^96 - 1")
    (p (ahref "https://www.secg.org/sec2-v2.pdf"
        "SEC 2: Recommended Elliptic Curve Domain Parameters")
      " (Section 2.4.2) calls it @($p$), and specifies its value in hexadecimal:")
    (codeblock "0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff")))

(assert-event (equal (integer-length (nist-p-256-base-prime)) 256))

(assert-event (equal (nist-p-256-base-prime)
    115792089210356248762697446949407573530086143415290314195533631308867097853951))

(assert-event (equal (nist-p-256-base-prime)
    (+ (- (expt 2 256) (expt 2 224))
      (expt 2 192)
      (expt 2 96)
      -1)))