Tracking MX project performance fixes

[Baltoli]

@jberthold and @virgil-serbanuta are working on optimizing symbolic execution of the MX- family of projects. Part of this work will entail making changes at the K level to improve performance. We'd ideally like to learn from this process and perhaps write up some guides on writing K code that performs well from the get-go.

Please log any MX PRs that are in aid of improved performance here:

[jberthold]

runtimeverification/kasmer-multiversx#108 addresses a problem with variable subsorting:
When a rule with variable A:SortA is matched against a configuration that has a variable B:SortB and SortA < SortB, the match will be conditional/indeterminate (causing an abort in booster, and matching with further rules/branching in kore-rpc).
This is the correct behaviour, but in this particular case, the variable B was only introduced temporarily (programmatically in the python client code) to temporarily abstract unnecessary payload. It is easy to make this mistake of picking too general a sort when abstracting. pyk will insert the required injections SortA -> SortB automatically so the fix was easy.

[jberthold]

Some book-keeping of past PRs related to mx-backend performance:

• Make numberCvtOp total wasm-semantics#631:
  Refactoring to make a function on the RHS of a rewrite rule total (booster aborts if a RHS contains partial functions unless the rule is marked as preserves-definedness)
• Add dummy state for newWasmInstance cut point rule mx-semantics#262:
  Execution is interrupted at the newWasmInstance rule to compute this new WASM instance externally (using LLVM from the python client). However, when marking a rule as a cut-point-rule, the following next state (RHS of the rule) will still be computed and returned. The PR introduced an intermediate execution state that requires no computation to avoid the duplicate computation.
• Mark #distinctBits as "no-evaluators" wasm-semantics#632 and Mark a number of rules as preserving definedness mx-semantics#263:
  Run-off-the-mill PRs to mark rules as preserving definedness (avoiding fallbacks) and a fully-symbolic function as no-evaluators to avoid LLVM errors (which may also cause fallbacks but mainly warning messages).

[jberthold]

Recent PRs

• Fix fallback on bigIntSign mx-semantics#289
  Refactors a rule that included a two-stage match in Map fields (paraphrased: <a> K |-> K2 ...</a> <b> K2 |-> V ... </b>) to avoid a natch abort.
• Definedness improvements wasm-semantics#651 and mark signed load instruction as preserving wasm-semantics#654
  Mark a few rules as preserves-definedness (including justification for the added attributes in comments)
• Use two rules for 'select' to avoid if-then-else on valstack wasm-semantics#655
  Avoid pushing an unevaluated #if B #then exp1 #else exp2 #fi into a configuration cell, by forcing the decision depending on B (Caveat: This modifies the branching structure and may duplicate work so it might not always be better!)

[jberthold]

• Hotfix ListBytes:getOrDefault with List:get mx-semantics#313
  Uses built-in list indexing, instead of matching on the list structure, for a getOrDefault function on custom lists
• Mark updateSparseBytes(setRange) as preserving definedness, add #signed simplification kasmer-multiversx#176
  Adds a simplification for custom functions (partial), and marks another that uses replaceAtBytes as preserving definedness

Summary of obtained speedups in this issue comment