Comments

evm_arithmetization/src/cpu/control_flow.rs

@@ -78,16 +78,14 @@ pub(crate) fn eval_packed_generic<P: PackedField>(
     );
     yield_constr.constraint_transition(is_prover_input * (lv.is_kernel_mode - nv.is_kernel_mode));
 
-    // Check the helper value in the general columns.
+    // Check the helper value in the general columns. We do not need to enforce that
+    // it is set to 0 if the operation is a `PROVER_INPUT`, as the latter is a
+    // kernel-only instruction. This is enforced in the `decode` module.
     yield_constr.constraint(
         lv.op.push_prover_input
             * ((lv.is_kernel_mode + lv.general.push().push_prover_input_not_kernel) - P::ONES),
     );
 
-    // The general column should be not be set when the operation is a
-    // `PROVER_INPUT`.
-    yield_constr.constraint(is_prover_input * lv.general.push().push_prover_input_not_kernel);
-
     // If a non-CPU cycle row is followed by a CPU cycle row, then:
     //  - the `program_counter` of the CPU cycle row is `main` (the entry point of
     //    our kernel),
@@ -115,12 +113,6 @@ pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
 
     let next_halt_state = builder.sub_extension(one, is_cpu_cycle_next);
 
-    let is_prover_input = builder.mul_sub_extension(
-        lv.op.push_prover_input,
-        lv.opcode_bits[5],
-        lv.op.push_prover_input,
-    );
-
     // Once we start executing instructions, then we continue until the end of the
     // table or we reach dummy padding rows. This, along with the constraints on
     // the first row, enforces that operation flags and the halt flag are
@@ -145,13 +137,20 @@ pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
         yield_constr.constraint_transition(builder, kernel_constr);
 
         // Same constraints as before, for PROVER_INPUT.
+        let is_prover_input = builder.mul_sub_extension(
+            lv.op.push_prover_input,
+            lv.opcode_bits[5],
+            lv.op.push_prover_input,
+        );
         let pc_constr = builder.mul_add_extension(is_prover_input, pc_diff, is_prover_input);
         yield_constr.constraint_transition(builder, pc_constr);
         let kernel_constr = builder.mul_extension(is_prover_input, kernel_diff);
         yield_constr.constraint_transition(builder, kernel_constr);
     }
 
-    // Check the helper value in the general columns.
+    // Check the helper value in the general columns. We do not need to enforce that
+    // it is set to 0 if the operation is a `PROVER_INPUT`, as the latter is a
+    // kernel-only instruction. This is enforced in the `decode` module.
     {
         let temp = builder.add_extension(
             lv.is_kernel_mode,
@@ -162,16 +161,6 @@ pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
         yield_constr.constraint(builder, constr);
     }
 
-    // The general column should be not be set when the operation is a
-    // `PROVER_INPUT`.
-    {
-        let constr = builder.mul_extension(
-            is_prover_input,
-            lv.general.push().push_prover_input_not_kernel,
-        );
-        yield_constr.constraint(builder, constr);
-    }
-
     // If a non-CPU cycle row is followed by a CPU cycle row, then:
     //  - the `program_counter` of the CPU cycle row is `main` (the entry point of
     //    our kernel),

evm_arithmetization/src/witness/operation.rs

@@ -388,8 +388,6 @@ pub(crate) fn generate_push<F: Field, T: Transition<F>>(
 
     // This is necessary to filter out PUSH instructions from the BytePackingStark
     // CTl when happening in the KERNEL context.
-    //
-    // Note that we don't need to
     row.general.push_mut().push_prover_input_not_kernel = F::ONE - row.is_kernel_mode;
 
     if code_context != KERNEL_CONTEXT {