fix(ssa_gen): Add constraint on slice length before popping

[aakoshh]

Description

Problem*

Resolves #9266 and #9269

Summary*

• Adds constrain 1 <= slice_length in Brillig before calls to slice_pop_front and slice_pop_back.
• Changes decrement_slice_length in the simplify module to use checked sub in Brillig.
• Fixes simplify_slice_pop_back to stop decrementing the length beyond the number of elements
• Runs execution_failure tests with both default and --force-brillig. In a follow-up PR we could potentially run these tests with the SSA interpreter as well.

Additional Context

With this the integration test correctly fails:

❯ cargo run -q -p nargo_cli -- execute --force --silence-warnings --force-brillig --show-ssa-pass Initial
After Initial SSA:
g0 = Field -282608142060723387702497189224219065418
g1 = u32 1
g2 = make_array [Field -282608142060723387702497189224219065418] : [Field]

brillig(inline) fn main f0 {
  b0():
    inc_rc g2
    inc_rc g2                                     	// src/main.nr:3:18
    constrain u1 0 == u1 1, "Index out of bounds" 	// src/main.nr:4:18
    v7, v8, v9 = call slice_pop_back(u32 0, g2) -> (u32, [Field], Field)	// src/main.nr:4:18
    inc_rc v8                                     	// src/main.nr:4:18
    return v9
}

error: Assertion failed: Index out of bounds
  ┌─ src/main.nr:4:18
  │
4 │     let (_, f) = a.pop_back();
  │                  ----------
  │
  = Call stack:
    1. src/main.nr:4:18

Failed assertion

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]

Changes to Brillig bytecode sizes

Generated at commit: c1afcced080e0cb6f0ede4a997a2a0b3a2b5aa94, compared to commit: e7fb7f3bf083de9fc6d430e7c30a571ea94534e4

🧾 Summary (10% most significant diffs)

Program	Brillig opcodes (+/-)	%
slice_regex_inliner_max	+318 ❌	+17.43%
regression_9312_inliner_max	+5 ❌	+2.48%
regression_9312_inliner_min	+5 ❌	+2.48%
regression_9312_inliner_zero	+5 ❌	+2.48%

---

Full diff report 👇

Program	Brillig opcodes (+/-)	%
slice_regex_inliner_max	2,142 (+318)	+17.43%
regression_9312_inliner_max	207 (+5)	+2.48%
regression_9312_inliner_min	207 (+5)	+2.48%
regression_9312_inliner_zero	207 (+5)	+2.48%
array_sort_inliner_max	421 (+3)	+0.72%
array_sort_inliner_zero	421 (+3)	+0.72%
array_sort_inliner_min	455 (+3)	+0.66%
slice_dynamic_index_inliner_max	2,088 (+6)	+0.29%
slice_dynamic_index_inliner_zero	2,088 (+6)	+0.29%
slice_dynamic_index_inliner_min	2,229 (+6)	+0.27%
slices_inliner_zero	1,653 (+3)	+0.18%
slices_inliner_max	1,694 (+3)	+0.18%
uhashmap_inliner_max	11,646 (+18)	+0.15%
slices_inliner_min	2,171 (+3)	+0.14%
hashmap_inliner_max	17,431 (+18)	+0.10%
uhashmap_inliner_zero	6,875 (+6)	+0.09%
uhashmap_inliner_min	7,290 (+6)	+0.08%
hashmap_inliner_zero	7,730 (+6)	+0.08%
hashmap_inliner_min	8,793 (+6)	+0.07%
slice_regex_inliner_min	1,844 (-5)	-0.27%
slice_regex_inliner_zero	1,595 (-5)	-0.31%

[github-actions]

Changes to number of Brillig opcodes executed

Generated at commit: c1afcced080e0cb6f0ede4a997a2a0b3a2b5aa94, compared to commit: e7fb7f3bf083de9fc6d430e7c30a571ea94534e4

🧾 Summary (10% most significant diffs)

Program	Brillig opcodes (+/-)	%
slice_regex_inliner_max	+602 ❌	+21.64%
slice_regex_inliner_zero	+98 ❌	+2.54%
regression_9312_inliner_max	+4 ❌	+2.50%
regression_9312_inliner_min	+4 ❌	+2.50%
regression_9312_inliner_zero	+4 ❌	+2.50%

---

Full diff report 👇

