feat(memory): allow more than 1 memory reads in the same clock cycle (same context & word address)

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)
 

air/src/constraints/chiplets/memory/mod.rs

@@ -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.
 ];
@@ -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);
 }
@@ -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.
 ///
@@ -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)]

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],
     };

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.
 
 >$$

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);
 }

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);

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 when the address being written to.
             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 when the address being written to.
             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(

processor/src/chiplets/memory/tests.rs

@@ -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],
@@ -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;

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}")]

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,48 @@ 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: _ })
+        );
+    }
+
+    /// Ensures that reading twice in the same clock cycle does NOT result in an error.
+    #[test]
+    fn read_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 in the same clock cycle
+        process.ensure_trace_capacity();
+        process.op_mload().unwrap();
+        process.op_mload().unwrap();
+    }
+
     // HELPER METHODS
     // --------------------------------------------------------------------------------------------