wip15

Author: kunxian-xia

extensions/native/circuit/src/sumcheck/air.rs

@@ -244,12 +244,11 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
             );
 
         // Termination condition
-        // TODO: enable this
-        // assert_array_eq(
-        //     &mut builder.when::<AB::Expr>(is_end.into()),
-        //     eval_acc,
-        //     [AB::F::ZERO; 4],
-        // );
+        assert_array_eq(
+            &mut builder.when::<AB::Expr>(is_end.into()),
+            eval_acc,
+            [AB::F::ZERO; 4],
+        );
 
         // Randomness transition
         assert_array_eq(
@@ -439,12 +438,11 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
             prod_row_specific.eval_rlc,
             eval_rlc,
         );
-        // TODO: enable this
-        // assert_array_eq::<_, _, _, { EXT_DEG }>(
-        //     &mut builder.when(next.prod_acc),
-        //     FieldExtension::add(next.eval_acc, next_prod_row_specific.eval_rlc),
-        //     eval_acc,
-        // );
+        assert_array_eq::<_, _, _, { EXT_DEG }>(
+            &mut builder.when(next.prod_acc),
+            FieldExtension::add(next.eval_acc, next_prod_row_specific.eval_rlc),
+            eval_acc,
+        );
 
         ///////////////////////////////////////
         // Logup spec evaluation
@@ -587,11 +585,10 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
 
         // Accumulate into global accumulator `eval_acc`
         // when round < max_round - 2
-        // TODO: enable this
-        // assert_array_eq::<_, _, _, { EXT_DEG }>(
-        //     &mut builder.when(next.logup_acc),
-        //     FieldExtension::add(next.eval_acc, next_logup_row_specfic.eval_rlc),
-        //     eval_acc,
-        // );
+        assert_array_eq::<_, _, _, { EXT_DEG }>(
+            &mut builder.when(next.logup_acc),
+            FieldExtension::add(next.eval_acc, next_logup_row_specfic.eval_rlc),
+            eval_acc,
+        );
     }
 }

extensions/native/circuit/src/sumcheck/chip.rs

@@ -452,7 +452,6 @@ where
 
         let head_row = &mut rows[0];
         head_row.last_timestamp = F::from_canonical_u32(cur_timestamp + 1);
-        head_row.eval_acc = eval_acc;
 
         let head_specific: &mut HeaderSpecificCols<F> =
             head_row.specific[..HeaderSpecificCols::<F>::width()].borrow_mut();
@@ -464,6 +463,24 @@ where
             &mut head_specific.write_records,
         );
 
+        for row in rows.iter_mut() {
+            if row.header_row == F::ONE {
+                row.eval_acc = eval_acc;
+            } else if row.prod_row == F::ONE {
+                let specific: &mut ProdSpecificCols<F> =
+                    row.specific[..ProdSpecificCols::<F>::width()].borrow_mut();
+
+                eval_acc = FieldExtension::subtract(eval_acc, specific.eval_rlc);
+                row.eval_acc = eval_acc;
+            } else if row.logup_row == F::ONE {
+                let specific: &mut LogupSpecificCols<F> =
+                    row.specific[..LogupSpecificCols::<F>::width()].borrow_mut();
+                eval_acc = FieldExtension::subtract(eval_acc, specific.eval_rlc);
+                row.eval_acc = eval_acc;
+            }
+        }
+        assert_eq!(eval_acc, elem_to_ext(F::from_canonical_u32(0)),);
+
         *state.pc = state.pc.wrapping_add(DEFAULT_PC_STEP);
         Ok(())
     }