		Search-engine friendly clone of the ACL2 documentation.

Poseidon-rate-2-alpha-17

Hash2-many

Hash any reasonable number of inputs to any number of outputs using RATE=2

Signature
(hash2-many inputs count) → outputs
Arguments: inputs — Guard (fe-listp inputs primes::*bls12-377-scalar-field-prime*).; count — Guard (natp count).
Returns: outputs — Type (fe-listp outputs primes::*bls12-377-scalar-field-prime*).

The inputs and outputs are field elements.

This interface function prepends a domain-separation field element and a field element whose value is the remaining number of inputs, and then calls the main hash function.

The number of inputs must be less than the field size so that the length field is expressable.

Definitions and Theorems

Function: hash2-many

(defun hash2-many (inputs count)
 (declare
  (xargs
       :guard (and (fe-listp inputs
                             primes::*bls12-377-scalar-field-prime*)
                   (natp count))))
 (declare
      (xargs :guard (fep (len inputs)
                         primes::*bls12-377-scalar-field-prime*)))
 (let ((__function__ 'hash2-many))
   (declare (ignorable __function__))
   (let ((preimage-and-inputs (cons (rate-2-domain-fe)
                                    (cons (len inputs) inputs))))
     (hash preimage-and-inputs
           (rate-2-alpha-17-parameters)
           count))))

Theorem: fe-listp-of-hash2-many

(defthm fe-listp-of-hash2-many
  (b* ((outputs (hash2-many inputs count)))
    (fe-listp outputs
              primes::*bls12-377-scalar-field-prime*))
  :rule-classes :rewrite)

Theorem: true-listp-of-hash2-many

(defthm true-listp-of-hash2-many
  (b* ((outputs (hash2-many inputs count)))
    (true-listp outputs))
  :rule-classes :type-prescription)

Theorem: len-of-hash2-many

(defthm len-of-hash2-many
  (b* ((?outputs (hash2-many inputs count)))
    (equal (len outputs) (nfix count))))