diff --git a/evm/src/keccak_sponge/keccak_sponge_stark.rs b/evm/src/keccak_sponge/keccak_sponge_stark.rs index 3fe59f74..cb2c6091 100644 --- a/evm/src/keccak_sponge/keccak_sponge_stark.rs +++ b/evm/src/keccak_sponge/keccak_sponge_stark.rs @@ -361,40 +361,242 @@ impl, const D: usize> Stark for KeccakSpongeS fn eval_packed_generic( &self, vars: StarkEvaluationVars, - _yield_constr: &mut ConstraintConsumer

, + yield_constr: &mut ConstraintConsumer

, ) where FE: FieldExtension, P: PackedField, { - let _local_values: &KeccakSpongeColumnsView

= vars.local_values.borrow(); + let local_values: &KeccakSpongeColumnsView

= vars.local_values.borrow(); + let next_values: &KeccakSpongeColumnsView

= vars.next_values.borrow(); - // TODO: Each flag (full-input block, final block or implied dummy flag) must be boolean. - // TODO: before_rate_bits, block_bits and is_final_input_len must contain booleans. + // Each flag (full-input block, final block or implied dummy flag) must be boolean. + let is_full_input_block = local_values.is_full_input_block; + yield_constr.constraint(is_full_input_block * (is_full_input_block - P::ONES)); - // TODO: Sum of is_final_input_len should equal is_final_block (which will be 0 or 1). + let is_final_block = local_values.is_final_block; + yield_constr.constraint(is_final_block * (is_final_block - P::ONES)); - // TODO: If this is the first row, the original sponge state should be 0 and already_absorbed_bytes = 0. - // TODO: If this is a final block, the next row's original sponge state should be 0 and already_absorbed_bytes = 0. + for &is_final_len in local_values.is_final_input_len.iter() { + yield_constr.constraint(is_final_len * (is_final_len - P::ONES)); + } - // TODO: If this is a full-input block, the next row's address, time and len must match. - // TODO: If this is a full-input block, the next row's "before" should match our "after" state. - // TODO: If this is a full-input block, the next row's already_absorbed_bytes should be ours plus 136. + // Ensure that full-input block and final block flags are not set to 1 at the same time. + yield_constr.constraint(is_final_block * is_full_input_block); - // TODO: 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. + // Sum of is_final_input_len should equal is_final_block (which will be 0 or 1). + let is_final_input_len_sum: P = local_values.is_final_input_len.iter().copied().sum(); + yield_constr.constraint(is_final_input_len_sum - is_final_block); - // TODO: is_final_input_len implies `len - already_absorbed == i`. + // If this is a full-input block, is_final_input_len should contain all 0s. + yield_constr.constraint(is_full_input_block * is_final_input_len_sum); + + // If this is the first row, the original sponge state should be 0 and already_absorbed_bytes = 0. + let already_absorbed_bytes = local_values.already_absorbed_bytes; + yield_constr.constraint_first_row(already_absorbed_bytes); + for &original_rate_elem in local_values.original_rate_u32s.iter() { + yield_constr.constraint_first_row(original_rate_elem); + } + for &original_capacity_elem in local_values.original_capacity_u32s.iter() { + yield_constr.constraint_first_row(original_capacity_elem); + } + + // If this is a final block, the next row's original sponge state should be 0 and already_absorbed_bytes = 0. + yield_constr.constraint_transition(is_final_block * next_values.already_absorbed_bytes); + for &original_rate_elem in next_values.original_rate_u32s.iter() { + yield_constr.constraint_transition(is_final_block * original_rate_elem); + } + for &original_capacity_elem in next_values.original_capacity_u32s.iter() { + yield_constr.constraint_transition(is_final_block * original_capacity_elem); + } + + // If this is a full-input block, the next row's address, time and len must match as well as its timestamp. + yield_constr.constraint_transition( + is_full_input_block * (local_values.context - next_values.context), + ); + yield_constr.constraint_transition( + is_full_input_block * (local_values.segment - next_values.segment), + ); + yield_constr + .constraint_transition(is_full_input_block * (local_values.virt - next_values.virt)); + yield_constr.constraint_transition( + is_full_input_block * (local_values.timestamp - next_values.timestamp), + ); + + // If this is a full-input block, the next row's "before" should match our "after" state. + for (¤t_after, &next_before) in local_values + .updated_state_u32s + .iter() + .zip(next_values.original_rate_u32s.iter()) + { + yield_constr.constraint_transition(is_full_input_block * (next_before - current_after)); + } + for (¤t_after, &next_before) in local_values + .updated_state_u32s + .iter() + .skip(KECCAK_RATE_U32S) + .zip(next_values.original_capacity_u32s.iter()) + { + yield_constr.constraint_transition(is_full_input_block * (next_before - current_after)); + } + + // If this is a full-input block, the next row's already_absorbed_bytes should be ours plus 136. + yield_constr.constraint_transition( + is_full_input_block + * (already_absorbed_bytes + P::from(FE::from_canonical_u64(136)) + - next_values.already_absorbed_bytes), + ); + + // 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. + let is_dummy = P::ONES - is_full_input_block - is_final_block; + yield_constr.constraint_transition( + is_dummy * (next_values.is_full_input_block + next_values.is_final_block), + ); + + // If this is a final block, is_final_input_len implies `len - already_absorbed == i`. + let offset = local_values.len - already_absorbed_bytes; + for (i, &is_final_len) in local_values.is_final_input_len.iter().enumerate() { + let entry_match = offset - P::from(FE::from_canonical_usize(i)); + yield_constr.constraint(is_final_len * entry_match); + } } fn eval_ext_circuit( &self, - _builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder, + builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder, vars: StarkEvaluationTargets, - _yield_constr: &mut RecursiveConstraintConsumer, + yield_constr: &mut RecursiveConstraintConsumer, ) { - let _local_values: &KeccakSpongeColumnsView> = - vars.local_values.borrow(); + let local_values: &KeccakSpongeColumnsView> = vars.local_values.borrow(); + let next_values: &KeccakSpongeColumnsView> = vars.next_values.borrow(); - // TODO + let one = builder.one_extension(); + + // Each flag (full-input block, final block or implied dummy flag) must be boolean. + let is_full_input_block = local_values.is_full_input_block; + let constraint = builder.mul_sub_extension( + is_full_input_block, + is_full_input_block, + is_full_input_block, + ); + yield_constr.constraint(builder, constraint); + + let is_final_block = local_values.is_final_block; + let constraint = builder.mul_sub_extension(is_final_block, is_final_block, is_final_block); + yield_constr.constraint(builder, constraint); + + for &is_final_len in local_values.is_final_input_len.iter() { + let constraint = builder.mul_sub_extension(is_final_len, is_final_len, is_final_len); + yield_constr.constraint(builder, constraint); + } + + // Ensure that full-input block and final block flags are not set to 1 at the same time. + let constraint = builder.mul_extension(is_final_block, is_full_input_block); + yield_constr.constraint(builder, constraint); + + // Sum of is_final_input_len should equal is_final_block (which will be 0 or 1). + let mut is_final_input_len_sum = builder.add_extension( + local_values.is_final_input_len[0], + local_values.is_final_input_len[1], + ); + for &input_len in local_values.is_final_input_len.iter().skip(2) { + is_final_input_len_sum = builder.add_extension(is_final_input_len_sum, input_len); + } + let constraint = builder.sub_extension(is_final_input_len_sum, is_final_block); + yield_constr.constraint(builder, constraint); + + // If this is a full-input block, is_final_input_len should contain all 0s. + let constraint = builder.mul_extension(is_full_input_block, is_final_input_len_sum); + yield_constr.constraint(builder, constraint); + + // If this is the first row, the original sponge state should be 0 and already_absorbed_bytes = 0. + let already_absorbed_bytes = local_values.already_absorbed_bytes; + yield_constr.constraint_first_row(builder, already_absorbed_bytes); + for &original_rate_elem in local_values.original_rate_u32s.iter() { + yield_constr.constraint_first_row(builder, original_rate_elem); + } + for &original_capacity_elem in local_values.original_capacity_u32s.iter() { + yield_constr.constraint_first_row(builder, original_capacity_elem); + } + + // If this is a final block, the next row's original sponge state should be 0 and already_absorbed_bytes = 0. + let constraint = builder.mul_extension(is_final_block, next_values.already_absorbed_bytes); + yield_constr.constraint_transition(builder, constraint); + for &original_rate_elem in next_values.original_rate_u32s.iter() { + let constraint = builder.mul_extension(is_final_block, original_rate_elem); + yield_constr.constraint_transition(builder, constraint); + } + for &original_capacity_elem in next_values.original_capacity_u32s.iter() { + let constraint = builder.mul_extension(is_final_block, original_capacity_elem); + yield_constr.constraint_transition(builder, constraint); + } + + // If this is a full-input block, the next row's address, time and len must match as well as its timestamp. + let context_diff = builder.sub_extension(local_values.context, next_values.context); + let constraint = builder.mul_extension(is_full_input_block, context_diff); + yield_constr.constraint_transition(builder, constraint); + + let segment_diff = builder.sub_extension(local_values.segment, next_values.segment); + let constraint = builder.mul_extension(is_full_input_block, segment_diff); + yield_constr.constraint_transition(builder, constraint); + + let virt_diff = builder.sub_extension(local_values.virt, next_values.virt); + let constraint = builder.mul_extension(is_full_input_block, virt_diff); + yield_constr.constraint_transition(builder, constraint); + + let timestamp_diff = builder.sub_extension(local_values.timestamp, next_values.timestamp); + let constraint = builder.mul_extension(is_full_input_block, timestamp_diff); + yield_constr.constraint_transition(builder, constraint); + + // If this is a full-input block, the next row's "before" should match our "after" state. + for (¤t_after, &next_before) in local_values + .updated_state_u32s + .iter() + .zip(next_values.original_rate_u32s.iter()) + { + let diff = builder.sub_extension(next_before, current_after); + let constraint = builder.mul_extension(is_full_input_block, diff); + yield_constr.constraint_transition(builder, constraint); + } + for (¤t_after, &next_before) in local_values + .updated_state_u32s + .iter() + .skip(KECCAK_RATE_U32S) + .zip(next_values.original_capacity_u32s.iter()) + { + let diff = builder.sub_extension(next_before, current_after); + let constraint = builder.mul_extension(is_full_input_block, diff); + yield_constr.constraint_transition(builder, constraint); + } + + // If this is a full-input block, the next row's already_absorbed_bytes should be ours plus 136. + let absorbed_bytes = + builder.add_const_extension(already_absorbed_bytes, F::from_canonical_u64(136)); + let absorbed_diff = + builder.sub_extension(absorbed_bytes, next_values.already_absorbed_bytes); + let constraint = builder.mul_extension(is_full_input_block, absorbed_diff); + yield_constr.constraint_transition(builder, constraint); + + // 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. + let is_dummy = { + let tmp = builder.sub_extension(one, is_final_block); + builder.sub_extension(tmp, is_full_input_block) + }; + let constraint = { + let tmp = + builder.add_extension(next_values.is_final_block, next_values.is_full_input_block); + builder.mul_extension(is_dummy, tmp) + }; + yield_constr.constraint_transition(builder, constraint); + + // If this is a final block, is_final_input_len implies `len - already_absorbed == i`. + let offset = builder.sub_extension(local_values.len, already_absorbed_bytes); + for (i, &is_final_len) in local_values.is_final_input_len.iter().enumerate() { + let index = builder.constant_extension(F::from_canonical_usize(i).into()); + let entry_match = builder.sub_extension(offset, index); + + let constraint = builder.mul_extension(is_final_len, entry_match); + yield_constr.constraint(builder, constraint); + } } fn constraint_degree(&self) -> usize {