Incremental exploration based kprove using rpc endpoints

[ehildenb]

Blocked on: #1447
Blocked on: #1440
Blocked on: runtimeverification/pyk#100
Blocked on: #1458
Blocked on: runtimeverification/pyk#112
Blocked on: #1462
Blocked on: runtimeverification/pyk#118
Blocked on: #1476
Blocked on: runtimeverification/haskell-backend#3386
Blocked on: runtimeverification/k#3059
Blocked on: #1484
Blocked on: #1478
Blocked on: #1480

This brings in a decent amount of functionality needed for making progress incremental on Foundry proofs:

• Adds KEVM.{is_terminal,extract_branches}, which help with auto-exploration.
• Adds auto-exploration strategy based prover, which stores branch points for inspection (as opposed to using direct calls to kprove).
  • Use option --max-iterations to limit how many calls to prover to make while exploring.
  • Use option --max-depth to limit how long each exploration step will let the prover run.
  • Use option --no-simplify-init to turn of simplification of the initial state (up to 2 minutes at proof startup, does not need to be repeated on subsequent runs).

Doing something like kevm foundry-prove --test MyContract.MyTest --max-depth 100 will make sure that every 100'th step is saved in the KCFG. That way you can save progress in case the prover crashes, and you can resume exploration from a later state with more lemmas in context.

[ehildenb]

As an example of using this functionality, I do:

kevm foundry-kompile tests/foundry/out --verbose

Then I can run the proof I want, with --max-iterations 1 (and default --max-depth 250), and then I display the resulting CFG:

kevm foundry-prove tests/foundry/out --test UintTypeTest.test_uint8 --max-depth 250 --verbose --max-iterations 1
kevm foundry-show-cfg tests/foundry/out UintTypeTest.test_uint8

And I get something like this:

I want to inspect the node f6f72d..8384b2, which is 250 steps after the initial node, so I run:

kevm foundry-show-cfg tests/foundry/out UintTypeTest.test_uint8 --node f6f72d..8384b2

And I get this (highly truncated) output:

Now I want to continue exploration, without any depth bound, so I simple call foundry-prove again, but without the --max-iterations argument. Any additional --lemma argument I add will be used from this point on, but not to simplify original executions:

kevm foundry-prove tests/foundry/out --test UintTypeTest.test_uint8 --max-depth 250 --verbose

This leads to the following CFG eventually (has explored 2 times, then gotten stuck, cannot make progress, proof not passing):

After playing with the CFG a bit, and exploring more of the behaviors, I decide it's time to start the exploration over, so I add eth --reinit command to foundry-prove, which brings us back to the initial proof state (just init and target states present):

kevm foundry-prove tests/foundry/out --test UintTypeTest.test_uint8 --max-depth 250 --verbose --reinit

[ehildenb]

Subsumed by: #1538