Add support for user-defined \\equals simplification

[ana-pantilie]

Fixes #3040

Scope:

Estimate:

---

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

• Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
• Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
• Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
• Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-totalSupply.sh	-0.000135	0.003473
test/regression-evm/test-sha3_bigSize.sh	-0.000397	0
test/regression-evm/test-lemmas.sh	-0.000719	-0.000346
test/regression-evm/test-addu48u48.sh	-0.000154	-0.003390
test/regression-evm/test-branching-no-invalid.sh	-0.000402	0
test/regression-evm/test-sumTo10.sh	-0.000009	-0.000011
test/regression-evm/test-mul0.sh	-0.000298	0
test/regression-evm/test-straight-line-no-invalid.sh	-0.000469	0
test/regression-evm/test-straight-line.sh	-0.000457	0
test/regression-evm/test-pop1.sh	-0.000401	0
test/regression-evm/test-branching-invalid.sh	-0.000379	0
test/regression-evm/test-add0.sh	-0.000307	0
test/regression-evm/test-dsvalue-peek-pass-rough.sh	-0.000136	-0.005036
test/regression-evm/test-and0.sh	-0.000305	0
test/regression-evm/test-sum-to-n.sh	-0.000394	-0.006369
test/regression-evm/test-storagevar03.sh	-0.000206	0.000017
test/regression-wasm/test-simple-arithmetic.sh	-0.001031	0.000334
test/regression-wasm/test-loops.sh	-0.000942	0.000381
test/regression-wasm/test-memory.sh	-0.001016	0.000306
test/regression-wasm/test-wrc20.sh	-0.000066	-0.000094
test/regression-wasm/test-locals.sh	-0.000967	0.002018

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-totalSupply.sh	0.003836	-0.000203
test/regression-evm/test-sha3_bigSize.sh	0.002893	0
test/regression-evm/test-lemmas.sh	0.005136	0.001130
test/regression-evm/test-addu48u48.sh	0.007459	0.001086
test/regression-evm/test-branching-no-invalid.sh	0.003070	0
test/regression-evm/test-sumTo10.sh	0.001636	-0.027061
test/regression-evm/test-mul0.sh	0.002653	0
test/regression-evm/test-straight-line-no-invalid.sh	0.003233	0
test/regression-evm/test-straight-line.sh	0.003197	0.000031
test/regression-evm/test-pop1.sh	0.002943	0.000027
test/regression-evm/test-branching-invalid.sh	0.003024	0
test/regression-evm/test-add0.sh	0.002679	0.000027
test/regression-evm/test-dsvalue-peek-pass-rough.sh	0.003950	0.000760
test/regression-evm/test-and0.sh	0.002679	0
test/regression-evm/test-sum-to-n.sh	0.002982	0.007069
test/regression-evm/test-storagevar03.sh	0.004328	-0.003200
test/regression-wasm/test-simple-arithmetic.sh	0.005934	-0.000713
test/regression-wasm/test-loops.sh	0.006156	-0.000555
test/regression-wasm/test-memory.sh	0.005912	-0.000450
test/regression-wasm/test-wrc20.sh	0.003392	0.022622
test/regression-wasm/test-locals.sh	0.005678	-0.001330

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-branching-no-invalid.sh	-0.114757	0.000022
test/regression-evm/test-totalSupply.sh	0.004001	0.312160
test/regression-evm/test-dsvalue-peek-pass-rough.sh	0.005159	0.004677
test/regression-evm/test-addu48u48.sh	0.007443	-0.014293
test/regression-evm/test-storagevar03.sh	0.004556	0.007056
test/regression-evm/test-add0.sh	-0.092054	0.000013
test/regression-evm/test-straight-line.sh	-0.129976	0.000008
test/regression-evm/test-and0.sh	-0.092046	0.000013
test/regression-evm/test-pop1.sh	-0.114507	0.000013
test/regression-evm/test-mul0.sh	-0.090209	0.000013
test/regression-evm/test-straight-line-no-invalid.sh	-0.133345	0.000048
test/regression-evm/test-sha3_bigSize.sh	-0.110680	0.000039
test/regression-evm/test-branching-invalid.sh	-0.112297	0.000008
test/regression-evm/test-sumTo10.sh	-0.007685	0.055158
test/regression-evm/test-sum-to-n.sh	0.002797	0.004911
test/regression-evm/test-lemmas.sh	0.004877	0.005952
test/regression-wasm/test-memory.sh	0.004906	0.016553
test/regression-wasm/test-loops.sh	0.005990	0.016565
test/regression-wasm/test-simple-arithmetic.sh	0.004507	0.016619
test/regression-wasm/test-wrc20.sh	0.003638	0.027779
test/regression-wasm/test-locals.sh	0.003962	0.006906

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-branching-no-invalid.sh	0.004912	-0.000027
test/regression-evm/test-totalSupply.sh	0.003830	-0.000428
test/regression-evm/test-dsvalue-peek-pass-rough.sh	0.003928	0.003819
test/regression-evm/test-addu48u48.sh	0.007455	-0.014993
test/regression-evm/test-storagevar03.sh	0.004333	0.000317
test/regression-evm/test-add0.sh	0.004230	0
test/regression-evm/test-straight-line.sh	0.005307	0
test/regression-evm/test-and0.sh	0.004228	0
test/regression-evm/test-pop1.sh	0.004829	0
test/regression-evm/test-mul0.sh	0.004166	0.000027
test/regression-evm/test-straight-line-no-invalid.sh	0.005357	0
test/regression-evm/test-sha3_bigSize.sh	0.004721	0
test/regression-evm/test-branching-invalid.sh	0.004787	0
test/regression-evm/test-sumTo10.sh	0.001802	0.000027
test/regression-evm/test-sum-to-n.sh	0.002997	0.002684
test/regression-evm/test-lemmas.sh	0.005130	0.000120
test/regression-wasm/test-memory.sh	0.005958	-0.000802
test/regression-wasm/test-loops.sh	0.006143	-0.000802
test/regression-wasm/test-simple-arithmetic.sh	0.005877	-0.000672
test/regression-wasm/test-wrc20.sh	0.003398	0.017913
test/regression-wasm/test-locals.sh	0.005669	-0.000857

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-branching-no-invalid.sh	-0.114761	0.000022
test/regression-evm/test-totalSupply.sh	0.003989	0.308267
test/regression-evm/test-dsvalue-peek-pass-rough.sh	0.005117	0.005241
test/regression-evm/test-addu48u48.sh	0.007444	-0.003262
test/regression-evm/test-storagevar03.sh	0.004580	0.006107
test/regression-evm/test-add0.sh	-0.092051	0.000013
test/regression-evm/test-straight-line.sh	-0.129976	0.000008
test/regression-evm/test-and0.sh	-0.092046	0.000013
test/regression-evm/test-pop1.sh	-0.114507	0.000013
test/regression-evm/test-mul0.sh	-0.090206	0.000013
test/regression-evm/test-straight-line-no-invalid.sh	-0.133354	0.000021
test/regression-evm/test-sha3_bigSize.sh	-0.110680	0.000039
test/regression-evm/test-branching-invalid.sh	-0.112297	0.000008
test/regression-evm/test-sumTo10.sh	-0.007685	0.055158
test/regression-evm/test-sum-to-n.sh	0.002815	0.002987
test/regression-evm/test-lemmas.sh	0.004882	0.007821
test/regression-wasm/test-memory.sh	0.004930	0.016554
test/regression-wasm/test-loops.sh	0.005987	0.016565
test/regression-wasm/test-simple-arithmetic.sh	0.004630	0.016818
test/regression-wasm/test-wrc20.sh	0.003640	0.007424
test/regression-wasm/test-locals.sh	0.003962	0.006906

