feat(ssa): Following an always failing binary, replace instructions with defaults until the next predicate

[aakoshh]

Description

Problem*

Follow up for #9195 (comment)

Summary*

Adds new logic to remove_unreachable_instructions to handle always failing binary instructions which are under a predicate by entering an UnreachableUnderPredicate mode, in which instructions that have side effects get removed, and their results replaced by default values. This mode persists until the next enable_side_effects instruction, or the end of the block.

The reasoning to do so is that if the binary operation is known to fail, then until side effect conditions change, it doesn't matter if it was enabled or not, the subsequent operations cannot have an effect, so we can get rid of them. We keep their results, because within the same block those might be used, but we replace them with default values that may not even appear in the SSA as instructions, such as numeric constants.

Additional Context

Looking at the SSA of the program from the predecessor ticket, it changes as follows:

❯ cargo run -q -p nargo_cli -- execute --force --show-ssa --silence-warnings --show-ssa-pass "step 31" --show-ssa-pass "step 32"
After Mem2Reg (4) (step 31):
g0 = u32 0
g1 = make_array [] : [Field]

acir(inline) predicate_pure fn main f0 {
  b0(v2: u1, v3: u1, v4: Field):
    enable_side_effects v2
    v6 = mod u32 2050918985, u32 0                	// src/main.nr:7:20
    constrain u1 0 == v2, "Index out of bounds"   	// src/main.nr:7:20
    v8 = make_array [] : [Field]                  	// src/main.nr:7:20
    v9 = array_get v8, index v6 -> Field          	// src/main.nr:7:17
    enable_side_effects u1 0
    v11 = call f1(u32 0) -> Field                 	// src/main.nr:14:29
    v12 = truncate v11 to 32 bits, max_bit_size: 254	// src/main.nr:14:29
    v13 = cast v12 as u32                         	// src/main.nr:14:29
    v14 = not v3
    v15 = unchecked_mul v2, v14
    v16 = cast v15 as u32                         	// src/main.nr:14:29
    v18 = unchecked_mul v16, u32 766482358        	// src/main.nr:14:29
    v19 = not v2
    v20 = unchecked_mul v2, v19
    v21 = cast v2 as u32                          	// src/main.nr:14:29
    v22 = cast v20 as u32                         	// src/main.nr:14:29
    v23 = unchecked_mul v21, v18                  	// src/main.nr:14:29
    v25 = unchecked_mul v22, u32 1568313658       	// src/main.nr:14:29
    v26 = unchecked_add v23, v25                  	// src/main.nr:14:29
    enable_side_effects v2
    v27 = call f1(v26) -> Field                   	// src/main.nr:11:17
    enable_side_effects v19
    v29 = mod u32 779011912, u32 0                	// src/main.nr:28:20
    constrain v2 == u1 1, "Index out of bounds"   	// src/main.nr:28:20
    v31 = array_get v8, index v29 -> Field        	// src/main.nr:28:17
    enable_side_effects u1 1
    v32 = cast v2 as Field                        	// src/main.nr:7:17
    v33 = cast v19 as Field                       	// src/main.nr:7:17
    v34 = mul v32, v9                             	// src/main.nr:7:17
    v35 = mul v33, v31                            	// src/main.nr:7:17
    v36 = add v34, v35                            	// src/main.nr:7:17
    v37 = mul v32, v27                            	// src/main.nr:11:17
    v38 = mul v33, v4                             	// src/main.nr:11:17
    v39 = add v37, v38                            	// src/main.nr:11:17
    return v36, v39
}
brillig(inline) predicate_pure fn func_1_proxy f1 {
  b0(v2: u32):
    return Field 0
}

After Remove Unreachable Instructions (1) (step 32):
g0 = u32 0
g1 = make_array [] : [Field]

acir(inline) predicate_pure fn main f0 {
  b0(v2: u1, v3: u1, v4: Field):
    enable_side_effects v2
    v6 = mod u32 2050918985, u32 0                	// src/main.nr:7:20
    constrain u1 0 == v2, "attempt to calculate the remainder with a divisor of zero"	// src/main.nr:7:20
    v8 = make_array [] : [Field]                  	// src/main.nr:7:20
    enable_side_effects u1 0
    v10 = call f1(u32 0) -> Field                 	// src/main.nr:14:29
    v11 = truncate v10 to 32 bits, max_bit_size: 254	// src/main.nr:14:29
    v12 = cast v11 as u32                         	// src/main.nr:14:29
    v13 = not v3
    v14 = unchecked_mul v2, v13
    v15 = cast v14 as u32                         	// src/main.nr:14:29
    v17 = unchecked_mul v15, u32 766482358        	// src/main.nr:14:29
    v18 = not v2
    v19 = unchecked_mul v2, v18
    v20 = cast v2 as u32                          	// src/main.nr:14:29
    v21 = cast v19 as u32                         	// src/main.nr:14:29
    v22 = unchecked_mul v20, v17                  	// src/main.nr:14:29
    v24 = unchecked_mul v21, u32 1568313658       	// src/main.nr:14:29
    v25 = unchecked_add v22, v24                  	// src/main.nr:14:29
    enable_side_effects v2
    v26 = call f1(v25) -> Field                   	// src/main.nr:11:17
    enable_side_effects v18
    v28 = mod u32 779011912, u32 0                	// src/main.nr:28:20
    constrain v2 == u1 1, "attempt to calculate the remainder with a divisor of zero"	// src/main.nr:28:20
    enable_side_effects u1 1
    v30 = cast v2 as Field                        	// src/main.nr:7:17
    v31 = cast v18 as Field                       	// src/main.nr:7:17
    v33 = mul v30, Field 0                        	// src/main.nr:7:17
    v34 = mul v31, Field 0                        	// src/main.nr:7:17
    v35 = add v33, v34                            	// src/main.nr:7:17
    v36 = mul v30, v26                            	// src/main.nr:11:17
    v37 = mul v31, v4                             	// src/main.nr:11:17
    v38 = add v36, v37                            	// src/main.nr:11:17
    return v35, v38
}
brillig(inline) predicate_pure fn func_1_proxy f1 {
  b0(v2: u32):
    return Field 0
}

error: Failed constraint
   ┌─ src/main.nr:28:20
   │
28 │                 k[(779011912_u32 % k.len())]
   │                    -----------------------
   │
   = Call stack:
     1. src/main.nr:28:20

Failed to solve program: 'Cannot satisfy constraint'

So the result is the same, but notice these changes:

After Remove Unreachable Instructions (1) (step 32):
g0 = u32 0
g1 = make_array [] : [Field]

acir(inline) predicate_pure fn main f0 {
  b0(v2: u1, v3: u1, v4: Field):
    enable_side_effects v2
    // Binary operation known to fail if v2 is enabled
    v6 = mod u32 2050918985, u32 0                	
    // New constraint added under the same predicate. 
    // Old constraint removed as known to pass
    constrain u1 0 == v2, "attempt to calculate the remainder with a divisor of zero"	 
    // make_array was kept because it has no side effect
    v8 = make_array [] : [Field]     
    // The array_get is gone, because its result is just a Field
    enable_side_effects u1 0                         
...       	
    v18 = not v2
...                	
    enable_side_effects v18
    // Binary operation known to fail if v2 is disabled
    v28 = mod u32 779011912, u32 0 
    // New constraint under the same condition as the modulo           	
    constrain v2 == u1 1, "attempt to calculate the remainder with a divisor of zero"	
    // The array_get is gone
    enable_side_effects u1 1
...
    // Instead of using the results of the array_get, using constant Field 0                   	
    v33 = mul v30, Field 0                        	
    v34 = mul v31, Field 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 'Test Suite Duration'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: 0a24d9c	Previous: e7a98f2	Ratio
test_report_zkpassport_noir-ecdsa_	132 s	105 s	1.26

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

CC: @TomAFrench

[aakoshh]

Fuzzing found an example in https://github.com/noir-lang/noir/actions/runs/16296162751/job/46019184144?pr=9211 where the minimal pipeline returns a non-zero value, while the full return 0. It minimises to this:

global G_A: [Field] = &[];
fn main(a: u32) -> pub Field {
    match a {
        4166865152 => G_A[(102921721_u32 % G_A.len())],
        2676856374 => (a as Field),
        _ => -339696707650690765565390531789020390020,
    }
}

The culprit seems to be the "EnableSideEffectsIf removal" pass, which follows this stage, and removes all interim enable_side_effects instructions between v6 = mod u32 102921721, u32 0 and v21 = mul v18, Field -339696707650690765565390531789020390020, and that has_side_effect thought that Field multiplication can fail:

After Simplify conditionals for unconstrained (1) (step 24):
g0 = u32 0
g1 = make_array [] : [Field]

acir(inline) predicate_pure fn main f0 {
  b0(v2: u32):
    v4 = eq v2, u32 4166865152
    enable_side_effects v4
    v6 = mod u32 102921721, u32 0                 	// src/main.nr:4:28
    constrain u1 0 == v4, "Index out of bounds"   	// src/main.nr:4:28
    v8 = make_array [] : [Field]                  	// src/main.nr:4:28
    v9 = array_get v8, index v6 -> Field          	// src/main.nr:4:23
    v10 = not v4
    enable_side_effects v10
    v12 = eq v2, u32 2676856374                   	// src/main.nr:4:23
    v13 = unchecked_mul v10, v12                  	// src/main.nr:4:23
    enable_side_effects v13                       	// src/main.nr:4:23
    v14 = cast v2 as Field                        	// src/main.nr:5:24
    v15 = not v12                                 	// src/main.nr:4:23
    v16 = unchecked_mul v10, v15                  	// src/main.nr:4:23
    enable_side_effects v10                       	// src/main.nr:4:23
    v17 = cast v13 as Field                       	// src/main.nr:5:24
    v18 = cast v16 as Field                       	// src/main.nr:5:24
    v19 = mul v17, v14                            	// src/main.nr:5:24
    v21 = mul v18, Field -339696707650690765565390531789020390020	// src/main.nr:5:24
    v22 = add v19, v21                            	// src/main.nr:5:24
    enable_side_effects u1 1
    v24 = cast v4 as Field                        	// src/main.nr:4:23
    v25 = cast v10 as Field                       	// src/main.nr:4:23
    v26 = mul v24, v9                             	// src/main.nr:4:23
    v27 = mul v25, v22                            	// src/main.nr:4:23
    v28 = add v26, v27                            	// src/main.nr:4:23
    return v28
}

I made has_side_effect a bit more nuanced and then it worked, but to be safe I switched to using requires_acir_gen_predicate to match the other pass.

[github-actions]

Changes to Brillig bytecode sizes

Generated at commit: 4feb33f2fa728e9ccc7f91b4c942c548db370ecf, compared to commit: e7a98f2ffb2521b834747bf9a40dc7be1f813bcd

🧾 Summary (10% most significant diffs)

Program	Brillig opcodes (+/-)	%
tuple_inputs_inliner_min	-2 ✅	-0.68%
tuple_inputs_inliner_zero	-2 ✅	-0.68%

---

Full diff report 👇

Program	Brillig opcodes (+/-)	%
uhashmap_inliner_min	7,284 (-1)	-0.01%
uhashmap_inliner_zero	6,869 (-1)	-0.01%
hashmap_inliner_min	8,787 (-2)	-0.02%
slices_inliner_min	2,168 (-2)	-0.09%
tuple_inputs_inliner_max	314 (-2)	-0.63%
tuple_inputs_inliner_min	290 (-2)	-0.68%
tuple_inputs_inliner_zero	290 (-2)	-0.68%

[github-actions]

Changes to number of Brillig opcodes executed

Generated at commit: 4feb33f2fa728e9ccc7f91b4c942c548db370ecf, compared to commit: e7a98f2ffb2521b834747bf9a40dc7be1f813bcd

🧾 Summary (10% most significant diffs)

Program	Brillig opcodes (+/-)	%
tuple_inputs_inliner_min	-1 ✅	-0.17%
tuple_inputs_inliner_zero	-1 ✅	-0.17%
tuple_inputs_inliner_max	-1 ✅	-0.19%

---

Full diff report 👇

Program	Brillig opcodes (+/-)	%
tuple_inputs_inliner_min	577 (-1)	-0.17%
tuple_inputs_inliner_zero	577 (-1)	-0.17%
tuple_inputs_inliner_max	535 (-1)	-0.19%

[github-actions]

⚠️ Performance Alert ⚠️

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

Benchmark suite	Current: 859e15a	Previous: e7a98f2	Ratio
rollup-base-private	21.28 s	16.54 s	1.29

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

CC: @TomAFrench

[asterite]

Some weeks ago I noticed that binary operations could be simplified, so for example if they always overflow we could replace them with a constrain failure. That was actually the first way I implemented that logic instead of eventually adding it to remove_unreachable_operations. The problem with that approach is that insert_binary assumes it's always going to give back one result, but when we simplify it to a constrain failure that's not the case anymore, so an unwrap() there fails. We can change insert_binary to return an Option but then a lot of code stops compiling and we have to consider each call case by case. But maybe that's fine: if the binary operation is known to fail there's no point in adding more instructions after that, if those depend on the result.

I'm going to try that in a separate PR just to see if it works, because I think it makes sense.

[asterite]

In the end what I said above could be done but would require handling of unreachable earlier, which is the reason why we didn't do something different in the first place. So this PR is the best thing to do 👍