fix(acir_gen): Keep range checks before side effects

[aakoshh]

Description

Problem*

Resolves #9335

Summary*

Changes the redundant_range optimisation to keep range constraints which are stricter than the previously known constraint, unless there is an even stricter constraint further down the line and before the next potential side effect.

To minimise the increase in opcodes, I'm passing some information about Brillig functions to the ACIR optimisers, which should indicate whether they might have visible side effects, currently defined as calling oracle functions.

The new version also treats MEM operations like it used to handle assertions in that it is considered to replace an equivalent strength RANGE constraint.

Additional Context

Take this code, where the multiplication can result in an overflow:

global G_B: u64 = 2288862572;
fn main(a: u64) -> pub u64 {
    let b = a * 18259827970668162041_u64;
    println(f"b = {b}");
    // assert(b == G_B, "YHV");
    b
}

This resulted in the following ACIR:

BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
BLACKBOX::RANGE [(_2, 64)] []
BRILLIG CALL func 0: inputs: [EXPR [ 1 ], [EXPR [ 98 ], EXPR [ 32 ], EXPR [ 61 ], EXPR [ 32 ], EXPR [ 123 ], EXPR [ 98 ], EXPR [ 125 ]], EXPR [ 1 ], EXPR [ (1, _2) 0 ]], outputs: []
EXPR [ (1, _1) (-1, _2) 0 ]

So a is _0, b is _2, and _2 is range constrained to fit into 64 bits, which catches any overflow before we pass _2 to the Brillig call.

With the assert uncomment the ACIR changes into this:

BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
BRILLIG CALL func 0: inputs: [EXPR [ 1 ], [EXPR [ 98 ], EXPR [ 32 ], EXPR [ 61 ], EXPR [ 32 ], EXPR [ 123 ], EXPR [ 98 ], EXPR [ 125 ]], EXPR [ 1 ], EXPR [ (1, _2) 0 ]], outputs: []
EXPR [ (1, _2) -2288862572 ]
EXPR [ (1, _1) -2288862572 ]

_2 is now constrained to equal -2288862572, which implies 32 bits; this results in the removal of the 64 bit range constraint, because the optimisation pass knows it can save this opcode because there will be a stricter one. However, this allows the circuit to execute the Brillig call, which has a visible side effect.

With the changes in this PR, the new ACIR looks like this:

BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
BLACKBOX::RANGE [(_2, 64)] []
BRILLIG CALL func 0: inputs: [EXPR [ 1 ], [EXPR [ 98 ], EXPR [ 32 ], EXPR [ 61 ], EXPR [ 32 ], EXPR [ 123 ], EXPR [ 98 ], EXPR [ 125 ]], EXPR [ 1 ], EXPR [ (1, _2) 0 ]], outputs: []
EXPR [ (1, _2) -2288862572 ]
EXPR [ (1, _1) -2288862572 ]

We keep the range constraint on _2, with the 64 bits it used originally (see discussion below for why using 32 bits would be incorrect).

A different example is the following (notice that we don't print b, just something completely unrelated):

global G_B: u64 = 2288862572;
fn main(a: u64) -> pub u64 {
    let b = a * 18259827970668162041_u64;
    println("Now you see me");
    assert(b == G_B, "YHV");
    b
}

If we delay the constraint on b until the assert, we see the effect of println; for this reason we keep any range constraint that straddles a side effect, not just constraints on the inputs/outputs of Brillig calls.

To illustrate in a different way:

RANGE(w1, 64)  // drop because we have 32 before the Brillig call
RANGE(w1, 128) // drop because it's less strict than 64
RANGE(w1, 32)  // keep because this is the strictest before the Brillig call
BRILLIG CALL ...
RANGE(w1, 64)  // drop because we already have 32
BRILLIG CALL ...
RANGE(w1, 16)  // drop because we will have 0 before the end
ASSERT w1 == 0

Documentation*

Check one:

• No documentation needed.
• Documentation included in this PR.
• [For Experimental Features] Documentation 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]

⚠️ 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: 48468a5	Previous: 1748cbe	Ratio
sha512-100-bytes	0.14 s	0.11 s	1.27

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

CC: @TomAFrench

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Opcode count'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.10.

Benchmark suite	Current: 752d323	Previous: 18b01b3	Ratio
sha512-100-bytes	22229 opcodes	13173 opcodes	1.69

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: 53f0187	Previous: 8d78909	Ratio
test_report_zkpassport_noir-ecdsa_	3 s	2 s	1.50

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

