Fixtype of Poseidon parameters.

This is a product type introduced by fty::defprod.

- prime — prime
- rate — posp
- capacity — posp
- alpha — integerp
- full-rounds-half — natp
- partial-rounds — natp
- constants
- mds
- rate-then-capacity-p — booleanp
- ascending-p — booleanp
- partial-first-p — booleanp

The following invariant is enforced on the fields:

(and (fe-list-listp constants prime) (all-len-equal-p constants (+ rate capacity)) (equal (len constants) (+ (* 2 full-rounds-half) partial-rounds)) (fe-list-listp mds prime) (all-len-equal-p mds (+ rate capacity)) (equal (len mds) (+ rate capacity)))

Our definition of Poseidon is parameterized over the following aspects:

- A prime number
p , which defines the prime field\mathbb{F}_p . - The rate
r , i.e. the number of the elements in the state vector against which inputs and outputs are absorbed or squeezed. This is a positive integer. - The capacity
c , i.e. the number of the elements in the state vector that participate in the permutations but against which inputs and output are not absorbed or squeezed. This is a positive integer. - The exponent
\alpha used in the S-boxes. This is normally taken from a small set of integers, all positive except for -1, also based on the primep . Mathematically, S-boxes can be defined with any integer\alpha , and thus we allow any integer. For negative integers, we map 0 to 0, as done for the choice of -1 described in the paper. - The number
R_f of full rounds before and after the partial rounds, which is half of the total number of full roundsR_F . This should be a positive integer, but mathematically we can define Poseidon even if this is 0 (i.e. no full rounds), so we allow any natural number. - The number
R_P of partial rounds. This should be a positive integer, but mathematically we can define Poseidon even if this is 0 (i.e. no partial rounds), so we allow any natural number. - The constants to add to the state vector as part of the permutation.
These are organized as a list of lists of field elements.
Each element of the outer list corresponds to a round,
so the length of the outer list is
R_F + R_P (i.e.2 R_f + R_P ). Each inner list hasr + c elements, which matches the length of the state vector. - The MDS matrix, which is organized as a list of lists of field elements.
(MDS stands for Maximum Distance Separable, but we do not describe here
how the matrix is constructed.)
This is a square matrix, so the length of the outer list is
r + c and each inner list has also lengthr + c . We can equivalently view this as a list of rows or columns; if rows, we must view the state as a column vector; if columns, we must the state as a row vector. The multiplication between the matrix and the vector gives the same result (viewed either as column or row vector). - The state is represented as a list in ACL2.
The state has two parts, corresponding to the
r andc elements. Looking at the ACL2 list, we could have either the former before the latter or the latter before the former:+------------------+--------------+| r elements | c elements |+------------------+--------------++--------------+------------------+| c elements | r elements |+--------------+------------------+

So we include a boolean parameter that says whether, in the ACL2 list, the rate elements come before the capacity elements or vice versa. - Regardless of the choice described just above, there is another choice,
namely the direction in which inputs or outputs
are absorbed or squeezed against the
r elements of the state, which also form an ACL2 list (sublist of the state vector). We can either absorb or squeeze them with ascending list indices, or with descending list indices. In other words, in the illustrations above, we either go rightward (if ascending) or leftward (if descending). So we introduce a parameter for this choice. - In a partial round, the S-box is applied only to one element of the state. The element is at one end of the state vector, but it could be either the first or the last element in the ACL2 list. So we introduce a parameter for this choice. Mathematically, we could generalize this to an arbitrary position within the state vector; we could even generalize full and partial rounds to sets of indices; however, at this time this generality seems unnecessary.

- Param-fix
- Fixing function for param structures.
- Paramp
- Recognizer for param structures.
- Make-param
- Basic constructor macro for param structures.
- Param->prime
- Get the
`prime`field from a param. - Param-equiv
- Basic equivalence relation for param structures.
- Param->rate-then-capacity-p
- Get the
`rate-then-capacity-p`field from a param. - Param->partial-first-p
- Get the
`partial-first-p`field from a param. - Change-param
- Modifying constructor for param structures.
- Param->full-rounds-half
- Get the
`full-rounds-half`field from a param. - Param->constants
- Get the
`constants`field from a param. - Param->ascending-p
- Get the
`ascending-p`field from a param. - Param->partial-rounds
- Get the
`partial-rounds`field from a param. - Param->mds
- Get the
`mds`field from a param. - Param->capacity
- Get the
`capacity`field from a param. - Param->rate
- Get the
`rate`field from a param. - Param->alpha
- Get the
`alpha`field from a param.