Closed jberthold closed 1 week ago
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.
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.
Using mx-backend from PR https://github.com/runtimeverification/kasmer-multiversx/pull/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 | new select rule |
...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.
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.
How does this affect overall performance on some real-world proofs? Not just fallback number, but overall time consumed?
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.
Go ahead and merge then!
The rule for
select
was previously pushing (potentially unevaluated)#if..#then..#else
expressions on thevalstack
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 inint-encoding
).