		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-q

The Jubjub prime q_\mathbb{J} [ZPS:5.4.9.3].

Signature
(jubjub-q) → q
Returns: q — Type (primep q).

This defines the prime field over which Jubjub is defined.

It is the same as r_\mathbb{S} [ZPS:5.4.9.2], which is defined in our cryptograhic library.

Definitions and Theorems

Function: jubjub-q

(defun jubjub-q nil
  (declare (xargs :guard t))
  (let ((__function__ 'jubjub-q))
    (declare (ignorable __function__))
    (primes::bls12-381-scalar-field-prime)))

Theorem: primep-of-jubjub-q

(defthm primep-of-jubjub-q
  (b* ((q (jubjub-q))) (primep q))
  :rule-classes :rewrite)

Theorem: jubjub-q-not-two

(defthm jubjub-q-not-two
  (not (equal (jubjub-q) 2)))