		Search-engine friendly clone of the ACL2 documentation.

Baby-jubjub

Baby-jubjub-order/8

The prime that is 1/8th of the order of BabyJubjub.

Signature
(baby-jubjub-order/8) → order/8
Returns: order/8 — Type (dm::primep order/8).

RFC 8032 says the order of the curve should be 2^c l where l is a large prime. The prime factorization of baby-jubjub-order is

2^3 \times
     2736030358979909402780800718157159386076813972158567259200215660948447373041

so this looks suitable for the Edwards-Curve Digital Signature Algorithm (EdDSA).

Also, SafeCurves requires l to be at least 2^200. The length of this prime is 251.

This prime is primes::baby-jubjub-subgroup-prime, but we introduce a shorter synonym for it here, which conveys that it is the BabyJubjub order divided by 8.

Definitions and Theorems

Function: baby-jubjub-order/8

(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: primep-of-baby-jubjub-order/8

(defthm primep-of-baby-jubjub-order/8
  (b* ((order/8 (baby-jubjub-order/8)))
    (dm::primep order/8))
  :rule-classes :rewrite)