		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-d

The Jubjub coefficient d_\mathbb{J} [ZPS:5.4.9.3].

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

We show that this coefficient is not a square using Euler's criterion. We use the fast modular exponentiation operation from the arithmetic-3 library to calculate the modular exponentiation of the coefficient, which must be different from 1 in order for the criterion to apply.

Definitions and Theorems

Function: jubjub-d

(defun jubjub-d nil
  (declare (xargs :guard t))
  (let ((__function__ 'jubjub-d))
    (declare (ignorable __function__))
    (neg (div 10240 10241 (jubjub-q))
         (jubjub-q))))

Theorem: return-type-of-jubjub-d

(defthm return-type-of-jubjub-d
  (b* ((d (jubjub-d))) (fep d (jubjub-q)))
  :rule-classes :rewrite)

Theorem: jubjub-d-not-zero

(defthm jubjub-d-not-zero
  (not (equal (jubjub-d) 0)))

Theorem: jubjub-d-not-equal-to-a

(defthm jubjub-d-not-equal-to-a
  (not (equal (jubjub-d) (jubjub-a))))

Theorem: not-pfield-squarep-of-jubjub-d

(defthm not-pfield-squarep-of-jubjub-d
  (not (ecurve::pfield-squarep (jubjub-d)
                               (jubjub-q))))