Program	Brillig opcodes (+/-)	%
slice_regex_inliner_max	3,384 (+602)	+21.64%
slice_regex_inliner_zero	3,957 (+98)	+2.54%
regression_9312_inliner_max	164 (+4)	+2.50%
regression_9312_inliner_min	164 (+4)	+2.50%
regression_9312_inliner_zero	164 (+4)	+2.50%
slice_regex_inliner_min	4,483 (+100)	+2.28%
array_sort_inliner_max	903 (+8)	+0.89%
array_sort_inliner_zero	903 (+8)	+0.89%
array_sort_inliner_min	995 (+7)	+0.71%
hashmap_inliner_max	52,002 (+48)	+0.09%
slice_dynamic_index_inliner_max	4,623 (+4)	+0.09%
slice_dynamic_index_inliner_zero	4,623 (+4)	+0.09%
slice_dynamic_index_inliner_min	4,810 (+4)	+0.08%
slices_inliner_max	2,492 (+2)	+0.08%
slices_inliner_zero	2,759 (+2)	+0.07%
hashmap_inliner_zero	66,843 (+48)	+0.07%
hashmap_inliner_min	73,400 (+48)	+0.07%
slices_inliner_min	3,807 (+2)	+0.05%
uhashmap_inliner_max	144,586 (+48)	+0.03%
uhashmap_inliner_zero	168,828 (+48)	+0.03%
uhashmap_inliner_min	176,742 (+48)	+0.03%

[asterite]

Nice! I wonder if the constrain could be added to the SSA, before invoking those functions. Maybe that way optimizations could discard some constraints if they are known to hold, etc.

[aakoshh]

Good question, I haven’t thought about that because it worked already for ACIR (albeit with slightly different message, talking about the array being 1 long but the index -1), and I saw there is an add_overflow_check in Brillig codegen.

[aakoshh]

To be fair the compiler generated call slice_pop_back(u32 0, g2) so it knows exactly that after popping an item from a 1 long slice it’s left with 0 elements, so it could even forego that and just do a constraint instead of a call. So I agree we can have a look at this.

[aakoshh]

It could even be handled by the remove_unreachable_instructions pass

[asterite]

I haven’t thought about that because it worked already for ACIR

Ah, then there must be a reason for that. If we go the SSA route it will likely make things worse for ACIR, so I'd say the fix here is probably good.

[aakoshh]

Actually there already are some checks inserted, but it says push and pop don't need them:

noir/compiler/noirc_evaluator/src/ssa/ssa_gen/mod.rs

