		Search-engine friendly clone of the ACL2 documentation.

Jubjub-a

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

We show that this coefficient is a square by exhibiting a square root of it.

Function: jubjub-a

(defun jubjub-a nil
  (declare (xargs :guard t))
  (let ((__function__ 'jubjub-a))
    (declare (ignorable __function__))
    (neg 1 (jubjub-q))))

Theorem: return-type-of-jubjub-a

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

Theorem: jubjub-a-not-zero

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

Theorem: pfield-squarep-of-jubjub-a

(defthm pfield-squarep-of-jubjub-a
  (ecurve::pfield-squarep (jubjub-a)
                          (jubjub-q)))