CC: @TomAFrench

[github-actions]

Changes to circuit sizes

Generated at commit: 44badefc944743b28c60e48722861188ee297bc0, compared to commit: 8d7890923b674b0f893081a38e33436172218ae2

🧾 Summary (10% most significant diffs)

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
nested_dyn_array_regression_5782	-1 ✅	-3.70%	-1 ✅	-1.01%
array_dynamic_blackbox_input	-128 ✅	-16.86%	-175 ✅	-1.85%

---

Full diff report 👇

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
regression_8236	16 (-1)	-5.88%	2,795 (-1)	-0.04%
lambda_from_array	807 (-2)	-0.25%	3,306 (-7)	-0.21%
array_to_slice	45 (-1)	-2.17%	2,887 (-7)	-0.24%
databus_two_calldata	40 (-4)	-9.09%	2,875 (-10)	-0.35%
semaphore_depth_10	5,700 (-63)	-1.09%	16,134 (-79)	-0.49%
nested_dyn_array_regression_5782	26 (-1)	-3.70%	98 (-1)	-1.01%
array_dynamic_blackbox_input	631 (-128)	-16.86%	9,267 (-175)	-1.85%

[aakoshh]

I investigated the regression on lambda_from_array as well.

We had for example this code:

fn main(x: u32) {
    lambdas_in_array_literal(x - 1);
}
fn lambdas_in_array_literal(x: u32) {
    let xs = [|| println("hi"), || println("bye"), || println("wow"), || println("big")];
    (xs[x])();
}

Resulting in this ACIR:

Compiled ACIR for main (non-transformed):
func 0
current witness index : _485
private parameters indices : [_0]
public parameters indices : []
return value indices : []
BLACKBOX::RANGE [(_0, 32)] []
EXPR [ (1, _0) (-1, _1) -1 ]
...
BLACKBOX::RANGE [(_1, 2)] []
EXPR [ (-1, _164) 18 ]
EXPR [ (-1, _165) 19 ]
EXPR [ (-1, _166) 20 ]
EXPR [ (-1, _167) 21 ]
INIT (id: 1, len: 4, witnesses: [_164, _165, _166, _167])
MEM (id: 1, read at: EXPR [ (1, _1) 0 ], value: EXPR [ (1, _168) 0 ]) 
BRILLIG CALL func 3: inputs: [EXPR [ (1, _168) -7 ]], outputs: [_169]
...

So the array has 4 elements and we got a RANGE constraint to limit x - 1 as witness _1 to 2 bits. We might expect that MEM would make this RANGE redundant, because it also implies indexing the array of size 4, however this did not happen for two reasons:

• Only AssertZero was considered as implied, which is the only kind of constraint considered to make an equal length RANGE redundant. Not sure why, but this is how it worked in the original.
• The implied size from INIT was 3, not 2, so even if it was treated like AssertZero, it was considered less strict than the RANGE.

I changed this so MEM is allowed to take precedence over RANGE, and by limiting the number of bits to what is required to represent the maximum index value, rather than the array size.

(In the original code x - 1 is also used to index an array of size 1, which results in a EXPR [ (1, _1) 0 ] appear in the code, and for that reason all RANGE constraints were removed).

[jfecher]

@aakoshh can you bump up the time for rollup-block-root-empty a bit?

CC @vezenovm for review

[socket-security]

Review the following changes in direct dependencies. Learn more about Socket for GitHub.

Diff	Package	Supply Chain Security	Vulnerability	Quality	Maintenance	License
	@​web/​test-runner-playwright@​0.11.1
	@​web/​dev-server-import-maps@​0.2.1
	@​web/​dev-server-esbuild@​0.3.6
	toml@​3.0.0
	@​ltd/​j-toml@​1.38.0
	tslog@​4.9.3
	@​esm-bundle/​chai@​4.3.4
	ethers@​6.15.0
	@​web/​test-runner@​0.20.2
	@​nomicfoundation/​hardhat-chai-matchers@​2.1.0
	smol-toml@​1.4.2
	hardhat@​2.26.3
	@​aztec/​bb.js@​0.87.0
	@​nomicfoundation/​hardhat-ethers@​3.1.0

View full report

[vezenovm]

CC @vezenovm for review

Will be taking a look today.

[vezenovm]

Looks good! I would like to get the ACIR parser working in other crates but we can do that in follow-up work. One of the main reasons for the ACIR parser was being able to test the ACVM compiler as well as the ACIR gen which both live in different crates.