Main definition of the Poseidon hash function.

See poseidon for an overview.

Poseidon is parameterized over a number of aspects,
such as the round constants, the MDS matrix, etc.
We capture all these parameters in the `param` data structure,
which also includes parameters for aspects that
are not explicitly described in the Poseidon paper
but that nevertheless need to be made precise in the definition.
Perhaps these latter aspects are disambiguated
by the reference implementation of Poseidon
(which is also linked from the aforementioned web site),
but it stil makes mathematical sense to parameterize the definition
over those aspects.
These are all described in detail in `param`.
The top-level functions of our specification of Poseidon
take a `param` as an input.

Poseidon uses a sponge construction, which is a more general concept.
In a sponge construction,
one can absorb any number of elements,
squeeze any number of elements,
and again absorb more elements and then squeeze them,
and so on.
We formalize this by explicating the state of the sponge in `sponge`,
which consists of not only the current vector of elements,
but also an index within the vector
where elements are absorbed or squeezed next,
and an indication of whether we are absorbing or squeezing;
this is described in more detail in `sponge`.
We define functions `absorb` and `squeeze`
to absorb and squeeze elements,
which take as input and return as output a sponge state,
besides the other natural inputs and outputs.
This is similar to some existing implementations of Poseidon.

The aforementioned `absorb` and `squeeze` functions
take or return multiple input or output elements.
If these functions were defined ``directly'',
they would be somewhat complicated because of the need to handle
a number of inputs or outputs that will start from the current index
and that may require one or more permutations and index wrap-arounds.
This is especially the case because, as described in `param`,
we support several different ways to absorb and squeeze elements.
To keep things simpler,
we define functions `absorb1` and `squeeze1`
that absorb or squeeze a single input or output element:
these are much simpler to define and understand,
even with the several different ways to absorb and squeeze elements.
Then we define `absorb` and `squeeze`
by simply iterating `absorb1` and `squeeze1`.

At the very top level, we define a function `hash`
that maps any number of inputs to any number of outputs.
This is defined by internally creating and using a sponge state.
Note that there is no need to include any explicit notion of padding,
which can be performed externally to Poseidon proper as defined here.

- Param
- Fixtype of Poseidon parameters.
- Hashp
- Hash according to just the Poseidon permutation.
- Absorb1
- Absorb one element into the sponge.
- Sponge
- Fixtype of sponge states.
- Hash
- Hash any number of inputs to any number of outputs.
- All-rounds
- Perform all the rounds in a permutation.
- Sponge-validp
- Check if a sponge state is valid with respect to given parameters.
- Squeeze1
- Squeeze one element from the sponge.
- Sub-words-partial
- Apply the partial S-box substitution to the state vector.
- Squeeze
- Squeeze any number of elements from the sponge.
- Round
- Perform a round.
- Partial-rounds
- Perform a sequence of partial rounds.
- Mode
- Fixtype of sponge modes.
- Full-rounds
- Perform a sequence of full rounds.
- Permute
- Permutation.
- Sub-words
- Apply the S-box substitution to the state vector.
- Add-round-constants
- Add round constants to the state vector.
- Mix-layer
- Multiply the MDS matrix and the state vector.
- Dot-product
- Dot product of a matrix row and the state vector.
- Absorb
- Absorb any number of elements into the sponge.
- Pow-by-alpha
- Raise a field element to the
\alpha power. - Param->size
- Size of the state vector, i.e.
r + c . - Sub-words-full
- Apply the full S-box substitution to the state vector.
- Param->capacity-then-rate-p
- Negation of the
`param->rate-then-capacity-p`parameter. - Param->partial-last-p
- Negation of the
`param->partial-first-p`parameter. - Param-additional-theorems
- Additional theorems about the parameters in
`param`. - Param->rounds
- Total number of rounds, i.e.
2 R_f + R_P = R_F + R_P . - Param->descending-p
- Negation of the
`param->ascending-p`parameter. - Init-sponge
- Initial sponge state.