		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-add

Group addition on Edwards-BLS12.

Signature
(edwards-bls12-add point1 point2) → point
Arguments: point1 — Guard (edwards-bls12-pointp point1).; point2 — Guard (edwards-bls12-pointp point2).
Returns: point — Type (edwards-bls12-pointp point), given (and (edwards-bls12-pointp point1) (edwards-bls12-pointp point2)).

Definitions and Theorems

Function: edwards-bls12-add

(defun edwards-bls12-add (point1 point2)
  (declare (xargs :guard (and (edwards-bls12-pointp point1)
                              (edwards-bls12-pointp point2))))
  (let ((acl2::__function__ 'edwards-bls12-add))
    (declare (ignorable acl2::__function__))
    (twisted-edwards-add point1 point2 (edwards-bls12-curve))))

Theorem: edwards-bls12-pointp-of-edwards-bls12-add

(defthm edwards-bls12-pointp-of-edwards-bls12-add
  (implies (and (edwards-bls12-pointp point1)
                (edwards-bls12-pointp point2))
           (b* ((point (edwards-bls12-add point1 point2)))
             (edwards-bls12-pointp point)))
  :rule-classes :rewrite)