Use two rules for 'select' to avoid if-then-else on valstack

[jberthold]

The rule for select was previously pushing (potentially unevaluated) #if..#then..#else expressions on the valstack which may later cause fall-backs due to indeterminate matching of operations with the arguments (operations would typically expect a fixed number type, which is hidden under the #if).
This change splits the logic for #select into two rules , forcing the rewrite to decide which branch to take (or whether to explore both) already when executing the #select.

Requires the linked companion PR in mx-backend to avoid a spurious second branch (adding some simplifications in int-encoding).

[ehildenb]

Use two rules will likely result in state splitting, which will probably make performance worse.

What might improve things is to make a specific select_if(Int, Int, Int) -> Int function, which does the selection but is total/type-checked/not-polymorphic, to preserve definedness.

That, or just marking the rule as preserving definedness?

Either way, then we need to axiomatize it, with axioms like:

rule X <Int select_if(_, Y, Z) => true requires X <Int Y andBool X <Int Z [simplification]
rule X <Int select_if(C, Y, Z) => true requires (C impliesBool X <Int Y) andBool (notBool C impliesBool X <Int Z) [simplification]

For example.

[jberthold]

Use two rules will likely result in state splitting, which will probably make performance worse.

The split happens either way, but it is correct that the shape of the graph changes (we move the split).
The problem is that a later BinOp instruction is trying to match its two arguments on the valstack, and cannot match the #if P(VarX) #then <TYPE> a #else <TYPE> b #fi with a simple <T'> VarY (paraphrasing here... I can retrieve the exact matching problem if required). That instruction will fall back to kore-rpc because of the failing match.

I tried to float the <TYPE> _ part to the outside but that creates other problems due to some overloading in the semantics (don't remember the exact details any more).

What might improve things is to make a specific select_if(Int, Int, Int) -> Int function, which does the selection but is total/type-checked/not-polymorphic, to preserve definedness.

That, or just marking the rule as preserving definedness?

Either way, then we need to axiomatize it, with axioms like:

rule X <Int select_if(_, Y, Z) => true requires X <Int Y andBool X <Int Z [simplification]
rule X <Int select_if(C, Y, Z) => true requires (C impliesBool X <Int Y) andBool (notBool C impliesBool X <Int Z) [simplification]

Happy to try the approach of replacing #if by a custom select_if and adding targeted simplifications for all the operations we need - but this fall-back occurs more than 100 times in the 5 proofs we use in the analysis, so there might be many simplifications required.

FWIW my tests of this change in mx-backend (with additional simplifications) do not show any substantial slowdown in any of the proofs.

[jberthold]

Using mx-backend from PR runtimeverification/kasmer-multiversx#158 together with this change, the following fall-backs were observed in the suite of proofs (excluding coindrip):

Rule	Reason	Count	ID
MANBUFOPS.getBuffer	constraint	57	rewrite 1534054
...source/wasm-semantics/wasm.md : (457, 10)	constraint	57	rewrite 4d4d997
...source/wasm-semantics/wasm.md : (517, 10)	constraint	29	rewrite 5d0f59f
KASMER.kasmerAssume-true	constraint	18	rewrite 1806d64
BASEOPS.executeOnDestContextWithTypedArgs	match	10	rewrite 3c7633d
...source/mx-semantics/elrond-config.md : (187, 10)	constraint	10	rewrite 4eb1a24
...mx-semantics/vmhooks/manBufOps.md : (230, 10)	constraint	9	rewrite 26f0e15
...mx-semantics/vmhooks/baseOps.md : (435, 10)	match	6	rewrite 1d98dd2
...source/wasm-semantics/wasm.md : (510, 10)	match	4	rewrite 75b1dcd
ESDT.determineIsSCCallAfter-call	constraint	4	rewrite 79fbf18
KASMER.kasmerWriteToStorage-empty	constraint	3	rewrite 29cae46
ESDT.checkAllowedToExecute-pass	match	3	rewrite ecb18e3
ELROND-NODE.checkBool-f	constraint	2	rewrite e9c0a69
...mx-semantics/vmhooks/baseOps.md : (417, 10)	match	1	rewrite 55f27ce
...source/mx-semantics/elrond-config.md : (306, 10)	constraint	1	rewrite 746198e
ELROND-CONFIG.memLoad-zero-length	constraint	1	rewrite b0db328
...mx-semantics/vmhooks/baseOps.md : (406, 9)	match	1	rewrite c21cd6e

Most of these fallbacks are now due to constraint uncertainty, e.g. potential branching on rule conditions. One of the main reasons is the new select rule (...source/wasm-semantics/wasm.md : (457, 10) ) - which is not a surprise if the fallbacks in question are indeed true branches.

[ehildenb]

I'm still really skeptical of this change. If we have a split earlier in the execution, that will double the amount of work we need to do to get from where the split is made now (right at select) to where it was made later (at teh point where the reasoning was needed). It's always better to split later when possible! In KEVM and Kontrol, for example, we're trying to even merge nodes back together, to reduce how many nodes we have on the frontier.

[ehildenb]

How does this affect overall performance on some real-world proofs? Not just fallback number, but overall time consumed?

[jberthold]

How does this affect overall performance on some real-world proofs? Not just fallback number, but overall time consumed?

The best comparison measurements I have are from recent Burak's PRs (merged last week), the master measurements included here are older.

Test	2024 06 18 masters	Burak's PRs (merged)	tweaked select
add_liquidity	15308	14586	14380
all_tokens_claimed	killed after 36h	./.	./.
call_add	135	126	124
call_add_twice	221	204	202
change_quorum	2640	2304	2318
fund	204	184	182
swap	6537	6411	6194

Short proofs did not speed utp significantly, the biggest improvement is in the swap proof, slightly smaller improvement in add_liquidity.
The map removal/simplification PRs will probably have higher impact than this, but it is an improvement.

[ehildenb]

Go ahead and merge then!