Merge pull request #104 from valida-xyz/fix_deg_4_mem

Fix degree 4 memory constraint

basic/tests/test_prover.rs

@@ -223,8 +223,7 @@ fn prove_fibonacci() {
 
     type Quotient = QuotientMmcs<Val, Challenge, ValMmcs>;
     type MyFriConfig = FriConfigImpl<Val, Challenge, Quotient, ChallengeMmcs, Challenger>;
-    // TODO: Change log_blowup from 2 to 1 once degree >3 constraints are eliminated.
-    let fri_config = MyFriConfig::new(2, 40, 8, challenge_mmcs);
+    let fri_config = MyFriConfig::new(1, 40, 8, challenge_mmcs);
     let ldt = FriLdt { config: fri_config };
 
     type Pcs = FriBasedPcs<MyFriConfig, ValMmcs, Dft, Challenger>;

memory/src/columns.rs

@@ -18,8 +18,8 @@ pub struct MemoryCols<T> {
     /// Whether memory operation is a read
     pub is_read: T,
 
-    /// Whether memory operation is a real read, not a dummy.
-    pub is_real: T,
+    /// Whether memory operation is a write
+    pub is_write: T,
 
     /// Either addr' - addr (if address is changed), or clk' - clk (if address is not changed)
     pub diff: T,

memory/src/lib.rs

@@ -162,9 +162,10 @@ where
         let mut fields = vec![is_read, clk, addr];
         fields.extend(value);
 
+        let is_real = VirtualPairCol::sum_main(vec![MEM_COL_MAP.is_read, MEM_COL_MAP.is_write]);
         let receive = Interaction {
             fields,
-            count: VirtualPairCol::single_main(MEM_COL_MAP.is_real),
+            count: is_real,
             argument_index: machine.mem_bus(),
         };
         vec![receive]
@@ -184,17 +185,15 @@ impl MemoryChip {
                 cols.addr = F::from_canonical_u32(addr);
                 cols.value = value.transform(F::from_canonical_u8);
                 cols.is_read = F::one();
-                cols.is_real = F::one();
             }
             Operation::Write(addr, value) => {
                 cols.addr = F::from_canonical_u32(addr);
                 cols.value = value.transform(F::from_canonical_u8);
-                cols.is_real = F::one();
+                cols.is_write = F::one();
             }
             Operation::DummyRead(addr, value) => {
                 cols.addr = F::from_canonical_u32(addr);
                 cols.value = value.transform(F::from_canonical_u8);
-                cols.is_read = F::one();
             }
         }
 

memory/src/stark.rs

@@ -27,21 +27,33 @@ impl MemoryChip {
         let local: &MemoryCols<AB::Var> = main.row_slice(0).borrow();
         let next: &MemoryCols<AB::Var> = main.row_slice(1).borrow();
 
-        // Address equality
+        // Flags should be boolean.
+        builder.assert_bool(local.is_read);
+        builder.assert_bool(local.is_write);
+        builder.assert_bool(local.is_read + local.is_write);
+        builder.assert_bool(local.addr_not_equal);
+
+        let addr_delta = next.addr - local.addr;
+        let addr_equal = AB::Expr::one() - local.addr_not_equal;
+
+        // Ensure addr_not_equal is set correctly.
         builder
             .when_transition()
             .when(local.addr_not_equal)
-            .assert_one((next.addr - local.addr) * local.diff_inv);
-        builder.assert_bool(local.addr_not_equal);
+            .assert_one(addr_delta.clone() * local.diff_inv);
+        builder
+            .when_transition()
+            .when(addr_equal.clone())
+            .assert_zero(addr_delta.clone());
 
-        // Non-contiguous
+        // diff should match either the address delta or the clock delta, based on addr_not_equal.
         builder
             .when_transition()
             .when(local.addr_not_equal)
-            .assert_eq(local.diff, next.addr - local.addr);
+            .assert_eq(local.diff, addr_delta.clone());
         builder
             .when_transition()
-            .when_ne(local.addr_not_equal, AB::Expr::one())
+            .when(addr_equal.clone())
             .assert_eq(local.diff, next.clk - local.clk);
 
         // Read/write
@@ -50,14 +62,15 @@ impl MemoryChip {
             builder
                 .when_transition()
                 .when(next.is_read)
-                .when(next.is_real) // FIXME: Degree constraint 4, need to remove
-                .when_ne(local.addr_not_equal, AB::Expr::one())
+                .when(addr_equal.clone())
                 .assert_eq(value_next, value);
         }
-        builder
-            .when(next.is_read)
-            .when(next.is_real)
-            .assert_eq(local.addr, next.addr);
+
+        // TODO: This disallows reading unitialized memory? Not sure that's desired, it depends on
+        // how we implement continuations. If we end up defaulting to zero, then we should replace
+        // this with
+        //     when(is_read).when(addr_delta).assert_zero(value_next);
+        builder.when(next.is_read).assert_zero(addr_delta);
 
         // Counter increments from zero.
         builder.when_first_row().assert_zero(local.counter);