Merge pull request #1192 from topos-protocol/misc_constraints

evm/src/arithmetic/byte.rs

@@ -318,8 +318,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     }
     let t = F::Extension::from(F::from_canonical_u64(32));
     let t = builder.constant_extension(t);
-    let idx0_hi = builder.mul_extension(idx_decomp[5], t);
-    let t = builder.add_extension(idx0_lo5, idx0_hi);
+    let t = builder.mul_add_extension(idx_decomp[5], t, idx0_lo5);
     let t = builder.sub_extension(idx[0], t);
     let t = builder.mul_extension(is_byte, t);
     yield_constr.constraint(builder, t);

evm/src/cpu/decode.rs

@@ -118,39 +118,33 @@ pub fn eval_packed_generic<P: PackedField>(
     lv: &CpuColumnsView<P>,
     yield_constr: &mut ConstraintConsumer<P>,
 ) {
-    let cycle_filter: P = COL_MAP.op.iter().map(|&col_i| lv[col_i]).sum();
-
     // Ensure that the kernel flag is valid (either 0 or 1).
     let kernel_mode = lv.is_kernel_mode;
-    yield_constr.constraint(cycle_filter * kernel_mode * (kernel_mode - P::ONES));
+    yield_constr.constraint(kernel_mode * (kernel_mode - P::ONES));
 
     // Ensure that the opcode bits are valid: each has to be either 0 or 1.
     for bit in lv.opcode_bits {
-        yield_constr.constraint(cycle_filter * bit * (bit - P::ONES));
+        yield_constr.constraint(bit * (bit - P::ONES));
     }
 
     // Check that the instruction flags are valid.
     // First, check that they are all either 0 or 1.
     for (_, _, _, flag_col) in OPCODES {
         let flag = lv[flag_col];
-        yield_constr.constraint(cycle_filter * flag * (flag - P::ONES));
+        yield_constr.constraint(flag * (flag - P::ONES));
     }
     // Manually check the logic_op flag combining AND, OR and XOR.
-    // TODO: This would go away once cycle_filter is replaced by the sum
-    // of all CPU opcode flags.
     let flag = lv.op.logic_op;
-    yield_constr.constraint(cycle_filter * flag * (flag - P::ONES));
+    yield_constr.constraint(flag * (flag - P::ONES));
 
     // Now check that they sum to 0 or 1.
     // Includes the logic_op flag encompassing AND, OR and XOR opcodes.
-    // TODO: This would go away once cycle_filter is replaced by the sum
-    // of all CPU opcode flags.
     let flag_sum: P = OPCODES
         .into_iter()
         .map(|(_, _, _, flag_col)| lv[flag_col])
         .sum::<P>()
         + lv.op.logic_op;
-    yield_constr.constraint(cycle_filter * flag_sum * (flag_sum - P::ONES));
+    yield_constr.constraint(flag_sum * (flag_sum - P::ONES));
 
     // Finally, classify all opcodes, together with the kernel flag, into blocks
     for (oc, block_length, kernel_only, col) in OPCODES {
@@ -176,8 +170,7 @@ pub fn eval_packed_generic<P: PackedField>(
 
         // If unavailable + opcode_mismatch is 0, then the opcode bits all match and we are in the
         // correct mode.
-        let constr = lv[col] * (unavailable + opcode_mismatch);
-        yield_constr.constraint(cycle_filter * constr);
+        yield_constr.constraint(lv[col] * (unavailable + opcode_mismatch));
     }
 }
 
@@ -188,20 +181,18 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
 ) {
     let one = builder.one_extension();
 
-    let cycle_filter = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| lv[col_i]));
+    // Note: The constraints below do not need to be restricted to CPU cycles.
 
     // Ensure that the kernel flag is valid (either 0 or 1).
     let kernel_mode = lv.is_kernel_mode;
     {
         let constr = builder.mul_sub_extension(kernel_mode, kernel_mode, kernel_mode);
-        let constr = builder.mul_extension(cycle_filter, constr);
         yield_constr.constraint(builder, constr);
     }
 
     // Ensure that the opcode bits are valid: each has to be either 0 or 1.
     for bit in lv.opcode_bits {
         let constr = builder.mul_sub_extension(bit, bit, bit);
-        let constr = builder.mul_extension(cycle_filter, constr);
         yield_constr.constraint(builder, constr);
     }
 
@@ -210,29 +201,22 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     for (_, _, _, flag_col) in OPCODES {
         let flag = lv[flag_col];
         let constr = builder.mul_sub_extension(flag, flag, flag);
-        let constr = builder.mul_extension(cycle_filter, constr);
         yield_constr.constraint(builder, constr);
     }
     // Manually check the logic_op flag combining AND, OR and XOR.
-    // TODO: This would go away once cycle_filter is replaced by the sum
-    // of all CPU opcode flags.
     let flag = lv.op.logic_op;
     let constr = builder.mul_sub_extension(flag, flag, flag);
