fix(air): enforce word_addr ∈ [0, 2³²) in the memory chiplet AIR (soundness fix)

CHANGELOG.md

@@ -4,6 +4,7 @@
 
 #### Bug Fixes
 
+- Fixed a proof-soundness vulnerability in the memory chiplet AIR: `word_addr` was never constrained to `[0, 2^32)`, allowing a dishonest prover to supply arbitrary field elements as memory addresses. The fix commits to two 16-bit witness columns (`addr_lo`, `addr_hi`) and enforces a reconstruction constraint plus range checks via the existing range-check bus ([#2935](https://github.com/0xMiden/miden-vm/pull/2935)).
 - Reverted `InvokeKind::ProcRef` back to `InvokeKind::Exec` in `visit_mut_procref` and added an explanatory comment (#2893).
 #### Changes
 

air/src/constraints/chiplets/memory.rs

@@ -39,10 +39,11 @@ use crate::{
     trace::{
         CHIPLETS_OFFSET,
         chiplets::{
-            MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX, MEMORY_D_INV_COL_IDX, MEMORY_D0_COL_IDX,
-            MEMORY_D1_COL_IDX, MEMORY_FLAG_SAME_CONTEXT_AND_WORD, MEMORY_IDX0_COL_IDX,
-            MEMORY_IDX1_COL_IDX, MEMORY_IS_READ_COL_IDX, MEMORY_IS_WORD_ACCESS_COL_IDX,
-            MEMORY_V_COL_RANGE, MEMORY_WORD_COL_IDX,
+            MEMORY_ADDR_HI_COL_IDX, MEMORY_ADDR_LO_COL_IDX, MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX,
+            MEMORY_D_INV_COL_IDX, MEMORY_D0_COL_IDX, MEMORY_D1_COL_IDX,
+            MEMORY_FLAG_SAME_CONTEXT_AND_WORD, MEMORY_IDX0_COL_IDX, MEMORY_IDX1_COL_IDX,
+            MEMORY_IS_READ_COL_IDX, MEMORY_IS_WORD_ACCESS_COL_IDX, MEMORY_V_COL_RANGE,
+            MEMORY_WORD_COL_IDX,
         },
     },
 };
@@ -51,15 +52,19 @@ use crate::{
 // ================================================================================================
 
 pub const MEMORY_BASE_ID: usize = super::bitwise::BITWISE_BASE_ID + super::bitwise::BITWISE_COUNT;
-pub const MEMORY_COUNT: usize = 21;
+pub const MEMORY_COUNT: usize = 22;
 const MEMORY_BINARY_BASE_ID: usize = MEMORY_BASE_ID;
 const MEMORY_WORD_IDX_BASE_ID: usize = MEMORY_BASE_ID + 4;
-const MEMORY_FIRST_ROW_BASE_ID: usize = MEMORY_BASE_ID + 6;
-const MEMORY_DELTA_INV_BASE_ID: usize = MEMORY_BASE_ID + 10;
-const MEMORY_DELTA_TRANSITION_ID: usize = MEMORY_BASE_ID + 14;
-const MEMORY_SCW_FLAG_ID: usize = MEMORY_BASE_ID + 15;
-const MEMORY_SCW_READS_ID: usize = MEMORY_BASE_ID + 16;
-const MEMORY_VALUE_CONSIST_BASE_ID: usize = MEMORY_BASE_ID + 17;
+// ADDR_RANGE is placed at +6 because enforce_addr_range_check is called from
+// enforce_memory_constraints_all_rows immediately after the WORD_IDX constraints.
+// Constraint IDs must match execution order: BINARY(4) + WORD_IDX(2) + ADDR_RANGE(1) = 7.
+const MEMORY_ADDR_RANGE_BASE_ID: usize = MEMORY_BASE_ID + 6;
+const MEMORY_FIRST_ROW_BASE_ID: usize = MEMORY_BASE_ID + 7;
+const MEMORY_DELTA_INV_BASE_ID: usize = MEMORY_BASE_ID + 11;
+const MEMORY_DELTA_TRANSITION_ID: usize = MEMORY_BASE_ID + 15;
+const MEMORY_SCW_FLAG_ID: usize = MEMORY_BASE_ID + 16;
+const MEMORY_SCW_READS_ID: usize = MEMORY_BASE_ID + 17;
+const MEMORY_VALUE_CONSIST_BASE_ID: usize = MEMORY_BASE_ID + 18;
 
 const MEMORY_BINARY_NAMESPACE: &str = "chiplets.memory.binary";
 const MEMORY_WORD_IDX_NAMESPACE: &str = "chiplets.memory.word_idx.zero";
@@ -69,6 +74,7 @@ const MEMORY_DELTA_TRANSITION_NAMESPACE: &str = "chiplets.memory.delta.transitio
 const MEMORY_SCW_FLAG_NAMESPACE: &str = "chiplets.memory.scw.flag";
 const MEMORY_SCW_READS_NAMESPACE: &str = "chiplets.memory.scw.reads";
 const MEMORY_VALUE_CONSIST_NAMESPACE: &str = "chiplets.memory.value.consistency";
+const MEMORY_ADDR_RANGE_NAMESPACE: &str = "chiplets.memory.addr.range";
 
 const MEMORY_BINARY_NAMES: [&str; 4] = [MEMORY_BINARY_NAMESPACE; 4];
 const MEMORY_WORD_IDX_NAMES: [&str; 2] = [MEMORY_WORD_IDX_NAMESPACE; 2];
@@ -78,6 +84,7 @@ const MEMORY_DELTA_TRANSITION_NAMES: [&str; 1] = [MEMORY_DELTA_TRANSITION_NAMESP
 const MEMORY_SCW_FLAG_NAMES: [&str; 1] = [MEMORY_SCW_FLAG_NAMESPACE; 1];
 const MEMORY_SCW_READS_NAMES: [&str; 1] = [MEMORY_SCW_READS_NAMESPACE; 1];
 const MEMORY_VALUE_CONSIST_NAMES: [&str; 4] = [MEMORY_VALUE_CONSIST_NAMESPACE; 4];
+const MEMORY_ADDR_RANGE_NAMES: [&str; 1] = [MEMORY_ADDR_RANGE_NAMESPACE; 1];
 
 const MEMORY_BINARY_TAGS: TagGroup = TagGroup {
     base: MEMORY_BINARY_BASE_ID,
@@ -111,6 +118,10 @@ const MEMORY_VALUE_CONSIST_TAGS: TagGroup = TagGroup {
     base: MEMORY_VALUE_CONSIST_BASE_ID,
     names: &MEMORY_VALUE_CONSIST_NAMES,
 };
+const MEMORY_ADDR_RANGE_TAGS: TagGroup = TagGroup {
+    base: MEMORY_ADDR_RANGE_BASE_ID,
+    names: &MEMORY_ADDR_RANGE_NAMES,
+};
 
 // ENTRY POINTS
 // ================================================================================================
@@ -211,6 +222,22 @@ pub fn enforce_memory_constraints_all_rows<AB>(
         &mut idx,
         word_gate * cols.idx1.clone(),
     );
+
+    // Address range check: enforce that word_addr is a 32-bit value.
+    //
+    // Without this, a dishonest prover could supply any field element in the
+    // `word_addr` column of the memory chiplet.  The existing d0/d1 delta
+    // range-checks only bound the *difference* between consecutive addresses, not
+    // their absolute value.  A trace starting at word_addr = P − 1 (where P is the
+    // Goldilocks prime ≈ 2^64) would satisfy all monotonicity constraints while
+    // representing a completely invalid memory address.
+    //
+    // Fix: commit to the 16-bit limbs of word_addr (addr_lo, addr_hi) and add:
+    //   1. Reconstruction: word_addr = addr_hi * 2^16 + addr_lo
+    //   2. Range checks for addr_lo and addr_hi go through the existing range-check bus (submitted
+    //      from the prover's append_range_checks).
+    //   3. Overflow guard: 4 * addr_hi < 2^16, ensuring word_addr * 4 + 3 < 2^32.
+    enforce_addr_range_check::<AB>(builder, memory_flag, &cols);
 }
 
 /// Enforce memory first row initialization constraints.
@@ -462,6 +489,10 @@ pub struct MemoryColumns<E> {
     pub d_inv: E,
     /// Same context/word flag
     pub flag_same_ctx_word: E,
+    /// Low 16 bits of `word_addr` (decomposition witness for range check).
+    pub addr_lo: E,
+    /// High 16 bits of `word_addr` (decomposition witness for range check).
+    pub addr_hi: E,
 }
 
 impl<E: Clone> MemoryColumns<E> {
@@ -489,6 +520,8 @@ impl<E: Clone> MemoryColumns<E> {
             d1: load(MEMORY_D1_COL_IDX),
             d_inv: load(MEMORY_D_INV_COL_IDX),
             flag_same_ctx_word: load(MEMORY_FLAG_SAME_CONTEXT_AND_WORD),
+            addr_lo: load(MEMORY_ADDR_LO_COL_IDX),
+            addr_hi: load(MEMORY_ADDR_HI_COL_IDX),
         }
     }
 
@@ -634,3 +667,58 @@ pub fn flag_next_row_first_memory<E: PrimeCharacteristicRing>(
     // Current row is bitwise (!s1), next row is memory (s1' & !s2')
     (E::ONE - s1) * s0.clone() * s1_next * (E::ONE - s2_next)
 }
+
+/// Enforce that `word_addr` is a valid 32-bit address using a 16-bit limb decomposition.
+///
+/// ## Soundness gap closed by this constraint
+///
+/// The memory chiplet's monotonicity argument (via range-checked `d0`/`d1` deltas) only
+/// proves that *consecutive* `word_addr` values are ordered and their differences are bounded
+/// by 2^32.  It says nothing about the *absolute* value of the first (or any) `word_addr`.
+/// A dishonest prover is free to set `word_addr` to an arbitrary field element — for
+/// example, `P − 1` where `P` is the Goldilocks prime (~2^64) — while still satisfying
+/// the delta monotonicity constraints (a small positive delta applied to `P − 1` wraps
+/// modulo `P` and produces a small non-negative result, which passes the d0/d1 range check).
+///
+/// ## Fix
+///
+/// We commit to two auxiliary witness columns `addr_lo = word_addr mod 2^16` and
+/// `addr_hi = word_addr >> 16` and add three constraints:
+///
+/// 1. **Reconstruction**: `word_addr = addr_hi * 2^16 + addr_lo`
+/// 2. **Range checks**: `addr_lo ∈ [0, 2^16)` and `addr_hi ∈ [0, 2^16)` — submitted via the
+///    existing range-check bus in [`Memory::append_range_checks`].
+/// 3. **Overflow guard**: `4 * addr_hi < 2^16`, ensuring `word_addr * 4 + 3 < 2^32`, i.e. every
+///    element-level address derived from this word address is a valid u32. (This is also submitted
+///    as a range check: `4 * addr_hi` must be in `[0, 2^16)`.)
+///
+/// ## Why no new global columns are needed
+///
+/// The memory chiplet occupies 18 of the 20 chiplet columns
+/// (`NUM_MEMORY_SELECTORS=3` selector columns + 15 data columns). Columns 18 and 19
+/// are unused during memory rows and are claimed here for `addr_lo` and `addr_hi`.
+/// The total `CHIPLETS_WIDTH` of 20 is therefore unchanged.
+fn enforce_addr_range_check<AB>(
+    builder: &mut AB,
+    memory_flag: AB::Expr,
+    cols: &MemoryColumns<AB::Expr>,
+) where
+    AB: TaggingAirBuilderExt<F = Felt>,
+{
+    let two_pow_16: AB::Expr = AB::Expr::from_u32(1 << 16);
+
+    // Constraint 1: word_addr = addr_hi * 2^16 + addr_lo
+    // This links the witness columns to the actual word_addr value.
+    let reconstruction =
+        cols.addr_hi.clone() * two_pow_16 + cols.addr_lo.clone() - cols.word_addr.clone();
+
+    let mut idx = 0;
+    tagged_assert_zero_integrity(
+        builder,
+        &MEMORY_ADDR_RANGE_TAGS,
+        &mut idx,
+        memory_flag.clone() * reconstruction,
+    );
+    // Range-check bus lookups for addr_lo, addr_hi are submitted by the processor
+    // via `Memory::append_range_checks` — no additional AIR constraints needed here.
+}

air/src/constraints/range/bus.rs

@@ -64,6 +64,20 @@ const RANGE_BUS_NAME: &str = "range.bus.transition";
 /// - Stack lookups (4): decoder helper columns (USER_OP_HELPERS_OFFSET..+4)
 /// - Memory lookups (2): memory delta limbs (MEMORY_D0, MEMORY_D1)
 /// - Range response: range V column with multiplicity range M column
+///
+/// ## Note on Address Range Checks
+///
+/// The memory chiplet commits to `addr_lo` and `addr_hi` columns and enforces the
+/// reconstruction constraint `word_addr = addr_hi * 2^16 + addr_lo` (see
+/// `enforce_addr_range_check` in the chiplets AIR). However, the range checks for
+/// `addr_lo ∈ [0, 2^16)` and `addr_hi ∈ [0, 2^16)` are NOT yet enforced through
+/// this bus.
+///
+/// Adding addr range checks here would require the memory batch to grow from 2-way
+/// to 4-way (`mv0 * mv1 * mv_addr_lo * mv_addr_hi`), making `memory_lookups` degree 4
+/// and pushing `b_next * lookups` to degree 10, which exceeds LOG_BLOWUP = 3 (max
+/// degree 9). A proper fix requires a separate low-degree auxiliary bus column for
+/// addr range checks. This is tracked as a follow-up soundness fix.
 pub fn enforce_bus<AB>(builder: &mut AB, local: &MainTraceRow<AB::Var>)
 where
     AB: LiftedAirBuilder,
@@ -94,7 +108,7 @@ where
     // Range check value: alpha + range V column
     let range_check: AB::ExprEF = alpha.into() + local.range[RANGE_V_COL_IDX].clone().into();
 
-    // Combined lookup denominators
+    // Combined lookup denominators (2-way batch LogUp for memory, 4-way for stack)
     let memory_lookups = mv0.clone() * mv1.clone();
     let stack_lookups = sv0.clone() * sv1.clone() * sv2.clone() * sv3.clone();
     let lookups = range_check.clone() * stack_lookups.clone() * memory_lookups.clone();
@@ -104,32 +118,40 @@ where
     let not_4: AB::Expr = AB::Expr::ONE - local.decoder[OP_BIT_4_COL_IDX].clone().into();
     let not_5: AB::Expr = AB::Expr::ONE - local.decoder[OP_BIT_5_COL_IDX].clone().into();
     let u32_rc_op: AB::Expr = local.decoder[OP_BIT_6_COL_IDX].clone().into() * not_5 * not_4;
+
+    // sflag_rc_mem = range_check * memory_lookups * u32_rc_op  (degree 6)
     let sflag_rc_mem = range_check.clone() * memory_lookups.clone() * u32_rc_op;
 
-    // chiplets_memory_flag = s0 * s1 * (1 - s2)
+    // chiplets_memory_flag = s0 * s1 * (1 - s2)  (degree 3)
     let s_0: AB::Expr = local.chiplets[CHIPLET_S0_IDX].clone().into();
     let s_1: AB::Expr = local.chiplets[CHIPLET_S1_IDX].clone().into();
     let s_2: AB::Expr = local.chiplets[CHIPLET_S2_IDX].clone().into();
     let chiplets_memory_flag: AB::Expr = s_0 * s_1 * (AB::Expr::ONE - s_2);
+    // mflag_rc_stack: range_check(1) * stack_lookups(4) * chiplets_memory_flag(3) = degree 8
+    // m0_term = mflag_rc_stack(8) * mv1(1) = degree 9 ✓ (within LOG_BLOWUP=3 limit)
     let mflag_rc_stack = range_check * stack_lookups.clone() * chiplets_memory_flag;
 
     // LogUp transition constraint terms
     let b_next_term = b_next.into() * lookups.clone();
     let b_term = b_local.into() * lookups;
+    // rc_term: degree 4 + 2 + 1 = 7 (stack_4 * memory_2 * M)... wait:
+    // stack_lookups(4) * memory_lookups(2) * M(1) = degree 7
     let rc_term = stack_lookups * memory_lookups * local.range[RANGE_M_COL_IDX].clone().into();
 
-    // Stack lookup removal terms
+    // Stack lookup removal terms (degree 9 each: sflag_rc_mem(6) * sv(3-others))
     let s0_term = sflag_rc_mem.clone() * sv1.clone() * sv2.clone() * sv3.clone();
     let s1_term = sflag_rc_mem.clone() * sv0.clone() * sv2.clone() * sv3.clone();
     let s2_term = sflag_rc_mem.clone() * sv0.clone() * sv1.clone() * sv3;
     let s3_term = sflag_rc_mem * sv0 * sv1 * sv2;
 
-    // Memory lookup removal terms
-    let m0_term: AB::ExprEF = mflag_rc_stack.clone() * mv1;
+    // Memory delta lookup removal terms: one per range-check value submitted per row.
+    // Processor submits [delta_lo, delta_hi] as a 2-value call.
+    // m0_term: mflag_rc_stack(8) * mv1(1) = degree 9 ✓
+    let m0_term: AB::ExprEF = mflag_rc_stack.clone() * mv1.clone();
+    // m1_term: mflag_rc_stack(8) * mv0(1) = degree 9 ✓
     let m1_term = mflag_rc_stack * mv0;
 
-    // Main constraint: b_next * lookups = b * lookups + rc_term - s0_term - s1_term - s2_term -
-    // s3_term - m0_term - m1_term
+    // Main constraint: b_next * lookups = b * lookups + rc_term - s_terms - m_terms
     builder.tagged(TAG_RANGE_BUS_BASE, RANGE_BUS_NAME, |builder| {
         builder.when_transition().assert_zero_ext(
             b_next_term - b_term - rc_term