miden_air/trace/chiplets/
memory.rs

1use miden_core::WORD_SIZE;
2
3use super::{Felt, ONE, Range, ZERO, create_range};
4
5// CONSTANTS
6// ================================================================================================
7
8/// Number of columns needed to record an execution trace of the memory chiplet.
9pub const TRACE_WIDTH: usize = 15;
10
11// --- OPERATION SELECTORS ------------------------------------------------------------------------
12
13/// Specifies the value of the `READ_WRITE` column when the operation is a write.
14pub const MEMORY_WRITE: Felt = ZERO;
15/// Specifies the value of the `READ_WRITE` column when the operation is a read.
16pub const MEMORY_READ: Felt = ONE;
17/// Specifies the value of the `ELEMENT_OR_WORD` column when the operation is over an element.
18pub const MEMORY_ACCESS_ELEMENT: Felt = ZERO;
19/// Specifies the value of the `ELEMENT_OR_WORD` column when the operation is over a word.
20pub const MEMORY_ACCESS_WORD: Felt = ONE;
21
22// --- BUS LABELS ------------------------------------------------------------------------
23
24// All bus labels encode the chiplet selector (1, 1, 0), as well as the read/write and element/word
25// columns. The purpose of the label is to force the chiplet to assign the correct values to the
26// read/write and element/word columns. We also include the chiplet selector as a unique identifier
27// for memory chiplet labels (to ensure they don't collide with labels from other chiplets).
28
29/// Unique label when r/w=0 and e/w=0, computed as the full chiplet selector with the bits reversed,
30/// plus one.
31/// `selector = [1, 1, 0 | 0, 0]`, `flag = rev(selector) + 1 = [0, 0 | 0, 1, 1] + 1 = 4`
32pub const MEMORY_WRITE_ELEMENT_LABEL: u8 = 0b00011 + 1;
33
34/// Unique label when r/w=0 and e/w=1, computed as the full chiplet selector with the bits reversed,
35/// plus one.
36/// `selector = [1, 1, 0 | 0, 1]`, `flag = rev(selector) + 1 = [1, 0 | 0, 1, 1] + 1 = 20`
37pub const MEMORY_WRITE_WORD_LABEL: u8 = 0b10011 + 1;
38
39/// Unique label when r/w=1 and e/w=0, computed as the full chiplet selector with the bits reversed,
40/// plus one.
41/// `selector = [1, 1, 0 | 1, 0]`, `flag = rev(selector) + 1 = [0, 1 | 0, 1, 1] + 1 = 12`
42pub const MEMORY_READ_ELEMENT_LABEL: u8 = 0b01011 + 1;
43
44/// Unique label when r/w=1 and e/w=1, computed as the full chiplet selector with the bits reversed,
45/// plus one.
46/// `selector = [1, 1, 0 | 1, 1]`, `flag = rev(selector) + 1 = [1, 1 | 0, 1, 1] + 1 = 28`
47pub const MEMORY_READ_WORD_LABEL: u8 = 0b11011 + 1;
48
49// --- COLUMN ACCESSOR INDICES WITHIN THE CHIPLET -------------------------------------------------
50
51/// Column to hold whether the operation is a read or write.
52pub const IS_READ_COL_IDX: usize = 0;
53/// Column to hold the whether the operation was over an element or a word.
54pub const IS_WORD_ACCESS_COL_IDX: usize = IS_READ_COL_IDX + 1;
55/// Column to hold the context ID of the current memory context.
56pub const CTX_COL_IDX: usize = IS_WORD_ACCESS_COL_IDX + 1;
57/// Column to hold the word (i.e. group of 4 memory slots, referred to by the address of the first
58/// slot in the word).
59pub const WORD_COL_IDX: usize = CTX_COL_IDX + 1;
60/// Column to hold the first bit of the index of the address in the word.
61pub const IDX0_COL_IDX: usize = WORD_COL_IDX + 1;
62/// Column to hold the second bit of the index of the address in the word.
63pub const IDX1_COL_IDX: usize = IDX0_COL_IDX + 1;
64/// Column for the clock cycle in which the memory operation occurred.
65pub const CLK_COL_IDX: usize = IDX1_COL_IDX + 1;
66/// Columns to hold the values stored at a given memory context, word, and clock cycle after
67/// the memory operation. When reading from a new word, these are initialized to zero.
68pub const V_COL_RANGE: Range<usize> = create_range(CLK_COL_IDX + 1, WORD_SIZE);
69/// Column for the lower 16-bits of the delta between two consecutive context IDs, addresses, or
70/// clock cycles.
71pub const D0_COL_IDX: usize = V_COL_RANGE.end;
72/// Column for the upper 16-bits of the delta between two consecutive context IDs, addresses, or
73/// clock cycles.
74pub const D1_COL_IDX: usize = D0_COL_IDX + 1;
75/// Column for the inverse of the delta between two consecutive context IDs, addresses, or clock
76/// cycles, used to enforce that changes are correctly constrained.
77pub const D_INV_COL_IDX: usize = D1_COL_IDX + 1;
78/// Column to hold the flag indicating whether the current memory operation is in the same word and
79/// same context as the previous operation.
80pub const FLAG_SAME_CONTEXT_AND_WORD: usize = D_INV_COL_IDX + 1;
miden_air/trace/chiplets/memory.rs

miden_air/trace/chiplets/
memory.rs
