Skip to content

Commit

Permalink
Fix degree 4 memory constraint
Browse files Browse the repository at this point in the history
We want all constraints to be degree 3 or less. To address this, I removed `is_real` and added `is_write`. Also refactor memory constraints a bit.
  • Loading branch information
dlubarov committed Jan 25, 2024
1 parent 44eaa9a commit 0c8c9aa
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 20 deletions.
3 changes: 1 addition & 2 deletions basic/tests/test_prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>;
Expand Down
4 changes: 2 additions & 2 deletions memory/src/columns.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
7 changes: 3 additions & 4 deletions memory/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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();
}
}

Expand Down
37 changes: 25 additions & 12 deletions memory/src/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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);
Expand Down

0 comments on commit 0c8c9aa

Please sign in to comment.