		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-pointp

Recognize elements of \mathbb{J} [ZPS:5.4.9.3].

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

These are the points on the Jubjub curve.

These are all finite points.

Definitions and Theorems

Function: jubjub-pointp

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

Theorem: booleanp-of-jubjub-pointp

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

Theorem: point-finite-when-jubjub-pointp

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