		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Group-hash

The function \mathsf{GroupHash_\mathsf{URS}^{\mathbb{J}^{(r)*}}} [ZPS:5.4.9.5].

Signature
(group-hash d m) → point?
Arguments: d — Guard (byte-listp d).; m — Guard (byte-listp m).
Returns: point? — Type (maybe-jubjub-pointp point?).

[ZPS] allows the argument M to have any length, but there is a (large) limit (see guard of blake2s-256). The limit here must be diminished by 64, which is the length of \mathsf{URS}.

Definitions and Theorems

Function: group-hash

(defun group-hash (d m)
 (declare (xargs :guard (and (byte-listp d) (byte-listp m))))
 (declare (xargs :guard (and (= (len d) 8)
                             (<= (len m)
                                 (- blake::*max-input-bytes* 64)))))
 (let ((__function__ 'group-hash))
   (declare (ignorable __function__))
   (b* ((hash (blake2s-256 d (append *urs* m)))
        (point (jubjub-abst (leos2bsp hash)))
        ((unless (jubjub-pointp point)) nil)
        (qoint (jubjub-mul (jubjub-h) point))
        ((when (equal qoint (twisted-edwards-zero)))
         nil))
     qoint)))

Theorem: maybe-jubjub-pointp-of-group-hash

(defthm maybe-jubjub-pointp-of-group-hash
  (b* ((point? (group-hash d m)))
    (maybe-jubjub-pointp point?))
  :rule-classes :rewrite)