		Search-engine friendly clone of the ACL2 documentation.

Birational-montgomery-twisted-edwards

Montgomery-to-twisted-edwards

Map a Montgomery curve to a twisted Edwards curve.

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

Given the Montgomery curve's coefficients A and B, the twisted Edwards curve's coefficients are a = (A + 2) / B and d = (A - 2) B, which are well-defined because B \neq 0. The prime is of course unchanged.

We also allow a non-zero scaling factor to be applied to B in the calculation of a and d. This can be set to 1.

The guard proofs require to show that a and d are not 0, which follows from the conditions on A. It also requires showing that a \neq d: this reduces (via locally included prime field rules) to A + 2 \neq A - 2 and thus to 2 \neq -2, but this is not immediately obvious because it is modular, i.e. it really is 2 \neq p - 2; so we use a local lemma to reduce this to p \neq 4, and another local lemma to show that 4 is not prime.

Definitions and Theorems

Function: montgomery-to-twisted-edwards

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

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

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

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

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

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