		Search-engine friendly clone of the ACL2 documentation.

Birational-montgomery-twisted-edwards

Twisted-edwards-point-to-montgomery-point

Map a point on a Twisted Edwards curve to the corresponding point on the corresponding Montgomery curve.

Signature
(twisted-edwards-point-to-montgomery-point point curve scaling) → point1
Arguments: point — Guard (pointp point).; curve — Guard (twisted-edwards-curvep curve).; scaling — Guard (posp scaling).
Returns: point1 — Type (pointp point1).

For now we only define the mapping for the points for which the rational formulas work. That is, we require the denominators to be non-zero in the guard.

We also allow a non-zero scaling factor to be applied to the ordinate after its calculation from the twisted Edwards coordinates. This can be set to 1.

It remains to prove that the resulting point is on the Montgomery curve corresponding to the twisted Edwards curve. It also remains to extend the mapping to other points (the ones for which the rational formulas do not work).

Definitions and Theorems

Function: twisted-edwards-point-to-montgomery-point

(defun twisted-edwards-point-to-montgomery-point
       (point curve scaling)
  (declare (xargs :guard (and (pointp point)
                              (twisted-edwards-curvep curve)
                              (posp scaling))))
  (declare
       (xargs :guard (and (point-on-twisted-edwards-p point curve)
                          (not (equal (point-finite->x point) 0))
                          (not (equal (point-finite->y point) 1))
                          (fep scaling
                               (twisted-edwards-curve->p curve)))))
  (let
   ((acl2::__function__ 'twisted-edwards-point-to-montgomery-point))
   (declare (ignorable acl2::__function__))
   (b* ((p (twisted-edwards-curve->p curve))
        (tex (point-finite->x point))
        (tey (point-finite->y point))
        (mx (div (add 1 tey p) (sub 1 tey p) p))
        (my (div (add 1 tey p)
                 (mul (sub 1 tey p) tex p)
                 p))
        (y (mul (acl2::pos-fix scaling) my p)))
     (point-finite mx y))))

Theorem: pointp-of-twisted-edwards-point-to-montgomery-point

(defthm pointp-of-twisted-edwards-point-to-montgomery-point
  (b* ((point1 (twisted-edwards-point-to-montgomery-point
                    point curve scaling)))
    (pointp point1))
  :rule-classes :rewrite)

Theorem: twisted-edwards-point-to-montgomery-point-of-point-fix-point

(defthm twisted-edwards-point-to-montgomery-point-of-point-fix-point
 (equal
   (twisted-edwards-point-to-montgomery-point (point-fix point)
                                              curve scaling)
   (twisted-edwards-point-to-montgomery-point point curve scaling)))

Theorem: twisted-edwards-point-to-montgomery-point-point-equiv-congruence-on-point

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

Theorem: twisted-edwards-point-to-montgomery-point-of-twisted-edwards-curve-fix-curve

(defthm
 twisted-edwards-point-to-montgomery-point-of-twisted-edwards-curve-fix-curve
 (equal
   (twisted-edwards-point-to-montgomery-point
        point (twisted-edwards-curve-fix curve)
        scaling)
   (twisted-edwards-point-to-montgomery-point point curve scaling)))

Theorem: twisted-edwards-point-to-montgomery-point-twisted-edwards-curve-equiv-congruence-on-curve

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

Theorem: twisted-edwards-point-to-montgomery-point-of-pos-fix-scaling

(defthm twisted-edwards-point-to-montgomery-point-of-pos-fix-scaling
 (equal
   (twisted-edwards-point-to-montgomery-point
        point curve (acl2::pos-fix scaling))
   (twisted-edwards-point-to-montgomery-point point curve scaling)))

Theorem: twisted-edwards-point-to-montgomery-point-pos-equiv-congruence-on-scaling

(defthm
 twisted-edwards-point-to-montgomery-point-pos-equiv-congruence-on-scaling
 (implies
  (acl2::pos-equiv scaling scaling-equiv)
  (equal
     (twisted-edwards-point-to-montgomery-point point curve scaling)
     (twisted-edwards-point-to-montgomery-point
          point curve scaling-equiv)))
 :rule-classes :congruence)