The function
(edwards-bls12-point->v point) → v
This function can be defined on any finite point (in fact, on any pair), but it is only used on Edwards-BLS12 points.
This is always below the Edwards-BLS12 field prime.
Function:
(defun edwards-bls12-point->v (point) (declare (xargs :guard (edwards-bls12-pointp point))) (let ((acl2::__function__ 'edwards-bls12-point->v)) (declare (ignorable acl2::__function__)) (point-finite->y point)))
Theorem:
(defthm natp-of-edwards-bls12-point->v (b* ((v (edwards-bls12-point->v point))) (natp v)) :rule-classes :type-prescription)
Theorem:
(defthm edwards-bls12-point->v-upper-bound (implies (edwards-bls12-pointp point) (b* ((?v (edwards-bls12-point->v point))) (< v (edwards-bls12-q)))) :rule-classes :linear)