Map a point on a Twisted Edwards curve to the corresponding point on the corresponding Montgomery curve.
(twisted-edwards-point-to-montgomery-point point curve scaling) → 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).
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)