Fast scalar multiplication in the twisted Edwards group.
(twisted-edwards-mul-fast scalar point curve) → point1
This is the same as twisted-edwards-mul but using
only doubling and addition in order to reduce the execution time to
In the future we will either replace the body of
Function:
(defun twisted-edwards-mul-fast-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-fast-nonneg)) (declare (ignorable acl2::__function__)) (if (zp scalar) (twisted-edwards-zero) (if (evenp scalar) (let ((half-scalar-mul (twisted-edwards-mul-fast-nonneg (/ scalar 2) point curve))) (twisted-edwards-add half-scalar-mul half-scalar-mul curve)) (twisted-edwards-add point (twisted-edwards-mul-fast-nonneg (- scalar 1) point curve) curve)))))
Theorem:
(defthm pointp-of-twisted-edwards-mul-fast-nonneg (b* ((point1 (twisted-edwards-mul-fast-nonneg scalar point curve))) (pointp point1)) :rule-classes :rewrite)
Theorem:
(defthm point-on-twisted-edwards-p-of-twisted-edwards-mul-fast-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-fast-nonneg scalar point curve) curve)))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-of-0 (equal (twisted-edwards-mul-fast-nonneg 0 point curve) (twisted-edwards-zero)))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-of-1 (implies (point-on-twisted-edwards-p point curve) (equal (twisted-edwards-mul-fast-nonneg 1 point curve) (point-fix point))))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-of-zero (equal (twisted-edwards-mul-fast-nonneg scalar (twisted-edwards-zero) curve) (twisted-edwards-zero)))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-of-nfix-scalar (equal (twisted-edwards-mul-fast-nonneg (nfix scalar) point curve) (twisted-edwards-mul-fast-nonneg scalar point curve)))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-nat-equiv-congruence-on-scalar (implies (nat-equiv scalar scalar-equiv) (equal (twisted-edwards-mul-fast-nonneg scalar point curve) (twisted-edwards-mul-fast-nonneg scalar-equiv point curve))) :rule-classes :congruence)
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-of-point-fix-point (equal (twisted-edwards-mul-fast-nonneg scalar (point-fix point) curve) (twisted-edwards-mul-fast-nonneg scalar point curve)))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-point-equiv-congruence-on-point (implies (point-equiv point point-equiv) (equal (twisted-edwards-mul-fast-nonneg scalar point curve) (twisted-edwards-mul-fast-nonneg scalar point-equiv curve))) :rule-classes :congruence)
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-of-twisted-edwards-curve-fix-curve (equal (twisted-edwards-mul-fast-nonneg scalar point (twisted-edwards-curve-fix curve)) (twisted-edwards-mul-fast-nonneg scalar point curve)))
Theorem:
(defthm twisted-edwards-mul-fast-nonneg-twisted-edwards-curve-equiv-congruence-on-curve (implies (twisted-edwards-curve-equiv curve curve-equiv) (equal (twisted-edwards-mul-fast-nonneg scalar point curve) (twisted-edwards-mul-fast-nonneg scalar point curve-equiv))) :rule-classes :congruence)
Function:
(defun twisted-edwards-mul-fast (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-fast)) (declare (ignorable acl2::__function__)) (b* ((scalar (ifix scalar))) (if (>= scalar 0) (twisted-edwards-mul-fast-nonneg scalar point curve) (twisted-edwards-neg (twisted-edwards-mul-fast-nonneg (- scalar) point curve) curve)))))
Theorem:
(defthm pointp-of-twisted-edwards-mul-fast (b* ((point1 (twisted-edwards-mul-fast scalar point curve))) (pointp point1)) :rule-classes :rewrite)
Theorem:
(defthm point-on-twisted-edwards-p-of-twisted-edwards-mul-fast (implies (and (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve)) (b* ((?point1 (twisted-edwards-mul-fast scalar point curve))) (point-on-twisted-edwards-p point1 curve))))
Theorem:
(defthm twisted-edwards-mul-fast-of-0 (equal (twisted-edwards-mul-fast 0 point curve) (twisted-edwards-zero)))
Theorem:
(defthm twisted-edwards-mul-fast-of-1 (implies (point-on-twisted-edwards-p point curve) (equal (twisted-edwards-mul-fast 1 point curve) (point-fix point))))
Theorem:
(defthm twisted-edwards-mul-fast-of-zero (equal (twisted-edwards-mul-fast scalar (twisted-edwards-zero) curve) (twisted-edwards-zero)))
Theorem:
(defthm twisted-edwards-mul-fast-of-minus1 (implies (point-on-twisted-edwards-p point curve) (equal (twisted-edwards-mul-fast -1 point curve) (twisted-edwards-neg point curve))))
Theorem:
(defthm twisted-edwards-neg-of-mul-fast (implies (and (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve)) (equal (twisted-edwards-neg (twisted-edwards-mul-fast scalar point curve) curve) (twisted-edwards-mul-fast (- (ifix scalar)) point curve))))
Theorem:
(defthm twisted-edwards-mul-fast-of-ifix-scalar (equal (twisted-edwards-mul-fast (ifix scalar) point curve) (twisted-edwards-mul-fast scalar point curve)))
Theorem:
(defthm twisted-edwards-mul-fast-int-equiv-congruence-on-scalar (implies (acl2::int-equiv scalar scalar-equiv) (equal (twisted-edwards-mul-fast scalar point curve) (twisted-edwards-mul-fast scalar-equiv point curve))) :rule-classes :congruence)
Theorem:
(defthm twisted-edwards-mul-fast-of-point-fix-point (equal (twisted-edwards-mul-fast scalar (point-fix point) curve) (twisted-edwards-mul-fast scalar point curve)))
Theorem:
(defthm twisted-edwards-mul-fast-point-equiv-congruence-on-point (implies (point-equiv point point-equiv) (equal (twisted-edwards-mul-fast scalar point curve) (twisted-edwards-mul-fast scalar point-equiv curve))) :rule-classes :congruence)
Theorem:
(defthm twisted-edwards-mul-fast-of-twisted-edwards-curve-fix-curve (equal (twisted-edwards-mul-fast scalar point (twisted-edwards-curve-fix curve)) (twisted-edwards-mul-fast scalar point curve)))
Theorem:
(defthm twisted-edwards-mul-fast-twisted-edwards-curve-equiv-congruence-on-curve (implies (twisted-edwards-curve-equiv curve curve-equiv) (equal (twisted-edwards-mul-fast scalar point curve) (twisted-edwards-mul-fast scalar point curve-equiv))) :rule-classes :congruence)