		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Hash

Hash any number of inputs to any number of outputs.

Signature
(hash inputs param count) → outputs
Arguments: inputs — Guard (fe-listp inputs (param->prime param)).; param — Guard (paramp param).; count — Guard (natp count).
Returns: outputs — Type (fe-listp outputs (param->prime param)).

We initialize the sponge, we absorb all the inputs, and we squeeze all the outputs.

Note that inputs that only differ in one input having more trailing zeros than the other and not exceeeding a multiple of the rate length result in the same outputs. For instance, if r is 10, the inputs (17), @'(17 0)'), (17 0 0), etc. (up to (17 0 0 0 0 0 0 0 0 0) yield the same output, because the initial state vector consists of all zeros, and absorbing a 0 does not change the corresponding element. Therefore, the ACL2 function defined here should not be normally used as a collision-resistant hash; instead, a caller of this function should use padding, or other techniques like domain separation, to supply input strings that do not lead to the aforementioned collisions. The exact nature of these techniques is application-dependent; Poseidon itself does not appear to prescribe particular techniques.

Definitions and Theorems

Function: hash

(defun hash (inputs param count)
  (declare
       (xargs :guard (and (paramp param)
                          (natp count)
                          (fe-listp inputs (param->prime param)))))
  (let ((__function__ 'hash))
    (declare (ignorable __function__))
    (b* ((sponge (init-sponge (param->size param)))
         (sponge (absorb inputs sponge param))
         ((mv outputs &)
          (squeeze count sponge param)))
      outputs)))

Theorem: fe-listp-of-hash

(defthm fe-listp-of-hash
  (b* ((outputs (hash inputs param count)))
    (fe-listp outputs (param->prime param)))
  :rule-classes :rewrite)

Theorem: true-listp-of-hash

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

Theorem: len-of-hash

(defthm len-of-hash
  (b* ((?outputs (hash inputs param count)))
    (equal (len outputs) (nfix count))))

Theorem: consp-of-hash

(defthm consp-of-hash
  (b* ((?outputs (hash inputs param count)))
    (equal (consp outputs)
           (< 0 (nfix count)))))