		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Point-on-jubjub-p

Check if a point is on the Jubjub curve [ZPS:5.4.9.3].

Signature
(point-on-jubjub-p point) → yes/no
Arguments: point — Guard (ecurve::pointp point).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: point-on-jubjub-p

(defun point-on-jubjub-p (point)
  (declare (xargs :guard (ecurve::pointp point)))
  (let ((__function__ 'point-on-jubjub-p))
    (declare (ignorable __function__))
    (ecurve::point-on-twisted-edwards-p point (jubjub-curve))))

Theorem: booleanp-of-point-on-jubjub-p

(defthm booleanp-of-point-on-jubjub-p
  (b* ((yes/no (point-on-jubjub-p point)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: point-on-jubjub-p-of-point-fix-point

(defthm point-on-jubjub-p-of-point-fix-point
  (equal (point-on-jubjub-p (ecurve::point-fix point))
         (point-on-jubjub-p point)))

Theorem: point-on-jubjub-p-point-equiv-congruence-on-point

(defthm point-on-jubjub-p-point-equiv-congruence-on-point
  (implies (ecurve::point-equiv point point-equiv)
           (equal (point-on-jubjub-p point)
                  (point-on-jubjub-p point-equiv)))
  :rule-classes :congruence)