[kompile|kprovex] Simplify rules ahead of time

[ehildenb]

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.

[radumereuta]

Please investigate if the haskell backend can do this simplification with a tool that we can call from kompile.

[ana-pantilie]

The backend already simplifies the LHS of rewrite rules and equations at start-up. We could move this to kompile inside the kore-kompile tool described above, and measure the performance outcome. I would say this is a small task, because the functionality already exists and only needs to be moved to a separate tool. After that, we can try doing other simplification as well.