		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-point->u

The function \mathcal{U} in [ZPS:5.4.9.4].

Signature
(jubjub-point->u point) → u
Arguments: point — Guard (jubjub-pointp point).
Returns: u — Type (natp u).

[ZPS] defines this function on any finite point (in fact, on any pair), but it is only used on Jubjub points.

This is always below the Jubjub field prime.

Definitions and Theorems

Function: jubjub-point->u

(defun jubjub-point->u (point)
  (declare (xargs :guard (jubjub-pointp point)))
  (let ((__function__ 'jubjub-point->u))
    (declare (ignorable __function__))
    (ecurve::point-finite->x point)))

Theorem: natp-of-jubjub-point->u

(defthm natp-of-jubjub-point->u
  (b* ((u (jubjub-point->u point)))
    (natp u))
  :rule-classes :type-prescription)

Theorem: jubjub-point->u-upper-bound

(defthm jubjub-point->u-upper-bound
  (implies (jubjub-pointp point)
           (b* ((acl2::?u (jubjub-point->u point)))
             (< u (jubjub-q))))
  :rule-classes :linear)

Theorem: fep-of-jubjub-point->u

(defthm fep-of-jubjub-point->u
  (implies (jubjub-pointp point)
           (b* ((acl2::?u (jubjub-point->u point)))
             (fep u (jubjub-q)))))