Remove toPattern from Kore.Step.Simplification.Iff

[dopamane]

Fixes #2610

---

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-straight-line-no-invalid.sh	0.000049	0
test/regression-evm/test-straight-line.sh	0.000044	0.000000
test/regression-evm/test-branching-no-invalid.sh	0.000044	-0.000000
test/regression-evm/test-add0.sh	0.000051	0
test/regression-evm/test-sum-to-n.sh	0.000065	-0.000996
test/regression-evm/test-sumTo10.sh	0.000031	-0.003460
test/regression-evm/test-pop1.sh	0.000046	0.000000
test/regression-evm/test-branching-invalid.sh	0.000033	0
test/regression-wasm/test-loops.sh	0.000078	0.000140
test/regression-wasm/test-wrc20.sh	0.000068	-0.000434
test/regression-wasm/test-locals.sh	0.000051	0.000122
test/regression-wasm/test-simple-arithmetic.sh	0.000061	-0.000016
test/regression-wasm/test-memory.sh	0.000079	-0.000108

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-straight-line-no-invalid.sh	0.001100	-0.057364
test/regression-evm/test-straight-line.sh	0.001095	0
test/regression-evm/test-branching-no-invalid.sh	0.001058	-0.000000
test/regression-evm/test-add0.sh	0.001049	0
test/regression-evm/test-sum-to-n.sh	0.001189	0.001295
test/regression-evm/test-sumTo10.sh	0.000632	0.001704
test/regression-evm/test-pop1.sh	0.001111	0.000000
test/regression-evm/test-branching-invalid.sh	0.001041	0
test/regression-wasm/test-loops.sh	0.001278	0.000131
test/regression-wasm/test-wrc20.sh	0.000912	-0.000015
test/regression-wasm/test-locals.sh	0.001596	0.000275
test/regression-wasm/test-simple-arithmetic.sh	0.001586	0.000020
test/regression-wasm/test-memory.sh	0.001383	-0.000075

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-straight-line-no-invalid.sh	0.001100	0
test/regression-evm/test-straight-line.sh	0.001094	0
test/regression-evm/test-branching-no-invalid.sh	0.001058	0
test/regression-evm/test-add0.sh	0.001049	0.000001
test/regression-evm/test-sum-to-n.sh	0.001187	-0.000535
test/regression-evm/test-sumTo10.sh	0.000632	0.000726
test/regression-evm/test-pop1.sh	0.001111	0
test/regression-evm/test-branching-invalid.sh	0.001024	0
test/regression-wasm/test-loops.sh	0.001250	0.000131
test/regression-wasm/test-wrc20.sh	0.000902	-0.000311
test/regression-wasm/test-locals.sh	0.001596	0.000276
test/regression-wasm/test-simple-arithmetic.sh	0.001572	0.000020
test/regression-wasm/test-memory.sh	0.001317	-0.000076

[ttuegel]

I made a truth table to check this change, and found that the old output is equivalent to the new output. After that, I found a clear way to show that. Consider the second and third clauses, we have:

old: ( \ceil(f) ∧ \ceil(g) ∧ \ceil(h) ) ∨ ( \ceil(f) ∧ \ceil(h) )

If we do some factoring, we find:

old: \ceil(f) ∧ \ceil(h) ∧ ( \ceil(g) ∨ \top )

Look at the last conjunct: \ceil(g) ∨ \top. This is just \top. In other words, this term completely subsumes the last two clauses:

old: \ceil(f) ∧ \ceil(h)

In the new output, we are going to do the same factoring trick:

new: ( \ceil(f) ∧ \ceil(g) ∧ \ceil(h) ) ∨ ( \ceil(f) ∧ \not \ceil(g) ∧ \ceil(h) )
new: \ceil(f) ∧ \ceil(h) ∧ ( \ceil(g) ∨ \not \ceil(g) )
new: \ceil(f) ∧ \ceil(h)

So, the output in either case is equivalent. The output changes because it isn't minimal, in the sense that we don't do this kind of simplification.

[dopamane]

Thank you, this is really helpful!

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-straight-line-no-invalid.sh	0.000048	0
test/regression-evm/test-straight-line.sh	0.000044	0
test/regression-evm/test-branching-no-invalid.sh	0.000045	0
test/regression-evm/test-add0.sh	0.000039	0
test/regression-evm/test-sum-to-n.sh	0.000066	0.001188
test/regression-evm/test-sumTo10.sh	0.000030	0.004032
test/regression-evm/test-pop1.sh	0.000038	0
test/regression-evm/test-branching-invalid.sh	0.000022	0
test/regression-wasm/test-loops.sh	0.000075	0.000054
test/regression-wasm/test-wrc20.sh	0.000044	0.013995
test/regression-wasm/test-locals.sh	0.000061	0.000040
test/regression-wasm/test-simple-arithmetic.sh	0.000072	-0.000190
test/regression-wasm/test-memory.sh	0.000081	-0.000014

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-straight-line-no-invalid.sh	0.000048	0
test/regression-evm/test-straight-line.sh	0.000044	0
test/regression-evm/test-branching-no-invalid.sh	0.000045	0
test/regression-evm/test-add0.sh	0.000039	0
test/regression-evm/test-sum-to-n.sh	0.000065	-0.000974
test/regression-evm/test-sumTo10.sh	0.000030	-0.001696
test/regression-evm/test-pop1.sh	0.000067	0
test/regression-evm/test-branching-invalid.sh	0.000042	0
test/regression-wasm/test-loops.sh	0.000103	0.000054
test/regression-wasm/test-wrc20.sh	0.000066	-0.000826
test/regression-wasm/test-locals.sh	0.000061	0.000040
test/regression-wasm/test-simple-arithmetic.sh	0.000079	-0.000188
test/regression-wasm/test-memory.sh	0.000089	-0.000014

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-straight-line-no-invalid.sh	0.000048	0
test/regression-evm/test-straight-line.sh	0.000044	0
test/regression-evm/test-branching-no-invalid.sh	0.000045	0
test/regression-evm/test-add0.sh	0.000021	0.000038
test/regression-evm/test-sum-to-n.sh	0.000066	0.000968
test/regression-evm/test-sumTo10.sh	0.000030	-0.000654
test/regression-evm/test-pop1.sh	0.000037	0
test/regression-evm/test-branching-invalid.sh	0.000049	0.000074
test/regression-wasm/test-loops.sh	0.000074	0.000147
test/regression-wasm/test-wrc20.sh	0.000046	0.008666
test/regression-wasm/test-locals.sh	0.000060	0.000041
test/regression-wasm/test-simple-arithmetic.sh	0.000072	-0.000190
test/regression-wasm/test-memory.sh	0.000083	0.000048