The prime that is 1/8th of the order of BabyJubjub.
(baby-jubjub-order/8) → order/8
RFC 8032 says the order of the curve should be
so this looks suitable for the Edwards-Curve Digital Signature Algorithm (EdDSA).
Also, SafeCurves requires
This prime is
Function:
(defun baby-jubjub-order/8 nil (declare (xargs :guard t)) (let ((acl2::__function__ 'baby-jubjub-order/8)) (declare (ignorable acl2::__function__)) (primes::baby-jubjub-subgroup-prime)))
Theorem:
(defthm primep-of-baby-jubjub-order/8 (b* ((order/8 (baby-jubjub-order/8))) (dm::primep order/8)) :rule-classes :rewrite)