		Search-engine friendly clone of the ACL2 documentation.

Baby-jubjub

Baby-jubjub-order

Order (i.e. number of points) of the BabyJubjub curve.

Signature
(baby-jubjub-order) → order
Returns: order — Type (natp order).

BabyJubjub, as the twisted Edwards curve with a = 168700 and d = 168696, is birationally equivalent to the Montgomery curve with

\begin{array}{l}
     A = 2(a+d)/(a-d) = 2*(168700 + 168696)/(168700 - 168696) = 168698
     \\
     B = 4/(a-d) = 1
     \end{array}

So the Montgomery curve is

y^2 = x^3 + 168698x^2 + x

Now, represent that in Weierstrass form:

y^2 + a_1 x y + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6

We have:

[a_1, a_2, a_3, a_4, a_6] = [0, 168698, 0, 1, 0]

In Sage, which can be used at https://sagecell.sagemath.org, type this Sage code:

P = 21888242871839275222246405745257275088548364400416034343698204186575808495617
E = EllipticCurve(GF(P),[0,168698,0,1,0])
E.cardinality()

Clicking the `Evaluate' button will yield BabyJubjub order.

Definitions and Theorems

Function: baby-jubjub-order

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

Theorem: natp-of-baby-jubjub-order

(defthm natp-of-baby-jubjub-order
  (b* ((order (baby-jubjub-order)))
    (natp order))
  :rule-classes :rewrite)