		Search-engine friendly clone of the ACL2 documentation.

Baby-jubjub

Baby-jubjub-curve

The BabyJubjub curve.

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

The fact that a is a square and d is not a square (see baby-jubjub-a and baby-jubjub-d) means that BabyJubjub is a complete twisted Edwards curve, i.e. the addition formula is complete (works for all points).

Definitions and Theorems

Function: baby-jubjub-curve

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

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

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

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

(defthm twisted-edwards-curve-completep-of-baby-jubjub-curve
  (twisted-edwards-curve-completep (baby-jubjub-curve)))