diff --git a/basic/tests/test_prover.rs b/basic/tests/test_prover.rs index 0f6ad415..78a04f64 100644 --- a/basic/tests/test_prover.rs +++ b/basic/tests/test_prover.rs @@ -223,8 +223,7 @@ fn prove_fibonacci() { type Quotient = QuotientMmcs; type MyFriConfig = FriConfigImpl; - // 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; diff --git a/memory/src/columns.rs b/memory/src/columns.rs index 0ceb0251..73ef6f4d 100644 --- a/memory/src/columns.rs +++ b/memory/src/columns.rs @@ -18,8 +18,8 @@ pub struct MemoryCols { /// 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, diff --git a/memory/src/lib.rs b/memory/src/lib.rs index 320fe401..61049fc5 100644 --- a/memory/src/lib.rs +++ b/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(); } } diff --git a/memory/src/stark.rs b/memory/src/stark.rs index 3335fa70..f8c0701d 100644 --- a/memory/src/stark.rs +++ b/memory/src/stark.rs @@ -27,21 +27,33 @@ impl MemoryChip { let local: &MemoryCols = main.row_slice(0).borrow(); let next: &MemoryCols = 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);