Map a twisted Edwards curve to a Montgomery curve.
(twisted-edwards-to-montgomery tecurve scaling) → mcurve
Given the twisted Edwards curve's coefficients
We also allow a non-zero scaling factor to be applied to
The guard proofs require to show that
Function:
(defun twisted-edwards-to-montgomery (tecurve scaling) (declare (xargs :guard (and (twisted-edwards-curvep tecurve) (posp scaling)))) (declare (xargs :guard (fep scaling (twisted-edwards-curve->p tecurve)))) (let ((acl2::__function__ 'twisted-edwards-to-montgomery)) (declare (ignorable acl2::__function__)) (b* (((twisted-edwards-curve tecurve) tecurve) (a-d (sub tecurve.a tecurve.d tecurve.p)) (a+d (add tecurve.a tecurve.d tecurve.p)) (ma (mul 2 (div a+d a-d tecurve.p) tecurve.p)) (mb (div (mod 4 tecurve.p) a-d tecurve.p)) (b (mul (acl2::pos-fix scaling) mb tecurve.p))) (make-montgomery-curve :p tecurve.p :a ma :b b))))
Theorem:
(defthm montgomery-curvep-of-twisted-edwards-to-montgomery (b* ((mcurve (twisted-edwards-to-montgomery tecurve scaling))) (montgomery-curvep mcurve)) :rule-classes :rewrite)
Theorem:
(defthm twisted-edwards-to-montgomery-of-twisted-edwards-curve-fix-tecurve (equal (twisted-edwards-to-montgomery (twisted-edwards-curve-fix tecurve) scaling) (twisted-edwards-to-montgomery tecurve scaling)))
Theorem:
(defthm twisted-edwards-to-montgomery-twisted-edwards-curve-equiv-congruence-on-tecurve (implies (twisted-edwards-curve-equiv tecurve tecurve-equiv) (equal (twisted-edwards-to-montgomery tecurve scaling) (twisted-edwards-to-montgomery tecurve-equiv scaling))) :rule-classes :congruence)
Theorem:
(defthm twisted-edwards-to-montgomery-of-pos-fix-scaling (equal (twisted-edwards-to-montgomery tecurve (acl2::pos-fix scaling)) (twisted-edwards-to-montgomery tecurve scaling)))
Theorem:
(defthm twisted-edwards-to-montgomery-pos-equiv-congruence-on-scaling (implies (acl2::pos-equiv scaling scaling-equiv) (equal (twisted-edwards-to-montgomery tecurve scaling) (twisted-edwards-to-montgomery tecurve scaling-equiv))) :rule-classes :congruence)