fix!: AVM was missing range check on remainder for div in ALU

[dbanks12]

The Bug

The AVM's ALU division circuit (alu.pil) constrains integer division a / b = c with remainder r (stored in helper1) via:

DIV_OPS_NON_U128 * (ib * ic - ia + sel_op_div * helper1) = 0;

This enforces b * c + r = a (i.e., a - r = b * c). A separate greater-than check ensures r < b.

However, the remainder helper1 was never range-checked to fit within the operand's bit-width (max_bits). A malicious prover could set helper1 to an arbitrarily large field element (e.g., close to the field modulus) that satisfies b * c + r = a (mod p) and r < b in the field, but does not represent a valid unsigned integer remainder. This would allow forging incorrect division results.

The Exploit

For non-u128 integer division (u8, u16, u32, u64), a prover can choose a remainder r that is a large field element (not a valid unsigned integer) but still satisfies:

1. b * c + r ≡ a (mod p) — the main division relation
2. r < b — the greater-than check (which operates over the full field)

Without a range check on r, the prover can manipulate the quotient c to be any value they want, completely breaking the soundness of integer division.

The Fix

Added a lookup-based range check on the remainder:

#[RANGE_CHECK_DIV_REMAINDER]
sel_div_no_err { helper1, max_bits } in range_check.sel_alu { range_check.value, range_check.rng_chk_bits };

This ensures helper1 (the remainder) fits within max_bits (e.g., 32 bits for u32), preventing the prover from using oversized field elements as the remainder.

The simulation (alu.cpp) was also updated to emit the corresponding assert_range event, and unit tests were updated to expect the new range check call.

[dbanks12]

• fix!: AVM was missing range check on remainder for div in ALU #21066 👈 (View in Graphite)
• v4

This stack of pull requests is managed by Graphite. Learn more about stacking.

[jeanmon]

LGTM

[AztecBot]

Flakey Tests

🤖 says: This CI run detected 1 tests that failed, but were tolerated due to a .test_patterns.yml entry.

\033FLAKED\033 (8;;http://ci.aztec-labs.com/c8699c69a935e021�c8699c69a935e0218;;�):  yarn-project/end-to-end/scripts/run_test.sh simple src/e2e_epochs/epochs_mbps.parallel.test.ts "builds multiple blocks per slot with transactions anchored to checkpointed block" (203s) (code: 0) group:e2e-p2p-epoch-flakes