		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-mul-nonneg

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

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)