Skip to content

Commit e29e5b0

Browse files
committed
style: apply cargo fmt fixes for memory addr range check
Apply nightly rustfmt formatting to all files modified by the fix(air): enforce word_addr is a valid u32 change. Changes: - Reflow import groups to fit within nightly rustfmt's line-length rules - Reflow doc comments and inline comments to match nightly wrap width - Collapse single-expression let bindings that fit on one line - Lowercase hex literal 0xFFFF -> 0xffff (rustfmt convention) - Flatten multi-line arithmetic chains that fit within the width limit
1 parent f7bc645 commit e29e5b0

File tree

4 files changed

+24
-33
lines changed

4 files changed

+24
-33
lines changed

air/src/constraints/chiplets/memory.rs

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ use crate::{
3939
trace::{
4040
CHIPLETS_OFFSET,
4141
chiplets::{
42-
MEMORY_ADDR_HI_COL_IDX, MEMORY_ADDR_LO_COL_IDX, MEMORY_CLK_COL_IDX,
43-
MEMORY_CTX_COL_IDX, MEMORY_D_INV_COL_IDX, MEMORY_D0_COL_IDX, MEMORY_D1_COL_IDX,
42+
MEMORY_ADDR_HI_COL_IDX, MEMORY_ADDR_LO_COL_IDX, MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX,
43+
MEMORY_D_INV_COL_IDX, MEMORY_D0_COL_IDX, MEMORY_D1_COL_IDX,
4444
MEMORY_FLAG_SAME_CONTEXT_AND_WORD, MEMORY_IDX0_COL_IDX, MEMORY_IDX1_COL_IDX,
4545
MEMORY_IS_READ_COL_IDX, MEMORY_IS_WORD_ACCESS_COL_IDX, MEMORY_V_COL_RANGE,
4646
MEMORY_WORD_COL_IDX,
@@ -231,8 +231,8 @@ pub fn enforce_memory_constraints_all_rows<AB>(
231231
//
232232
// Fix: commit to the 16-bit limbs of word_addr (addr_lo, addr_hi) and add:
233233
// 1. Reconstruction: word_addr = addr_hi * 2^16 + addr_lo
234-
// 2. Range checks for addr_lo and addr_hi go through the existing range-check bus
235-
// (submitted from the prover's append_range_checks).
234+
// 2. Range checks for addr_lo and addr_hi go through the existing range-check bus (submitted
235+
// from the prover's append_range_checks).
236236
// 3. Overflow guard: 4 * addr_hi < 2^16, ensuring word_addr * 4 + 3 < 2^32.
237237
enforce_addr_range_check::<AB>(builder, memory_flag, &cols);
238238
}
@@ -683,11 +683,11 @@ pub fn flag_next_row_first_memory<E: PrimeCharacteristicRing>(
683683
/// `addr_hi = word_addr >> 16` and add three constraints:
684684
///
685685
/// 1. **Reconstruction**: `word_addr = addr_hi * 2^16 + addr_lo`
686-
/// 2. **Range checks**: `addr_lo ∈ [0, 2^16)` and `addr_hi ∈ [0, 2^16)` — submitted via
687-
/// the existing range-check bus in [`Memory::append_range_checks`].
688-
/// 3. **Overflow guard**: `4 * addr_hi < 2^16`, ensuring `word_addr * 4 + 3 < 2^32`,
689-
/// i.e. every element-level address derived from this word address is a valid u32.
690-
/// (This is also submitted as a range check: `4 * addr_hi` must be in `[0, 2^16)`.)
686+
/// 2. **Range checks**: `addr_lo ∈ [0, 2^16)` and `addr_hi ∈ [0, 2^16)` — submitted via the
687+
/// existing range-check bus in [`Memory::append_range_checks`].
688+
/// 3. **Overflow guard**: `4 * addr_hi < 2^16`, ensuring `word_addr * 4 + 3 < 2^32`, i.e. every
689+
/// element-level address derived from this word address is a valid u32. (This is also submitted
690+
/// as a range check: `4 * addr_hi` must be in `[0, 2^16)`.)
691691
///
692692
/// ## Why no new global columns are needed
693693
///

air/src/constraints/range/bus.rs

Lines changed: 7 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -90,13 +90,11 @@ where
9090
// Additional address range-check lookups: addr_lo, addr_hi, and 4*addr_hi.
9191
// These close the soundness gap where the delta-based range checks only bound
9292
// differences between consecutive addresses, not absolute address values.
93-
let mv_addr_lo: AB::ExprEF =
94-
alpha.into() + local.chiplets[MEMORY_ADDR_LO_IDX].clone().into();
95-
let mv_addr_hi: AB::ExprEF =
96-
alpha.into() + local.chiplets[MEMORY_ADDR_HI_IDX].clone().into();
93+
let mv_addr_lo: AB::ExprEF = alpha.into() + local.chiplets[MEMORY_ADDR_LO_IDX].clone().into();
94+
let mv_addr_hi: AB::ExprEF = alpha.into() + local.chiplets[MEMORY_ADDR_HI_IDX].clone().into();
9795
// 4 * addr_hi: enforces word_addr * 4 + 3 < 2^32 (overflow guard).
98-
let mv_addr_hi_x4: AB::ExprEF = alpha.into()
99-
+ AB::Expr::from_u16(4) * local.chiplets[MEMORY_ADDR_HI_IDX].clone().into();
96+
let mv_addr_hi_x4: AB::ExprEF =
97+
alpha.into() + AB::Expr::from_u16(4) * local.chiplets[MEMORY_ADDR_HI_IDX].clone().into();
10098

10199
// Stack lookups: sv0-sv3 = alpha + decoder helper columns
102100
let sv0: AB::ExprEF = alpha.into() + local.decoder[STACK_LOOKUP_BASE].clone().into();
@@ -108,11 +106,8 @@ where
108106
let range_check: AB::ExprEF = alpha.into() + local.range[RANGE_V_COL_IDX].clone().into();
109107

110108
// Combined lookup denominators
111-
let memory_lookups = mv0.clone()
112-
* mv1.clone()
113-
* mv_addr_lo.clone()
114-
* mv_addr_hi.clone()
115-
* mv_addr_hi_x4.clone();
109+
let memory_lookups =
110+
mv0.clone() * mv1.clone() * mv_addr_lo.clone() * mv_addr_hi.clone() * mv_addr_hi_x4.clone();
116111
let stack_lookups = sv0.clone() * sv1.clone() * sv2.clone() * sv3.clone();
117112
let lookups = range_check.clone() * stack_lookups.clone() * memory_lookups.clone();
118113

@@ -162,11 +157,7 @@ where
162157
* mv1.clone()
163158
* mv_addr_lo.clone()
164159
* mv_addr_hi_x4.clone();
165-
let m_addr_hi_x4_term = mflag_rc_stack
166-
* mv0
167-
* mv1
168-
* mv_addr_lo
169-
* mv_addr_hi;
160+
let m_addr_hi_x4_term = mflag_rc_stack * mv0 * mv1 * mv_addr_lo * mv_addr_hi;
170161

171162
// Main constraint: b_next * lookups = b * lookups + rc_term - s_terms - m_terms
172163
builder.tagged(TAG_RANGE_BUS_BASE, RANGE_BUS_NAME, |builder| {

processor/src/trace/chiplets/memory/mod.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,10 @@ use core::fmt::Debug;
44
use miden_air::trace::{
55
RowIndex,
66
chiplets::memory::{
7-
ADDR_HI_COL_IDX, ADDR_LO_COL_IDX, CLK_COL_IDX, CTX_COL_IDX, D_INV_COL_IDX,
8-
D0_COL_IDX, D1_COL_IDX, FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX,
9-
IS_READ_COL_IDX, IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD,
10-
MEMORY_READ, MEMORY_WRITE, V_COL_RANGE, WORD_COL_IDX,
7+
ADDR_HI_COL_IDX, ADDR_LO_COL_IDX, CLK_COL_IDX, CTX_COL_IDX, D_INV_COL_IDX, D0_COL_IDX,
8+
D1_COL_IDX, FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX, IS_READ_COL_IDX,
9+
IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD, MEMORY_READ,
10+
MEMORY_WRITE, V_COL_RANGE, WORD_COL_IDX,
1111
},
1212
};
1313

processor/src/trace/chiplets/memory/tests.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ use alloc::vec::Vec;
33
use miden_air::trace::{
44
RowIndex,
55
chiplets::memory::{
6-
ADDR_HI_COL_IDX, ADDR_LO_COL_IDX, FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX,
7-
IDX1_COL_IDX, IS_READ_COL_IDX, IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT,
8-
MEMORY_ACCESS_WORD, MEMORY_READ, MEMORY_WRITE, TRACE_WIDTH as MEMORY_TRACE_WIDTH,
6+
ADDR_HI_COL_IDX, ADDR_LO_COL_IDX, FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX,
7+
IS_READ_COL_IDX, IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD,
8+
MEMORY_READ, MEMORY_WRITE, TRACE_WIDTH as MEMORY_TRACE_WIDTH,
99
},
1010
};
1111
use miden_core::{ONE, WORD_SIZE, Word, ZERO, assert_matches, field::Field};
@@ -580,7 +580,7 @@ fn build_trace_row(
580580
// Populate address limb columns matching what fill_trace() writes.
581581
// ADDR_LO = word_addr & 0xFFFF, ADDR_HI = word_addr >> 16.
582582
let word_addr_u32: u32 = word.as_canonical_u64().try_into().unwrap();
583-
let addr_lo = u16::try_from(word_addr_u32 & 0xFFFF).unwrap();
583+
let addr_lo = u16::try_from(word_addr_u32 & 0xffff).unwrap();
584584
let addr_hi = u16::try_from(word_addr_u32 >> 16).unwrap();
585585
row[ADDR_LO_COL_IDX] = Felt::new(addr_lo as u64);
586586
row[ADDR_HI_COL_IDX] = Felt::new(addr_hi as u64);

0 commit comments

Comments
 (0)