		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Point-on-montgomery-p

Check if a point is on a Montgomery curve.

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

The primality requirement in the guard of this function is not strictly needed to define this function, but in general we should only deal with well-formed curves. In particular, curves whose p is prime.

The point at infinity is on the cure. A finite 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.

Definitions and Theorems

Function: point-on-montgomery-p

(defun point-on-montgomery-p (point curve)
  (declare (xargs :guard (and (pointp point)
                              (montgomery-curvep curve))))
  (let ((acl2::__function__ 'point-on-montgomery-p))
    (declare (ignorable acl2::__function__))
    (b* ((p (montgomery-curve->p curve))
         (a (montgomery-curve->a curve))
         (b (montgomery-curve->b curve))
         ((when (eq (point-kind point) :infinite))
          t)
         (x (point-finite->x point))
         (y (point-finite->y point))
         ((unless (< x p)) nil)
         ((unless (< y p)) nil)
         (x^2 (mul x x p))
         (x^3 (mul x x^2 p))
         (y^2 (mul y y p))
         (a.x^2 (mul a x^2 p))
         (b.y^2 (mul b y^2 p))
         (x^3+a.x^2+x (add x^3 (add a.x^2 x p) p)))
      (equal b.y^2 x^3+a.x^2+x))))

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

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

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

(defthm point-on-montgomery-p-of-point-fix-point
  (equal (point-on-montgomery-p (point-fix point)
                                curve)
         (point-on-montgomery-p point curve)))

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

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

Theorem: point-on-montgomery-p-of-montgomery-curve-fix-curve

(defthm point-on-montgomery-p-of-montgomery-curve-fix-curve
  (equal (point-on-montgomery-p point (montgomery-curve-fix curve))
         (point-on-montgomery-p point curve)))

Theorem: point-on-montgomery-p-montgomery-curve-equiv-congruence-on-curve

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