Logic 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 logical operations(xor, and, or) using CPUStark in EVM, but for our needs we use the Stark only for xor operation proving with state and input blocks in KeccakSpongeStark.

Circuit

Private inputs include data fields about each value:

• operator flag of logical operator

• input0 first operand of logical operation

• input1 second operand of logical operation

• result of logical operation

Columns that are used in trace rows generation:

• IS_AND flag that describes AND operation, must be boolean

• IS_OR flag that describes OR operation, must be boolean

• IS_XOR flag that describes XOR operation, must be boolean

• INPUT0 left operand(256 bits) of operation that are decomposed from U256

• INPUT1 right operand(256 bits) of operation that are decomposed from U256

• RESULT the result of operation that is packed in 32 bits from U256

Constraints

The Logic Stark aims to constrain the following aspects:

• Ensure that all bits are indeed bits.

• The result will be ‘input0 OP input1 = sum coeff * (input0 + input1) + and coeff(input0 AND input1)‘. AND => sum coeff = 0, and coeff = 1, OR => sum coeff = 1, and coeff = -1, XOR => sum coeff = 1, and coeff = -2

The function is used in proving STARK using CTL:

• 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, input1 and flag of xor operation. This function guarantees that xor operation of state and block_bytes is correct.