miden_air/trace/
mod.rs

1use core::ops::Range;
2
3use chiplets::hasher::RATE_LEN;
4use miden_core::utils::range;
5
6mod challenges;
7pub use challenges::Challenges;
8
9pub mod chiplets;
10pub mod decoder;
11pub mod range;
12pub mod stack;
13
14mod rows;
15pub use rows::{RowIndex, RowIndexError};
16
17mod main_trace;
18pub use main_trace::{MainTrace, MainTraceRow};
19pub use miden_crypto::stark::air::AuxBuilder;
20
21// CONSTANTS
22// ================================================================================================
23
24/// The minimum length of the execution trace. This is the minimum required to support range checks.
25pub const MIN_TRACE_LEN: usize = 64;
26
27// MAIN TRACE LAYOUT
28// ------------------------------------------------------------------------------------------------
29
30//      system          decoder           stack      range checks       chiplets
31//    (6 columns)     (24 columns)    (19 columns)    (2 columns)     (20 columns)
32// ├───────────────┴───────────────┴───────────────┴───────────────┴─────────────────┤
33
34pub const SYS_TRACE_OFFSET: usize = 0;
35pub const SYS_TRACE_WIDTH: usize = 6;
36pub const SYS_TRACE_RANGE: Range<usize> = range(SYS_TRACE_OFFSET, SYS_TRACE_WIDTH);
37
38pub const CLK_COL_IDX: usize = SYS_TRACE_OFFSET;
39pub const CTX_COL_IDX: usize = SYS_TRACE_OFFSET + 1;
40pub const FN_HASH_OFFSET: usize = SYS_TRACE_OFFSET + 2;
41pub const FN_HASH_RANGE: Range<usize> = range(FN_HASH_OFFSET, 4);
42
43// decoder trace
44pub const DECODER_TRACE_OFFSET: usize = SYS_TRACE_RANGE.end;
45pub const DECODER_TRACE_WIDTH: usize = 24;
46pub const DECODER_TRACE_RANGE: Range<usize> = range(DECODER_TRACE_OFFSET, DECODER_TRACE_WIDTH);
47
48// Stack trace
49pub const STACK_TRACE_OFFSET: usize = DECODER_TRACE_RANGE.end;
50pub const STACK_TRACE_WIDTH: usize = 19;
51pub const STACK_TRACE_RANGE: Range<usize> = range(STACK_TRACE_OFFSET, STACK_TRACE_WIDTH);
52
53/// Label for log_precompile transcript state messages on the virtual table bus.
54pub const LOG_PRECOMPILE_LABEL: u8 = miden_core::operations::opcodes::LOGPRECOMPILE;
55
56pub mod log_precompile {
57    use core::ops::Range;
58
59    use miden_core::utils::range;
60
61    use super::chiplets::hasher::{CAPACITY_LEN, DIGEST_LEN};
62
63    // HELPER REGISTER LAYOUT
64    // --------------------------------------------------------------------------------------------
65
66    /// Decoder helper register index where the hasher address is stored for `log_precompile`.
67    pub const HELPER_ADDR_IDX: usize = 0;
68    /// Decoder helper register offset where `CAP_PREV` begins; spans four consecutive registers.
69    pub const HELPER_CAP_PREV_OFFSET: usize = 1;
70    /// Range covering the four helper registers holding `CAP_PREV`.
71    pub const HELPER_CAP_PREV_RANGE: Range<usize> = range(HELPER_CAP_PREV_OFFSET, CAPACITY_LEN);
72
73    // STACK LAYOUT (TOP OF STACK)
74    // --------------------------------------------------------------------------------------------
75    // After executing `log_precompile`, the top 12 stack elements contain `[R0, R1, CAP_NEXT]`
76    // in LE (structural) order.
77
78    pub const STACK_R0_BASE: usize = 0;
79    pub const STACK_R0_RANGE: Range<usize> = range(STACK_R0_BASE, DIGEST_LEN);
80
81    pub const STACK_R1_BASE: usize = STACK_R0_RANGE.end;
82    pub const STACK_R1_RANGE: Range<usize> = range(STACK_R1_BASE, DIGEST_LEN);
83
84    pub const STACK_CAP_NEXT_BASE: usize = STACK_R1_RANGE.end;
85    pub const STACK_CAP_NEXT_RANGE: Range<usize> = range(STACK_CAP_NEXT_BASE, CAPACITY_LEN);
86
87    /// Stack range containing `COMM` prior to executing `log_precompile`.
88    pub const STACK_COMM_RANGE: Range<usize> = STACK_R0_RANGE;
89    /// Stack range containing `TAG` prior to executing `log_precompile`.
90    pub const STACK_TAG_RANGE: Range<usize> = STACK_R1_RANGE;
91
92    // HASHER STATE LAYOUT
93    // --------------------------------------------------------------------------------------------
94    // The hasher permutation uses a 12-element state. With LE layout, the state is interpreted
95    // as [RATE0, RATE1, CAPACITY]:
96    // - RATE0 occupies the first 4 lanes (0..4),
97    // - RATE1 occupies the next 4 lanes (4..8),
98    // - CAPACITY occupies the last 4 lanes (8..12).
99    //
100    // For `log_precompile` this corresponds to:
101    // - input state words:  [COMM, TAG, CAP_PREV]
102    // - output state words: [R0,   R1,  CAP_NEXT]
103
104    pub const STATE_RATE_0_RANGE: Range<usize> = range(0, DIGEST_LEN);
105    pub const STATE_RATE_1_RANGE: Range<usize> = range(STATE_RATE_0_RANGE.end, DIGEST_LEN);
106    pub const STATE_CAP_RANGE: Range<usize> = range(STATE_RATE_1_RANGE.end, CAPACITY_LEN);
107}
108
109// Range check trace
110pub const RANGE_CHECK_TRACE_OFFSET: usize = STACK_TRACE_RANGE.end;
111pub const RANGE_CHECK_TRACE_WIDTH: usize = 2;
112pub const RANGE_CHECK_TRACE_RANGE: Range<usize> =
113    range(RANGE_CHECK_TRACE_OFFSET, RANGE_CHECK_TRACE_WIDTH);
114
115// Chiplets trace
116pub const CHIPLETS_OFFSET: usize = RANGE_CHECK_TRACE_RANGE.end;
117pub const CHIPLETS_WIDTH: usize = 20;
118pub const CHIPLETS_RANGE: Range<usize> = range(CHIPLETS_OFFSET, CHIPLETS_WIDTH);
119
120/// Shared chiplet selector columns at the start of the chiplets segment.
121pub const CHIPLET_SELECTORS_RANGE: Range<usize> = range(CHIPLETS_OFFSET, 5);
122pub const CHIPLET_S0_COL_IDX: usize = CHIPLET_SELECTORS_RANGE.start;
123pub const CHIPLET_S1_COL_IDX: usize = CHIPLET_SELECTORS_RANGE.start + 1;
124pub const CHIPLET_S2_COL_IDX: usize = CHIPLET_SELECTORS_RANGE.start + 2;
125pub const CHIPLET_S3_COL_IDX: usize = CHIPLET_SELECTORS_RANGE.start + 3;
126pub const CHIPLET_S4_COL_IDX: usize = CHIPLET_SELECTORS_RANGE.start + 4;
127
128pub const TRACE_WIDTH: usize = CHIPLETS_OFFSET + CHIPLETS_WIDTH;
129pub const PADDED_TRACE_WIDTH: usize = TRACE_WIDTH.next_multiple_of(RATE_LEN);
130
131// AUXILIARY COLUMNS LAYOUT
132// ------------------------------------------------------------------------------------------------
133
134//      decoder                     stack              range checks          chiplets
135//    (3 columns)                (1 column)             (1 column)          (3 column)
136// ├─────────────────────┴──────────────────────┴────────────────────┴───────────────────┤
137
138/// Decoder auxiliary columns
139pub const DECODER_AUX_TRACE_OFFSET: usize = 0;
140pub const DECODER_AUX_TRACE_WIDTH: usize = 3;
141pub const DECODER_AUX_TRACE_RANGE: Range<usize> =
142    range(DECODER_AUX_TRACE_OFFSET, DECODER_AUX_TRACE_WIDTH);
143
144/// Stack auxiliary columns
145pub const STACK_AUX_TRACE_OFFSET: usize = DECODER_AUX_TRACE_RANGE.end;
146pub const STACK_AUX_TRACE_WIDTH: usize = 1;
147pub const STACK_AUX_TRACE_RANGE: Range<usize> =
148    range(STACK_AUX_TRACE_OFFSET, STACK_AUX_TRACE_WIDTH);
149
150/// Range check auxiliary columns
151pub const RANGE_CHECK_AUX_TRACE_OFFSET: usize = STACK_AUX_TRACE_RANGE.end;
152pub const RANGE_CHECK_AUX_TRACE_WIDTH: usize = 1;
153pub const RANGE_CHECK_AUX_TRACE_RANGE: Range<usize> =
154    range(RANGE_CHECK_AUX_TRACE_OFFSET, RANGE_CHECK_AUX_TRACE_WIDTH);
155
156/// Chiplets virtual table auxiliary column.
157///
158/// This column combines two virtual tables:
159///
160/// 1. Hash chiplet's sibling table,
161/// 2. Kernel ROM chiplet's kernel procedure table.
162pub const HASH_KERNEL_VTABLE_AUX_TRACE_OFFSET: usize = RANGE_CHECK_AUX_TRACE_RANGE.end;
163pub const HASHER_AUX_TRACE_WIDTH: usize = 1;
164pub const HASHER_AUX_TRACE_RANGE: Range<usize> =
165    range(HASH_KERNEL_VTABLE_AUX_TRACE_OFFSET, HASHER_AUX_TRACE_WIDTH);
166
167/// Chiplets bus auxiliary columns.
168pub const CHIPLETS_BUS_AUX_TRACE_OFFSET: usize = HASHER_AUX_TRACE_RANGE.end;
169pub const CHIPLETS_BUS_AUX_TRACE_WIDTH: usize = 1;
170pub const CHIPLETS_BUS_AUX_TRACE_RANGE: Range<usize> =
171    range(CHIPLETS_BUS_AUX_TRACE_OFFSET, CHIPLETS_BUS_AUX_TRACE_WIDTH);
172
173/// ACE chiplet wiring bus.
174pub const ACE_CHIPLET_WIRING_BUS_OFFSET: usize = CHIPLETS_BUS_AUX_TRACE_RANGE.end;
175pub const ACE_CHIPLET_WIRING_BUS_WIDTH: usize = 1;
176pub const ACE_CHIPLET_WIRING_BUS_RANGE: Range<usize> =
177    range(ACE_CHIPLET_WIRING_BUS_OFFSET, ACE_CHIPLET_WIRING_BUS_WIDTH);
178
179/// Auxiliary trace segment width.
180pub const AUX_TRACE_WIDTH: usize = ACE_CHIPLET_WIRING_BUS_RANGE.end;
181
182/// Number of random challenges used for auxiliary trace constraints.
183pub const AUX_TRACE_RAND_CHALLENGES: usize = 2;
184
185/// Maximum number of coefficients used in bus message encodings.
186pub const MAX_MESSAGE_WIDTH: usize = 16;
187
188/// Bus message coefficient indices.
189///
190/// These define the standard positions for encoding bus messages using the pattern:
191/// `alpha + sum(beta_powers\[i\] * elem\[i\])` where:
192/// - `alpha` is the randomness base (accessed directly as `.alpha`)
193/// - `beta_powers\[i\] = beta^i` are the powers of beta
194///
195/// These indices refer to positions in the `beta_powers` array, not including alpha.
196///
197/// This layout is shared between:
198/// - AIR constraint builders (symbolic expressions): `Challenges<AB::ExprEF>`
199/// - Processor auxiliary trace builders (concrete field elements): `Challenges<E>`
200pub mod bus_message {
201    /// Label coefficient index: `beta_powers[0] = beta^0`.
202    ///
203    /// Used for transition type/operation label.
204    pub const LABEL_IDX: usize = 0;
205
206    /// Address coefficient index: `beta_powers[1] = beta^1`.
207    ///
208    /// Used for chiplet address.
209    pub const ADDR_IDX: usize = 1;
210
211    /// Node index coefficient index: `beta_powers[2] = beta^2`.
212    ///
213    /// Used for Merkle path position. Set to 0 for non-Merkle operations (SPAN, RESPAN, HPERM,
214    /// etc.).
215    pub const NODE_INDEX_IDX: usize = 2;
216
217    /// State start coefficient index: `beta_powers[3] = beta^3`.
218    ///
219    /// Beginning of hasher state. Hasher state occupies 8 consecutive coefficients:
220    /// `beta_powers[3..11]` (beta^3..beta^10) for `state[0..7]` (rate portion: RATE0 || RATE1).
221    pub const STATE_START_IDX: usize = 3;
222
223    /// Capacity start coefficient index: `beta_powers[11] = beta^11`.
224    ///
225    /// Beginning of hasher capacity. Hasher capacity occupies 4 consecutive coefficients:
226    /// `beta_powers[11..15]` (beta^11..beta^14) for `capacity[0..3]`.
227    pub const CAPACITY_START_IDX: usize = 11;
228
229    /// Capacity domain coefficient index: `beta_powers[12] = beta^12`.
230    ///
231    /// Second capacity element. Used for encoding operation-specific data (e.g., op_code in control
232    /// block messages).
233    pub const CAPACITY_DOMAIN_IDX: usize = CAPACITY_START_IDX + 1;
234}
miden_air/trace/mod.rs

miden_air/trace/
mod.rs
