		Search-engine friendly clone of the ACL2 documentation.

Jubjub-montgomery

Jubjub-montgomery-a

The Jubjub coefficient A_\mathbb{M} [ZPS:A.2].

Signature
(jubjub-montgomery-a) → a
Returns: a — Type (fep a (jubjub-q)).

Definitions and Theorems

Function: jubjub-montgomery-a

(defun jubjub-montgomery-a nil
  (declare (xargs :guard t))
  (let ((__function__ 'jubjub-montgomery-a))
    (declare (ignorable __function__))
    40962))

Theorem: return-type-of-jubjub-montgomery-a

(defthm return-type-of-jubjub-montgomery-a
  (b* ((a (jubjub-montgomery-a)))
    (fep a (jubjub-q)))
  :rule-classes :rewrite)

Theorem: jubjub-montgomery-a-not-plus-two

(defthm jubjub-montgomery-a-not-plus-two
  (not (equal (jubjub-montgomery-a) 2)))

Theorem: jubjub-montgomery-a-not-minus-two

(defthm jubjub-montgomery-a-not-minus-two
  (not (equal (jubjub-montgomery-a)
              (neg 2 (jubjub-q)))))