		Search-engine friendly clone of the ACL2 documentation.

Poseidon-rate-4-alpha-17

Hash4-many

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

Signature
(hash4-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 RATE elements to the input to construct the preimage: [ DOMAIN || LENGTH(INPUT) || [0; RATE-2] || INPUT ], 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: hash4-many

(defun hash4-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__ 'hash4-many))
   (declare (ignorable __function__))
   (let ((preimage-and-inputs
              (cons (rate-4-domain-fe)
                    (cons (len inputs)
                          (append (repeat 2 0) inputs)))))
     (hash preimage-and-inputs
           (rate-4-alpha-17-parameters)
           count))))

Theorem: fe-listp-of-hash4-many

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

Theorem: true-listp-of-hash4-many

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

Theorem: len-of-hash4-many

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