		Search-engine friendly clone of the ACL2 documentation.

Jubjub-montgomery

Jubjub-montgomery-b

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

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

Definitions and Theorems

Function: jubjub-montgomery-b

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

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

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

Theorem: jubjub-montgomery-b-not-zero

(defthm jubjub-montgomery-b-not-zero
  (not (equal (jubjub-montgomery-b) 0)))