		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-add

Group addition on a Montgomery curve.

Signature
(montgomery-add point1 point2 curve) → point3
Arguments: point1 — Guard (pointp point1).; point2 — Guard (pointp point2).; curve — Guard (montgomery-curvep curve).
Returns: point3 — Type (pointp point3).

We require, in the guard, both points to be on the curve. Indeed, the group addition operation is only defined on points on the curve, not on any points.

As in short Weierstrass curves, there are various cases to consider; things are not as uniform as in (complete) twisted Edwards curves. If either point is the one at infinity, the result is the other point. Otherwise, both points are finite, and we proceed as follows. If the two points have the same x coordinates and opposite y coordinates, the result is the point at infinity. Otherwise, if the points have the same x coordinates, then the y coordinates must also be the same, and different from 0, since both points are on the curve (we should formally prove this eventually, for validation): we are thus in the point doubling case, and the formula from the referenced papers applies. Finally, if the x coordinates differ, we are in the ``normal'' (but incomplete) case, and the formula from the referenced papers applies.

Note that, to verify guards, we need to use 3 \mod p instead of just 3, in case p = 3.

Definitions and Theorems

Function: montgomery-add

(defun montgomery-add (point1 point2 curve)
 (declare (xargs :guard (and (pointp point1)
                             (pointp point2)
                             (montgomery-curvep curve))))
 (declare (xargs :guard (and (point-on-montgomery-p point1 curve)
                             (point-on-montgomery-p point2 curve))))
 (let ((acl2::__function__ 'montgomery-add))
   (declare (ignorable acl2::__function__))
   (b* ((p (montgomery-curve->p curve))
        (a (montgomery-curve->a curve))
        (b (montgomery-curve->b curve))
        ((when (eq (point-kind point1) :infinite))
         (point-fix point2))
        ((when (eq (point-kind point2) :infinite))
         (point-fix point1))
        (x1 (point-finite->x point1))
        (y1 (point-finite->y point1))
        (x2 (point-finite->x point2))
        (y2 (point-finite->y point2))
        ((when (and (equal x1 x2)
                    (equal y1 (neg y2 p))))
         (point-infinite))
        ((when (equal x1 x2))
         (b* ((x x1)
              (y y1)
              (x^2 (mul x x p))
              (|3.X^2| (mul (mod 3 p) x^2 p))
              (a.x (mul a x p))
              (|2.A.X| (mul 2 a.x p))
              (b.y (mul b y p))
              (|2.B.Y| (mul 2 b.y p))
              (|3.X^2+2.A.X+1| (add |3.X^2| (add |2.A.X| 1 p) p))
              (l (div |3.X^2+2.A.X+1| |2.B.Y| p))
              (l^2 (mul l l p))
              (b.l^2 (mul b l^2 p))
              (|2.X| (mul 2 x p))
              (b.l^2-a (sub b.l^2 a p))
              (b.l^2-a-2.x (sub b.l^2-a |2.X| p))
              (x3 b.l^2-a-2.x)
              (x3-x (sub x3 x p))
              (l.[x3-x] (mul l x3-x p))
              (y+l.[x3-x] (add y l.[x3-x] p))
              (y3 (neg y+l.[x3-x] p)))
           (point-finite x3 y3)))
        (y2-y1 (sub y2 y1 p))
        (x2-x1 (sub x2 x1 p))
        (l (div y2-y1 x2-x1 p))
        (l^2 (mul l l p))
        (b.l^2 (mul b l^2 p))
        (b.l^2-a (sub b.l^2 a p))
        (b.l^2-a-x1 (sub b.l^2-a x1 p))
        (b.l^2-a-x1-x2 (sub b.l^2-a-x1 x2 p))
        (x3 b.l^2-a-x1-x2)
        (x3-x1 (sub x3 x1 p))
        (l.[x3-x1] (mul l x3-x1 p))
        (y1+l.[x3-x1] (add y1 l.[x3-x1] p))
        (y3 (neg y1+l.[x3-x1] p)))
     (point-finite x3 y3))))

Theorem: pointp-of-montgomery-add

(defthm pointp-of-montgomery-add
  (b* ((point3 (montgomery-add point1 point2 curve)))
    (pointp point3))
  :rule-classes :rewrite)

Theorem: montgomery-add-of-point-fix-point1

(defthm montgomery-add-of-point-fix-point1
  (equal (montgomery-add (point-fix point1)
                         point2 curve)
         (montgomery-add point1 point2 curve)))

Theorem: montgomery-add-point-equiv-congruence-on-point1

(defthm montgomery-add-point-equiv-congruence-on-point1
  (implies (point-equiv point1 point1-equiv)
           (equal (montgomery-add point1 point2 curve)
                  (montgomery-add point1-equiv point2 curve)))
  :rule-classes :congruence)

Theorem: montgomery-add-of-point-fix-point2

(defthm montgomery-add-of-point-fix-point2
  (equal (montgomery-add point1 (point-fix point2)
                         curve)
         (montgomery-add point1 point2 curve)))

Theorem: montgomery-add-point-equiv-congruence-on-point2

(defthm montgomery-add-point-equiv-congruence-on-point2
  (implies (point-equiv point2 point2-equiv)
           (equal (montgomery-add point1 point2 curve)
                  (montgomery-add point1 point2-equiv curve)))
  :rule-classes :congruence)

Theorem: montgomery-add-of-montgomery-curve-fix-curve

(defthm montgomery-add-of-montgomery-curve-fix-curve
  (equal (montgomery-add point1
                         point2 (montgomery-curve-fix curve))
         (montgomery-add point1 point2 curve)))

Theorem: montgomery-add-montgomery-curve-equiv-congruence-on-curve

(defthm montgomery-add-montgomery-curve-equiv-congruence-on-curve
  (implies (montgomery-curve-equiv curve curve-equiv)
           (equal (montgomery-add point1 point2 curve)
                  (montgomery-add point1 point2 curve-equiv)))
  :rule-classes :congruence)