koala-bear

(in-package "PRIMES")

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

(defprime koala-bear
  2130706433
  (3 (2 127) (24 1) (nil nil))
  :parents (crypto)
  :short "The koala-bear prime."
  :long (topstring (p "The koala-bear prime is defined by the formula "
      (code "2^31 - 2^24 + 1 = 2130706433")
      ", also known as the KoalaBear field prime.")
    (p "Ziren's zkVM (ZVM/Ziren) expresses AIR traces over this field so that "
      "every register column becomes a polynomial on a KoalaBear evaluation "
      "domain.")
    (p "Ziren's proof system runs its Machine Prover in KoalaBear before "
      "recursively translating the resulting STARK proofs into BN254 for "
      "Groth16 aggregation.")
    (p "Outside of Ziren, the KoalaBear prime is implemented inside Plonky3 as "
      "one of the ~32-bit, FRI-friendly fields for zero-knowledge systems.")
    (p "See also "
      (ahref "https://docs.zkm.io/design/arithmetization.html"
        "Ziren arithmetization")
      ", "
      (ahref "https://docs.zkm.io/design/prover-architecture/prover-architecture.html"
        "Ziren prover architecture")
      ", and "
      (ahref "https://hackmd.io/@Voidkai/BkNX3xUZA"
        ""Efficient Prime Fields for Zero-knowledge proof"."))))

(assert-event (equal (integer-length (koala-bear)) 31))

(assert-event (equal (koala-bear) 2130706433))

(assert-event (equal (koala-bear)
    (+ (- (expt 2 31) (expt 2 24)) 1)))