Lines 1051 to 1083 in d35a767

	self.codegen_intrinsic_call_checks(function, &arguments, call.location);
	Ok(self.insert_call(function, arguments, &call.return_type, call.location))
	}
	fn codegen_intrinsic_call_checks(
	&mut self,
	function: ValueId,
	arguments: &[ValueId],
	location: Location,
	) {
	if let Some(intrinsic) =
	self.builder.set_location(location).get_intrinsic_from_value(function)
	{
	match intrinsic {
	Intrinsic::SliceInsert => {
	let one = self.builder.length_constant(1u128);
	// We add one here in the case of a slice insert as a slice insert at the length of the slice
	// can be converted to a slice push back
	// This is unchecked as the slice length could be u32::max
	let len_plus_one = self.builder.insert_binary(
	arguments[0],
	BinaryOp::Add { unchecked: false },
	one,
	);
	self.codegen_access_check(arguments[2], len_plus_one);
	}
	Intrinsic::SliceRemove => {
	self.codegen_access_check(arguments[2], arguments[0]);
	}
	_ => {
	// Do nothing as the other intrinsics do not require checks

[aakoshh]

And even without those two, getting an index does get SSA constraints:

global G_A: [Field] = &[1, 2, 3];
fn main(i: u32) -> pub Field {
    G_A[i]
}

After Initial SSA:
g0 = Field 1
g1 = Field 2
g2 = Field 3
g3 = u32 3
g4 = make_array [Field 1, Field 2, Field 3] : [Field]

brillig(inline) fn main f0 {
  b0(v5: u32):
    v6 = lt v5, u32 3
    constrain v6 == u1 1, "Index out of bounds"
    v8 = array_get g4, index v5 -> Field          	// src/main.nr:3:5
    return v8
}

Perhaps @TomAFrench can tell us why this technique wasn't used for all intrinsic slice operations that can fail based on the size.

[vezenovm]

This looks to simply be an oversight @aakoshh. ACIR appropriately fails as we check memory block sizes, but for Brillig we need to lay down an explicit check as otherwise it will attempt to look in the invalid memory slot. It would be better to have this check in SSA gen.

If we go the SSA route it will likely make things worse for ACIR

We can gate the check by runtime during code gen.

[aakoshh]

It would be better to have this check in SSA gen.

To be clear, are you in favour of inserting a constraint in codegen_intrinsic_call_checks instead of the opcode I added?

I haven't completely figured out how that initial SSA is generated from the integration test, where the simplifications are hidden, but inserting a constraint seems easy enough.

[vezenovm]

To be clear, are you in favour of inserting a constraint in codegen_intrinsic_call_checks instead of the opcode I added?

Yes, as in general I prefer minimizing what code gen we do in Brillig/ACIR gen. When we have the check in SSA gen there is a chance that the check can be simplified out.

[TomAFrench]

Perhaps @TomAFrench can tell us why this technique wasn't used for all intrinsic slice operations that can fail based on the size.

Yeah, test coverage on slices tended to cover just the happy path so this was just omitted because it's not on the happy path and then we moved on to other features.

[aakoshh]

Dumb question:

This code:

global G_A: [Field] = &[-282608142060723387702497189224219065418];
fn main() -> pub Field {
    let (a, _) = G_A.pop_back();
    let (_, f) = a.pop_back();
    f
}

generates this initial SSA:

g0 = Field -282608142060723387702497189224219065418
g1 = u32 1
g2 = make_array [Field -282608142060723387702497189224219065418] : [Field]

brillig(inline) fn main f0 {
  b0():
    inc_rc g2
    v4 = unchecked_sub u32 0, u32 1
    inc_rc g2                                     	// src/main.nr:3:18
    v6, v7, v8 = call slice_pop_back(u32 0, g2) -> (u32, [Field], Field)	// src/main.nr:4:18
    inc_rc v7                                     	// src/main.nr:4:18
    return v8
}

Why does it look like v4 = unchecked_sub u32 0, u32 1 has its arguments in reverse?

(Actually I have no idea what v4 was supposed to be, I thought it's the updated length after popping from G_A, which does not appear in the SSA).

[vezenovm]

Why does it look like v4 = unchecked_sub u32 0, u32 1 has its arguments in reverse?

That subtraction comes from the slice_pop_back simplification under dfg/simplify. It looks like we mark slice length decrements as being unchecked, while increment are in fact checked. Another option to fix this bug would be to make the decrement checked. This would also most likely add extra constraints to ACIR though so we would want to look into gating this by the runtime as well if we went this route.

The first pop_back where the slice length is 1 gets simplified out and we are left with a single pop back.

[aakoshh]

Thanks. I thought it might be that, but didn't understand why we would do that in SSA when slice_pop_back returns the updated length (like v6). So the simplification knows what it would be and does this instead.

[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: 3cc298c	Previous: e7fb7f3	Ratio
test_report_AztecProtocol_aztec-packages_noir-projects_noir-protocol-circuits_crates_private-kernel-lib	2 s	1 s	2

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

CC: @TomAFrench

[aakoshh]

I did both. Making the decrement checked caused a panic with the call stack, which is fixed now.

It's a bit unfortunate that the decrement check says "attempt to subtract with overflow", which masks the original "Index out of bounds" error.

I was wondering if we need both checks:

• If we keep the intrinsic call check, but not the decrement check, then it could overflow and become u32::MAX, and then trivially pass a constraint 0 < length check.
• If we keep the decrement check, but not the intrinsic call check, then if it's not simplified, we get the panics, hangs and invalid return data. In fact it skips simplifying constant zero length slices, although I was thinking about when the length is unknown.

[vezenovm]

• If we keep the intrinsic call check, but not the decrement check, then it could overflow and become u32::MAX, and then trivially pass a constraint 0 < length check

If we have the intrinsic call check, which precedes the pop_back call itself, then we would prevent that overflow from occurring.

• If we keep the decrement check, but not the intrinsic call check, then if it's not simplified, we get the panics, hangs and invalid return data.

Good point. I say we just go with the intrinsic call check.

[aakoshh]

Ah wait, something's not right, now it fails even for the first pop 👀

[aakoshh]

then we would prevent that overflow from occurring.

I meant if we chained them together, something like this:

length1, slice1, elem1 = call slice_pop_back(length0, slice0)
length2, slice2, elem2 = call slice_pop_back(length1, slice1)

turned into:

length1 = unchecked_sub length0, 1                            // what if length1 becomes u32::MAX here
constrain 0 < length1, "Index out of bounds"                  // and passes this constraint
length2, slice2, elem2 = call slice_pop_back(length1, slice0) // then gives invalid result

[aakoshh]

So now this:

global G_A: [Field] = &[-282608142060723387702497189224219065418];
fn main() -> pub Field {
    let (a, f) = G_A.pop_back();
    f
}

generates:

g0 = Field -282608142060723387702497189224219065418
g1 = u32 1
g2 = make_array [Field -282608142060723387702497189224219065418] : [Field]

brillig(inline) fn main f0 {
  b0():
    inc_rc g2
    v4 = sub u32 0, u32 1                         	// src/main.nr:3:18
    inc_rc g2                                     	// src/main.nr:3:18
    return Field -282608142060723387702497189224219065418
}

and fails on the sub

[aakoshh]

Maybe it's

noir/compiler/noirc_evaluator/src/ssa/ir/dfg/simplify/call.rs

Line 558 in d35a767

flattened_len = decrement_slice_length(flattened_len, dfg, block);

Got it, there was an extra decrement after all the type-elements were popped, that's where the v4 was coming from.

[aakoshh]

I say we just go with the intrinsic call check.

I came to agree with this: the SlicePop* simplifications don't take effect unless length is a known constant, so we should be safe from overflows. With the extra decrement bug fixed, there's no need for checked operations.

[asterite]

LGTM