		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Coordinate-extract

The function \mathsf{Extract}_{\mathbb{J}^{(r)}} [ZPS:5.4.9.4].

Signature
(coordinate-extract point) → bits
Arguments: point — Guard (jubjub-pointp point).
Returns: bits — Type (bit-listp bits).

[ZPS] defines this on \mathbb{J}^{(r)}, not all of \mathbb{J}, but for now we define it on all of \mathbb{J} because we do not have an ACL2 definition of \mathbb{J}^{(r)} yet, and in fact the function is well-defined on all of \mathbb{J}.

Definitions and Theorems

Function: coordinate-extract

(defun coordinate-extract (point)
  (declare (xargs :guard (jubjub-pointp point)))
  (let ((__function__ 'coordinate-extract))
    (declare (ignorable __function__))
    (i2lebsp *l-merkle-sapling*
             (jubjub-point->u point))))

Theorem: bit-listp-of-coordinate-extract

(defthm bit-listp-of-coordinate-extract
  (b* ((bits (coordinate-extract point)))
    (bit-listp bits))
  :rule-classes :rewrite)

Theorem: len-of-coordinate-extract

(defthm len-of-coordinate-extract
  (b* ((?bits (coordinate-extract point)))
    (equal (len bits) *l-merkle-sapling*)))