Skip to content

Commit

Permalink
feat(memory): allow more than 1 memory access per clock cycle
Browse files Browse the repository at this point in the history
  • Loading branch information
plafer committed Jan 16, 2025
1 parent 29ef925 commit 039d97e
Show file tree
Hide file tree
Showing 9 changed files with 88 additions and 55 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
- Added `miden_core::mast::MastForest::advice_map` to load it into the advice provider before the `MastForest` execution (#1574).
- Optimized the computation of the DEEP queries in the recursive verifier (#1594).
- Added validity checks for the inputs to the recursive verifier (#1596).
- Allow multiple memory reads in the same clock cycle (#1626)

## 0.11.0 (2024-11-04)

Expand Down
32 changes: 30 additions & 2 deletions air/src/constraints/chiplets/memory/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,15 @@ mod tests;
// ================================================================================================

/// The number of constraints on the management of the memory chiplet.
pub const NUM_CONSTRAINTS: usize = 18;
pub const NUM_CONSTRAINTS: usize = 19;
/// The degrees of constraints on the management of the memory chiplet. All constraint degrees are
/// increased by 3 due to the selectors for the memory chiplet.
pub const CONSTRAINT_DEGREES: [usize; NUM_CONSTRAINTS] = [
5, 5, 5, 5, // Enforce that rw, ew, idx0 and idx1 are binary.
7, 6, 9, 8, // Constrain the values in the d inverse column.
8, // Enforce values in ctx, word, clk transition correctly.
7, // Enforce the correct value for the f_scw flag.
8, // Enforce that accesses in same context, word and clock are reads.
9, 9, 9, 9, // Constrain the values in the first row of the chiplet.
9, 9, 9, 9, // Constrain the values in all rows of the chiplet except the first.
];
Expand Down Expand Up @@ -77,6 +78,13 @@ pub fn enforce_constraints<E: FieldElement>(
index +=
enforce_flag_same_context_and_word(frame, &mut result[index..], memory_flag_not_last_row);

// Enforce that accesses in same context, word and clock are reads.
index += enforce_same_context_word_addr_and_clock(
frame,
&mut result[index..],
memory_flag_not_last_row,
);

// Constrain the memory values.
enforce_values(frame, &mut result[index..], memory_flag_not_last_row, memory_flag_first_row);
}
Expand Down Expand Up @@ -156,6 +164,26 @@ fn enforce_flag_same_context_and_word<E: FieldElement>(
1
}

/// Enforces that when memory is accessed in the same context, word, and clock cycle, the access is
/// a read.
fn enforce_same_context_word_addr_and_clock<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
memory_flag_not_last_row: E,
) -> usize {
// Note: when the context and word address don't change, `d_inv_next` contains the inverse of
// the clock change.
let clk_no_change = binary_not(frame.clk_change() * frame.d_inv_next());

result[0] = memory_flag_not_last_row
* frame.f_scw_next()
* clk_no_change
* binary_not(frame.is_read()) // read in current row
* binary_not(frame.is_read_next()); // read in next row

1
}

/// A constraint evaluation function to enforce that memory is initialized to zero when it is read
/// before being written and that when existing memory values are read they remain unchanged.
///
Expand Down Expand Up @@ -418,7 +446,7 @@ impl<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {

#[inline(always)]
fn clk_change(&self) -> E {
self.change(MEMORY_CLK_COL_IDX) - E::ONE
self.change(MEMORY_CLK_COL_IDX)
}

#[inline(always)]
Expand Down
2 changes: 1 addition & 1 deletion air/src/constraints/chiplets/memory/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ fn get_test_frame(

// Set the delta in the next row according to the specified delta type.
let delta: u64 = match delta_type {
MemoryTestDeltaType::Clock => delta_row[MemoryTestDeltaType::Clock as usize] - 1,
MemoryTestDeltaType::Clock => delta_row[MemoryTestDeltaType::Clock as usize],
MemoryTestDeltaType::Context => delta_row[MemoryTestDeltaType::Context as usize],
MemoryTestDeltaType::Word => delta_row[MemoryTestDeltaType::Word as usize],
};
Expand Down
13 changes: 2 additions & 11 deletions miden/tests/integration/operations/io_ops/mem_ops.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,3 @@
use processor::ContextId;
use prover::ExecutionError;
use test_utils::expect_exec_error_matches;
use vm_core::FieldElement;

use super::{apply_permutation, build_op_test, build_test, Felt, ToElements, TRUNCATE_STACK_PROC};

// LOADING SINGLE ELEMENT ONTO THE STACK (MLOAD)
Expand Down Expand Up @@ -237,7 +232,7 @@ fn read_after_write() {
// MISC
// ================================================================================================

/// Ensures that the processor returns an error when 2 memory operations occur in the same context,
/// Ensures that the processor returns no error when 2 memory operations occur in the same context,
/// at the same address, and in the same clock cycle (which is what RCOMBBASE does when `stack[13] =
/// stack[14] = 0`).
#[test]
Expand All @@ -246,9 +241,5 @@ fn mem_reads_same_clock_cycle() {

let test = build_test!(asm_op);

expect_exec_error_matches!(
test,
ExecutionError::DuplicateMemoryAccess{ctx, addr, clk }
if ctx == ContextId::from(0) && addr == 0 && clk == Felt::ONE
);
test.prove_and_verify(vec![0], false);
}
4 changes: 2 additions & 2 deletions processor/src/chiplets/memory/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -281,7 +281,7 @@ impl Memory {
} else if prev_addr != addr {
u64::from(addr - prev_addr)
} else {
clk - prev_clk - 1
clk - prev_clk
};

let (delta_hi, delta_lo) = split_u32_into_u16(delta);
Expand Down Expand Up @@ -359,7 +359,7 @@ impl Memory {
} else if prev_addr != felt_addr {
felt_addr - prev_addr
} else {
clk - prev_clk - ONE
clk - prev_clk
};

let (delta_hi, delta_lo) = split_element_u32_into_u16(delta);
Expand Down
30 changes: 20 additions & 10 deletions processor/src/chiplets/memory/segment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -167,9 +167,9 @@ impl MemorySegmentTrace {
let (word_addr, addr_idx_in_word) = addr_to_word_addr_and_idx(addr);

match self.0.entry(word_addr) {
// If this is the first access to the ctx/word pair, then all values in the word
// are initialized to 0, except for the address being written.
Entry::Vacant(vacant_entry) => {
// If this is the first access to the ctx/word pair, then all values in the word
// are initialized to 0, except for the address being written.
let word = {
let mut word = Word::default();
word[addr_idx_in_word as usize] = value;
Expand All @@ -185,12 +185,15 @@ impl MemorySegmentTrace {
vacant_entry.insert(vec![access]);
Ok(())
},
// If the ctx/word pair has been accessed before, then the values in the word are
// the same as the previous access, except for the address being written.
Entry::Occupied(mut occupied_entry) => {
// If the ctx/word pair has been accessed before, then the values in the word are
// the same as the previous access, except for the address being written.
let addr_trace = occupied_entry.get_mut();
if addr_trace.last().expect("empty address trace").clk() == clk {
Err(ExecutionError::DuplicateMemoryAccess { ctx, addr, clk })
// The same address is accessed more than once in the same clock cycle. This is
// an error, since this access is a write, and the only valid accesses are
// reads when in the same clock cycle.
Err(ExecutionError::IllegalMemoryAccess { ctx, addr, clk })
} else {
let word = {
let mut last_word = addr_trace.last().expect("empty address trace").word();
Expand Down Expand Up @@ -236,16 +239,19 @@ impl MemorySegmentTrace {
let access =
MemorySegmentAccess::new(clk, MemoryOperation::Write, MemoryAccessType::Word, word);
match self.0.entry(word_addr) {
// All values in the word are set to the word being written.
Entry::Vacant(vacant_entry) => {
// All values in the word are set to the word being written.
vacant_entry.insert(vec![access]);
Ok(())
},
// All values in the word are set to the word being written.
Entry::Occupied(mut occupied_entry) => {
// All values in the word are set to the word being written.
let addr_trace = occupied_entry.get_mut();
if addr_trace.last().expect("empty address trace").clk() == clk {
Err(ExecutionError::DuplicateMemoryAccess { ctx, addr, clk })
// The same address is accessed more than once in the same clock cycle. This is
// an error, since this access is a write, and the only valid accesses are
// reads when in the same clock cycle.
Err(ExecutionError::IllegalMemoryAccess { ctx, addr, clk })
} else {
addr_trace.push(access);
Ok(())
Expand Down Expand Up @@ -301,8 +307,12 @@ impl MemorySegmentTrace {
// If the ctx/word pair has been accessed before, then the values in the word are
// the same as the previous access.
let addr_trace = occupied_entry.get_mut();
if addr_trace.last().expect("empty address trace").clk() == clk {
Err(ExecutionError::DuplicateMemoryAccess { ctx, addr: word_addr, clk })
let last_access = addr_trace.last().expect("empty address trace");
if last_access.clk() == clk && last_access.operation() == MemoryOperation::Write {
// The same address is accessed more than once in the same clock cycle. This is
// an error, since the previous access was a write, and the only valid accesses
// are reads when in the same clock cycle.
Err(ExecutionError::IllegalMemoryAccess { ctx, addr: word_addr, clk })
} else {
let last_word = addr_trace.last().expect("empty address trace").word();
let access = MemorySegmentAccess::new(
Expand Down
27 changes: 13 additions & 14 deletions processor/src/chiplets/memory/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -510,6 +510,7 @@ fn read_trace_row(trace: &[Vec<Felt>], step: usize) -> [Felt; MEMORY_TRACE_WIDTH
row
}

/// Note: For this to work properly, the context and address accessed in the first row *must be* 0.
fn build_trace_row(
memory_access: MemoryAccess,
prev_row: [Felt; MEMORY_TRACE_WIDTH],
Expand Down Expand Up @@ -557,20 +558,18 @@ fn build_trace_row(
row[V_COL_RANGE.start + 2] = word_values[2];
row[V_COL_RANGE.start + 3] = word_values[3];

if prev_row != [ZERO; MEMORY_TRACE_WIDTH] {
let delta = if row[CTX_COL_IDX] != prev_row[CTX_COL_IDX] {
row[CTX_COL_IDX] - prev_row[CTX_COL_IDX]
} else if row[WORD_COL_IDX] != prev_row[WORD_COL_IDX] {
row[WORD_COL_IDX] - prev_row[WORD_COL_IDX]
} else {
row[CLK_COL_IDX] - prev_row[CLK_COL_IDX] - ONE
};

let (hi, lo) = super::split_element_u32_into_u16(delta);
row[D0_COL_IDX] = lo;
row[D1_COL_IDX] = hi;
row[D_INV_COL_IDX] = delta.inv();
}
let delta = if row[CTX_COL_IDX] != prev_row[CTX_COL_IDX] {
row[CTX_COL_IDX] - prev_row[CTX_COL_IDX]
} else if row[WORD_COL_IDX] != prev_row[WORD_COL_IDX] {
row[WORD_COL_IDX] - prev_row[WORD_COL_IDX]
} else {
row[CLK_COL_IDX] - prev_row[CLK_COL_IDX]
};

let (hi, lo) = super::split_element_u32_into_u16(delta);
row[D0_COL_IDX] = lo;
row[D1_COL_IDX] = hi;
row[D_INV_COL_IDX] = delta.inv();

if row[WORD_COL_IDX] == prev_row[WORD_COL_IDX] && row[CTX_COL_IDX] == prev_row[CTX_COL_IDX] {
row[FLAG_SAME_CONTEXT_AND_WORD] = ONE;
Expand Down
4 changes: 2 additions & 2 deletions processor/src/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,6 @@ pub enum ExecutionError {
DecoratorNotFoundInForest { decorator_id: DecoratorId },
#[error("division by zero at clock cycle {0}")]
DivideByZero(RowIndex),
#[error("memory address {addr} in context {ctx} accessed twice in clock cycle {clk}")]
DuplicateMemoryAccess { ctx: ContextId, addr: u32, clk: Felt },
#[error("failed to execute the dynamic code block provided by the stack with root {hex}; the block could not be found",
hex = to_hex(.0.as_bytes())
)]
Expand All @@ -60,6 +58,8 @@ pub enum ExecutionError {
},
#[error("failed to generate signature: {0}")]
FailedSignatureGeneration(&'static str),
#[error("memory address {addr} in context {ctx} was read and written, or written twice, in the same clock cycle {clk}")]
IllegalMemoryAccess { ctx: ContextId, addr: u32, clk: Felt },
#[error("Updating FMP register from {0} to {1} failed because {1} is outside of {FMP_MIN}..{FMP_MAX}")]
InvalidFmpValue(Felt, Felt),
#[error("FRI domain segment value cannot exceed 3, but was {0}")]
Expand Down
30 changes: 17 additions & 13 deletions processor/src/trace/tests/range.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,8 @@ fn b_range_trace_stack() {
/// This test checks that range check lookups from memory operations are balanced by the
/// range checks processed in the Range Checker.
///
/// The `StoreW` memory operation results in 2 16-bit range checks of 0, 0.
/// The `LoadW` memory operation results in 2 16-bit range checks of 0, 0.
/// The `StoreW` memory operation results in 2 16-bit range checks of 1, 0.
/// The `LoadW` memory operation results in 2 16-bit range checks of 5, 0.
#[test]
#[allow(clippy::needless_range_loop)]
fn b_range_trace_mem() {
Expand Down Expand Up @@ -109,11 +109,11 @@ fn b_range_trace_mem() {
// --- Check the memory processor's range check lookups. --------------------------------------

// There are two memory lookups. For each memory lookup, the context and address are unchanged,
// so the delta values indicated the clock cycle change i' - i - 1.
// StoreW is executed at cycle 1 (after the initial span), so i' - i - 1 = 0.
let (d0_store, d1_store) = (ZERO, ZERO);
// LoadW is executed at cycle 6, so i' - i - 1 = 6 - 1 - 1 = 4.
let (d0_load, d1_load) = (Felt::new(4), ZERO);
// so the delta values indicated the clock cycle change clk' - clk.
// StoreW is executed at cycle 1 (after the initial span), so clk' - clk = 1.
let (d0_store, d1_store) = (ONE, ZERO);
// LoadW is executed at cycle 6, so i' - i = 6 - 1 = 5.
let (d0_load, d1_load) = (Felt::new(5), ZERO);

// Include the lookups from the `MStoreW` operation at the next row.
expected -= (alpha - d0_store).inv() + (alpha - d1_store).inv();
Expand All @@ -129,20 +129,24 @@ fn b_range_trace_mem() {

// --- Check the range checker's lookups. -----------------------------------------------------

// We include 3 lookups of ZERO in the next row.
expected += alpha.inv().mul_base(Felt::new(3));
// We include 2 lookups of ZERO in the next row.
expected += alpha.inv().mul_base(Felt::new(2));
assert_eq!(expected, b_range[values_start + 1]);

// then we have one bridge row between 0 and 4 where the value does not change.
// We include 1 lookup of ONE in the next row.
expected += (alpha - d0_store).inv();
assert_eq!(expected, b_range[values_start + 2]);

// We include 1 lookup of 4 in the next row.
expected += (alpha - d0_load).inv();
// We have one bridge row between 1 and 5 where the value does not change.
assert_eq!(expected, b_range[values_start + 3]);

// We include 1 lookup of 5 in the next row.
expected += (alpha - d0_load).inv();
assert_eq!(expected, b_range[values_start + 4]);

// --- The value should now be ONE for the rest of the trace. ---------------------------------
assert_eq!(expected, ONE);
for i in (values_start + 3)..(b_range.len() - NUM_RAND_ROWS) {
for i in (values_start + 4)..(b_range.len() - NUM_RAND_ROWS) {
assert_eq!(ONE, b_range[i]);
}
}

0 comments on commit 039d97e

Please sign in to comment.