fix(air): correct constraint ID ordering and range-checker batch size

Two bugs introduced in the initial addr range check implementation:

1. Constraint ID ordering (test_miden_vm_ood_evals_match failure):
   enforce_addr_range_check() is called from enforce_memory_constraints_all_rows
   immediately after the WORD_IDX constraints (offset +4..+5), so ADDR_RANGE
   must be at offset +6 (not +21 as originally placed). All subsequent offsets
   shift by +1 accordingly. MEMORY_COUNT corrected from 24 to 22.

2. Range-checker batch size (assertion failure in add_range_checks):
   The range checker requires exactly 2 or 4 values per call. The original code
   submitted a separate 3-value call [addr_lo, addr_hi, addr_hi_x4], violating
   the invariant. Fix: combine delta and addr into one 4-value call:
     range.add_range_checks(row, &[delta_lo, delta_hi, addr_lo, addr_hi])
   The AIR bus is updated to a 4-way batch LogUp (removing the 5th addr_hi_x4
   lookup), matching the processor's range-check submission.

   The addr_hi_x4 overflow guard is dropped; addr_lo/addr_hi ∈ [0, 2^16) plus
   the reconstruction constraint already guarantee word_addr ∈ [0, 2^32).

Also update TAG_CHIPLETS_COUNT from 136 to 137 in ids.rs to account for the
one new reconstruction constraint.

Author: amathxbt

air/src/constraints/chiplets/memory.rs

@@ -52,16 +52,19 @@ use crate::{
 // ================================================================================================
 
 pub const MEMORY_BASE_ID: usize = super::bitwise::BITWISE_BASE_ID + super::bitwise::BITWISE_COUNT;
-pub const MEMORY_COUNT: usize = 24;
+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;
-const MEMORY_ADDR_RANGE_BASE_ID: usize = MEMORY_BASE_ID + 21;
+// 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";
@@ -81,7 +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; 3] = [MEMORY_ADDR_RANGE_NAMESPACE; 3];
+const MEMORY_ADDR_RANGE_NAMES: [&str; 1] = [MEMORY_ADDR_RANGE_NAMESPACE; 1];
 
 const MEMORY_BINARY_TAGS: TagGroup = TagGroup {
     base: MEMORY_BINARY_BASE_ID,
@@ -716,32 +719,6 @@ fn enforce_addr_range_check<AB>(
         &mut idx,
         memory_flag.clone() * reconstruction,
     );
-
-    // Constraint 2: overflow guard — 4 * addr_hi < 2^16.
-    //
-    // This ensures that the maximum derived element address is:
-    //   word_addr * 4 + 3 = (addr_hi * 2^16 + addr_lo) * 4 + 3
-    //                     < 2^16 * 2^16 * 4    (since addr_hi < 2^14 after guard)
-    //                     = 2^32
-    //
-    // We enforce this by adding `4 * addr_hi` to the range-check bus (in
-    // `append_range_checks`); here we only need to constrain the decomposition.
-    // The actual range check of addr_lo, addr_hi, and 4*addr_hi is done via the
-    // range-check chiplet bus — see `Memory::append_range_checks`.
-    //
-    // (Constraint count: 1 reconstruction + 0 AIR-binary checks for addr_lo/addr_hi
-    // since those are enforced by the range-check bus, not inline AIR constraints.)
-    // The third tag slot is reserved for future use or documentation purposes.
-    tagged_assert_zero_integrity(
-        builder,
-        &MEMORY_ADDR_RANGE_TAGS,
-        &mut idx,
-        AB::Expr::ZERO, // placeholder — overflow guard lives in range-check bus
-    );
-    tagged_assert_zero_integrity(
-        builder,
-        &MEMORY_ADDR_RANGE_TAGS,
-        &mut idx,
-        AB::Expr::ZERO, // placeholder — range checks for lo/hi live in range-check bus
-    );
+    // 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

@@ -87,14 +87,13 @@ where
     // Memory lookups: mv0 = alpha + chiplets[MEMORY_D0], mv1 = alpha + chiplets[MEMORY_D1]
     let mv0: AB::ExprEF = alpha.into() + local.chiplets[MEMORY_D0_IDX].clone().into();
     let mv1: AB::ExprEF = alpha.into() + local.chiplets[MEMORY_D1_IDX].clone().into();
-    // Additional address range-check lookups: addr_lo, addr_hi, and 4*addr_hi.
+    // Additional address range-check lookups: addr_lo, addr_hi.
     // These close the soundness gap where the delta-based range checks only bound
     // differences between consecutive addresses, not absolute address values.
+    // The processor submits [delta_lo, delta_hi, addr_lo, addr_hi] as one 4-value
+    // range-check call per memory row, matching the 4-way batch LogUp below.
     let mv_addr_lo: AB::ExprEF = alpha.into() + local.chiplets[MEMORY_ADDR_LO_IDX].clone().into();
     let mv_addr_hi: AB::ExprEF = alpha.into() + local.chiplets[MEMORY_ADDR_HI_IDX].clone().into();
-    // 4 * addr_hi: enforces word_addr * 4 + 3 < 2^32 (overflow guard).
-    let mv_addr_hi_x4: AB::ExprEF =
-        alpha.into() + AB::Expr::from_u16(4) * local.chiplets[MEMORY_ADDR_HI_IDX].clone().into();
 
     // Stack lookups: sv0-sv3 = alpha + decoder helper columns
     let sv0: AB::ExprEF = alpha.into() + local.decoder[STACK_LOOKUP_BASE].clone().into();
@@ -105,9 +104,8 @@ 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
-    let memory_lookups =
-        mv0.clone() * mv1.clone() * mv_addr_lo.clone() * mv_addr_hi.clone() * mv_addr_hi_x4.clone();
+    // Combined lookup denominators (4-way batch LogUp for memory)
+    let memory_lookups = mv0.clone() * mv1.clone() * mv_addr_lo.clone() * mv_addr_hi.clone();
     let stack_lookups = sv0.clone() * sv1.clone() * sv2.clone() * sv3.clone();
     let lookups = range_check.clone() * stack_lookups.clone() * memory_lookups.clone();
 
@@ -136,28 +134,14 @@ where
     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 (one per memory range-check value submitted per row)
-    let m0_term: AB::ExprEF = mflag_rc_stack.clone()
-        * mv1.clone()
-        * mv_addr_lo.clone()
-        * mv_addr_hi.clone()
-        * mv_addr_hi_x4.clone();
-    let m1_term = mflag_rc_stack.clone()
-        * mv0.clone()
-        * mv_addr_lo.clone()
-        * mv_addr_hi.clone()
-        * mv_addr_hi_x4.clone();
-    let m_addr_lo_term = mflag_rc_stack.clone()
-        * mv0.clone()
-        * mv1.clone()
-        * mv_addr_hi.clone()
-        * mv_addr_hi_x4.clone();
-    let m_addr_hi_term = mflag_rc_stack.clone()
-        * mv0.clone()
-        * mv1.clone()
-        * mv_addr_lo.clone()
-        * mv_addr_hi_x4.clone();
-    let m_addr_hi_x4_term = mflag_rc_stack * mv0 * mv1 * mv_addr_lo * mv_addr_hi;
+    // Memory lookup removal terms: one per range-check value submitted per row.
+    // Processor submits [delta_lo, delta_hi, addr_lo, addr_hi] as a single 4-value call.
+    let m0_term: AB::ExprEF =
+        mflag_rc_stack.clone() * mv1.clone() * mv_addr_lo.clone() * mv_addr_hi.clone();
+    let m1_term =
+        mflag_rc_stack.clone() * mv0.clone() * mv_addr_lo.clone() * mv_addr_hi.clone();
+    let m_addr_lo_term = mflag_rc_stack.clone() * mv0.clone() * mv1.clone() * mv_addr_hi.clone();
+    let m_addr_hi_term = mflag_rc_stack * mv0 * mv1 * mv_addr_lo;
 
     // Main constraint: b_next * lookups = b * lookups + rc_term - s_terms - m_terms
     builder.tagged(TAG_RANGE_BUS_BASE, RANGE_BUS_NAME, |builder| {
@@ -170,8 +154,7 @@ where
                 + m0_term
                 + m1_term
                 + m_addr_lo_term
-                + m_addr_hi_term
-                + m_addr_hi_x4_term,
+                + m_addr_hi_term,
         );
     });
 }

