		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-mul

Scalar multiplication [ZPS:4.1.8], on Jubjub.

Signature
(jubjub-mul scalar point) → point1
Arguments: scalar — Guard (integerp scalar).; point — Guard (jubjub-pointp point).
Returns: point1 — Type (jubjub-pointp point1), given (jubjub-pointp point).

Definitions and Theorems

Function: jubjub-mul

(defun jubjub-mul (scalar point)
  (declare (xargs :guard (and (integerp scalar)
                              (jubjub-pointp point))))
  (let ((__function__ 'jubjub-mul))
    (declare (ignorable __function__))
    (ecurve::twisted-edwards-mul scalar point (jubjub-curve))))

Theorem: jubjub-pointp-of-jubjub-mul

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