WHIR verifier protocol audit + VM/arena memory safety

crates/backend/air/Cargo.toml

@@ -6,3 +6,6 @@ edition.workspace = true
 [dependencies]
 field = { path = "../field", package = "mt-field" }
 poly = { path = "../poly", package = "mt-poly" }
+
+[dev-dependencies]
+koala_bear = { path = "../koala-bear", package = "mt-koala-bear" }

crates/backend/air/src/symbolic.rs

@@ -84,6 +84,10 @@ fn alloc_node<F: Field>(node: SymbolicNode<F>) -> u32 {
         let mut bytes = arena.borrow_mut();
         let node_size = std::mem::size_of::<SymbolicNode<F>>();
         let idx = bytes.len();
+        assert!(
+            idx <= u32::MAX as usize,
+            "symbolic arena overflow: index {idx} exceeds u32::MAX"
+        );
         bytes.resize(idx + node_size, 0);
         unsafe {
             std::ptr::write_unaligned(bytes.as_mut_ptr().add(idx) as *mut SymbolicNode<F>, node);
@@ -95,7 +99,14 @@ fn alloc_node<F: Field>(node: SymbolicNode<F>) -> u32 {
 pub fn get_node<F: Field>(idx: u32) -> SymbolicNode<F> {
     ARENA.with(|arena| {
         let bytes = arena.borrow();
-        unsafe { std::ptr::read_unaligned(bytes.as_ptr().add(idx as usize) as *const SymbolicNode<F>) }
+        let offset = idx as usize;
+        let node_size = std::mem::size_of::<SymbolicNode<F>>();
+        assert!(
+            offset.checked_add(node_size).is_some_and(|end| end <= bytes.len()),
+            "arena out-of-bounds: index {idx} (need {node_size} bytes, arena has {} bytes)",
+            bytes.len()
+        );
+        unsafe { std::ptr::read_unaligned(bytes.as_ptr().add(offset) as *const SymbolicNode<F>) }
     })
 }
 

crates/backend/air/tests/arena_safety.rs

@@ -0,0 +1,75 @@
+// Tests for arena bounds checking in symbolic expression handling.
+// Addresses issue #170: unchecked arena index enables out-of-bounds reads.
+
+use field::PrimeCharacteristicRing;
+use koala_bear::KoalaBear;
+use mt_air::{SymbolicExpression, get_node};
+
+type F = KoalaBear;
+
+#[test]
+#[should_panic(expected = "arena out-of-bounds")]
+fn get_node_oob_panics_on_empty_arena() {
+    // Constructing Operation(0) on an empty arena must panic with a bounds
+    // check, not trigger undefined behavior via read_unaligned.
+    let _: mt_air::SymbolicNode<F> = get_node(0);
+}
+
+#[test]
+#[should_panic(expected = "arena out-of-bounds")]
+fn get_node_oob_panics_on_large_index() {
+    // A fabricated large index must be caught by the bounds check.
+    let _: mt_air::SymbolicNode<F> = get_node(u32::MAX);
+}
+
+#[test]
+fn alloc_and_get_node_roundtrip() {
+    // Building a real expression through arithmetic triggers alloc_node
+    // internally. The resulting Operation index must be readable.
+    let a = SymbolicExpression::<F>::Variable(mt_air::SymbolicVariable::new(0));
+    let b = SymbolicExpression::<F>::Variable(mt_air::SymbolicVariable::new(1));
+    let sum = a + b;
+
+    if let SymbolicExpression::Operation(idx) = sum {
+        let node = get_node::<F>(idx);
+        assert_eq!(node.op, mt_air::SymbolicOperation::Add);
+    } else {
+        panic!("expected Operation variant from variable addition");
+    }
+}
+
+#[test]
+fn nested_expression_indices_are_valid() {
+    // Multiple levels of nesting must all produce valid arena indices.
+    let a = SymbolicExpression::<F>::Variable(mt_air::SymbolicVariable::new(0));
+    let b = SymbolicExpression::<F>::Constant(F::TWO);
+    let c = SymbolicExpression::<F>::Variable(mt_air::SymbolicVariable::new(1));
+
+    // (a * b) + c — two alloc_node calls
+    let product = a * b;
+    let sum = product + c;
+
+    if let SymbolicExpression::Operation(idx) = sum {
+        let node = get_node::<F>(idx);
+        assert_eq!(node.op, mt_air::SymbolicOperation::Add);
+        // The lhs should be the product Operation
+        if let SymbolicExpression::Operation(mul_idx) = node.lhs {
+            let mul_node = get_node::<F>(mul_idx);
+            assert_eq!(mul_node.op, mt_air::SymbolicOperation::Mul);
+        } else {
+            panic!("expected Operation for nested lhs");
+        }
+    } else {
+        panic!("expected Operation variant from nested expression");
+    }
+}
+
+#[test]
+fn constant_folding_bypasses_arena() {
+    // Constant + Constant should fold without arena allocation.
+    let a = SymbolicExpression::<F>::Constant(F::ONE);
+    let b = SymbolicExpression::<F>::Constant(F::TWO);
+    let sum = a + b;
+
+    assert!(matches!(sum, SymbolicExpression::Constant(_)));
+}

crates/lean_vm/src/diagnostics/error.rs

@@ -23,6 +23,7 @@ pub enum RunnerError {
         range: usize,
     },
     InvalidExtensionOp,
+    AddressOverflow,
     ParallelSegmentFailed(usize, Box<RunnerError>),
 }
 
@@ -55,6 +56,7 @@ impl Display for RunnerError {
                 )
             }
             Self::InvalidExtensionOp => write!(f, "invalid extension op"),
+            Self::AddressOverflow => write!(f, "address overflow: fp + offset exceeds usize"),
             Self::ParallelSegmentFailed(id, err) => {
                 write!(f, "parallel segment {id} failed: {err}")
             }

crates/lean_vm/src/isa/hint.rs

@@ -283,7 +283,8 @@ impl Hint {
                 let size = size.read_value(ctx.memory, ctx.fp)?.to_usize();
 
                 let allocation_start_addr = *ctx.ap;
-                ctx.memory.set(ctx.fp + *offset, F::from_usize(allocation_start_addr))?;
+                let addr = ctx.fp.checked_add(*offset).ok_or(RunnerError::AddressOverflow)?;
+                ctx.memory.set(addr, F::from_usize(allocation_start_addr))?;
                 *ctx.ap += size;
             }
             Self::Custom(hint, args) => {
@@ -292,7 +293,8 @@ impl Hint {
             Self::Inverse { arg, res_offset } => {
                 let value = arg.read_value(ctx.memory, ctx.fp)?;
                 let result = value.try_inverse().unwrap_or(F::ZERO);
-                ctx.memory.set(ctx.fp + *res_offset, result)?;
+                let addr = ctx.fp.checked_add(*res_offset).ok_or(RunnerError::AddressOverflow)?;
+                ctx.memory.set(addr, result)?;
             }
             Self::Print { line_info, content } => {
                 if let Some(diag) = &mut ctx.hints.diagnostics {
@@ -364,8 +366,8 @@ impl Hint {
                 offset_target,
             } => {
                 // Record a deref constraint: memory[target_addr] = memory[memory[src_addr]]
-                let src_addr = ctx.fp + offset_src;
-                let target_addr = ctx.fp + offset_target;
+                let src_addr = ctx.fp.checked_add(*offset_src).ok_or(RunnerError::AddressOverflow)?;
+                let target_addr = ctx.fp.checked_add(*offset_target).ok_or(RunnerError::AddressOverflow)?;
                 ctx.pending_deref_hints.push((target_addr, src_addr));
             }
             Self::Panic { message } => {
@@ -380,8 +382,13 @@ impl Hint {
             Self::HintWitness { name, destination } => {
                 let data = consume_next_hint_entry(ctx.hints.named_hints, name);
                 let dest_addr = match destination {
-                    HintWitnessDestination::Inline { offset } => ctx.fp + *offset,
-                    HintWitnessDestination::Indirect { ptr_offset } => ctx.memory.get(ctx.fp + *ptr_offset)?.to_usize(),
+                    HintWitnessDestination::Inline { offset } => {
+                        ctx.fp.checked_add(*offset).ok_or(RunnerError::AddressOverflow)?
+                    }
+                    HintWitnessDestination::Indirect { ptr_offset } => {
+                        let addr = ctx.fp.checked_add(*ptr_offset).ok_or(RunnerError::AddressOverflow)?;
+                        ctx.memory.get(addr)?.to_usize()
+                    }
                 };
                 ctx.memory.set_slice(dest_addr, data)?;
             }

crates/lean_vm/src/isa/instruction.rs

@@ -188,18 +188,27 @@ impl Instruction {
                 Ok(())
             }
             Self::Deref { shift_0, shift_1, res } => {
+                let base_addr = ctx.fp.checked_add(*shift_0).ok_or(RunnerError::AddressOverflow)?;
                 if res.is_value_unknown(ctx.memory, *ctx.fp) {
                     let memory_address_res = res.memory_address(*ctx.fp)?;
-                    let ptr = ctx.memory.get(*ctx.fp + shift_0)?;
-                    if let Ok(value) = ctx.memory.get(ptr.to_usize() + shift_1) {
+                    let ptr = ctx.memory.get(base_addr)?;
+                    let deref_addr = ptr
+                        .to_usize()
+                        .checked_add(*shift_1)
+                        .ok_or(RunnerError::AddressOverflow)?;
+                    if let Ok(value) = ctx.memory.get(deref_addr) {
                         ctx.memory.set(memory_address_res, value)?;
                     } else {
                         // Do nothing, we are probably in a range check, will be resolved later
                     }
                 } else {
                     let value = res.read_value(ctx.memory, *ctx.fp).unwrap();
-                    let ptr = ctx.memory.get(*ctx.fp + shift_0)?;
-                    ctx.memory.set(ptr.to_usize() + shift_1, value)?;
+                    let ptr = ctx.memory.get(base_addr)?;
+                    let deref_addr = ptr
+                        .to_usize()
+                        .checked_add(*shift_1)
+                        .ok_or(RunnerError::AddressOverflow)?;
+                    ctx.memory.set(deref_addr, value)?;
                 }
 
                 ctx.counts.deref += 1;

crates/lean_vm/src/isa/operands/mem_or_constant.rs

@@ -29,7 +29,10 @@ impl MemOrConstant {
     pub fn read_value(&self, memory: &impl MemoryAccess, fp: usize) -> Result<F, RunnerError> {
         match self {
             Self::Constant(c) => Ok(*c),
-            Self::MemoryAfterFp { offset } => memory.get(fp + *offset),
+            Self::MemoryAfterFp { offset } => {
+                let addr = fp.checked_add(*offset).ok_or(RunnerError::AddressOverflow)?;
+                memory.get(addr)
+            }
         }
     }
 
@@ -42,7 +45,10 @@ impl MemOrConstant {
     pub const fn memory_address(&self, fp: usize) -> Result<usize, RunnerError> {
         match self {
             Self::Constant(_) => Err(RunnerError::NotAPointer),
-            Self::MemoryAfterFp { offset } => Ok(fp + *offset),
+            Self::MemoryAfterFp { offset } => match fp.checked_add(*offset) {
+                Some(addr) => Ok(addr),
+                None => Err(RunnerError::AddressOverflow),
+            },
         }
     }
 }

crates/lean_vm/src/isa/operands/mem_or_fp_or_constant.rs

@@ -20,8 +20,14 @@ impl MemOrFpOrConstant {
     /// Read the value from memory, return fp, or return the constant
     pub fn read_value(&self, memory: &impl MemoryAccess, fp: usize) -> Result<F, RunnerError> {
         match self {
-            Self::MemoryAfterFp { offset } => memory.get(fp + *offset),
-            Self::FpRelative { offset } => Ok(F::from_usize(fp + *offset)),
+            Self::MemoryAfterFp { offset } => {
+                let addr = fp.checked_add(*offset).ok_or(RunnerError::AddressOverflow)?;
+                memory.get(addr)
+            }
+            Self::FpRelative { offset } => {
+                let addr = fp.checked_add(*offset).ok_or(RunnerError::AddressOverflow)?;
+                Ok(F::from_usize(addr))
+            }
             Self::Constant(c) => Ok(*c),
         }
     }
@@ -34,7 +40,10 @@ impl MemOrFpOrConstant {
     /// Get the memory address (returns error for Fp and constants)
     pub const fn memory_address(&self, fp: usize) -> Result<usize, RunnerError> {
         match self {
-            Self::MemoryAfterFp { offset } => Ok(fp + *offset),
+            Self::MemoryAfterFp { offset } => match fp.checked_add(*offset) {
+                Some(addr) => Ok(addr),
+                None => Err(RunnerError::AddressOverflow),
+            },
             Self::FpRelative { .. } => Err(RunnerError::NotAPointer),
             Self::Constant(_) => Err(RunnerError::NotAPointer),
         }

crates/lean_vm/tests/address_safety.rs

@@ -0,0 +1,97 @@
+// Tests for checked arithmetic in memory address computation.
+// Addresses issue #176: fp+offset overflow enables wrong memory access.
+
+use backend::PrimeCharacteristicRing;
+use lean_vm::{F, MemOrConstant, MemOrFpOrConstant, Memory, RunnerError};
+
+#[test]
+fn read_value_overflow_returns_error() {
+    // fp + offset that overflows usize must return AddressOverflow, not wrap.
+    let mem = Memory::new(vec![F::ONE; 16]);
+    let operand = MemOrConstant::MemoryAfterFp { offset: usize::MAX };
+    let fp = 1usize;
+
+    let result = operand.read_value(&mem, fp);
+    assert!(result.is_err());
+    assert_eq!(result.unwrap_err(), RunnerError::AddressOverflow);
+}
+
+#[test]
+fn memory_address_overflow_returns_error() {
+    let operand = MemOrConstant::MemoryAfterFp { offset: usize::MAX };
+    let fp = 1usize;
+
+    let result = operand.memory_address(fp);
+    assert!(result.is_err());
+    assert_eq!(result.unwrap_err(), RunnerError::AddressOverflow);
+}
+
+#[test]
+fn read_value_no_overflow_works() {
+    // Normal operation: fp=4, offset=2 → address 6 → reads mem[6].
+    let mut data = vec![F::ZERO; 8];
+    data[6] = F::from_u32(42);
+    let mem = Memory::new(data);
+    let operand = MemOrConstant::MemoryAfterFp { offset: 2 };
+
+    let result = operand.read_value(&mem, 4);
+    assert_eq!(result.unwrap(), F::from_u32(42));
+}
+
+#[test]
+fn memory_address_no_overflow_works() {
+    let operand = MemOrConstant::MemoryAfterFp { offset: 10 };
+    assert_eq!(operand.memory_address(5).unwrap(), 15);
+}
+
+#[test]
+fn constant_read_ignores_fp() {
+    // Constants don't compute addresses, so overflow is irrelevant.
+    let mem = Memory::new(vec![F::ZERO; 4]);
+    let operand = MemOrConstant::Constant(F::from_u32(99));
+
+    let result = operand.read_value(&mem, usize::MAX);
+    assert_eq!(result.unwrap(), F::from_u32(99));
+}
+
+#[test]
+fn is_value_unknown_with_overflow() {
+    // Overflow makes the value "unknown" (returns error → true).
+    let mem = Memory::new(vec![F::ONE; 4]);
+    let operand = MemOrConstant::MemoryAfterFp { offset: usize::MAX };
+    assert!(operand.is_value_unknown(&mem, 1));
+}
+
+// --- MemOrFpOrConstant: same overflow pattern ---
+
+#[test]
+fn fp_or_constant_memory_read_overflow() {
+    let mem = Memory::new(vec![F::ONE; 16]);
+    let operand = MemOrFpOrConstant::MemoryAfterFp { offset: usize::MAX };
+    assert_eq!(operand.read_value(&mem, 1).unwrap_err(), RunnerError::AddressOverflow);
+}
+
+#[test]
+fn fp_or_constant_fp_relative_overflow() {
+    // FpRelative computes fp + offset as a field element value, not a memory address.
+    // Overflow must still be caught before the conversion.
+    let mem = Memory::new(vec![F::ONE; 4]);
+    let operand = MemOrFpOrConstant::FpRelative { offset: usize::MAX };
+    assert_eq!(operand.read_value(&mem, 1).unwrap_err(), RunnerError::AddressOverflow);
+}
+
+#[test]
+fn fp_or_constant_memory_address_overflow() {
+    let operand = MemOrFpOrConstant::MemoryAfterFp { offset: usize::MAX };
+    assert_eq!(operand.memory_address(1).unwrap_err(), RunnerError::AddressOverflow);
+}
+
+#[test]
+fn fp_or_constant_normal_operation() {
+    let mut data = vec![F::ZERO; 8];
+    data[5] = F::from_u32(77);
+    let mem = Memory::new(data);
+    let operand = MemOrFpOrConstant::MemoryAfterFp { offset: 2 };
+    assert_eq!(operand.read_value(&mem, 3).unwrap(), F::from_u32(77));
+    assert_eq!(operand.memory_address(3).unwrap(), 5);
+}