secp256k1-group-prime

(in-package "PRIMES")

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

(defprime secp256k1-group-prime
  115792089237316195423570985008687907852837564279074904382605163141518161494337
  (7 (2 3
      149
      631
      107361793816595537
      174723607534414371449
      341948486974166000522343609283189)
    (6 1 1 1 1 1 1)
    (nil nil
      nil
      nil
      (3 (2 16699 85831 4681609)
        (4 1 1 1)
        (nil nil nil (23 (2 3 97 2011) (3 1 1 1) (nil nil nil nil))))
      (3 (2 17 59 4051 120233 44706919)
        (3 1 1 1 1 1)
        (nil nil
          nil
          nil
          nil
          (6 (2 3 797 9349) (1 1 1 1) (nil nil nil nil))))
      (2 (2 3 109 29047611873442575647497758179)
        (2 3 1 1)
        (nil nil
          nil
          (2 (2 293 305873 545358713 297159362677)
            (1 1 1 1 1)
            (nil nil
              nil
              (5 (2 41 59 28181) (3 1 1 1) (nil nil nil nil))
              (2 (2 3 11 461 1627771)
                (2 2 1 1 1)
                (nil nil
                  nil
                  nil
                  (3 (2 3 5 29 1871) (1 1 1 1 1) (nil nil nil nil nil)))))))))))

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