		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-curve

The Jubjub curve [ZPS:5.4.9.3].

Signature
(jubjub-curve) → curve
Returns: curve — Type (ecurve::twisted-edwards-curvep curve).

We show that it is complete.

Definitions and Theorems

Function: jubjub-curve

(defun jubjub-curve nil
  (declare (xargs :guard t))
  (let ((__function__ 'jubjub-curve))
    (declare (ignorable __function__))
    (ecurve::make-twisted-edwards-curve :p (jubjub-q)
                                        :a (jubjub-a)
                                        :d (jubjub-d))))

Theorem: twisted-edwards-curvep-of-jubjub-curve

(defthm twisted-edwards-curvep-of-jubjub-curve
  (b* ((curve (jubjub-curve)))
    (ecurve::twisted-edwards-curvep curve))
  :rule-classes :rewrite)

Theorem: twisted-edwards-curve-completep-of-jubjub-curve

(defthm twisted-edwards-curve-completep-of-jubjub-curve
  (ecurve::twisted-edwards-curve-completep (jubjub-curve)))