Module LibResult.Poseidon

poseidon128_full_round ~matrix ~k (x0, y0, z0) returns [x1; y1; z1] where (x1, y1, z1) is the result of applying a (shifted) Poseidon full round (parametrized by matrix and k) to the 3-registers state (x0, y0, z0).

Here, matrix is a 3 x 3 matrix and k is a vector of 3 elements. Note that this is a shifted round, that is, the S-box is applied first, followed by the linear layer. Namely: (x1, y1, z1) = matrix * (x0^5, y0^5, z0^5) + k.

poseidon128_four_partial_rounds ~matrix ~k (x0, y0, z0) returns [x4; y4; z4] where (x4, y4, z4) is the result of applying four (shifted) Poseidon partial round (parametrized by matrix and ks) to the 3-registers state (x0, y0, z0).

Here, matrix is a 3 x 3 matrix and ks is an array of 4 vectors of 3 elements each (one vector for each of the 4 rounds).

In particular, for i = 1,...,4: (xi, yi, zi) = matrix * (x_{i-1}, y_{i-1}, z_{i-1}^5) + ki.