Fix SHA256 word range checks and U32ADD carry constraints

CHANGELOG.md

@@ -6,6 +6,7 @@
 - Rejected non-syscall references to exported kernel procedures in the linker ([#2902](https://github.com/0xMiden/miden-vm/issues/2902)).
 - Reverted the `MainTrace` typed row storage change that caused a large `blake3_1to1` trace-building regression ([#2949](https://github.com/0xMiden/miden-vm/pull/2949)).
 - Fixed Falcon `mod_12289` remainder validation and `u64::rotr` overflow handling for rotations by `0` and `32` ([#2968](https://github.com/0xMiden/miden-vm/pull/2968)).
+- Hardened SHA256 message word range checks and U32ADD/U32ADD3 carry constraints, updating recursive verifier relation digest artifacts ([#3021](https://github.com/0xMiden/miden-vm/pull/3021)).
 
 #### Bug Fixes
 

air/src/config.rs

@@ -85,10 +85,10 @@ pub fn pcs_params() -> PcsParams {
 /// Compile-time constant binding the Fiat-Shamir transcript to the Miden VM AIR.
 /// Must match the constants in `crates/lib/core/asm/sys/vm/mod.masm`.
 pub const RELATION_DIGEST: [Felt; 4] = [
-    Felt::new_unchecked(3886624411320157031),
-    Felt::new_unchecked(5903371486919752653),
-    Felt::new_unchecked(170319297396068280),
-    Felt::new_unchecked(5221005507035467697),
+    Felt::new_unchecked(9959184209071024919),
+    Felt::new_unchecked(8083906424746801292),
+    Felt::new_unchecked(2491326376870921885),
+    Felt::new_unchecked(2800937775438555033),
 ];
 
 /// Observes PCS protocol parameters into the challenger.

air/src/constraints/stack/stack_arith/mod.rs

@@ -194,7 +194,7 @@ pub fn enforce_main<AB>(
     let u32_v_lo = uop_h1 * TWO_POW_16 + uop_h0;
     let u32_v_hi = uop_h3.clone() * TWO_POW_16 + uop_h2.clone();
     let u32_v48 = uop_h2 * TWO_POW_32 + u32_v_lo.clone();
-    let u32_v64 = uop_h3 * TWO_POW_48 + u32_v48.clone();
+    let u32_v64 = uop_h3.clone() * TWO_POW_48 + u32_v48.clone();
 
     // Element validity check for u32split/u32mul/u32madd.
     // u32_v_hi_comp * u32_v_lo is intrinsic (symmetry test: setting either factor to 0 hides a
@@ -218,10 +218,13 @@ pub fn enforce_main<AB>(
     }
 
     builder.when(is_u32split).assert_eq(s0.clone(), u32_v64.clone());
-    builder.when(is_u32add).assert_eq(s0.clone() + s1.clone(), u32_v48.clone());
     builder
-        .when(is_u32add3)
+        .when(is_u32add.clone())
+        .assert_eq(s0.clone() + s1.clone(), u32_v48.clone());
+    builder
+        .when(is_u32add3.clone())
         .assert_eq(s0.clone() + s1.clone() + s2.clone(), u32_v48);
+    builder.when(is_u32add + is_u32add3).assert_zero(uop_h3);
 
     // U32SUB: s1 = s0 + s1' - s0' * 2^32, s0' is boolean (borrow), s1' = v_lo.
     {

air/src/constraints/stack/stack_arith/tests.rs

@@ -2,7 +2,7 @@ use alloc::vec::Vec;
 
 use miden_core::{
     Felt,
-    field::{PrimeCharacteristicRing, PrimeField64, QuadFelt},
+    field::{Field, PrimeCharacteristicRing, PrimeField64, QuadFelt},
     operations::opcodes,
 };
 use miden_crypto::stark::{
@@ -132,6 +132,16 @@ fn eval_stack_arith(local: &MainCols<Felt>, next: &MainCols<Felt>) -> Vec<QuadFe
     builder.evaluations
 }
 
+fn assert_constraints_accept(local: &MainCols<Felt>, next: &MainCols<Felt>, message: &str) {
+    let evaluations = eval_stack_arith(local, next);
+    assert!(evaluations.iter().all(|value| *value == QuadFelt::ZERO), "{message}");
+}
+
+fn assert_constraints_reject(local: &MainCols<Felt>, next: &MainCols<Felt>, message: &str) {
+    let evaluations = eval_stack_arith(local, next);
+    assert!(evaluations.iter().any(|value| *value != QuadFelt::ZERO), "{message}");
+}
+
 #[test]
 fn stack_arith_u32add_constraints_allow_non_u32_operands() {
     let non_u32 = Felt::new_unchecked(Felt::ORDER_U64 - 1);
@@ -148,10 +158,89 @@ fn stack_arith_u32add_constraints_allow_non_u32_operands() {
     assert_eq!(op_flags.u32add(), Felt::ONE);
     assert_eq!(op_flags.u32sub(), Felt::ZERO);
 
-    let evaluations = eval_stack_arith(&local, &next);
-    assert!(
-        evaluations.iter().all(|value| *value == QuadFelt::ZERO),
-        "expected U32ADD constraints to accept a non-u32 operand with forged u32 outputs"
+    assert_constraints_accept(
+        &local,
+        &next,
+        "expected U32ADD constraints to accept a non-u32 operand with forged u32 outputs",
+    );
+}
+
+#[test]
+fn stack_arith_u32add_constraints_reject_forged_high_carry_limb() {
+    let mut local = generate_test_row(opcodes::U32ADD as usize);
+    local.stack.top[0] = Felt::ZERO;
+    local.stack.top[1] = Felt::ZERO;
+    set_u32_helpers(&mut local, 0, 1 << 16);
+
+    let mut next = generate_test_row(0);
+    next.stack.top[0] = Felt::ZERO;
+    next.stack.top[1] = Felt::new_unchecked(1 << 16);
+
+    let op_flags: OpFlags<Felt> = OpFlags::new(&local.decoder, &local.stack, &next.decoder);
+    assert_eq!(op_flags.u32add(), Felt::ONE);
+
+    assert_constraints_reject(
+        &local,
+        &next,
+        "expected U32ADD constraints to reject carry values with a nonzero high limb",
+    );
+}
+
+#[test]
+fn stack_arith_u32add3_constraints_reject_forged_high_carry_limb() {
+    let mut local = generate_test_row(opcodes::U32ADD3 as usize);
+    local.stack.top[0] = Felt::ZERO;
+    local.stack.top[1] = Felt::ZERO;
+    local.stack.top[2] = Felt::ZERO;
+    set_u32_helpers(&mut local, 0, 1 << 16);
+
+    let mut next = generate_test_row(0);
+    next.stack.top[0] = Felt::ZERO;
+    next.stack.top[1] = Felt::new_unchecked(1 << 16);
+
+    let op_flags: OpFlags<Felt> = OpFlags::new(&local.decoder, &local.stack, &next.decoder);
+    assert_eq!(op_flags.u32add3(), Felt::ONE);
+
+    assert_constraints_reject(
+        &local,
+        &next,
+        "expected U32ADD3 constraints to reject carry values with a nonzero high limb",
+    );
+}
+
+#[test]
+fn stack_arith_u64_overflowing_add_rejects_forged_low_limb_carry() {
+    let mut add_local = generate_test_row(opcodes::U32ADD as usize);
+    add_local.stack.top[0] = Felt::ZERO;
+    add_local.stack.top[1] = Felt::ZERO;
+    set_u32_helpers(&mut add_local, 0, 1 << 16);
+
+    let mut add_next = generate_test_row(opcodes::U32ADD3 as usize);
+    add_next.stack.top[0] = Felt::ZERO;
+    add_next.stack.top[1] = Felt::new_unchecked(1 << 16);
+    add_next.stack.top[2] = Felt::ZERO;
+    add_next.stack.top[3] = Felt::ZERO;
+
+    let mut add3_local = generate_test_row(opcodes::U32ADD3 as usize);
+    add3_local.stack.top[0] = Felt::new_unchecked(1 << 16);
+    add3_local.stack.top[1] = Felt::ZERO;
+    add3_local.stack.top[2] = Felt::ZERO;
+    add3_local.stack.top[3] = Felt::ZERO;
+    set_u32_helpers(&mut add3_local, 1 << 16, 0);
+
+    let mut add3_next = generate_test_row(0);
+    add3_next.stack.top[0] = Felt::new_unchecked(1 << 16);
+    add3_next.stack.top[1] = Felt::ZERO;
+
+    assert_constraints_reject(
+        &add_local,
+        &add_next,
+        "expected the forged low-limb carry in u64::overflowing_add to be rejected at U32ADD",
+    );
+    assert_constraints_accept(
+        &add3_local,
+        &add3_next,
+        "expected U32ADD3 to accept honest propagation of a 65536 carry once it is on the stack",
     );
 }
 
@@ -174,9 +263,69 @@ fn stack_arith_u32sub_constraints_allow_non_u32_operands() {
     assert_eq!(op_flags.u32sub(), Felt::ONE);
     assert_eq!(op_flags.u32add(), Felt::ZERO);
 
-    let evaluations = eval_stack_arith(&local, &next);
-    assert!(
-        evaluations.iter().all(|value| *value == QuadFelt::ZERO),
-        "expected U32SUB constraints to accept a non-u32 operand with forged u32 outputs"
+    assert_constraints_accept(
+        &local,
+        &next,
+        "expected U32SUB constraints to accept a non-u32 operand with forged u32 outputs",
+    );
+}
+
+#[test]
+fn stack_arith_u32mul_constraints_allow_non_u32_sha256_rotr_operand() {
+    let non_u32 = Felt::new_unchecked((u32::MAX as u64) + 2);
+    let rotr_7_multiplier = Felt::new_unchecked(1 << 25);
+    let product = non_u32.as_canonical_u64() * rotr_7_multiplier.as_canonical_u64();
+    let lo = product as u32;
+    let hi = (product >> 32) as u32;
+
+    assert!(non_u32.as_canonical_u64() > u32::MAX as u64);
+
+    let mut local = generate_test_row(opcodes::U32MUL as usize);
+    local.stack.top[0] = rotr_7_multiplier;
+    local.stack.top[1] = non_u32;
+    set_u32_helpers(&mut local, lo, hi);
+    local.decoder.hasher_state[6] = Felt::new_unchecked(u32::MAX as u64 - hi as u64).inverse();
+
+    let mut next = generate_test_row(0);
+    next.stack.top[0] = Felt::new_unchecked(lo as u64);
+    next.stack.top[1] = Felt::new_unchecked(hi as u64);
+
+    let op_flags: OpFlags<Felt> = OpFlags::new(&local.decoder, &local.stack, &next.decoder);
+    assert_eq!(op_flags.u32mul(), Felt::ONE);
+
+    assert_constraints_accept(
+        &local,
+        &next,
+        "expected U32MUL constraints to accept a non-u32 operand with forged rotr outputs",
+    );
+}
+
+#[test]
+fn stack_arith_u32div_constraints_allow_non_u32_sha256_shr_operand() {
+    let non_u32 = Felt::new_unchecked((u32::MAX as u64) + 2);
+    let divisor = Felt::new_unchecked(8);
+    let quotient = Felt::new_unchecked(non_u32.as_canonical_u64() / divisor.as_canonical_u64());
+    let remainder = Felt::new_unchecked(non_u32.as_canonical_u64() % divisor.as_canonical_u64());
+    let lo = (non_u32.as_canonical_u64() - quotient.as_canonical_u64()) as u32;
+    let hi = (divisor.as_canonical_u64() - remainder.as_canonical_u64() - 1) as u32;
+
+    assert!(non_u32.as_canonical_u64() > u32::MAX as u64);
+
+    let mut local = generate_test_row(opcodes::U32DIV as usize);
+    local.stack.top[0] = divisor;
+    local.stack.top[1] = non_u32;
+    set_u32_helpers(&mut local, lo, hi);
+
+    let mut next = generate_test_row(0);
+    next.stack.top[0] = remainder;
+    next.stack.top[1] = quotient;
+
+    let op_flags: OpFlags<Felt> = OpFlags::new(&local.decoder, &local.stack, &next.decoder);
+    assert_eq!(op_flags.u32div(), Felt::ONE);
+
+    assert_constraints_accept(
+        &local,
+        &next,
+        "expected U32DIV constraints to accept a non-u32 operand with forged shr outputs",
     );
 }

air/src/snapshots/miden_air__config__tests__relation_digest_matches_current_air.snap

@@ -3,5 +3,5 @@ source: air/src/config.rs
 expression: snapshot
 ---
 num_inputs: 568
-num_eval_gates: 5540
-relation_digest: [3886624411320157031, 5903371486919752653, 170319297396068280, 5221005507035467697]
+num_eval_gates: 5548
+relation_digest: [9959184209071024919, 8083906424746801292, 2491326376870921885, 2800937775438555033]

crates/lib/core/asm/crypto/hashes/sha256.masm

@@ -1508,6 +1508,27 @@ proc consume_padding_message_schedule
     movdn.7
 end
 
+#! Asserts that all words in a 512-bit SHA256 message block are valid u32 values.
+#!
+#! Input: [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15, ...]
+#! Output: [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15, ...]
+#!
+#! Where:
+#! - m0 through m15 are the 32-bit words of the SHA256 message block.
+#!
+#! Panics if:
+#! - any message word is not a valid 32-bit unsigned integer.
+proc assert_message_block_u32
+    u32assertw.err="invalid sha256 message word"
+    movupw.3
+    u32assertw.err="invalid sha256 message word"
+    movupw.3
+    u32assertw.err="invalid sha256 message word"
+    movupw.3
+    u32assertw.err="invalid sha256 message word"
+    movupw.3
+end
+
 #! SHA256 2-to-1 hash (merge): Given 64 -bytes input, computes 32 -bytes SHA256 digest
 #!
 #! Input: [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15, ...]
@@ -1520,7 +1541,14 @@ end
 #! maintaining big endian byte order.
 #!
 #! SHA256 digest is represented in terms of eight 32 -bit words ( big endian byte order ).
+#!
+#! Panics if:
+#! - any input message word is not a valid 32-bit unsigned integer.
+#!
+#! Invocation: exec
 pub proc merge
+    exec.assert_message_block_u32
+
     push.0x5be0cd19.0x1f83d9ab.0x9b05688c.0x510e527f
     push.0xa54ff53a.0x3c6ef372.0xbb67ae85.0x6a09e667
 
@@ -1542,11 +1570,17 @@ end
 #! maintaining big endian byte order.
 #!
 #! SHA256 digest is represented in terms of eight 32 -bit words ( big endian byte order ).
+#!
+#! Panics if:
+#! - any input message word is not a valid 32-bit unsigned integer.
+#!
+#! Invocation: exec
 pub proc hash
     # apply padding, see padding rule in section 5.1.1 of
     # https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf
     push.256.0.0.0.0.0.0.2147483648
     swapdw
+    exec.assert_message_block_u32
 
     push.0x5be0cd19.0x1f83d9ab.0x9b05688c.0x510e527f
     push.0xa54ff53a.0x3c6ef372.0xbb67ae85.0x6a09e667
@@ -1561,6 +1595,12 @@ end
 #!
 #! Input:  [addr, len, ...]
 #! Output: [dig0, dig1, dig2, dig3, dig4, dig5, dig6, dig7, ...]
+#!
+#! Panics if:
+#! - any loaded message word is not a valid 32-bit unsigned integer.
+#! - padding range checks fail.
+#!
+#! Invocation: exec
 @locals(48)
 pub proc hash_bytes
     # loc.0 (input address)
@@ -1611,10 +1651,10 @@ pub proc hash_bytes
     # Consume sha256 blocks
     loc_load.28 u32assert neq.0
     while.true
-        padw loc_load.0 u32assert u32overflowing_add.12 assertz.err="range check failed: padding" mem_loadw_be movdnw.2
-        padw loc_load.0 u32assert u32overflowing_add.8 assertz.err="range check failed: padding" mem_loadw_be movdnw.2
-        padw loc_load.0 u32assert u32overflowing_add.4 assertz.err="range check failed: padding" mem_loadw_be movdnw.2
-        padw loc_load.0 u32assert u32overflowing_add.0 assertz.err="range check failed: padding" mem_loadw_be movdnw.2
+        padw loc_load.0 u32assert u32overflowing_add.12 assertz.err="range check failed: padding" mem_loadw_be u32assertw.err="invalid sha256 message word" movdnw.2
+        padw loc_load.0 u32assert u32overflowing_add.8 assertz.err="range check failed: padding" mem_loadw_be u32assertw.err="invalid sha256 message word" movdnw.2
+        padw loc_load.0 u32assert u32overflowing_add.4 assertz.err="range check failed: padding" mem_loadw_be u32assertw.err="invalid sha256 message word" movdnw.2
+        padw loc_load.0 u32assert u32overflowing_add.0 assertz.err="range check failed: padding" mem_loadw_be u32assertw.err="invalid sha256 message word" movdnw.2
         exec.prepare_message_schedule_and_consume
 
         loc_load.0 u32assert u32overflowing_add.16 assertz.err="range check failed: padding" loc_store.0