libcrux_sha3_portable_keccak_zero_5a
lit.st[0U][0U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[0U][1U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[0U][2U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[0U][3U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[0U][4U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[1U][0U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[1U][1U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[1U][2U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[1U][3U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[1U][4U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[2U][0U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[2U][1U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[2U][2U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[2U][3U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[2U][4U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[3U][0U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[3U][1U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[3U][2U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[3U][3U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[3U][4U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[4U][0U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[4U][1U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[4U][2U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[4U][3U] = libcrux_sha3_portable_keccak_zero_5a();
lit.st[4U][4U] = libcrux_sha3_portable_keccak_zero_5a();