Hash any reasonable number of inputs to any number of outputs using RATE=2
(hash2-many inputs count) → outputs
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.
Function:
(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:
(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:
(defthm true-listp-of-hash2-many (b* ((outputs (hash2-many inputs count))) (true-listp outputs)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-hash2-many (b* ((?outputs (hash2-many inputs count))) (equal (len outputs) (nfix count))))