# 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.

Last updated