		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Param

Fixtype of Poseidon parameters.

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

Fields

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

Additional Requirements

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 prime p. 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 rounds R_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 has r + 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 length r + 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 and c 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.

Subtopics

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.