The function
(edwards-bls12-point->u point) → u
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->u (point) (declare (xargs :guard (edwards-bls12-pointp point))) (let ((acl2::__function__ 'edwards-bls12-point->u)) (declare (ignorable acl2::__function__)) (point-finite->x point)))
Theorem:
(defthm natp-of-edwards-bls12-point->u (b* ((u (edwards-bls12-point->u point))) (natp u)) :rule-classes :type-prescription)
Theorem:
(defthm edwards-bls12-point->u-upper-bound (implies (edwards-bls12-pointp point) (b* ((acl2::?u (edwards-bls12-point->u point))) (< u (edwards-bls12-q)))) :rule-classes :linear)