		Search-engine friendly clone of the ACL2 documentation.

Poseidon-rate-4-alpha-17

Hash4

Hash any reasonable number of inputs to a single field output using RATE=4

Signature
(hash4 inputs) → output
Arguments: inputs — Guard (fe-listp inputs primes::*bls12-377-scalar-field-prime*).
Returns: output — Type (fep output primes::*bls12-377-scalar-field-prime*).

The inputs and output are field elements.

This interface function prepends a domain-separation field element and a remaining input-length field element, and then calls the main hash function with an output count of 1.

The number of inputs must be less than the field size.

Definitions and Theorems

Function: hash4

(defun hash4 (inputs)
 (declare
   (xargs :guard (fe-listp inputs
                           primes::*bls12-377-scalar-field-prime*)))
 (declare
      (xargs :guard (fep (len inputs)
                         primes::*bls12-377-scalar-field-prime*)))
 (let ((__function__ 'hash4))
   (declare (ignorable __function__))
   (first (hash4-many inputs 1))))

Theorem: fep-of-hash4

(defthm fep-of-hash4
  (b* ((output (hash4 inputs)))
    (fep output
         primes::*bls12-377-scalar-field-prime*))
  :rule-classes :rewrite)