-    let constr = builder.mul_extension(cycle_filter, constr);
     yield_constr.constraint(builder, constr);
 
     // Now check that they sum to 0 or 1.
     // Includes the logic_op flag encompassing AND, OR and XOR opcodes.
-    // TODO: This would go away once cycle_filter is replaced by the sum
-    // of all CPU opcode flags.
     {
         let mut flag_sum = lv.op.logic_op;
         for (_, _, _, flag_col) in OPCODES {
             let flag = lv[flag_col];
             flag_sum = builder.add_extension(flag_sum, flag);
         }
         let constr = builder.mul_sub_extension(flag_sum, flag_sum, flag_sum);
-        let constr = builder.mul_extension(cycle_filter, constr);
         yield_constr.constraint(builder, constr);
     }
 
@@ -263,7 +247,6 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
         // correct mode.
         let constr = builder.add_extension(unavailable, opcode_mismatch);
         let constr = builder.mul_extension(lv[col], constr);
-        let constr = builder.mul_extension(cycle_filter, constr);
         yield_constr.constraint(builder, constr);
     }
 }

evm/src/cpu/membus.rs

@@ -49,11 +49,11 @@ pub fn eval_packed<P: PackedField>(
     lv: &CpuColumnsView<P>,
     yield_constr: &mut ConstraintConsumer<P>,
 ) {
-    let is_cpu_cycle: P = COL_MAP.op.iter().map(|&col_i| lv[col_i]).sum();
-    // Validate `lv.code_context`. It should be 0 if in kernel mode and `lv.context` if in user
-    // mode.
-    yield_constr
-        .constraint(is_cpu_cycle * (lv.code_context - (P::ONES - lv.is_kernel_mode) * lv.context));
+    // Validate `lv.code_context`.
+    // It should be 0 if in kernel mode and `lv.context` if in user mode.
+    // Note: This doesn't need to be filtered to CPU cycles, as this should also be satisfied
+    // during Kernel bootstrapping.
+    yield_constr.constraint(lv.code_context - (P::ONES - lv.is_kernel_mode) * lv.context);
 
     // Validate `channel.used`. It should be binary.
     for channel in lv.mem_channels {
@@ -66,13 +66,13 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     lv: &CpuColumnsView<ExtensionTarget<D>>,
     yield_constr: &mut RecursiveConstraintConsumer<F, D>,
 ) {
-    // Validate `lv.code_context`. It should be 0 if in kernel mode and `lv.context` if in user
-    // mode.
+    // Validate `lv.code_context`.
+    // It should be 0 if in kernel mode and `lv.context` if in user mode.
+    // Note: This doesn't need to be filtered to CPU cycles, as this should also be satisfied
+    // during Kernel bootstrapping.
     let diff = builder.sub_extension(lv.context, lv.code_context);
     let constr = builder.mul_sub_extension(lv.is_kernel_mode, lv.context, diff);
-    let is_cpu_cycle = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| lv[col_i]));
-    let filtered_constr = builder.mul_extension(is_cpu_cycle, constr);
-    yield_constr.constraint(builder, filtered_constr);
+    yield_constr.constraint(builder, constr);
 
     // Validate `channel.used`. It should be binary.
     for channel in lv.mem_channels {

evm/src/cross_table_lookup.rs

@@ -399,7 +399,7 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const
         consumer.constraint_first_row(*local_z - select(local_filter, combine(vars.local_values)));
         // Check `Z(gw) = combination * Z(w)`
         consumer.constraint_transition(
-            *next_z - *local_z * select(next_filter, combine(vars.next_values)),
+            *local_z * select(next_filter, combine(vars.next_values)) - *next_z,
         );
     }
 }
@@ -524,8 +524,7 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
             .collect::<Vec<_>>();
         let combined_next = challenges.combine_circuit(builder, &next_columns_eval);
         let selected_next = select(builder, next_filter, combined_next);
-        let mut transition = builder.mul_extension(*local_z, selected_next);
-        transition = builder.sub_extension(*next_z, transition);
+        let transition = builder.mul_sub_extension(*local_z, selected_next, *next_z);
         consumer.constraint_transition(builder, transition);
     }
 }

evm/src/memory/memory_stark.rs

@@ -408,7 +408,6 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
             let diff = builder.sub_extension(next_addr_context, addr_context);
             builder.sub_extension(diff, one)
         };
-        let context_range_check = builder.mul_extension(context_first_change, context_diff);
         let segment_diff = {
             let diff = builder.sub_extension(next_addr_segment, addr_segment);
             builder.sub_extension(diff, one)
@@ -423,7 +422,9 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
         let timestamp_range_check = builder.mul_extension(address_unchanged, timestamp_diff);
 
         let computed_range_check = {
-            let mut sum = builder.add_extension(context_range_check, segment_range_check);
+            // context_range_check = context_first_change * context_diff
+            let mut sum =
+                builder.mul_add_extension(context_first_change, context_diff, segment_range_check);
             sum = builder.add_extension(sum, virtual_range_check);
             builder.add_extension(sum, timestamp_range_check)
         };