		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-mul

Scalar multiplication in the Montgomery group.

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

If the group were multiplicative, this would be exponentiation. Since the Montgomery 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.

To verify the guards of the recursive auxiliary function, we need to show that it returns a point on the curve, which follows from closure. However, to avoid putting the non-executable montgomery-add-closure in the guard of this function and all its callers, for now we check explicitly, in the function, that the recursive call returns a point on the curve. If it does not, we return an irrelevant point. This lets us verify the guards. Then we prove that, under the closure assumption, multiplication always returns a point on the curve.

Definitions and Theorems

Function: montgomery-mul-nonneg

(defun montgomery-mul-nonneg (scalar point curve)
  (declare (xargs :guard (and (natp scalar)
                              (pointp point)
                              (montgomery-curvep curve))))
  (declare (xargs :guard (point-on-montgomery-p point curve)))
  (let ((acl2::__function__ 'montgomery-mul-nonneg))
    (declare (ignorable acl2::__function__))
    (b* (((when (zp scalar)) (montgomery-zero))
         (point1 (montgomery-mul-nonneg (1- scalar)
                                        point curve))
         ((unless (point-on-montgomery-p point1 curve))
          (ec-call (point-fix :irrelevant))))
      (montgomery-add point point1 curve))))

Theorem: pointp-of-montgomery-mul-nonneg

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

Theorem: point-on-montgomery-p-of-montgomery-mul-nonneg

(defthm point-on-montgomery-p-of-montgomery-mul-nonneg
 (implies (and (montgomery-add-closure)
               (point-on-montgomery-p point curve))
          (b* ((?point1 (montgomery-mul-nonneg scalar point curve)))
            (point-on-montgomery-p point1 curve))))

Theorem: montgomery-mul-nonneg-of-0

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

Theorem: montgomery-mul-nonneg-of-1

(defthm montgomery-mul-nonneg-of-1
  (equal (montgomery-mul-nonneg 1 point curve)
         (point-fix point)))

Theorem: montgomery-mul-nonneg-of-zero

(defthm montgomery-mul-nonneg-of-zero
  (equal (montgomery-mul-nonneg scalar (montgomery-zero)
                                curve)
         (montgomery-zero)))

Theorem: montgomery-mul-nonneg-of-nfix-scalar

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

Theorem: montgomery-mul-nonneg-nat-equiv-congruence-on-scalar

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

Theorem: montgomery-mul-nonneg-of-point-fix-point

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

Theorem: montgomery-mul-nonneg-point-equiv-congruence-on-point

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

Theorem: montgomery-mul-nonneg-of-montgomery-curve-fix-curve

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

Theorem: montgomery-mul-nonneg-montgomery-curve-equiv-congruence-on-curve

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

Function: montgomery-mul

(defun montgomery-mul (scalar point curve)
  (declare (xargs :guard (and (integerp scalar)
                              (pointp point)
                              (montgomery-curvep curve))))
  (declare (xargs :guard (point-on-montgomery-p point curve)))
  (let ((acl2::__function__ 'montgomery-mul))
    (declare (ignorable acl2::__function__))
    (b* ((scalar (ifix scalar))
         ((when (>= scalar 0))
          (montgomery-mul-nonneg scalar point curve))
         (point1 (montgomery-mul-nonneg (- scalar)
                                        point curve))
         ((unless (point-on-montgomery-p point1 curve))
          (ec-call (point-fix :irrelevant))))
      (montgomery-neg point1 curve))))

Theorem: pointp-of-montgomery-mul

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

Theorem: point-on-montgomery-p-of-montgomery-mul

(defthm point-on-montgomery-p-of-montgomery-mul
  (implies (and (montgomery-add-closure)
                (point-on-montgomery-p point curve))
           (b* ((?point1 (montgomery-mul scalar point curve)))
             (point-on-montgomery-p point1 curve))))

Theorem: montgomery-mul-of-0

(defthm montgomery-mul-of-0
  (equal (montgomery-mul 0 point curve)
         (montgomery-zero)))

Theorem: montgomery-mul-of-1

(defthm montgomery-mul-of-1
  (equal (montgomery-mul 1 point curve)
         (point-fix point)))

Theorem: montgomery-mul-of-zero

(defthm montgomery-mul-of-zero
  (equal (montgomery-mul scalar (montgomery-zero)
                         curve)
         (montgomery-zero)))

Theorem: montgomery-mul-of-minus1

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

Theorem: montgomery-neg-of-mul

(defthm montgomery-neg-of-mul
 (implies (and (montgomery-add-closure)
               (point-on-montgomery-p point curve))
          (equal (montgomery-neg (montgomery-mul scalar point curve)
                                 curve)
                 (montgomery-mul (- (ifix scalar))
                                 point curve))))

Theorem: montgomery-mul-of-ifix-scalar

(defthm montgomery-mul-of-ifix-scalar
  (equal (montgomery-mul (ifix scalar)
                         point curve)
         (montgomery-mul scalar point curve)))

Theorem: montgomery-mul-int-equiv-congruence-on-scalar

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

Theorem: montgomery-mul-of-point-fix-point

(defthm montgomery-mul-of-point-fix-point
  (equal (montgomery-mul scalar (point-fix point)
                         curve)
         (montgomery-mul scalar point curve)))

Theorem: montgomery-mul-point-equiv-congruence-on-point

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

Theorem: montgomery-mul-of-montgomery-curve-fix-curve

(defthm montgomery-mul-of-montgomery-curve-fix-curve
  (equal (montgomery-mul scalar
                         point (montgomery-curve-fix curve))
         (montgomery-mul scalar point curve)))

Theorem: montgomery-mul-montgomery-curve-equiv-congruence-on-curve

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