[kompile|kprovex] Simplify rules ahead of time

Start with the kompile and kprovex paths described in the issue, and inspect tests/specs/mcd/bin_runtime.k along with the linked bytecode example. Compare the initial simplification behavior and evaluate the proposed LLVM-at-kompile-time and kore-kompile approaches. Done means safely simplifying large concrete expressions ahead of proof execution with measured performance improvement.

In KEVM proofs over large bytecodes, the backend spends quite a bit of time on the initial simplification of the configuration, in particular in parsing the input bytecode and calling #computeValidJumpDests.

          <program>   #binRuntime(Vat)                         </program>
          <jumpDests> #computeValidJumpDests(#binRuntime(Vat)) </jumpDests>

Once this simplification happens, it seems that the large concrete set/byte-array stored don't have as significant algorithmic overhead, just the initial simplification (no hard data backing up this observation). I changed the bytecode from the original, to just the bytecode "0x60" instead, and running kompile && kprovex --depth 0 dropped from 276s to 199s. So roughly 75s to simplify the big concrete set, and we have 72/113 KEVM proofs running in under 600s (so 10% speedup on all those), and 15/113 KEVM proofs running in under 180s (so 33% speedup on all those).

These are included in the kompiled definition, so this simplification to the actual large concrete sets could even happen as early as kompile time. If it happened at kompile time, it's more acceptable for it to take a while, because it only needs to happen once. There are two approaches I could see for this to happen at kompile time:

• Kompile an LLVM backend at komplie-time as well, and store it in a subdirectory. Use it to evaluate specific concrete expressions in the definition. This is probably faster, except for having to build two backends (Haskell and LLVM).
• Haskell backend exposes a kore-kompile command, which takes a kore definition and applies as many safe simplifications as possible to the definition ahead of time. This approach probably will yield more simplifications ultimately, because the Haskell backend can be much more aggressive about partially evaluating things. The backend could basically just try to simplify the RHS of as many rules as possible, and could even do functional case-splitting if directed to (maybe an attribute on the function symbol? something to consider later). It could tune the simplification over time to produce definitions more suited to its own symbolic execution.