		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-rstar-pointp

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

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

These are the points order r_\mathbb{J}. That is, the points in \mathbb{J}^{(r)} minus \mathcal{O}_\mathbb{J}.

Definitions and Theorems

Function: jubjub-rstar-pointp

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

Theorem: booleanp-of-jubjub-rstar-pointp

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

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

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