		Search-engine friendly clone of the ACL2 documentation.

Birational-montgomery-twisted-edwards

Twisted-edwards-to-montgomery

Map a twisted Edwards curve to a Montgomery curve.

Signature
(twisted-edwards-to-montgomery tecurve scaling) → mcurve
Arguments: tecurve — Guard (twisted-edwards-curvep tecurve).; scaling — Guard (posp scaling).
Returns: mcurve — Type (montgomery-curvep mcurve).

Given the twisted Edwards curve's coefficients a and d, the Montgomery coefficients are A = 2 (a + d) / (a - d) and B = 4 / (a - d), which are well-defined because a \neq d.

We also allow a non-zero scaling factor to be applied to B after its calculation from a and d. This can be set to 1.

The guard proofs require to show that A is neither 2 nor -2 and B is not 0. This is carried out via a number of rules from the prime fields library, along with a few specific lemmas that involve particular constants that appear in the formulas.

Definitions and Theorems

Function: twisted-edwards-to-montgomery

(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: montgomery-curvep-of-twisted-edwards-to-montgomery

(defthm montgomery-curvep-of-twisted-edwards-to-montgomery
  (b* ((mcurve (twisted-edwards-to-montgomery tecurve scaling)))
    (montgomery-curvep mcurve))
  :rule-classes :rewrite)

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

(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: twisted-edwards-to-montgomery-twisted-edwards-curve-equiv-congruence-on-tecurve

(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: twisted-edwards-to-montgomery-of-pos-fix-scaling

(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: twisted-edwards-to-montgomery-pos-equiv-congruence-on-scaling

(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)