		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-neg

Group negation, on Jubjub.

Signature
(jubjub-neg point) → -point
Arguments: point — Guard (jubjub-pointp point).
Returns: -point — Type (jubjub-pointp -point), given (jubjub-pointp point).

This is the inverse with respect to jubjub-add.

Definitions and Theorems

Function: jubjub-neg

(defun jubjub-neg (point)
  (declare (xargs :guard (jubjub-pointp point)))
  (let ((__function__ 'jubjub-neg))
    (declare (ignorable __function__))
    (ecurve::twisted-edwards-neg point (jubjub-curve))))

Theorem: jubjub-pointp-of-jubjub-neg

(defthm jubjub-pointp-of-jubjub-neg
  (implies (jubjub-pointp point)
           (b* ((-point (jubjub-neg point)))
             (jubjub-pointp -point)))
  :rule-classes :rewrite)