		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Point-on-twisted-edwards-p

Check if a point is on a twisted Edwards curve.

Signature
(point-on-twisted-edwards-p point curve) → yes/no
Arguments: point — Guard (pointp point).; curve — Guard (twisted-edwards-curvep curve).
Returns: yes/no — Type (booleanp yes/no).

A point (x, y) is on the curve if and only if its components satisfy the curve equation. We require its components to be below the prime, i.e. that the point is in the cartesian product of the prime field. The point at infinity is not part of a twisted Edwards curve; only finite points are.

Definitions and Theorems

Function: point-on-twisted-edwards-p

(defun point-on-twisted-edwards-p (point curve)
  (declare (xargs :guard (and (pointp point)
                              (twisted-edwards-curvep curve))))
  (let ((acl2::__function__ 'point-on-twisted-edwards-p))
    (declare (ignorable acl2::__function__))
    (b* ((p (twisted-edwards-curve->p curve))
         (a (twisted-edwards-curve->a curve))
         (d (twisted-edwards-curve->d curve))
         ((when (eq (point-kind point) :infinite))
          nil)
         (x (point-finite->x point))
         (y (point-finite->y point))
         ((unless (< x p)) nil)
         ((unless (< y p)) nil)
         (x^2 (mul x x p))
         (y^2 (mul y y p))
         (x^2.y^2 (mul x^2 y^2 p))
         (a.x^2 (mul a x^2 p))
         (a.x^2+y^2 (add a.x^2 y^2 p))
         (|1+D.X^2.Y^2| (add 1 (mul d x^2.y^2 p) p)))
      (equal a.x^2+y^2 |1+D.X^2.Y^2|))))

Theorem: booleanp-of-point-on-twisted-edwards-p

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

Theorem: point-on-twisted-edwards-is-finite

(defthm point-on-twisted-edwards-is-finite
  (implies (point-on-twisted-edwards-p point curve)
           (equal (point-kind point) :finite))
  :rule-classes :forward-chaining)

Theorem: point-on-twisted-edwards-p-of-point-fix-point

(defthm point-on-twisted-edwards-p-of-point-fix-point
  (equal (point-on-twisted-edwards-p (point-fix point)
                                     curve)
         (point-on-twisted-edwards-p point curve)))

Theorem: point-on-twisted-edwards-p-point-equiv-congruence-on-point

(defthm point-on-twisted-edwards-p-point-equiv-congruence-on-point
  (implies (point-equiv point point-equiv)
           (equal (point-on-twisted-edwards-p point curve)
                  (point-on-twisted-edwards-p point-equiv curve)))
  :rule-classes :congruence)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-curve-fix-curve

(defthm
      point-on-twisted-edwards-p-of-twisted-edwards-curve-fix-curve
  (equal (point-on-twisted-edwards-p
              point (twisted-edwards-curve-fix curve))
         (point-on-twisted-edwards-p point curve)))

Theorem: point-on-twisted-edwards-p-twisted-edwards-curve-equiv-congruence-on-curve

(defthm
 point-on-twisted-edwards-p-twisted-edwards-curve-equiv-congruence-on-curve
 (implies (twisted-edwards-curve-equiv curve curve-equiv)
          (equal (point-on-twisted-edwards-p point curve)
                 (point-on-twisted-edwards-p point curve-equiv)))
 :rule-classes :congruence)