KeccakSponge proof

The purpose of this Stark is to prove integrity of sponge operations as a part of building Keccak. KeccakSponge proof via zk-STARKs enables efficient verification of sponge operations as a part of building Keccak hashes that included in Patricia Merkle Trie and connect with other STARKs as Logic, Keccak, Data while proving using CTL's.

Circuit

Private inputs include data fields about each value:

• input includes bytes for hashing

• timestamp at which inputs are read

Columns that are used in trace rows generation:

• is_full_input_block 1 if this row represents a full input block, i.e. one in which each byte is an input byte, not a padding byte; 0 otherwise.

• timestamp the timestamp at which inputs should be read from memory.

• len The length of the original input, in bytes.

• already_absorbed_bytes the number of input bytes that have already been absorbed prior to this block,

• is_final_input_len If this row represents a final block row, the i-th entry should be 1 if the final chunk of input has length i (in other words if len - already_absorbed_bytes == i), otherwise 0. If this row represents a full input block, this should contain all 0s.

• original_rate_u32s the initial rate part of the sponge, at the start of this step.

• original_capacity_u32s: the capacity part of the sponge, encoded as 32-bit chunks, at the start of this step,

• block_bytes the block being absorbed, which may contain input bytes and/or padding bytes,

• xored_rate u32s the rate part of the sponge, encoded as 32-bit chunks, after the current block is xor’d in,but before the permutation is applied.,

• updated_state_u32s the entire state (rate + capacity) of the sponge, encoded as 32-bit chunks, after the permutation is applied.

• updated_state_bytes the entire state of the sponge as 32 bytes.

Constraints

The KeccakSponge Stark aims to constrain the following aspects:

• Each flag (full-input block, final block or implied dummy flag) must be boolean.

• Ensure that full-input block and final block flags are not set to 1 at the same time.

• If this is the first row, the original sponge state should be 0 and already_absorbed_bytes is equal to 0.

• If this is a final block, the next row’s original sponge state should be 0 and already_absorbed_bytes = 0.

• If this is a full-input block, the next row’s ”before” should match our ”after” state.

• If this is a full-input block, the next row’s already_absorbed_bytes should be ours plus 136.

• A dummy row is always followed by another dummy row, so the prover can’t put dummy rows ”in between” to avoid the above checks.

• If this is a final block, is final input len implies len - already_absorbed_bytes == i.

The functions are used in proving STARK using CTL:

• ctl_data_block_bytes() using filter when we have leaf, node, root data in Data table is equal to concatenation columns of xored_rate_u32s, original_capacity_u32s, updated_state_u32s for input block in KeccakSponge table.

• ctl_keccak sponge(): typed_data of child hash in Data table have to be equal to updated_state_bytes in KeccakSponge table when it’s the final input block.

• ctl_keccak() 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.

• ctl_logic() prove that concatenation columns of original_rate_u32s, block_bytes, xored_rate_u32s and flag of xor operation in KeccakSponge table is equal to concatenation of input0(256 bits), input1(256 bits) and flag of xor operation. This function guarantees that xor operation of state and block_bytes is correct.