		Search-engine friendly clone of the ACL2 documentation.

Baby-jubjub

Baby-jubjub-pointp

Recognize the points on the BabyJubjub curve.

Signature
(baby-jubjub-pointp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

These are all finite points.

Definitions and Theorems

Function: baby-jubjub-pointp

(defun baby-jubjub-pointp (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'baby-jubjub-pointp))
    (declare (ignorable acl2::__function__))
    (and (ecurve::pointp x)
         (point-on-baby-jubjub-p x))))

Theorem: booleanp-of-baby-jubjub-pointp

(defthm booleanp-of-baby-jubjub-pointp
  (b* ((yes/no (baby-jubjub-pointp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: point-finite-when-baby-jubjub-pointp

(defthm point-finite-when-baby-jubjub-pointp
  (implies (baby-jubjub-pointp x)
           (equal (ecurve::point-kind x) :finite)))