		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-add

Group addition on a twisted Edwards curve.

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

We require, in the guard, the curve to be complete. Otherwise, this definition does not work in all cases; in particular, the guards could not be verified, due to the possibility that the denominators are 0.

We also 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.

The points on the curve are always finite, and the result is also a finite point. Its coordinates are calculated as shown in the paper referenced in twisted-edwards.

We verify the guards from lemmas from the closure proof, which involves proving that the denominators are not 0. The guard proof is explained in comments in this file.

Definitions and Theorems

Function: twisted-edwards-add

(defun twisted-edwards-add (point1 point2 curve)
 (declare (xargs :guard (and (pointp point1)
                             (pointp point2)
                             (twisted-edwards-curvep curve))))
 (declare
     (xargs :guard (and (twisted-edwards-curve-completep curve)
                        (point-on-twisted-edwards-p point1 curve)
                        (point-on-twisted-edwards-p point2 curve))))
 (let ((acl2::__function__ 'twisted-edwards-add))
   (declare (ignorable acl2::__function__))
   (b* ((p (twisted-edwards-curve->p curve))
        (a (twisted-edwards-curve->a curve))
        (d (twisted-edwards-curve->d curve))
        ((unless (mbt (eq (point-kind point1) :finite)))
         (point-finite 0 0))
        ((unless (mbt (eq (point-kind point2) :finite)))
         (point-finite 0 0))
        (x1 (point-finite->x point1))
        (y1 (point-finite->y point1))
        (x2 (point-finite->x point2))
        (y2 (point-finite->y point2))
        (d.x1.x2.y1.y2 (mul d (mul x1 (mul x2 (mul y1 y2 p) p) p)
                            p))
        (x3-numerator (add (mul x1 y2 p) (mul y1 x2 p) p))
        (x3-denominator (add 1 d.x1.x2.y1.y2 p))
        (y3-numerator (sub (mul y1 y2 p)
                           (mul a (mul x1 x2 p) p)
                           p))
        (y3-denominator (sub 1 d.x1.x2.y1.y2 p))
        (x3 (div x3-numerator x3-denominator p))
        (y3 (div y3-numerator y3-denominator p)))
     (point-finite x3 y3))))

Theorem: pointp-of-twisted-edwards-add

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

Theorem: d.x1.x2.y1.y2-not-one-on-curve-and-points

(defthm d.x1.x2.y1.y2-not-one-on-curve-and-points
 (implies
     (and (twisted-edwards-curve-completep curve)
          (point-on-twisted-edwards-p point1 curve)
          (point-on-twisted-edwards-p point2 curve))
     (b* (((twisted-edwards-curve curve) curve)
          (x1 (point-finite->x point1))
          (y1 (point-finite->y point1))
          (x2 (point-finite->x point2))
          (y2 (point-finite->y point2)))
       (not (equal (mul curve.d
                        (mul x1 (mul x2 (mul y1 y2 curve.p) curve.p)
                             curve.p)
                        curve.p)
                   1)))))

Theorem: d.x1.x2.y1.y2-not-minus-one-on-curve-and-points

(defthm d.x1.x2.y1.y2-not-minus-one-on-curve-and-points
 (implies
     (and (twisted-edwards-curve-completep curve)
          (point-on-twisted-edwards-p point1 curve)
          (point-on-twisted-edwards-p point2 curve))
     (b* (((twisted-edwards-curve curve) curve)
          (x1 (point-finite->x point1))
          (y1 (point-finite->y point1))
          (x2 (point-finite->x point2))
          (y2 (point-finite->y point2)))
       (not (equal (mul curve.d
                        (mul x1 (mul x2 (mul y1 y2 curve.p) curve.p)
                             curve.p)
                        curve.p)
                   (1- curve.p))))))

Theorem: 1+d.x1.x2.y1.y2-not-0

(defthm 1+d.x1.x2.y1.y2-not-0
 (implies
  (and (twisted-edwards-curve-completep curve)
       (point-on-twisted-edwards-p point1 curve)
       (point-on-twisted-edwards-p point2 curve))
  (b* (((twisted-edwards-curve curve) curve)
       (x1 (point-finite->x point1))
       (y1 (point-finite->y point1))
       (x2 (point-finite->x point2))
       (y2 (point-finite->y point2)))
   (not
       (equal (add 1
                   (mul curve.d
                        (mul x1 (mul x2 (mul y1 y2 curve.p) curve.p)
                             curve.p)
                        curve.p)
                   curve.p)
              0)))))

Theorem: 1-d.x1.x2.y1.y2-not-0

(defthm 1-d.x1.x2.y1.y2-not-0
 (implies
  (and (twisted-edwards-curve-completep curve)
       (point-on-twisted-edwards-p point1 curve)
       (point-on-twisted-edwards-p point2 curve))
  (b* (((twisted-edwards-curve curve) curve)
       (x1 (point-finite->x point1))
       (y1 (point-finite->y point1))
       (x2 (point-finite->x point2))
       (y2 (point-finite->y point2)))
   (not
       (equal (sub 1
                   (mul curve.d
                        (mul x1 (mul x2 (mul y1 y2 curve.p) curve.p)
                             curve.p)
                        curve.p)
                   curve.p)
              0)))))

Theorem: twisted-edwards-add-of-point-fix-point1

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

Theorem: twisted-edwards-add-point-equiv-congruence-on-point1

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

Theorem: twisted-edwards-add-of-point-fix-point2

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

Theorem: twisted-edwards-add-point-equiv-congruence-on-point2

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

Theorem: twisted-edwards-add-of-twisted-edwards-curve-fix-curve

(defthm twisted-edwards-add-of-twisted-edwards-curve-fix-curve
  (equal (twisted-edwards-add point1 point2
                              (twisted-edwards-curve-fix curve))
         (twisted-edwards-add point1 point2 curve)))

Theorem: twisted-edwards-add-twisted-edwards-curve-equiv-congruence-on-curve

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