		Search-engine friendly clone of the ACL2 documentation.

Jubjub-montgomery

Jubjub-montgomery-curve

The Jubjub curve in Montgomery form [ZPS:A.2].

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

Definitions and Theorems

Function: jubjub-montgomery-curve

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

Theorem: montgomery-curvep-of-jubjub-montgomery-curve

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