Hashp
Hash according to just the Poseidon permutation.
- Signature
(hashp 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)), given (and (paramp param)
(fe-listp inputs (param->prime param))
(<= (len inputs) (param->size param))
(<= count (param->size param)))
.
Some applications do not use the Poseidon sponge,
but instead just use the Poseidon permutation.
That is, given r + c or fewer field elements,
which fit into a Poseidon state vector,
we can apply permute,
obtain an output state vector of r + c field elements,
and select possibly all or a prefix of them.
Since a single field element may consist of hundreds of bits,
just a few field elements (even just one)
may well suffice as inputs and outputs for certain applications.
This ACL2 function formalizes this hash based on just the permutation;
the p in the name of hashp conveys that.
The function has guards limiting the number of inputs and outputs.
If there are fewer than r + c inputs,
we pad them with zeros,
in line with the full Poseidon sponge.
Poseidon itself prescribes no padding,
which is application-dependent,
and can be applied prior to calling this ACL2 function;
if exactly r + c field elements are passed to this function,
this function does not add any padding zeros.
Since permute takes as input
the full Poseidon parameters param,
this hashp function also takes them as input.
However, as in permute, not all of the parameters are needed,
namely the ones related to the sponge like ascending-p.
Additionally, the permutation only depends on param->size,
not on the specifics of rate r and capacity c (just their sum).
We may consider changing permute and this function
to only take the necessary parameters at some point.
Definitions and Theorems
Function: hashp
(defun hashp (inputs param count)
(declare
(xargs :guard (and (paramp param)
(natp count)
(fe-listp inputs (param->prime param)))))
(declare (xargs :guard (and (<= (len inputs) (param->size param))
(<= count (param->size param)))))
(let ((__function__ 'hashp))
(declare (ignorable __function__))
(b* ((stat (append inputs
(repeat (- (param->size param) (len inputs))
0)))
(new-stat (permute stat param)))
(take count new-stat))))
Theorem: fe-listp-of-hashp
(defthm fe-listp-of-hashp
(implies (and (paramp param)
(fe-listp inputs (param->prime param))
(<= (len inputs) (param->size param))
(<= count (param->size param)))
(b* ((outputs (hashp inputs param count)))
(fe-listp outputs (param->prime param))))
:rule-classes :rewrite)
Theorem: true-listp-of-hashp
(defthm true-listp-of-hashp
(b* ((outputs (hashp inputs param count)))
(true-listp outputs))
:rule-classes :type-prescription)
Theorem: len-of-hashp
(defthm len-of-hashp
(b* ((?outputs (hashp inputs param count)))
(equal (len outputs) (nfix count))))
