Map a point on a Montgomery curve to the corresponding point on the corresponding twisted Edwards curve.
(montgomery-point-to-twisted-edwards-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 abscissa after its calculation from the Montgomery coordinates. This can be set to 1.
It remains to prove that the resulting point is on the twisted Edwards curve corresponding to the Montgomery curve. It also remains to extend the mapping to other points (the ones for which the rational formulas do not work).
Function:
(defun montgomery-point-to-twisted-edwards-point (point curve scaling) (declare (xargs :guard (and (pointp point) (montgomery-curvep curve) (posp scaling)))) (declare (xargs :guard (and (point-on-montgomery-p point curve) (not (eq (point-kind point) :infinite)) (not (equal (point-finite->x point) (neg 1 (montgomery-curve->p curve)))) (not (equal (point-finite->y point) 0)) (fep scaling (montgomery-curve->p curve))))) (let ((acl2::__function__ 'montgomery-point-to-twisted-edwards-point)) (declare (ignorable acl2::__function__)) (b* ((p (montgomery-curve->p curve)) (mx (point-finite->x point)) (my (point-finite->y point)) (tex (div mx my p)) (x (mul (acl2::pos-fix scaling) tex p)) (tey (div (sub mx 1 p) (add mx 1 p) p))) (point-finite x tey))))
Theorem:
(defthm pointp-of-montgomery-point-to-twisted-edwards-point (b* ((point1 (montgomery-point-to-twisted-edwards-point point curve scaling))) (pointp point1)) :rule-classes :rewrite)
Theorem:
(defthm montgomery-point-to-twisted-edwards-point-of-point-fix-point (equal (montgomery-point-to-twisted-edwards-point (point-fix point) curve scaling) (montgomery-point-to-twisted-edwards-point point curve scaling)))
Theorem:
(defthm montgomery-point-to-twisted-edwards-point-point-equiv-congruence-on-point (implies (point-equiv point point-equiv) (equal (montgomery-point-to-twisted-edwards-point point curve scaling) (montgomery-point-to-twisted-edwards-point point-equiv curve scaling))) :rule-classes :congruence)
Theorem:
(defthm montgomery-point-to-twisted-edwards-point-of-montgomery-curve-fix-curve (equal (montgomery-point-to-twisted-edwards-point point (montgomery-curve-fix curve) scaling) (montgomery-point-to-twisted-edwards-point point curve scaling)))
Theorem:
(defthm montgomery-point-to-twisted-edwards-point-montgomery-curve-equiv-congruence-on-curve (implies (montgomery-curve-equiv curve curve-equiv) (equal (montgomery-point-to-twisted-edwards-point point curve scaling) (montgomery-point-to-twisted-edwards-point point curve-equiv scaling))) :rule-classes :congruence)
Theorem:
(defthm montgomery-point-to-twisted-edwards-point-of-pos-fix-scaling (equal (montgomery-point-to-twisted-edwards-point point curve (acl2::pos-fix scaling)) (montgomery-point-to-twisted-edwards-point point curve scaling)))
Theorem:
(defthm montgomery-point-to-twisted-edwards-point-pos-equiv-congruence-on-scaling (implies (acl2::pos-equiv scaling scaling-equiv) (equal (montgomery-point-to-twisted-edwards-point point curve scaling) (montgomery-point-to-twisted-edwards-point point curve scaling-equiv))) :rule-classes :congruence)