		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-point-satisfies-curve-equation

A Jubjub point satisfies the curve equation.

Definitions and Theorems

Theorem: jubjub-point-satisfies-curve-equation

(defthm jubjub-point-satisfies-curve-equation
  (implies (jubjub-pointp uv)
           (b* ((u (jubjub-point->u uv))
                (v (jubjub-point->v uv))
                (u^2 (mul u u (jubjub-q)))
                (v^2 (mul v v (jubjub-q)))
                (u^2.v^2 (mul u^2 v^2 (jubjub-q)))
                (a.u^2 (mul (jubjub-a) u^2 (jubjub-q)))
                (d.u^2.v^2 (mul (jubjub-d) u^2.v^2 (jubjub-q))))
             (equal (add a.u^2 v^2 (jubjub-q))
                    (add 1 d.u^2.v^2 (jubjub-q))))))