Introduce RPC based prover to kevm

[ehildenb]

Blocked on: #1527
Blocked on: runtimeverification/pyk#173
Blocked on: #1544
Blocked on: #1560

This PR makes several steps to making RPC based proving possible with KEVM:

• Names the various CALL* rules so that they can be broken on.
• Makes use of new upstreamed RPC based prover in all pyk-based prover (including kevm prove ... --pyk and kevm foundry-prove ...). These come with several options for controlling execution/KCFG construction:
  • --max-iterations: maximum number of times to expand the KCFG created between initial and target states in an attempt to show all-path reachability.
  • --max-depth: maximum K steps to take for each leg of symbolic execution when expanding the KCFG from the initial state to the target state.
  • --[no-]implication-every-block: check implication every time that a state is returned from symbolic execution (or not).
  • --break-on-calls: save the pre-state every time there is a contract call, from right before the call.
  • --break-every-step: save a state every opcode that is executed.
• Adds command kevm foundry-remove-node ... which allows remove nodes (and successors) from a KCFG so you can restart from a prior state with lemmas added, for example.
• Adds command kevm foundry-simplify-node ... [--replace] which allows calling the simplification routine on a given node and printing the results, and optionally also replacing the given node in eth KCFG.
• Adds command kevm view-kcfg --definition path/to/kompiled path/to/kcfg-file.json, for viewing KCFGS produced with kevm prove .... --pyk --save-directory path/to.
• Enables the --pyk option for as many haskell proofs as possible on CI, lists the ones failing with pyk in tests/failing-symbolic.pyk.
• Increases the parallelism for both Haskell and Foundry proofs on CI due to lower overhead of RPC based proving.
• Disables two foundry tests that actually were being vacuously proved by reaching #Bottom.
• Corrects the way that logging levels are handled.
• Passes in the KEVM.short_info as a pretty-printer for the KCFG behavior view, and for viewing KCFGs in foundry-kcfg-show.

Note that CI time is reduced to ~35 minutes for Haskell backend proofs, and just over an hour for Foundry proofs (down from 3.5-4 hours!).