		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-mul

Scalar multiplication on Edwards-BLS12.

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

Definitions and Theorems

Function: edwards-bls12-mul

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

Theorem: edwards-bls12-pointp-of-edwards-bls12-mul

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