fix(evm_arithmetization): remove duplicate constraint in keccak_stark

[shuklaayush]

Both the following constraints evaluate to the same constraint:

zk_evm/evm_arithmetization/src/keccak/keccak_stark.rs

Lines 278 to 285 in d0bc5ec

	// The filter must be 0 or 1.
	let filter = local_values[reg_step(NUM_ROUNDS - 1)];
	yield_constr.constraint(filter * (filter - P::ONES));
	// If this is not the final step, the filter must be off.
	let final_step = local_values[reg_step(NUM_ROUNDS - 1)];
	let not_final_step = P::ONES - final_step;
	yield_constr.constraint(not_final_step * filter);

If $f = \text{local\_values[reg\_step(NUM\_ROUNDS - 1)]}$ then

 let filter = local_values[reg_step(NUM_ROUNDS - 1)]; 
 yield_constr.constraint(filter * (filter - P::ONES)); 

corresponds to $f * (f - 1)$ and

 let final_step = local_values[reg_step(NUM_ROUNDS - 1)]; 
 let not_final_step = P::ONES - final_step; 
 yield_constr.constraint(not_final_step * filter); 

corresponds to $(1-f)*f$

[shuklaayush]

I have a feeling that even the first constraint might be unnecessary since the reg_step values should already be constrained in the eval_round_flags function:

zk_evm/evm_arithmetization/src/keccak/round_flags.rs

Lines 14 to 40 in d0bc5ec

	pub(crate) fn eval_round_flags<F: Field, P: PackedField<Scalar = F>>(
	vars: &EvmStarkFrame<P, F, NUM_COLUMNS>,
	yield_constr: &mut ConstraintConsumer<P>,
	) {
	let local_values = vars.get_local_values();
	let next_values = vars.get_next_values();
	// Initially, the first step flag should be 1 while the others should be 0.
	yield_constr.constraint_first_row(local_values[reg_step(0)] - F::ONE);
	for i in 1..NUM_ROUNDS {
	yield_constr.constraint_first_row(local_values[reg_step(i)]);
	}
	// Flags should circularly increment, or be all zero for padding rows.
	let next_any_flag = (0..NUM_ROUNDS).map(|i| next_values[reg_step(i)]).sum::<P>();
	for i in 0..NUM_ROUNDS {
	let current_round_flag = local_values[reg_step(i)];
	let next_round_flag = next_values[reg_step((i + 1) % NUM_ROUNDS)];
	yield_constr.constraint_transition(next_any_flag * (next_round_flag - current_round_flag));
	}
	// Padding rows should always be followed by padding rows.
	let current_any_flag = (0..NUM_ROUNDS)
	.map(|i| local_values[reg_step(i)])
	.sum::<P>();
	yield_constr.constraint_transition(next_any_flag * (current_any_flag - F::ONE));
	}

However, I'm not sure how this eval_round_flags implementation constrains the trace to have proper values. For one keccak permutation, it should be a 24x24 diagonal matrix

1 0 0 ... 0
0 1 0 ... 0
...
0 0 0 ... 1

But if you replace everything except the first row with all zeros then it'll still satisfy the constraints. For example, with the following first two rows

1 0 0 ... 0
0 0 0 ... 0

the next_any_flag is $0$ and current_any_flag is $1$ so the constraints are still satisfied. All subsequent rows contain only $0$ and hence, also satisfy the constraints

[Nashtare]

Hi @shuklaayush! Thank you for this PR!
Indeed, following some refactoring we did a few months ago on the eval_round_flags function, the first two constraints in KeccakStark::eval_packed_generic seem indeed overconstraining.

Regarding your following comment:

However, I'm not sure how this eval_round_flags implementation constrains the trace to have proper values. For one keccak permutation, it should be a 24x24 diagonal matrix

1 0 0 ... 0
0 1 0 ... 0
...
0 0 0 ... 1
But if you replace everything except the first row with all zeros then it'll still satisfy the constraints. For example, with the following first two rows

1 0 0 ... 0
0 0 0 ... 0
the next_any_flag is
and current_any_flag is
so the constraints are still satisfied. All subsequent rows contain only
and hence, also satisfy the constraints

I agree the current constraints do not enforce a proper continuation of the permutation rounds. I think a simple way to address it however is to update the constraint in eval_round_flags under this comment:
// Flags should circularly increment, or be all zero for padding rows.
by adding a third term to the product, equal to (P::ONES - local_values[reg_step(NUM_ROUNDS - 1)]) (i.e. for the final round flag).
That way, you can't transition to a padding row with all flags turned off unless you are currently on the last round of a permutation. The current constraint to be modified is of degree 2, so can support the additional multiplicand.

