Keccak proof

This implementation of Stark was taken from mir-protocol respectively LogicStark, KeccakSpongeStark. Keccak proof via zk-STARKs enables efficient verification of permutations as a part of building Keccak hashes that included in Patricia Merkle Trie and connect with other STARKs as Logic, KeccakSponge, Data while proving using CTL's.

Circuit

Private inputs include data fields about each value:

• input includes bytes for hashing

Columns that are used in trace rows generation:

• START_PREIMAGE are used to hold the original input to a permutation, i.e. the input to the first round.

• START_A to store the input for a permutation.

• START_C are used to hold xor(A[x, 0], A[x, 1], A[x, 2], A[x, 3], A[x, 4]) operation

• START_C_PRIME are used to hold xor(C[x, z], C[x - 1, z], C[x + 1, z - 1]) operation

• START_A_PRIME are used to hold xor(A[x, y], C[x - 1], ROT(C[x + 1], 1)) operation

• START_A_PRIME_PRIME are used to hold xor(B[x, y], and (B[x + 1, y], B[x + 2, y])) operation

• START_A_PRIME_PRIME_0_0_BITS is similar to START_A_PRIME_PRIME, this element is used for bit-level operations.

• REG_A_PRIME_PRIME_PRIME_0_0_LO are used to hold lower bits of START_A_PRIME_PRIME_0_0_BITS

• REG_A_PRIME_PRIME_PRIME_0_0_HI are used to hold higher bits of START_A_PRIME_PRIME_0_0_BITS

• REG_FILTER is a register which indicates if a row should be included in the CTL. Should be 1 only for certain rows which are final steps, i.e. with reg_step(23) = 1

Constraints

The Keccak Stark aims to constrain the following aspects:

• The REG_FILTER must be 0 or 1 and if this is not the final step, the REG_FILTER must be off.

• If this is not the final step, the local and next preimages must match.

$$C'[x, z] = C[x, z] \oplus C[x - 1, z] \oplus C[x + 1, z - 1]$$

• Check that the input limbs are consistent with A' and D.

$$A[x, y, z] = A'[x, y, z] \oplus D[x, y, z] = A'[x, y, z] \oplus C[x - 1, z] \oplus C[x + 1, z - 1] = A'[x, y, z] \oplus C[x, z] \oplus C'[x, z]$$

$$\bigoplus_{i=0}^4 A'[x, i, z] = C'[x, z] , \ \forall \ x, z: \text{diff}\cdot(\text{diff} - 2)\cdot(\text{diff}-4) = 0, \ \\where \ \text{diff}= \sum_{i=0}^{4} A'[x, i, z] - C'[x, z]$$

• Enforce that previous round’s output equals the next round’s input.

$$A''[x, y] = \text{xor}(B[x, y], \text{and}(B[x + 1, y], B[x + 2, y]))$$

$$A'''[0, 0] = A''[0, 0] \oplus \text{RC}$$

ctl_keccak() function to prove that concatenation columns of xored_rate_u32s, original_capacity_u32s, updated_state_u32s in KeccakSpongeStark equal to concatenated permutation input and output in KeccakStark.