[dwightguth]

This solves my issue in the C semantics. There was some kind of weird other issue that was interfering with the simplification rule being applied in some cases, but I no longer seem to be able to reproduce whatever it was. I figure we can address it later if we run into it again.

The code looks okay to my admittedly novice eye as well. I would recommend Max reviewing the code as well before merging, but this is good to go as far as I'm concerned.

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	0.004230	0
test/regression-evm/test-totalSupply.sh	0.003833	-0.000264
test/regression-evm/test-straight-line.sh	0.005307	0
test/regression-evm/test-branching-no-invalid.sh	0.004914	0
test/regression-evm/test-pop1.sh	0.004830	0
test/regression-evm/test-lemmas.sh	0.005135	0.000601
test/regression-evm/test-mul0.sh	0.004154	0
test/regression-evm/test-branching-invalid.sh	0.004788	0
test/regression-evm/test-addu48u48.sh	0.007456	-0.003781
test/regression-evm/test-storagevar03.sh	0.004318	0.002795
test/regression-evm/test-dsvalue-peek-pass-rough.sh	0.003943	-0.000988
test/regression-evm/test-sum-to-n.sh	0.002991	-0.000063
test/regression-evm/test-sumTo10.sh	0.001802	0
test/regression-evm/test-sha3_bigSize.sh	0.004698	0
test/regression-evm/test-and0.sh	0.004217	0
test/regression-evm/test-straight-line-no-invalid.sh	0.005355	0
test/regression-wasm/test-loops.sh	0.006155	-0.000732
test/regression-wasm/test-simple-arithmetic.sh	0.005873	-0.000716
test/regression-wasm/test-wrc20.sh	0.003405	-0.000380
test/regression-wasm/test-memory.sh	0.005932	-0.001035
test/regression-wasm/test-locals.sh	0.005669	-0.000857