		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-mul

Scalar multiplication in the twisted Edwards group.

Signature
(twisted-edwards-mul scalar point curve) → point1
Arguments: scalar — Guard (integerp scalar).; point — Guard (pointp point).; curve — Guard (twisted-edwards-curvep curve).
Returns: point1 — Type (pointp point1).

If the group were multiplicative, this would be exponentiation. Since the twisted Edwards group is additive, here we talk about scalar multiplication instead.

We first define the operation for non-negative scalars, by simple recursion in the same manner as exponentiation: multiplication by 0 yields the neutral element; multiplication by a non-zero scalar yields the sum of the point and the scalar multiplication by the scalar minus one. Then we extend it to negative scalars, by negating the result of multiplying by the negated scalar.

For the recursive auxiliary function on non-negative scalars, we need to defer guard verification; we first need to prove that it returns a point on the curve.

Definitions and Theorems

Function: twisted-edwards-mul-nonneg

(defun twisted-edwards-mul-nonneg (scalar point curve)
 (declare (xargs :guard (and (natp scalar)
                             (pointp point)
                             (twisted-edwards-curvep curve))))
 (declare
      (xargs :guard (and (twisted-edwards-curve-completep curve)
                         (point-on-twisted-edwards-p point curve))))
 (let ((acl2::__function__ 'twisted-edwards-mul-nonneg))
   (declare (ignorable acl2::__function__))
   (if (zp scalar)
       (twisted-edwards-zero)
     (twisted-edwards-add point
                          (twisted-edwards-mul-nonneg (1- scalar)
                                                      point curve)
                          curve))))

Theorem: pointp-of-twisted-edwards-mul-nonneg

(defthm pointp-of-twisted-edwards-mul-nonneg
  (b* ((point1 (twisted-edwards-mul-nonneg scalar point curve)))
    (pointp point1))
  :rule-classes :rewrite)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-mul-nonneg

(defthm point-on-twisted-edwards-p-of-twisted-edwards-mul-nonneg
  (implies (and (twisted-edwards-curve-completep curve)
                (pointp point)
                (point-on-twisted-edwards-p point curve))
           (point-on-twisted-edwards-p
                (twisted-edwards-mul-nonneg scalar point curve)
                curve)))

Theorem: twisted-edwards-mul-nonneg-of-0

(defthm twisted-edwards-mul-nonneg-of-0
  (equal (twisted-edwards-mul-nonneg 0 point curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-nonneg-of-1

(defthm twisted-edwards-mul-nonneg-of-1
  (implies (point-on-twisted-edwards-p point curve)
           (equal (twisted-edwards-mul-nonneg 1 point curve)
                  (point-fix point))))

Theorem: twisted-edwards-mul-nonneg-of-zero

(defthm twisted-edwards-mul-nonneg-of-zero
  (equal (twisted-edwards-mul-nonneg scalar (twisted-edwards-zero)
                                     curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-nonneg-of-nfix-scalar

(defthm twisted-edwards-mul-nonneg-of-nfix-scalar
  (equal (twisted-edwards-mul-nonneg (nfix scalar)
                                     point curve)
         (twisted-edwards-mul-nonneg scalar point curve)))

Theorem: twisted-edwards-mul-nonneg-nat-equiv-congruence-on-scalar

(defthm twisted-edwards-mul-nonneg-nat-equiv-congruence-on-scalar
 (implies
      (nat-equiv scalar scalar-equiv)
      (equal (twisted-edwards-mul-nonneg scalar point curve)
             (twisted-edwards-mul-nonneg scalar-equiv point curve)))
 :rule-classes :congruence)

Theorem: twisted-edwards-mul-nonneg-of-point-fix-point

(defthm twisted-edwards-mul-nonneg-of-point-fix-point
  (equal (twisted-edwards-mul-nonneg scalar (point-fix point)
                                     curve)
         (twisted-edwards-mul-nonneg scalar point curve)))

Theorem: twisted-edwards-mul-nonneg-point-equiv-congruence-on-point

(defthm twisted-edwards-mul-nonneg-point-equiv-congruence-on-point
 (implies
      (point-equiv point point-equiv)
      (equal (twisted-edwards-mul-nonneg scalar point curve)
             (twisted-edwards-mul-nonneg scalar point-equiv curve)))
 :rule-classes :congruence)

Theorem: twisted-edwards-mul-nonneg-of-twisted-edwards-curve-fix-curve

(defthm
      twisted-edwards-mul-nonneg-of-twisted-edwards-curve-fix-curve
  (equal (twisted-edwards-mul-nonneg
              scalar
              point (twisted-edwards-curve-fix curve))
         (twisted-edwards-mul-nonneg scalar point curve)))

Theorem: twisted-edwards-mul-nonneg-twisted-edwards-curve-equiv-congruence-on-curve

(defthm
 twisted-edwards-mul-nonneg-twisted-edwards-curve-equiv-congruence-on-curve
 (implies
      (twisted-edwards-curve-equiv curve curve-equiv)
      (equal (twisted-edwards-mul-nonneg scalar point curve)
             (twisted-edwards-mul-nonneg scalar point curve-equiv)))
 :rule-classes :congruence)

Function: twisted-edwards-mul

(defun twisted-edwards-mul (scalar point curve)
 (declare (xargs :guard (and (integerp scalar)
                             (pointp point)
                             (twisted-edwards-curvep curve))))
 (declare
      (xargs :guard (and (twisted-edwards-curve-completep curve)
                         (point-on-twisted-edwards-p point curve))))
 (let ((acl2::__function__ 'twisted-edwards-mul))
   (declare (ignorable acl2::__function__))
   (b* ((scalar (ifix scalar)))
     (if (>= scalar 0)
         (twisted-edwards-mul-nonneg scalar point curve)
       (twisted-edwards-neg (twisted-edwards-mul-nonneg (- scalar)
                                                        point curve)
                            curve)))))

Theorem: pointp-of-twisted-edwards-mul

(defthm pointp-of-twisted-edwards-mul
  (b* ((point1 (twisted-edwards-mul scalar point curve)))
    (pointp point1))
  :rule-classes :rewrite)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-mul

(defthm point-on-twisted-edwards-p-of-twisted-edwards-mul
  (implies (and (twisted-edwards-curve-completep curve)
                (pointp point)
                (point-on-twisted-edwards-p point curve))
           (b* ((?point1 (twisted-edwards-mul scalar point curve)))
             (point-on-twisted-edwards-p point1 curve))))

Theorem: twisted-edwards-mul-of-0

(defthm twisted-edwards-mul-of-0
  (equal (twisted-edwards-mul 0 point curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-of-1

(defthm twisted-edwards-mul-of-1
  (implies (point-on-twisted-edwards-p point curve)
           (equal (twisted-edwards-mul 1 point curve)
                  (point-fix point))))

Theorem: twisted-edwards-mul-of-zero

(defthm twisted-edwards-mul-of-zero
  (equal (twisted-edwards-mul scalar (twisted-edwards-zero)
                              curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-of-minus1

(defthm twisted-edwards-mul-of-minus1
  (implies (point-on-twisted-edwards-p point curve)
           (equal (twisted-edwards-mul -1 point curve)
                  (twisted-edwards-neg point curve))))

Theorem: twisted-edwards-neg-of-mul

(defthm twisted-edwards-neg-of-mul
 (implies
  (and (twisted-edwards-curve-completep curve)
       (pointp point)
       (point-on-twisted-edwards-p point curve))
  (equal
       (twisted-edwards-neg (twisted-edwards-mul scalar point curve)
                            curve)
       (twisted-edwards-mul (- (ifix scalar))
                            point curve))))

Theorem: twisted-edwards-mul-of-ifix-scalar

(defthm twisted-edwards-mul-of-ifix-scalar
  (equal (twisted-edwards-mul (ifix scalar)
                              point curve)
         (twisted-edwards-mul scalar point curve)))

Theorem: twisted-edwards-mul-int-equiv-congruence-on-scalar

(defthm twisted-edwards-mul-int-equiv-congruence-on-scalar
  (implies (acl2::int-equiv scalar scalar-equiv)
           (equal (twisted-edwards-mul scalar point curve)
                  (twisted-edwards-mul scalar-equiv point curve)))
  :rule-classes :congruence)

Theorem: twisted-edwards-mul-of-point-fix-point

(defthm twisted-edwards-mul-of-point-fix-point
  (equal (twisted-edwards-mul scalar (point-fix point)
                              curve)
         (twisted-edwards-mul scalar point curve)))

Theorem: twisted-edwards-mul-point-equiv-congruence-on-point

(defthm twisted-edwards-mul-point-equiv-congruence-on-point
  (implies (point-equiv point point-equiv)
           (equal (twisted-edwards-mul scalar point curve)
                  (twisted-edwards-mul scalar point-equiv curve)))
  :rule-classes :congruence)

Theorem: twisted-edwards-mul-of-twisted-edwards-curve-fix-curve

(defthm twisted-edwards-mul-of-twisted-edwards-curve-fix-curve
  (equal
       (twisted-edwards-mul scalar
                            point (twisted-edwards-curve-fix curve))
       (twisted-edwards-mul scalar point curve)))

Theorem: twisted-edwards-mul-twisted-edwards-curve-equiv-congruence-on-curve

(defthm
 twisted-edwards-mul-twisted-edwards-curve-equiv-congruence-on-curve
 (implies (twisted-edwards-curve-equiv curve curve-equiv)
          (equal (twisted-edwards-mul scalar point curve)
                 (twisted-edwards-mul scalar point curve-equiv)))
 :rule-classes :congruence)