		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Find-group-hash

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

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

Since we need to append a byte to the message input, we need to diminish its maximum size by one in the guard.

Definitions and Theorems

Function: find-group-hash-loop

(defun find-group-hash-loop (i d m)
 (declare (xargs :guard (and (natp i)
                             (byte-listp d)
                             (byte-listp m))))
 (declare
      (xargs :guard (and (= (len d) 8)
                         (< (len m)
                            (- blake::*blake2s-max-data-byte-length*
                               129)))))
 (let ((__function__ 'find-group-hash-loop))
   (declare (ignorable __function__))
   (if (mbt (natp i))
       (if (< i 256)
           (b* ((point? (group-hash d (append m (list i)))))
             (or point?
                 (find-group-hash-loop (1+ i) d m)))
         nil)
     (acl2::impossible))))

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

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

Function: find-group-hash

(defun find-group-hash (d m)
 (declare (xargs :guard (and (byte-listp d) (byte-listp m))))
 (declare
      (xargs :guard (and (= (len d) 8)
                         (< (len m)
                            (- blake::*blake2s-max-data-byte-length*
                               129)))))
 (let ((__function__ 'find-group-hash))
   (declare (ignorable __function__))
   (find-group-hash-loop 0 d m)))

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

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