diff --git a/CHANGELOG.md b/CHANGELOG.md index 68e6a79a9c..11ba91a263 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/air/src/constraints/chiplets/memory.rs b/air/src/constraints/chiplets/memory.rs index 2aa0472357..2552b23f0b 100644 --- a/air/src/constraints/chiplets/memory.rs +++ b/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( &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::(builder, memory_flag, &cols); } /// Enforce memory first row initialization constraints. @@ -462,6 +489,10 @@ pub struct MemoryColumns { 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 MemoryColumns { @@ -489,6 +520,8 @@ impl MemoryColumns { 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( // 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( + builder: &mut AB, + memory_flag: AB::Expr, + cols: &MemoryColumns, +) where + AB: TaggingAirBuilderExt, +{ + 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. +} diff --git a/air/src/constraints/range/bus.rs b/air/src/constraints/range/bus.rs index 07f4e6dcb6..eb32f72216 100644 --- a/air/src/constraints/range/bus.rs +++ b/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(builder: &mut AB, local: &MainTraceRow) 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 diff --git a/air/src/constraints/tagging/fixtures.rs b/air/src/constraints/tagging/fixtures.rs index 582ce11f61..81e5cffb19 100644 --- a/air/src/constraints/tagging/fixtures.rs +++ b/air/src/constraints/tagging/fixtures.rs @@ -1981,221 +1981,226 @@ pub fn current_group_expected() -> Vec { }, EvalRecord { id: 393, + namespace: "chiplets.memory.addr.range", + value: QuadFelt::new([Felt::new(12000934852794882889), Felt::new(0)]), + }, + EvalRecord { + id: 394, namespace: "chiplets.memory.first_row.zero", value: QuadFelt::new([Felt::new(16535341688150290637), Felt::new(0)]), }, EvalRecord { - id: 394, + id: 395, namespace: "chiplets.memory.first_row.zero", value: QuadFelt::new([Felt::new(10335801429662869046), Felt::new(0)]), }, EvalRecord { - id: 395, + id: 396, namespace: "chiplets.memory.first_row.zero", value: QuadFelt::new([Felt::new(17069212044771710732), Felt::new(0)]), }, EvalRecord { - id: 396, + id: 397, namespace: "chiplets.memory.first_row.zero", value: QuadFelt::new([Felt::new(2325691270454543127), Felt::new(0)]), }, EvalRecord { - id: 397, + id: 398, namespace: "chiplets.memory.delta.inv", value: QuadFelt::new([Felt::new(3175424288859001789), Felt::new(0)]), }, EvalRecord { - id: 398, + id: 399, namespace: "chiplets.memory.delta.inv", value: QuadFelt::new([Felt::new(2653406619128719065), Felt::new(0)]), }, EvalRecord { - id: 399, + id: 400, namespace: "chiplets.memory.delta.inv", value: QuadFelt::new([Felt::new(17858142172042463544), Felt::new(0)]), }, EvalRecord { - id: 400, + id: 401, namespace: "chiplets.memory.delta.inv", value: QuadFelt::new([Felt::new(6206863499132972446), Felt::new(0)]), }, EvalRecord { - id: 401, + id: 402, namespace: "chiplets.memory.delta.transition", value: QuadFelt::new([Felt::new(5078351230126014060), Felt::new(0)]), }, EvalRecord { - id: 402, + id: 403, namespace: "chiplets.memory.scw.flag", value: QuadFelt::new([Felt::new(18433800756547531428), Felt::new(0)]), }, EvalRecord { - id: 403, + id: 404, namespace: "chiplets.memory.scw.reads", value: QuadFelt::new([Felt::new(1473872865192822987), Felt::new(0)]), }, EvalRecord { - id: 404, + id: 405, namespace: "chiplets.memory.value.consistency", value: QuadFelt::new([Felt::new(11685142466069024125), Felt::new(0)]), }, EvalRecord { - id: 405, + id: 406, namespace: "chiplets.memory.value.consistency", value: QuadFelt::new([Felt::new(15197055428524072106), Felt::new(0)]), }, EvalRecord { - id: 406, + id: 407, namespace: "chiplets.memory.value.consistency", value: QuadFelt::new([Felt::new(14617718835619740558), Felt::new(0)]), }, EvalRecord { - id: 407, + id: 408, namespace: "chiplets.memory.value.consistency", value: QuadFelt::new([Felt::new(12293856690108503135), Felt::new(0)]), }, EvalRecord { - id: 408, + id: 409, namespace: "chiplets.ace.selector.binary", value: QuadFelt::new([Felt::new(2923257613600653893), Felt::new(0)]), }, EvalRecord { - id: 409, + id: 410, namespace: "chiplets.ace.selector.binary", value: QuadFelt::new([Felt::new(4182752542556273997), Felt::new(0)]), }, EvalRecord { - id: 410, + id: 411, namespace: "chiplets.ace.section.flags", value: QuadFelt::new([Felt::new(6988234832692930146), Felt::new(0)]), }, EvalRecord { - id: 411, + id: 412, namespace: "chiplets.ace.section.flags", value: QuadFelt::new([Felt::new(835405595669725766), Felt::new(0)]), }, EvalRecord { - id: 412, + id: 413, namespace: "chiplets.ace.section.flags", value: QuadFelt::new([Felt::new(17586531527103856415), Felt::new(0)]), }, EvalRecord { - id: 413, + id: 414, namespace: "chiplets.ace.section.flags", value: QuadFelt::new([Felt::new(17554338302334456122), Felt::new(0)]), }, EvalRecord { - id: 414, + id: 415, namespace: "chiplets.ace.section.flags", value: QuadFelt::new([Felt::new(7430977299237244825), Felt::new(0)]), }, EvalRecord { - id: 415, + id: 416, namespace: "chiplets.ace.section.transition", value: QuadFelt::new([Felt::new(9634147153406944231), Felt::new(0)]), }, EvalRecord { - id: 416, + id: 417, namespace: "chiplets.ace.section.transition", value: QuadFelt::new([Felt::new(3218972305890399047), Felt::new(0)]), }, EvalRecord { - id: 417, + id: 418, namespace: "chiplets.ace.section.transition", value: QuadFelt::new([Felt::new(13940329983080013930), Felt::new(0)]), }, EvalRecord { - id: 418, + id: 419, namespace: "chiplets.ace.section.transition", value: QuadFelt::new([Felt::new(10279516906957804027), Felt::new(0)]), }, EvalRecord { - id: 419, + id: 420, namespace: "chiplets.ace.read.ids", value: QuadFelt::new([Felt::new(12585176929173957399), Felt::new(0)]), }, EvalRecord { - id: 420, + id: 421, namespace: "chiplets.ace.read.to_eval", value: QuadFelt::new([Felt::new(30354383937781757), Felt::new(0)]), }, EvalRecord { - id: 421, + id: 422, namespace: "chiplets.ace.eval.op", value: QuadFelt::new([Felt::new(12481984196006840571), Felt::new(0)]), }, EvalRecord { - id: 422, + id: 423, namespace: "chiplets.ace.eval.result", value: QuadFelt::new([Felt::new(10009759308289170950), Felt::new(0)]), }, EvalRecord { - id: 423, + id: 424, namespace: "chiplets.ace.eval.result", value: QuadFelt::new([Felt::new(9663557940632289707), Felt::new(0)]), }, EvalRecord { - id: 424, + id: 425, namespace: "chiplets.ace.final.zero", value: QuadFelt::new([Felt::new(13957751954200526468), Felt::new(0)]), }, EvalRecord { - id: 425, + id: 426, namespace: "chiplets.ace.final.zero", value: QuadFelt::new([Felt::new(13589615335587828352), Felt::new(0)]), }, EvalRecord { - id: 426, + id: 427, namespace: "chiplets.ace.final.zero", value: QuadFelt::new([Felt::new(6818409555600730615), Felt::new(0)]), }, EvalRecord { - id: 427, + id: 428, namespace: "chiplets.ace.first_row.start", value: QuadFelt::new([Felt::new(613969461051885369), Felt::new(0)]), }, EvalRecord { - id: 428, + id: 429, namespace: "chiplets.kernel_rom.sfirst.binary", value: QuadFelt::new([Felt::new(9960038227923904827), Felt::new(0)]), }, EvalRecord { - id: 429, + id: 430, namespace: "chiplets.kernel_rom.digest.contiguity", value: QuadFelt::new([Felt::new(12113043600978981430), Felt::new(0)]), }, EvalRecord { - id: 430, + id: 431, namespace: "chiplets.kernel_rom.digest.contiguity", value: QuadFelt::new([Felt::new(15559322172686928295), Felt::new(0)]), }, EvalRecord { - id: 431, + id: 432, namespace: "chiplets.kernel_rom.digest.contiguity", value: QuadFelt::new([Felt::new(12593211604980696045), Felt::new(0)]), }, EvalRecord { - id: 432, + id: 433, namespace: "chiplets.kernel_rom.digest.contiguity", value: QuadFelt::new([Felt::new(4420066076215265302), Felt::new(0)]), }, EvalRecord { - id: 433, + id: 434, namespace: "chiplets.kernel_rom.first_row.start", value: QuadFelt::new([Felt::new(3652575802134874675), Felt::new(0)]), }, EvalRecord { - id: 434, + id: 435, namespace: "bus.boundary.first_row", value: QuadFelt::new([Felt::new(9595061266498737687), Felt::new(12539219129346040916)]), }, EvalRecord { - id: 435, + id: 436, namespace: "bus.boundary.first_row", value: QuadFelt::new([Felt::new(9906922257952985525), Felt::new(7135908125271346815)]), }, EvalRecord { - id: 436, + id: 437, namespace: "bus.boundary.first_row", value: QuadFelt::new([ Felt::new(12010012593361720439), @@ -2203,12 +2208,12 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 437, + id: 438, namespace: "bus.boundary.first_row", value: QuadFelt::new([Felt::new(15694046535368016026), Felt::new(2643587524945520847)]), }, EvalRecord { - id: 438, + id: 439, namespace: "bus.boundary.first_row", value: QuadFelt::new([ Felt::new(14293326901983424168), @@ -2216,47 +2221,47 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 439, + id: 440, namespace: "bus.boundary.first_row", value: QuadFelt::new([Felt::new(7543823668837069064), Felt::new(1474978857022258416)]), }, EvalRecord { - id: 440, + id: 441, namespace: "bus.boundary.first_row", value: QuadFelt::new([Felt::new(12608813705579209032), Felt::new(3989096837606726344)]), }, EvalRecord { - id: 441, + id: 442, namespace: "bus.boundary.first_row", value: QuadFelt::new([Felt::new(9950426725853620663), Felt::new(6907538708340539779)]), }, EvalRecord { - id: 442, + id: 443, namespace: "bus.boundary.last_row", value: QuadFelt::new([Felt::new(16755949710966147218), Felt::new(3829676215971849169)]), }, EvalRecord { - id: 443, + id: 444, namespace: "bus.boundary.last_row", value: QuadFelt::new([Felt::new(3258168421295425687), Felt::new(11322075087561196224)]), }, EvalRecord { - id: 444, + id: 445, namespace: "bus.boundary.last_row", value: QuadFelt::new([Felt::new(7867249080765390980), Felt::new(6932757161403890473)]), }, EvalRecord { - id: 445, + id: 446, namespace: "bus.boundary.last_row", value: QuadFelt::new([Felt::new(10129458707234267975), Felt::new(5812206347609968155)]), }, EvalRecord { - id: 446, + id: 447, namespace: "bus.boundary.last_row", value: QuadFelt::new([Felt::new(3253668216479680364), Felt::new(9725218274111543600)]), }, EvalRecord { - id: 447, + id: 448, namespace: "bus.boundary.last_row", value: QuadFelt::new([ Felt::new(10901759410743368556), @@ -2264,7 +2269,7 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 448, + id: 449, namespace: "bus.boundary.last_row", value: QuadFelt::new([ Felt::new(11130917779834521749), @@ -2272,12 +2277,12 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 449, + id: 450, namespace: "bus.boundary.last_row", value: QuadFelt::new([Felt::new(5654815015773734620), Felt::new(8487995846868635892)]), }, EvalRecord { - id: 450, + id: 451, namespace: "range.bus.transition", value: QuadFelt::new([ Felt::new(10365289165200035540), @@ -2285,12 +2290,12 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 451, + id: 452, namespace: "stack.overflow.bus.transition", value: QuadFelt::new([Felt::new(7384164985445418427), Felt::new(3858806565449404456)]), }, EvalRecord { - id: 452, + id: 453, namespace: "decoder.bus.p1.transition", value: QuadFelt::new([ Felt::new(11611432650982424455), @@ -2298,7 +2303,7 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 453, + id: 454, namespace: "decoder.bus.p2.transition", value: QuadFelt::new([ Felt::new(15040597896341508305), @@ -2306,182 +2311,182 @@ pub fn current_group_expected() -> Vec { ]), }, EvalRecord { - id: 454, + id: 455, namespace: "decoder.bus.p3.transition", value: QuadFelt::new([Felt::new(9395869302542898577), Felt::new(6472917827183803848)]), }, EvalRecord { - id: 455, + id: 456, namespace: "chiplets.bus.hash_kernel.transition", value: QuadFelt::new([Felt::new(4291070431816775519), Felt::new(7576850277917859979)]), }, EvalRecord { - id: 456, + id: 457, namespace: "chiplets.bus.chiplets.transition", value: QuadFelt::new([Felt::new(7990980974626587792), Felt::new(5675027937982935418)]), }, EvalRecord { - id: 457, + id: 458, namespace: "chiplets.bus.wiring.transition", value: QuadFelt::new([Felt::new(7613678356270986878), Felt::new(10445474671979834467)]), }, EvalRecord { - id: 458, + id: 459, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(15272471560572797098), Felt::new(0)]), }, EvalRecord { - id: 459, + id: 460, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(6210121216967517740), Felt::new(0)]), }, EvalRecord { - id: 460, + id: 461, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(6183121070077706579), Felt::new(0)]), }, EvalRecord { - id: 461, + id: 462, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(9532591940374591279), Felt::new(0)]), }, EvalRecord { - id: 462, + id: 463, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(6543026845990824540), Felt::new(0)]), }, EvalRecord { - id: 463, + id: 464, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(12968646586941648028), Felt::new(0)]), }, EvalRecord { - id: 464, + id: 465, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(15417838146196464330), Felt::new(0)]), }, EvalRecord { - id: 465, + id: 466, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(13833104913151358010), Felt::new(0)]), }, EvalRecord { - id: 466, + id: 467, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(16618206067970158350), Felt::new(0)]), }, EvalRecord { - id: 467, + id: 468, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(4151771141262045661), Felt::new(0)]), }, EvalRecord { - id: 468, + id: 469, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(10573320072889417521), Felt::new(0)]), }, EvalRecord { - id: 469, + id: 470, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(10186179372804063393), Felt::new(0)]), }, EvalRecord { - id: 470, + id: 471, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(4590904619046098580), Felt::new(0)]), }, EvalRecord { - id: 471, + id: 472, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(4720108777520454648), Felt::new(0)]), }, EvalRecord { - id: 472, + id: 473, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(1104703905961606104), Felt::new(0)]), }, EvalRecord { - id: 473, + id: 474, namespace: "public_inputs.stack_input", value: QuadFelt::new([Felt::new(4555570289354185559), Felt::new(0)]), }, EvalRecord { - id: 474, + id: 475, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(4934304800106382014), Felt::new(0)]), }, EvalRecord { - id: 475, + id: 476, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(5378514856609319392), Felt::new(0)]), }, EvalRecord { - id: 476, + id: 477, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(17190327489693035335), Felt::new(0)]), }, EvalRecord { - id: 477, + id: 478, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(12600879734326452251), Felt::new(0)]), }, EvalRecord { - id: 478, + id: 479, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(5557099402378706294), Felt::new(0)]), }, EvalRecord { - id: 479, + id: 480, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(13124668006842155196), Felt::new(0)]), }, EvalRecord { - id: 480, + id: 481, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(17115224159882577972), Felt::new(0)]), }, EvalRecord { - id: 481, + id: 482, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(329687429495640731), Felt::new(0)]), }, EvalRecord { - id: 482, + id: 483, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(17291436379366401128), Felt::new(0)]), }, EvalRecord { - id: 483, + id: 484, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(6803320890344610422), Felt::new(0)]), }, EvalRecord { - id: 484, + id: 485, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(11244089584150196777), Felt::new(0)]), }, EvalRecord { - id: 485, + id: 486, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(4009248599872349722), Felt::new(0)]), }, EvalRecord { - id: 486, + id: 487, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(16110944964025361102), Felt::new(0)]), }, EvalRecord { - id: 487, + id: 488, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(15140047176671544897), Felt::new(0)]), }, EvalRecord { - id: 488, + id: 489, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(16756664313597184040), Felt::new(0)]), }, EvalRecord { - id: 489, + id: 490, namespace: "public_inputs.stack_output", value: QuadFelt::new([Felt::new(2298685071572703448), Felt::new(0)]), }, diff --git a/air/src/constraints/tagging/ids.rs b/air/src/constraints/tagging/ids.rs index bb923c59ca..76ad57e021 100644 --- a/air/src/constraints/tagging/ids.rs +++ b/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. diff --git a/air/src/trace/chiplets/memory.rs b/air/src/trace/chiplets/memory.rs index 8b2475ce76..8aac833282 100644 --- a/air/src/trace/chiplets/memory.rs +++ b/air/src/trace/chiplets/memory.rs @@ -6,7 +6,7 @@ use super::{Felt, ONE, Range, ZERO, create_range}; // ================================================================================================ /// Number of columns needed to record an execution trace of the memory chiplet. -pub const TRACE_WIDTH: usize = 15; +pub const TRACE_WIDTH: usize = 17; // --- OPERATION SELECTORS ------------------------------------------------------------------------ @@ -78,3 +78,21 @@ pub const D_INV_COL_IDX: usize = D1_COL_IDX + 1; /// Column to hold the flag indicating whether the current memory operation is in the same word and /// same context as the previous operation. pub const FLAG_SAME_CONTEXT_AND_WORD: usize = D_INV_COL_IDX + 1; +/// Column to hold the low 16 bits of `word_addr`, used to range-check the absolute address +/// and close the AIR soundness gap described in [memory constraints docs]. +/// +/// A malicious prover could otherwise supply a `word_addr` larger than 2^32 in the chiplet +/// trace; the existing delta range-checks only bound *differences* between consecutive +/// addresses, not the absolute starting value. By committing to and range-checking the +/// 16-bit limbs we close that gap without adding new global trace columns (the memory +/// chiplet occupies 18 of the 20 available chiplet columns, leaving these two spare). +pub const ADDR_LO_COL_IDX: usize = FLAG_SAME_CONTEXT_AND_WORD + 1; +/// Column to hold the high 16 bits of `word_addr` (bits 16–31). +/// +/// Together with [`ADDR_LO_COL_IDX`], these two columns satisfy: +/// `word_addr = ADDR_HI * 2^16 + ADDR_LO`, with `ADDR_LO, ADDR_HI ∈ [0, 2^16)`. +/// +/// Additionally we enforce `4 * ADDR_HI < 2^16`, which guarantees that +/// `word_addr * 4 + 3 < 2^32` (i.e. every element address derived from this word +/// fits in the u32 range). +pub const ADDR_HI_COL_IDX: usize = ADDR_LO_COL_IDX + 1; diff --git a/air/src/trace/chiplets/mod.rs b/air/src/trace/chiplets/mod.rs index bf2fec08ec..2ced906a26 100644 --- a/air/src/trace/chiplets/mod.rs +++ b/air/src/trace/chiplets/mod.rs @@ -123,3 +123,7 @@ pub const MEMORY_D_INV_COL_IDX: usize = MEMORY_TRACE_OFFSET + memory::D_INV_COL_ /// and same word as the previous operation. pub const MEMORY_FLAG_SAME_CONTEXT_AND_WORD: usize = MEMORY_TRACE_OFFSET + memory::FLAG_SAME_CONTEXT_AND_WORD; +/// Global index of the low 16-bit address limb column in the memory chiplet trace. +pub const MEMORY_ADDR_LO_COL_IDX: usize = MEMORY_TRACE_OFFSET + memory::ADDR_LO_COL_IDX; +/// Global index of the high 16-bit address limb column in the memory chiplet trace. +pub const MEMORY_ADDR_HI_COL_IDX: usize = MEMORY_TRACE_OFFSET + memory::ADDR_HI_COL_IDX; diff --git a/processor/src/trace/chiplets/memory/mod.rs b/processor/src/trace/chiplets/memory/mod.rs index ff2ef64266..a6c068c272 100644 --- a/processor/src/trace/chiplets/memory/mod.rs +++ b/processor/src/trace/chiplets/memory/mod.rs @@ -4,8 +4,8 @@ use core::fmt::Debug; use miden_air::trace::{ RowIndex, chiplets::memory::{ - CLK_COL_IDX, CTX_COL_IDX, D_INV_COL_IDX, D0_COL_IDX, D1_COL_IDX, - FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX, IS_READ_COL_IDX, + ADDR_HI_COL_IDX, ADDR_LO_COL_IDX, CLK_COL_IDX, CTX_COL_IDX, D_INV_COL_IDX, D0_COL_IDX, + D1_COL_IDX, FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX, IS_READ_COL_IDX, IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD, MEMORY_READ, MEMORY_WRITE, V_COL_RANGE, WORD_COL_IDX, }, @@ -275,6 +275,14 @@ impl Memory { }; let (delta_hi, delta_lo) = split_u32_into_u16(delta); + // Range-check the delta limbs to enforce consecutive-address ordering. + // NOTE: addr_lo/addr_hi are committed in the trace and the AIR enforces + // word_addr = addr_hi*2^16 + addr_lo (reconstruction constraint), but + // the range checks addr_lo ∈ [0,2^16) and addr_hi ∈ [0,2^16) are NOT + // yet submitted here because adding them to the 2-way delta batch would + // require a 4-way batch (memory_lookups degree 4), pushing the LogUp + // bus transition constraint to degree 10 (> LOG_BLOWUP=3 limit of 9). + // A proper fix uses a separate low-degree B_ADDR auxiliary bus. range.add_range_checks(row, &[delta_lo, delta_hi]); // update values for the next iteration of the loop @@ -363,6 +371,13 @@ impl Memory { trace.set(row, FLAG_SAME_CONTEXT_AND_WORD, ZERO); }; + // Populate address limb columns: addr_lo = word_addr & 0xFFFF, + // addr_hi = word_addr >> 16. These are used by the AIR to enforce + // that word_addr is a valid 32-bit value (see enforce_addr_range_check). + let (addr_hi_u16, addr_lo_u16) = split_u32_into_u16(addr as u64); + trace.set(row, ADDR_LO_COL_IDX, Felt::new(addr_lo_u16 as u64)); + trace.set(row, ADDR_HI_COL_IDX, Felt::new(addr_hi_u16 as u64)); + // update values for the next iteration of the loop prev_ctx = ctx; prev_addr = felt_addr; diff --git a/processor/src/trace/chiplets/memory/tests.rs b/processor/src/trace/chiplets/memory/tests.rs index c936b43375..c635b68992 100644 --- a/processor/src/trace/chiplets/memory/tests.rs +++ b/processor/src/trace/chiplets/memory/tests.rs @@ -3,9 +3,9 @@ use alloc::vec::Vec; use miden_air::trace::{ RowIndex, chiplets::memory::{ - FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX, IS_READ_COL_IDX, - IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD, MEMORY_READ, - MEMORY_WRITE, TRACE_WIDTH as MEMORY_TRACE_WIDTH, + ADDR_HI_COL_IDX, ADDR_LO_COL_IDX, FLAG_SAME_CONTEXT_AND_WORD, IDX0_COL_IDX, IDX1_COL_IDX, + IS_READ_COL_IDX, IS_WORD_ACCESS_COL_IDX, MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD, + MEMORY_READ, MEMORY_WRITE, TRACE_WIDTH as MEMORY_TRACE_WIDTH, }, }; use miden_core::{ONE, WORD_SIZE, Word, ZERO, assert_matches, field::Field}; @@ -577,6 +577,14 @@ fn build_trace_row( row[FLAG_SAME_CONTEXT_AND_WORD] = ZERO; } + // Populate address limb columns matching what fill_trace() writes. + // ADDR_LO = word_addr & 0xFFFF, ADDR_HI = word_addr >> 16. + let word_addr_u32: u32 = word.as_canonical_u64().try_into().unwrap(); + let addr_lo = u16::try_from(word_addr_u32 & 0xffff).unwrap(); + let addr_hi = u16::try_from(word_addr_u32 >> 16).unwrap(); + row[ADDR_LO_COL_IDX] = Felt::new(addr_lo as u64); + row[ADDR_HI_COL_IDX] = Felt::new(addr_hi as u64); + row } diff --git a/processor/src/trace/chiplets/mod.rs b/processor/src/trace/chiplets/mod.rs index e45690918e..31a6e405a2 100644 --- a/processor/src/trace/chiplets/mod.rs +++ b/processor/src/trace/chiplets/mod.rs @@ -308,21 +308,14 @@ impl Chiplets { let rest = memory_fragment.push_column_slice(rest); ace_fragment.push_column_slice(rest); }, - 17 => { - // column 17 is relevant only for the memory chiplet + 17 | 18 | 19 => { + // columns 17-19 are relevant for the memory chiplet (col 17 = D_INV / FLAG_SCW, + // cols 18-19 = ADDR_LO / ADDR_HI) and the ACE chiplet // skip the hasher and bitwise chiplets let (_, rest) = column.split_at_mut(hasher.trace_len() + bitwise.trace_len()); let rest = memory_fragment.push_column_slice(rest); ace_fragment.push_column_slice(rest); }, - 18 | 19 => { - // column 18 and 19 are relevant only for the ACE chiplet - // skip the hasher, bitwise and memory chiplets - let (_, rest) = column.split_at_mut( - hasher.trace_len() + bitwise.trace_len() + memory.trace_len(), - ); - ace_fragment.push_column_slice(rest); - }, _ => panic!("invalid column index"), } }