nist-p-256-group-prime

(in-package "PRIMES")

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

(defprime nist-p-256-group-prime
  115792089210356248762697446949407573529996955224135760342422259061068512044369
  (7 (2 3
      71
      131
      373
      3407
      17449
      38189
      187019741
      622491383
      1002328039319
      2624747550333869278416773953)
    (4 1 1 1 1 1 1 1 1 1 1 1)
    (nil nil
      nil
      nil
      nil
      nil
      nil
      nil
      (2 (2 5 9350987)
        (2 1 1)
        (nil nil (2 (2 17 229 1201) (1 1 1 1) (nil nil nil nil))))
      (5 (2 311245691)
        (1 1)
        (nil (2 (2 5 7 17 29 311)
            (1 1 1 1 2 1)
            (nil nil nil nil nil nil))))
      (19 (2 126241 3969899)
        (1 1 1)
        (nil nil (2 (2 19 104471) (1 1 1) (nil nil nil))))
      (7 (2 3 1297 16879 208150935158385979)
        (6 2 1 1 1)
        (nil nil
          nil
          nil
          (2 (2 3 11 43 127 3023 191039911)
            (1 1 1 1 1 1 1)
            (nil nil
              nil
              nil
              nil
              nil
              (3 (2 3 5 41 155317) (1 1 1 1 1) (nil nil nil nil nil))))))))
  :parents (primes)
  :short "The NIST P-256 group order prime."
  :long (topstring (p "The NIST P-256 group order prime is the order of
     the Weierstrass elliptic curve @('NIST P-256'). This prime is used as the
     scalar field for ECDSA signature operations.")
    (p "The curve @('NIST P-256') is also called @('secp256r1').")
    (p (ahref "https://www.secg.org/sec2-v2.pdf"
        "SEC 2: Recommended Elliptic Curve Domain Parameters")
      " (Section 2.4.2) calls it @($n$) and specifies its value in hexadecimal:")
    (codeblock "0xffffffff00000000ffffffffffffffffbce6faada7179e84f3b9cac2fc632551")))

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

(assert-event (equal (nist-p-256-group-prime)
    115792089210356248762697446949407573529996955224135760342422259061068512044369))