		Search-engine friendly clone of the ACL2 documentation.

Baby-jubjub

Baby-jubjub-a

The coefficient a of the twisted Edwards equation of BabyJubjub.

Signature
(baby-jubjub-a) → a
Returns: a — Type (fep a (baby-jubjub-prime)).

This is not zero and is a square. We show that it is a square by exhibiting a square root, found using Mathematica's PowerMod.

Definitions and Theorems

Function: baby-jubjub-a

(defun baby-jubjub-a nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'baby-jubjub-a))
    (declare (ignorable acl2::__function__))
    168700))

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

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

Theorem: baby-jubjub-a-not-zero

(defthm baby-jubjub-a-not-zero
  (not (equal (baby-jubjub-a) 0)))

Theorem: pfield-squarep-of-baby-jubjub-a

(defthm pfield-squarep-of-baby-jubjub-a
  (pfield-squarep (baby-jubjub-a)
                  (baby-jubjub-prime)))