If that sounds correct to you, would you mind updating your PR to update this constraint? Thank you for reviewing this part of the codebase! 🙏🏼

[shuklaayush]

I agree the current constraints do not enforce a proper continuation of the permutation rounds. I think a simple way to address it however is to update the constraint in eval_round_flags under this comment:
// Flags should circularly increment, or be all zero for padding rows.
by adding a third term to the product, equal to (P::ONES - local_values[reg_step(NUM_ROUNDS - 1)]) (i.e. for the final round flag).
That way, you can't transition to a padding row with all flags turned off unless you are currently on the last round of a permutation. The current constraint to be modified is of degree 2, so can support the additional multiplicand.

Do you mean changing it to something like this?

    // Flags should circularly increment, or be all zero for padding rows.
    let next_any_flag = (0..NUM_ROUNDS).map(|i| next_values[reg_step(i)]).sum::<P>();
    let not_last_row = local_values[reg_step(NUM_ROUNDS - 1)] - F::ONE;
    for i in 0..NUM_ROUNDS {
        let current_round_flag = local_values[reg_step(i)];
        let next_round_flag = next_values[reg_step((i + 1) % NUM_ROUNDS)];
        yield_constr.constraint_transition(
            not_last_row * next_any_flag * (next_round_flag - current_round_flag),
        );
    }

I don't think this works either since you can still put any subsequent row as all zeros.

Something that might work is adding a + (next_any_flag - F::ONE) * current_any_flag * (last_row_flag - F::ONE) term to the constraint:

        yield_constr.constraint_transition(
            next_any_flag * (next_round_flag - current_round_flag)
+                + (next_any_flag - F::ONE) * current_any_flag * (last_row_flag - F::ONE),
        );

Btw, why not just do away with handling padding separately and just fill the extra rows with more keccak permutations? Seems like that's how it's done in plonky3

[Nashtare]

Ah sorry yeah what I suggested isn't fine, yours is.
I'd rather not take the plonky3 approach here for two reasons:

• needless extra permutations, even though these aren't the bottleneck, I'd rather not have to do them
• CTLs: we filter hash outputs from the last round flag. Adding dummy permutations would require additional filtering, typically through an additional column, to only consider actual permutations. I think to this regard, updating the constraint to properly enforce the transition to padding rows is a better approach.

[Nashtare]

Minor nits, otherwise it looks good! Thank you for fixing this @shuklaayush!

[shuklaayush]

Another concern that I have is that we're not constraining individual elements of a row to be bits while using the sum as a proxy for whether the row contains any $1$ or not. There can be cases where you fill the padding rows with elements that sum to $0\mod p$ (eg. $[1, p-1, ...]$) and the constraints would still satisfy

[Nashtare]

Last minor nit, then LGTM!

[Nashtare]

Another concern that I have is that we're not constraining individual elements of a row to be bits while using the sum as a proxy for whether the row contains any $1$ or not. There can be cases where you fill the padding rows with elements that sum to $0\mod p$ (eg. $[1, p-1, ...]$) and the constraints would still satisfy

Hmm yeah it seems we're missing boolean constraints on all flags except the first (through CTLs) and last one (used as filter). We definitely need to address those. Would you mind adding it to this PR? Thank you for catching this as well!

[Nashtare]

LGTM! Remains to constrain the round flags to be all boolean but this wasn't the initial purpose of this PR, so can be tackled separately.

[shuklaayush]

Hmm yeah it seems we're missing boolean constraints on all flags except the first (through CTLs) and last one (used as filter). We definitely need to address those. Would you mind adding it to this PR? Thank you for catching this as well!

I think all the flags before the padding rows are properly constrained to be 0 or 1 since they can only be equal to the value in the previous row and in the base case, the values in the first row are constrained to be 0 or 1. Only the values in the padding rows need to be additionally constrained to be bits.
Of course, constraining everything to be bits by adding a constraint of the form b * (b-1) also works but I'm not sure if that's overkill and if there's a better way to do this

[Nashtare]

Yes they are, what I had in mind when writing this is that specifically constraining them to be boolean only for padding rows would increase the degree, either through filtering or arbitrary periodic selectors (which starky doesn't support), so it's probably best to just add the boolean constraints globally.

[shuklaayush]

Cool, should I create another PR for that?

[Nashtare]

Sure go ahead and I'll merge this one! Thanks again!