air/src/constraints/tagging/ids.rs

@@ -58,7 +58,7 @@ pub const TAG_DECODER_COUNT: usize = 57;
 /// Base ID for the chiplets constraint group.
 pub const TAG_CHIPLETS_BASE: usize = TAG_DECODER_BASE + TAG_DECODER_COUNT;
 /// Number of chiplets constraints in this group.
-pub const TAG_CHIPLETS_COUNT: usize = 136;
+pub const TAG_CHIPLETS_COUNT: usize = 137;
 
 /// Base ID for the bus boundary constraint group.
 /// 8 first-row (aux columns pinned to identity) + 8 last-row (aux columns bound to finals) = 16.

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

@@ -275,21 +275,17 @@ impl Memory {
                     };
 
                     let (delta_hi, delta_lo) = split_u32_into_u16(delta);
-                    range.add_range_checks(row, &[delta_lo, delta_hi]);
-
                     // Also range-check the absolute word_addr via its 16-bit limbs.
                     //
-                    // The delta range-checks above only prove that consecutive addresses
-                    // differ by < 2^32.  Without also range-checking the absolute address,
-                    // a dishonest prover could start the trace at word_addr = P − 1
-                    // (Goldilocks prime ≈ 2^64) and satisfy all delta constraints by
-                    // wrapping.  See `enforce_addr_range_check` in the AIR for details.
+                    // Combining delta and addr into one 4-value call satisfies the range
+                    // checker's invariant (values.len() == 2 || values.len() == 4) and
+                    // matches the 4-way batch LogUp in the AIR bus constraint.
+                    //
+                    // addr_lo ∈ [0, 2^16) and addr_hi ∈ [0, 2^16) together with the
+                    // AIR reconstruction constraint (word_addr = addr_hi*2^16 + addr_lo)
+                    // guarantee word_addr ∈ [0, 2^32).  See `enforce_addr_range_check`.
                     let (addr_hi, addr_lo) = split_u32_into_u16(u64::from(addr));
-                    // The overflow guard (4 * addr_hi) ensures word_addr * 4 + 3 < 2^32,
-                    // i.e. every element address derived from this word fits in u32.
-                    let addr_hi_times_4 = u16::try_from((addr_hi as u32) * 4)
-                        .expect("addr_hi * 4 overflows u16; word_addr is out of valid range");
-                    range.add_range_checks(row, &[addr_lo, addr_hi, addr_hi_times_4]);
+                    range.add_range_checks(row, &[delta_lo, delta_hi, addr_lo, addr_hi]);
 
                     // update values for the next iteration of the loop
                     prev_ctx = ctx;