(twisted-edwards-mul-nonneg scalar point curve) → point1
Function:
(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:
(defthm pointp-of-twisted-edwards-mul-nonneg (b* ((point1 (twisted-edwards-mul-nonneg scalar point curve))) (pointp point1)) :rule-classes :rewrite)
Theorem:
(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:
(defthm twisted-edwards-mul-nonneg-of-0 (equal (twisted-edwards-mul-nonneg 0 point curve) (twisted-edwards-zero)))
Theorem:
(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:
(defthm twisted-edwards-mul-nonneg-of-zero (equal (twisted-edwards-mul-nonneg scalar (twisted-edwards-zero) curve) (twisted-edwards-zero)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)