chore: print ACIR AssertZero as an equation

[asterite]

Description

Problem

Resolves #9964

Summary

Now AssertZero expressions are printed as an equation. In the typical case that the expression looks like it's "assigning" to a witness (the largest witness in a linear combination), the expression is shown "as an assignment" to that witness. See #9970 (comment)

The ACIR parser in this case will parse any equation (there's a new test for this). This was done for simplicity (it's easier to parse an equation as a series of terms compared against other terms) but also for expressiveness, and further simplifications could be added and they'll always parse well. It might also help with writing ACIR tests as you can write the equation you want without having to follow a very specific order.

Additional Context

This isn't part of the auditing but:

1. I'll soon need to audit ACIR and this might help with that, as things become a bit easier to read/understand
2. I'm not finding bugs in any of the audit group passes, though I'll continue looking

There might be a few more special cases that we could print, like w0 = w1*w2, but here I just went with the ones I see are most common.

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: 6f07f9b	Previous: 323303f	Ratio
rollup-block-root-single-tx	0.005 s	0.003 s	1.67
rollup-checkpoint-merge	0.004 s	0.003 s	1.33

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: 6f07f9b	Previous: 323303f	Ratio
test_report_zkpassport_noir_rsa_	2 s	1 s	2

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

CC: @TomAFrench

[vezenovm]

There might be a few more special cases that we could print, like w0 = w1*w2, but here I just went with the ones I see are most common.

The more special cases we allow would also increase the complexity of the Display impl and the parser. I think just handling the most common simplifications is sufficient.

[asterite]

Sounds good, we can revert some of the simplifications (let me know which ones). I tried to leave the ones where they end with a single witness equal to something else, like a constant, witness or multiplication.

[asterite]

In the end now there's only one simplification when printing an AssertZero opcode, which I'll explain now.

I noticed that when ACIR is generated, we usually tend to equate a new witness to an expression that relies on previous witnesses. I think that this happens is not by chance, as it makes sense we slowly build a larger equation where new witness have conditions on previous witnesses, etc.

So, when printing, we find the largest witness that has a 1 or -1 coefficient, and we show that as equal to everything else. This turns out to be pretty accurate and, in most cases, the expressions are shown as "an assignment" to this new witness.

For example, here's part of the ACIR for the test_programs/execution_sucess/hashmap code:

EXPR w29105 = w29101*w29102 + w29101
BLACKBOX::RANGE [w29105]:32 bits []
EXPR w29106 = w29101*w29105 - w29101 + 1
MEM (id: 250, read at: EXPR [ (1, w29106) ], value: EXPR [ (1, w29107) ])
EXPR w29108 = w29101*w29102 + 2*w29101
BLACKBOX::RANGE [w29108]:32 bits []
EXPR w29109 = w29101*w29108 - w29101 + 1
MEM (id: 250, read at: EXPR [ (1, w29109) ], value: EXPR [ (1, w29110) ])
EXPR w29111 = w29101*w29102 + 3*w29101
BLACKBOX::RANGE [w29111]:32 bits []
EXPR w29112 = w29101*w29111
MEM (id: 250, read at: EXPR [ (1, w29112) ], value: EXPR [ (1, w29113) ])
EXPR w29114 = -w29104*w29113 + w29104
EXPR w29115 = -w26494 + w29107
BRILLIG CALL func 2: inputs: [EXPR [ (1, w29115) ]], outputs: [w29116]
EXPR w29117 = -w29115*w29116 + 1
EXPR 0 = w29115*w29117
EXPR w29118 = w29101*w29114
EXPR w29119 = w29117*w29118
EXPR w29120 = -w29117*w29118 + 1
EXPR w29121 = w26500 + 1
EXPR w29122 = w29101*w29120
EXPR w29123 = w29121*w29122

Note how every expression is almost always "the next witness must be equal to ...".

Another example, fold_2_to_17:

BLACKBOX::POSEIDON2_PERMUTATION [w7007, w7008, w7009, w7006] [w7010, w7011, w7012, w7013]
EXPR w7014 = w0 + w7010
EXPR w7015 = w0 + w7011
EXPR w7016 = w0 + w7012
BLACKBOX::POSEIDON2_PERMUTATION [w7014, w7015, w7016, w7013] [w7017, w7018, w7019, w7020]
EXPR w7021 = w0 + w7017
EXPR w7022 = w0 + w7018
EXPR w7023 = w0 + w7019
BLACKBOX::POSEIDON2_PERMUTATION [w7021, w7022, w7023, w7020] [w7024, w7025, w7026, w7027]
EXPR w7028 = w0 + w7024
EXPR w7029 = w0 + w7025
EXPR w7030 = w0 + w7026

And for this Noir program which I was just playing with:

fn main(x: u32, y: u32, z: u32) {
    assert_eq(z, x * 4 + y * 5 + 2);
}

we get this ACIR:

func 0
current witness: w6
private parameters: [w0, w1, w2]
public parameters: []
return values: []
BLACKBOX::RANGE [w0]:32 bits []
BLACKBOX::RANGE [w1]:32 bits []
BLACKBOX::RANGE [w2]:32 bits []
EXPR w3 = 4*w0
BLACKBOX::RANGE [w3]:32 bits []
EXPR w4 = 5*w1
BLACKBOX::RANGE [w4]:32 bits []
EXPR w5 = w3 + w4
BLACKBOX::RANGE [w5]:32 bits []
EXPR w6 = w5 + 2
BLACKBOX::RANGE [w6]:32 bits []
EXPR w6 = w2

It's very easy to see that w3 = 4*w0 represents x * 4, etc.

[vezenovm]

Some nits, but I think this makes reading ACIR much easier.

[vezenovm]

Looks good! Much prettier to read