Jubjub-abst
The function \mathsf{abst}_\mathbb{J} [ZPS:5.4.9.3].
- Signature
(jubjub-abst bits) → point?
- Arguments
- bits — Guard (bit-listp bits).
- Returns
- point? — Type (maybe-jubjub-pointp point?).
The definition in [ZPS] takes a square root u at some point,
which may or may not exist; if it does, it is not exactly specified.
So we use ecurve::pfield-squarep and pfield-square->root.
It should be the case that the definition
does not depend on the exact square root chosen;
we should prove that eventually.
Note that, when u = 0 and \tilde{u} = 1
(which happens, for instance, when the input bit sequence is
(1 0 ... 0 1), i.e. 254 zeros surrounded by ones),
the prescribed result is (q_\mathbb{J}, 1) in [ZPS].
However, we need to reduce that modulo q_\mathbb{J},
in order for it to be a field element in our model.
For simplicity, we do the reduction in all cases,
which always coerces an integer to the corresponding field element;
we do that via the field negation operation, to ease proofs.
To prove that this returns an optional Jubjub point,
we locally prove a key lemma, returns-lemma.
It says that, when the square of u is
the argument of the square root as used in the definition,
(u,v) is on the curve:
this is easily proved by simple algebraic manipulations,
which turn the equality of the square into the curve equation.
Definitions and Theorems
Function: jubjub-abst
(defun jubjub-abst (bits)
(declare (xargs :guard (bit-listp bits)))
(declare (xargs :guard (= (len bits) *jubjub-l*)))
(let ((__function__ 'jubjub-abst))
(declare (ignorable __function__))
(b* ((q (jubjub-q))
(a (jubjub-a))
(d (jubjub-d))
(v* (butlast bits 1))
(u~ (car (last bits)))
(v (lebs2ip v*))
((when (>= v q)) nil)
(a-d.v^2 (sub a (mul d (mul v v q) q) q))
((when (equal a-d.v^2 0)) nil)
(u^2 (div (sub 1 (mul v v q) q) a-d.v^2 q))
((unless (ecurve::pfield-squarep u^2 q))
nil)
(u (ecurve::pfield-square->root u^2 q)))
(if (= (mod u 2) u~)
(ecurve::point-finite u v)
(ecurve::point-finite (neg u q) v)))))
Theorem: maybe-jubjub-pointp-of-jubjub-abst
(defthm maybe-jubjub-pointp-of-jubjub-abst
(b* ((point? (jubjub-abst bits)))
(maybe-jubjub-pointp point?))
:rule-classes :rewrite)
