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