|
|
|---|
|
|
|
|---|
A Jubjub point with 0 ordinate is not in jubjub-r-pointp.
This indirectly depends on the associativity of twisted Edwards addition, so we add that as a hypothesis (see ecurve::twisted-edwards-add-associativity).
From the curve equation and the fact that the ordinate is 0,
it turns out that doubling the point yields point-0-m1.
Thus multiplying the point by 4 yields the zero point,
and therefore the point does not have order jubjub-r.
The point itself is not the zero point, which is
This is part of Theorem 5.4.3 in [ZPS].
Theorem:
(defthm not-jubjub-r-pointp-when-0-ordinate (implies (and (ecurve::twisted-edwards-add-associativity) (jubjub-pointp point) (equal (jubjub-point->v point) 0)) (not (jubjub-r-pointp point))) :rule-classes :rewrite)