fix(ssa): Cast to u64 when inserting OOB checks in DIE

[aakoshh]

Description

Problem

Resolves #10307

Summary

Changes the replace_array_instructions_with_out_of_bounds_checks to cast to u64 instead of u32 before putting a constraint on the maximum of the index, which should handle values that have potentially overflown when we calculate the flattened index of composite types.

Additional Context

In the failing Noir example, we have the following code:

    for _ in 0..1 {
        let _ = if c { a[b] } else { a[0] };
    }

c is going to be false, so during execution we should always access a[0], which should be fine, however b is a large number, and a is a [(bool, bool); 3], which means it has 2 elements per item, so to access b we have to look up 2*b, which is where the overflow happens: 2*b > u32::MAX.

Since #10110 we again use unchecked operations to calculate the index, so this overflow will not cause an immediate failure. Instead, we rely on ACIR protecting against OOB lookups during ArrayGet:

After Initial SSA:
acir(inline) fn main f0 {
  ...
  b4():
    v14 = load v6 -> [(u1, u1); 3]
    v16 = unchecked_mul v1, u32 2
    v17 = array_get v14, index v16 -> u1
  ...
}

The problem is that here the result of the lookup is unused, so the DIE pass removes the lookup, but because it could fail with OOB, it leaves behind a constraint that the index has to be less than 6, which is the number of slots in the array (3*2).

After Dead Instruction Elimination (1) (step 10):
acir(inline) predicate_pure fn main f0 {
...
  b4():
    v9 = unchecked_mul v1, u32 2
    v11 = lt v9, u32 6
    constrain v11 == u1 1, "Index out of bounds"
...
}

If we look at the generated ACIR opcodes, we see that a range constraint is inserted to check that the result of a division fits into 32 bits:

Compiled ACIR for main (non-transformed):
func 0
private parameters: [w0, w1, w2, w3, w4, w5, w6, w7]
public parameters: []
return values: [w8]
...
BRILLIG CALL func: 0, inputs: [2*w6 + 4294967290, 4294967296], outputs: [w9, w10]
BLACKBOX::RANGE input: w9, bits: 1
BLACKBOX::RANGE input: w10, bits: 32
ASSERT w10 = 2*w6 - 4294967296*w9 + 4294967290
ASSERT 0 = -w7*w9
...

With the changes in this PR, we'll have the following opcodes instead:

BRILLIG CALL func: 0, inputs: [2*w6 + 18446744073709551610, 18446744073709551616], outputs: [w9, w10]
BLACKBOX::RANGE input: w9, bits: 1
BLACKBOX::RANGE input: w10, bits: 64
ASSERT w10 = 2*w6 - 18446744073709551616*w9 + 18446744073709551610
ASSERT 0 = -w7*w9

We considered other alternatives:

• change all ops back to checked: but this is what we wanted to avoid by introducing the Unfit values into the SSA interpreter
• change any ops to checked for only those indexes which were protected by the array operations we remove in DIE: this would be more complex as we would have to revisit instructions we already inserted when we decide we are removing something

The approach in the PR is easy, since it only involves casting the index and the constant before we insert the constraint.

User Documentation

Check one:

• No user documentation needed.
• Changes in docs/ included in this PR.
• [For Experimental Features] Changes in docs/ to be submitted in a separate PR.

PR Checklist

• I have tested the changes locally.
• I have formatted the changes with Prettier and/or cargo fmt on default settings.

[github-actions]

Changes to circuit sizes

Generated at commit: d49f175d1a47253da474dddb3ce5cdcdaec9c0ff, compared to commit: 2a27b186687cab46e6976a68250833d63fd402ec

🧾 Summary (10% most significant diffs)

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
lambda_from_global_array	0 ➖	0.00%	+48 ❌	+1.69%
databus_composite_calldata	0 ➖	0.00%	+50 ❌	+1.59%

---

Full diff report 👇

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
lambda_from_global_array	28 (0)	0.00%	2,883 (+48)	+1.69%
databus_composite_calldata	136 (0)	0.00%	3,186 (+50)	+1.59%
regression_9206	6 (0)	0.00%	2,844 (+41)	+1.46%
lambda_from_array	1,833 (0)	0.00%	4,131 (+52)	+1.27%
nested_array_dynamic	2,986 (0)	0.00%	11,536 (+60)	+0.52%
regression_struct_array_conditional	68 (0)	0.00%	3,216 (+2)	+0.06%
sha512_100_bytes	13,173 (0)	0.00%	39,578 (+18)	+0.05%
array_oob_regression_7965	31 (0)	0.00%	2,876 (-5)	-0.17%

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Execution Time'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: 81c92d1	Previous: 2a27b18	Ratio
rollup-block-root-single-tx	0.003 s	0.002 s	1.50
rollup-checkpoint-merge	0.004 s	0.003 s	1.33
rollup-root	0.005 s	0.004 s	1.25

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Test Suite Duration'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: 81c92d1	Previous: 2a27b18	Ratio
test_report_zkpassport_noir_rsa_	2 s	1 s	2

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench