chore(ACIR): expand signed lt, div and mod in SSA

[asterite]

Description

Problem

Part of #10029

Summary

Additional Context

Given this program:

fn main(x: i8, y: i8) -> pub bool {
    x < y
}

The ACIR we get is this:

Compiled ACIR for main (non-transformed):
func 0
current witness: w10
private parameters: [w0, w1]
public parameters: []
return values: [w2]
BLACKBOX::RANGE [w0]:8 bits []
BLACKBOX::RANGE [w1]:8 bits []
BRILLIG CALL func 0: inputs: [w0, 128], outputs: [w3, w4]
BLACKBOX::RANGE [w3]:1 bits []
BLACKBOX::RANGE [w4]:7 bits []
EXPR w4 = w0 - 128*w3
BRILLIG CALL func 0: inputs: [w1, 128], outputs: [w5, w6]
BLACKBOX::RANGE [w5]:1 bits []
BLACKBOX::RANGE [w6]:7 bits []
EXPR w6 = w1 - 128*w5
BRILLIG CALL func 0: inputs: [w0 - w1 + 256, 256], outputs: [w7, w8]
BLACKBOX::RANGE [w7]:1 bits []
BLACKBOX::RANGE [w8]:8 bits []
EXPR w8 = w0 - w1 - 256*w7 + 256
EXPR w9 = -2*w3*w5 + w3 + w5
EXPR w10 = -w7 + 1
EXPR w10 = 2*w9*w10 + w2 - w9

unconstrained func 0
0: @10 = const u32 2
1: @11 = const u32 0
2: @0 = calldata copy [@11; @10]
3: @2 = field int_div @0, @1
4: @1 = field mul @2, @1
5: @1 = field sub @0, @1
6: @0 = @2
7: stop &[@11; @10]

It's huge! In the end, if we check what we do in ACIR (that is, the source code that produces this ACIR), it's understandable. The problem is that operations like "divide x by y" in ACIR result in some ACIR expressions that are then hard to reconstruct as "this is a division".

On the other hand, we start with this SSA:

acir(inline) fn main f0 {
  b0(v0: i8, v1: i8):
    v2 = lt v0, v1
    constrain v2 == u1 1
    return
}

Then now we transform it to this SSA:

acir(inline) fn main f0 {
  b0(v0: i8, v1: i8):
    v2 = cast v0 as u8
    v3 = cast v1 as u8
    v5 = div v2, u8 128
    v6 = cast v5 as u1
    v7 = div v3, u8 128
    v8 = cast v7 as u1
    v9 = xor v6, v8
    v10 = lt v2, v3
    v11 = xor v9, v10
    constrain v11 == u1 1
    return
}

It's also a lot of code but not as much as in ACIR, and what happens is easier to understand. Here we can see that we cast the values to their unsigned counterparts, then divide by 128 (presumably to check the sign). Then there's a comparison using these unsigned types and a couple of xor, which need an explanation... but all of this is also what happened in ACIR but it was far less clear.

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 'ACVM Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: 090ea14	Previous: 39f193c	Ratio
perfectly_parallel_batch_inversion_opcodes	2785109 ns/iter (± 9534)	2254940 ns/iter (± 1115)	1.24

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

CC: @TomAFrench

[github-actions]

Changes to circuit sizes

Generated at commit: 839415df5c9804a42a40a82c937390a790aa0214, compared to commit: 6898710858ee3e351a15e687bfeb6aa39715612f

🧾 Summary (10% most significant diffs)

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
signed_comparison	-20 ✅	-13.99%	-105 ✅	-34.31%
signed_cmp	-15 ✅	-23.81%	-102 ✅	-42.68%
regression_9971	0 ➖	0.00%	-109 ✅	-51.66%

---

Full diff report 👇

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
signed_inactive_division_by_zero	46 (+2)	+4.55%	2,813 (+2)	+0.07%
inactive_signed_bitshift	79 (-2)	-2.47%	2,842 (-10)	-0.35%
signed_arithmetic	178 (-11)	-5.82%	2,933 (-11)	-0.37%
regression_10008	13 (-7)	-35.00%	2,774 (-11)	-0.39%
regression_8726	51 (-20)	-28.17%	2,888 (-23)	-0.79%
signed_division	184 (-42)	-18.58%	3,680 (-37)	-1.00%
regression_1144_1169_2399_6609	254 (-69)	-21.36%	5,172 (-59)	-1.13%
bit_shifts_runtime	467 (-76)	-14.00%	4,714 (-166)	-3.40%
bit_shifts_comptime	51 (-14)	-21.54%	2,906 (-104)	-3.46%
signed_div	525 (-45)	-7.89%	556 (-45)	-7.49%
signed_comparison	123 (-20)	-13.99%	201 (-105)	-34.31%
signed_cmp	48 (-15)	-23.81%	137 (-102)	-42.68%
regression_9971	35 (0)	0.00%	102 (-109)	-51.66%

[asterite]

Huh, I didn't expect Brillig regressions as this PR shouldn't modify Brillig at all... on the other and we can see some ACIR improvements, which I expected because for example when doing signed bitshifts we were using signed "less than" but now it's a simpler unsigned comparison that can be done with less ACIR opcodes.

I'll check what's going on with Brillig...

[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: c2e0c77	Previous: 6898710	Ratio
test_report_noir-lang_sha512_	16 s	13 s	1.23

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

CC: @TomAFrench

[asterite]

Aaah... I didn't realize this pass ran on brillig too. I'll change it to not run on brillig for the "less than" case.

[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: 35f471d	Previous: 6898710	Ratio
rollup-block-root-single-tx	0.003 s	0.002 s	1.50

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

CC: @TomAFrench

[asterite]

Is this good or bad?

[guipublic]

Is this good or bad?

It's good, the circuit size is what matters at the end.

[aakoshh]

"divide x by y" in ACIR result in some ACIR expressions that are then hard to reconstruct as "this is a division"

Just to note that the new SSA mapping has 2 divs in it, so I imagine this would be mean it's even harder to recognise in ACIR that "this is a less-than" 😉

[asterite]

One more thing: for the Noir code in the very beginning of this issue, the previous ACIR was:

current witness: w10
private parameters: [w0, w1]
public parameters: []
return values: [w2]
BLACKBOX::RANGE [w0]:8 bits []
BLACKBOX::RANGE [w1]:8 bits []
BRILLIG CALL func 0: inputs: [w0, 128], outputs: [w3, w4]
BLACKBOX::RANGE [w3]:1 bits []
BLACKBOX::RANGE [w4]:7 bits []
EXPR w4 = w0 - 128*w3
BRILLIG CALL func 0: inputs: [w1, 128], outputs: [w5, w6]
BLACKBOX::RANGE [w5]:1 bits []
BLACKBOX::RANGE [w6]:7 bits []
EXPR w6 = w1 - 128*w5
BRILLIG CALL func 0: inputs: [w0 - w1 + 512, 512], outputs: [w7, w8]
BLACKBOX::RANGE [w7]:1 bits []
BLACKBOX::RANGE [w8]:9 bits []
EXPR w8 = w0 - w1 - 512*w7 + 512
EXPR w9 = -w7 + 1
EXPR w10 = -2*w3*w5 + w3 + w5
EXPR w10 = 2*w9*w10 + w2 - w9

Now it's:

current witness: w10
private parameters: [w0, w1]
public parameters: []
return values: [w2]
BLACKBOX::RANGE [w0]:8 bits []
BLACKBOX::RANGE [w1]:8 bits []
BRILLIG CALL func 0: inputs: [w0, 128], outputs: [w3, w4]
BLACKBOX::RANGE [w3]:1 bits []
BLACKBOX::RANGE [w4]:7 bits []
EXPR w4 = w0 - 128*w3
BRILLIG CALL func 0: inputs: [w1, 128], outputs: [w5, w6]
BLACKBOX::RANGE [w5]:1 bits []
BLACKBOX::RANGE [w6]:7 bits []
EXPR w6 = w1 - 128*w5
BRILLIG CALL func 0: inputs: [w0 - w1 + 256, 256], outputs: [w7, w8]
BLACKBOX::RANGE [w7]:1 bits []
BLACKBOX::RANGE [w8]:8 bits []
EXPR w8 = w0 - w1 - 256*w7 + 256
EXPR w9 = -2*w3*w5 + w3 + w5
EXPR w10 = -w7 + 1
EXPR w10 = 2*w9*w10 + w2 - w9

Note that we previously used 512 and now we use 256. These values are used to add the two signed values together so they don't underflow. I think the two programs should be equivalent. That said, I don't know why we ended up with 512 before... ah, or maybe when comparing the two values we added 256 twice because a helper ACIR function would also try to avoid underflow... not sure!

I just wanted to mention this because I fear this change might have introduced a bug, but on the other hand both ways to do this look good.

[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: bddecb5	Previous: 39f193c	Ratio
sha512-100-bytes	2.107 s	1.665 s	1.27

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

CC: @TomAFrench

[vezenovm]

Looks good to me! I generally am in favor of these moves from ACIR gen into our SSA.

[vezenovm]

Note that we previously used 512 and now we use 256. These values are used to add the two signed values together so they don't underflow. I think the two programs should be equivalent. That said, I don't know why we ended up with 512 before... ah, or maybe when comparing the two values we added 256 twice because a helper ACIR function would also try to avoid underflow... not sure!

In the old less_than_signed in ACIR gen we were using 1 << bit_size to check for underflows.