secp256k1-field-prime

(in-package "PRIMES")

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

(defprime secp256k1-field-prime
  115792089237316195423570985008687907853269984665640564039457584007908834671663
  (3 (2 3
      7
      13441
      205115282021455665897114700593932402728804164701536103180137503955397371)
    (1 1 1 1 1)
    (nil nil
      nil
      nil
      (10 (2 3
          5
          29
          31
          7723
          132896956044521568488119
          255515944373312847190720520512484175977)
        (1 1 1 2 1 1 1 1)
        (nil nil
          nil
          nil
          nil
          nil
          (6 (2 3 22149492674086928081353)
            (1 1 1)
            (nil nil
              (5 (2 3 5323 173378833005251801)
                (3 1 1 1)
                (nil nil
                  nil
                  (6 (2 5 2621 24809 13331831)
                    (3 2 1 1 1)
                    (nil nil
                      nil
                      nil
                      (13 (2 5 971 1373) (1 1 1 1) (nil nil nil nil))))))))
          (3 (2 7 11 1627 2657 4423 41201 96557 7240687 107590001)
            (3 2 1 1 1 1 1 1 1 1)
            (nil nil
              nil
              nil
              nil
              nil
              nil
              nil
              nil
              (3 (2 5 7 29 53) (4 4 1 1 1) (nil nil nil nil nil)))))))))

(assert-event (equal (secp256k1-field-prime)
    (- (- (- (- (- (- (- (expt 2 256) (expt 2 32)) (expt 2 9)) (expt 2 8))
            (expt 2 7))
          (expt 2 6))
        (expt 2 4))
      1)))

(assert-event (equal (integer-length (secp256k1-field-prime)) 256))