diff --git a/CHANGELOG.md b/CHANGELOG.md index 3e908eb10d..cf44198d15 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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) diff --git a/air/src/constraints/chiplets/memory/mod.rs b/air/src/constraints/chiplets/memory/mod.rs index d4c93c1bc7..3c911ab572 100644 --- a/air/src/constraints/chiplets/memory/mod.rs +++ b/air/src/constraints/chiplets/memory/mod.rs @@ -20,7 +20,7 @@ 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] = [ @@ -28,6 +28,7 @@ pub const CONSTRAINT_DEGREES: [usize; NUM_CONSTRAINTS] = [ 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. ]; @@ -77,6 +78,13 @@ pub fn enforce_constraints( 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); } @@ -156,6 +164,26 @@ fn enforce_flag_same_context_and_word( 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( + frame: &EvaluationFrame, + 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. /// @@ -418,7 +446,7 @@ impl EvaluationFrameExt for &EvaluationFrame { #[inline(always)] fn clk_change(&self) -> E { - self.change(MEMORY_CLK_COL_IDX) - E::ONE + self.change(MEMORY_CLK_COL_IDX) } #[inline(always)] diff --git a/air/src/constraints/chiplets/memory/tests.rs b/air/src/constraints/chiplets/memory/tests.rs index fb0cacf934..56de63ea14 100644 --- a/air/src/constraints/chiplets/memory/tests.rs +++ b/air/src/constraints/chiplets/memory/tests.rs @@ -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], }; diff --git a/docs/src/design/chiplets/memory.md b/docs/src/design/chiplets/memory.md index ac3a78319c..5788edbf57 100644 --- a/docs/src/design/chiplets/memory.md +++ b/docs/src/design/chiplets/memory.md @@ -176,16 +176,17 @@ where: - `word_addr` contains the memory address of the first element in the word. Values in this column must increase monotonically for a given context but there can be gaps between two consecutive values of up to $2^{32}$. Values in this column must be divisible by 4. Also, two consecutive values can be the same. - `idx0` and `idx1` are selector columns used to identify which element in the word is being accessed. Specifically, the index within the word is computed as `idx1 * 2 + idx0`. - However, when `ew` is set to $1$ (indicating that a word is accessed), these columns are meaningless and are set to $0$. -- `clk` contains clock cycle at which the memory operation happened. Values in this column must increase monotonically for a given context and memory word but there can be gaps between two consecutive values of up to $2^{32}$. In AIR constraint description below, we refer to this column as $i$. +- `clk` contains clock cycle at which the memory operation happened. Values in this column must increase monotonically for a given context and memory word but there can be gaps between two consecutive values of up to $2^{32}$. + - Unlike the previously described approaches, we allow `clk` to be constant in the same context/word address, with the restriction that when this is the case, then only reads are allowed. - `v0, v1, v2, v3` columns contain field elements stored at a given context/word/clock cycle after the memory operation. - Columns `d0` and `d1` contain lower and upper $16$ bits of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically: - When the context changes within a frame, these columns contain $(ctx' - ctx)$ in the "next" row. - When the context remains the same but the word address changes within a frame, these columns contain $(a' - a)$ in the "next" row. - - When both the context and the word address remain the same within a frame, these columns contain $(clk' - clk - 1)$ in the "next" row. + - When both the context and the word address remain the same within a frame, these columns contain $(clk' - clk)$ in the "next" row. - Column `t` contains the inverse of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically: - When the context changes within a frame, this column contains the inverse of $(ctx' - ctx)$ in the "next" row. - When the context remains the same but the word address changes within a frame, this column contains the inverse of $(a' - a)$ in the "next" row. - - When both the context and the word address remain the same within a frame, this column contains the inverse of $(clk' - clk - 1)$ in the "next" row. + - When both the context and the word address remain the same within a frame, this column contains the inverse of $(clk' - clk)$ in the "next" row. - Column `f_scw` stands for "flag same context and word address", which is set to $1$ when the current and previous rows have the same context and word address, and $0$ otherwise. For every memory access operation (i.e., read or write a word or element), a new row is added to the memory table. If neither `ctx` nor `addr` have changed, the `v` columns are set to equal the values from the previous row (except for any element written to). If `ctx` or `addr` have changed, then the `v` columns are initialized to $0$ (except for any element written to). @@ -265,10 +266,15 @@ To enforce the values of context ID, word address, and clock cycle grow monotoni f_{mem\_nl} \cdot \left(n_0 \cdot \Delta ctx + (1 - n_0) \cdot (n_1 \cdot \Delta a + (1 - n_1) \cdot \Delta clk) \right) - (2^{16} \cdot d_1' + d_0') = 0 \text{ | degree} = 8 $$ -Where $\Delta clk = clk' - clk - 1$. - In addition to this constraint, we also need to make sure that the values in registers $d_0$ and $d_1$ are less than $2^{16}$, and this can be done with [range checks](../range.md). +Next, we need to ensure that when the context, word address and clock are constant in a frame, then only read operations are allowed in that clock cycle. + +>$$ +f_{mem\_nl} \cdot f_{scw}' \cdot (1 - \Delta clk \cdot t') \cdot (1 - rw) \cdot (1 - rw') = 0 \text{ | degree} = 8 +$$ + + Next, for all frames where the "current" and "next" rows are in the chiplet, we need to ensure that the value of the `f_scw` column in the "next" row is set to $1$ when the context and word address are the same, and $0$ otherwise. >$$ diff --git a/miden/tests/integration/operations/io_ops/mem_ops.rs b/miden/tests/integration/operations/io_ops/mem_ops.rs index 0b0b5ab2d1..e2adc3e2d5 100644 --- a/miden/tests/integration/operations/io_ops/mem_ops.rs +++ b/miden/tests/integration/operations/io_ops/mem_ops.rs @@ -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) @@ -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] @@ -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); } diff --git a/processor/src/chiplets/memory/mod.rs b/processor/src/chiplets/memory/mod.rs index cab8336519..9e1d938e64 100644 --- a/processor/src/chiplets/memory/mod.rs +++ b/processor/src/chiplets/memory/mod.rs @@ -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); @@ -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); diff --git a/processor/src/chiplets/memory/segment.rs b/processor/src/chiplets/memory/segment.rs index 20ea1bb4f0..89eac5708b 100644 --- a/processor/src/chiplets/memory/segment.rs +++ b/processor/src/chiplets/memory/segment.rs @@ -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; @@ -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(); @@ -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(()) @@ -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( diff --git a/processor/src/chiplets/memory/tests.rs b/processor/src/chiplets/memory/tests.rs index 74123efa68..ca9c37ee12 100644 --- a/processor/src/chiplets/memory/tests.rs +++ b/processor/src/chiplets/memory/tests.rs @@ -510,6 +510,7 @@ fn read_trace_row(trace: &[Vec], 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], @@ -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; diff --git a/processor/src/errors.rs b/processor/src/errors.rs index 58009209e3..4851ff83d1 100644 --- a/processor/src/errors.rs +++ b/processor/src/errors.rs @@ -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()) )] @@ -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}")] diff --git a/processor/src/operations/io_ops.rs b/processor/src/operations/io_ops.rs index 9c6bc8782d..f9126b0740 100644 --- a/processor/src/operations/io_ops.rs +++ b/processor/src/operations/io_ops.rs @@ -264,13 +264,13 @@ impl Process { #[cfg(test)] mod tests { - use vm_core::{utils::ToElements, Word, ONE, ZERO}; + use vm_core::{assert_matches, utils::ToElements, Word, ONE, ZERO}; use super::{ super::{super::AdviceProvider, Operation, MIN_STACK_DEPTH}, Felt, Host, Process, }; - use crate::{AdviceSource, ContextId, DefaultHost}; + use crate::{AdviceSource, ContextId, DefaultHost, ExecutionError}; #[test] fn op_push() { @@ -635,6 +635,36 @@ mod tests { assert_eq!(expected, process.stack.trace_state()); } + /// Ensures that reading and writing in the same clock cycle results in an error. + #[test] + fn read_and_write_in_same_clock_cycle() { + let mut process = Process::new_dummy_with_decoder_helpers_and_empty_stack(); + assert_eq!(0, process.chiplets.memory().num_accessed_words()); + + // emulate reading and writing in the same clock cycle + process.ensure_trace_capacity(); + process.op_mload().unwrap(); + assert_matches!( + process.op_mstore(), + Err(ExecutionError::IllegalMemoryAccess { ctx: _, addr: _, clk: _ }) + ); + } + + /// Ensures that writing twice in the same clock cycle results in an error. + #[test] + fn write_twice_in_same_clock_cycle() { + let mut process = Process::new_dummy_with_decoder_helpers_and_empty_stack(); + assert_eq!(0, process.chiplets.memory().num_accessed_words()); + + // emulate reading and writing in the same clock cycle + process.ensure_trace_capacity(); + process.op_mstore().unwrap(); + assert_matches!( + process.op_mstore(), + Err(ExecutionError::IllegalMemoryAccess { ctx: _, addr: _, clk: _ }) + ); + } + // HELPER METHODS // -------------------------------------------------------------------------------------------- diff --git a/processor/src/trace/tests/range.rs b/processor/src/trace/tests/range.rs index 3e3f901d72..1d4444c756 100644 --- a/processor/src/trace/tests/range.rs +++ b/processor/src/trace/tests/range.rs @@ -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() { @@ -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(); @@ -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]); } }