		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-r-pointp

Recognize elements of \mathbb{J}^{(r)} [ZPS:5.4.9.3].

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

These are the points of order r_\mathbb{J} plus \mathcal{O}_\mathbb{J}.

Definitions and Theorems

Function: jubjub-r-pointp

(defun jubjub-r-pointp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'jubjub-r-pointp))
  (declare (ignorable __function__))
  (or (equal x (twisted-edwards-zero))
      (and (jubjub-pointp x)
           (ecurve::twisted-edwards-point-orderp x (jubjub-r)
                                                 (jubjub-curve))))))

Theorem: booleanp-of-jubjub-r-pointp

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

Theorem: jubjub-pointp-when-jubjub-r-pointp

(defthm jubjub-pointp-when-jubjub-r-pointp
  (implies (jubjub-r-pointp x)
           (jubjub-pointp x)))

Theorem: jubjub-point-of-neg

(defthm jubjub-point-of-neg
  (implies (and (ecurve::twisted-edwards-add-associativity)
                (jubjub-r-pointp point))
           (jubjub-r-pointp (jubjub-neg point))))