		Search-engine friendly clone of the ACL2 documentation.

Baby-jubjub

Baby-jubjub-d

The coefficient d of the twisted Edwards equation of BabyJubjub.

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

This is not zero, is different from a, and is not a square. We show that it is not a square using Euler's criterion: we use the fast modular exponentiation operation from the arithmetic-3 library to calculate the modular exponentiation of the coefficient, which must be different from 1 in order for the criterion to apply.

Definitions and Theorems

Function: baby-jubjub-d

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

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

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

Theorem: baby-jubjub-d-not-zero

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

Theorem: baby-jubjub-d-not-equal-to-a

(defthm baby-jubjub-d-not-equal-to-a
  (not (equal (baby-jubjub-d)
              (baby-jubjub-a))))

Theorem: not-pfield-squarep-of-baby-jubjub-d

(defthm not-pfield-squarep-of-baby-jubjub-d
  (not (pfield-squarep (baby-jubjub-d)
                       (baby-jubjub-prime))))