		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-add

Group addition [ZPS:4.1.8], on Jubjub.

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

Definitions and Theorems

Function: jubjub-add

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

Theorem: jubjub-pointp-of-jubjub-add

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