size_t_x2
libcrux_sha3_generic_keccak_KeccakState_17 *self, size_t_x2 index) {
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)1U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)2U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)3U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
&old, (KRML_CLITERAL(size_t_x2){.fst = (size_t)4U,
self, (KRML_CLITERAL(size_t_x2){.fst = i1, .snd = j}))[0U],
(KRML_CLITERAL(size_t_x2){
(KRML_CLITERAL(size_t_x2){
self, (KRML_CLITERAL(size_t_x2){.fst = (size_t)0U,