CFG visualization and progress saving

[ehildenb]

This PR is the simpler components pull out of #1443.

In particular, it has:

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

• Adds KEVM.add_invariant, and makes sure that the initial LHS states used for proofs are in the language invariant.
• The kevm foundry-prove command will now save the final counterexample state in the CFG on disk, so progress can be resumed from there.
• Adds kevm foundry-show OUT_DIR Contract.Test for displaying current CFG. Has options:
  • --[no-]minimize: minimize the configuration output.
  • --node NODE_ID: also display the selected node's configuration and constraints (respects --[no-]minimize, repetition allowed).
  • --node-delta NODE_ID_1,NODE_ID_2: display the configuration delta between the given nodes (respects --[no-]minimie, repetition allowed).
• Adds kevm foundry-list OUT_DIR for listing the current CFGs, and their progress towards being proved. Has options:
  • --[no-]details: show the details about progress to being proved for each CFG, instead of just their passed/failed state.

If you do something ilke kevm foundry-prove --depth 100 ..., the proof will fail at depth 100, and that state will be saved in the KCFG. Then you can continue progress from there with kevm foundry-prove ... again, and it will start from the 100th state the next time (you can add the --lemma argument the second call, for example). You can add the --reinit option to foundry-prove to start the proof over.

[ehildenb]

@lucasmt and @qian-hu if you could test that the new functionality (list, show, and proof resuming) are working as expected, taht would be good.

[qian-hu]

Proof resuming doesn't work well in my cases. When I run kevm foundry-prove the second time without adding --reinit, I'm getting a parsing error. The new claim file includes several unexpected _. But otherwise okay.

[ehildenb]

@qian-hu if everything else is working you should not press "Request Changes", because then I need to actually take some action to address your changes. See our GitHub Guidelines. As it is, you haven't actually given me anything actionable to do, I need to see the state that is not working for parsing, and ideally to see the entire input you are trying to run.

Also, it's a known issue that it cannot handle proof resuming from inside calls. I will be able to fix that too, but it will take me a couple weeks, it's not as straightforward as it sounds.

[lucasmt]

I've pushed a commit adding parenthesis when printing the up/Int operator, since it was causing a parser error when running kevm foundry-prove. Some constraints written to spec.k for the test I was trying to run contained expressions of the form #sizeByteArray(X) up/Int 32 *Int 32, and the parser considers them ambiguous without parentheses.

[lucasmt]

Now I am also getting the same error that @qian-hu mentioned when I try to run kevm foundry-prove the second time. For me the error looks like this:

[Error] Inner Parser: Parse error: unexpected token '_EXITCODE_CELL' following
token '_'.
	Source(/home/lucasmt/lsp-smart-contracts-verification/out/specs/erc725ytest-testsetdata1-spec.k)
	Location(40,19,40,33)
	40 |	               ( __EXITCODE_CELL => ?_EXIT_CODE_CELL_c89e25d9 )
	   .	                  ^~~~~~~~~~~~~~

It looks like there is an extra underscore being added to the variable names.

Everything else is working.

[qian-hu]

@ehildenb I see. Here is an example of the inputs and the error state. I do Kevm foundry-prove OUT_DIR --test Contract.Test --depth 100 --verbose after kevm foundry-kompile OUT_DIR --verbose, then run kevm foundry-prove OUT_DIR --test Contract.Test --verbose with/without --lemma argument. And I get a rewritten claim containing the following:

         <k>
           #halt
           ~> ( __CONTINUATION => ?_CONTINUATION )
         </k>
         <exit-code>
           ( __EXITCODE_CELL => ?_EXIT_CODE_CELL_c89e25d9 )
         </exit-code>

             <interimStates>
               ( __INTERIMSTATES_CELL => ?_INTERIMSTATES_CELL_c89e25d9 )
             </interimStates>
             <touchedAccounts>
               ( __TOUCHEDACCOUNTS_CELL => ?_TOUCHEDACCOUNTS_CELL_c89e25d9
             </touchedAccounts>

There are some unexpected token '_'. And the error is the same as @lucasmt provided.

New commit and everything else LGTM.

[tothtamas28]

Consider extracting definition_dir, use_dir, kcfg_dir, kcfg_file as functions of a new module config.py, e.g.

def kcfg_file(out_dir: Path, test_name: str) -> Path:
    return kcfg_dir(out_dir) / f'{test_name}.json'

[ehildenb]

You mean as helpers so we're not re-computing them over and again? Maybe they could be fields in the KEVM class so they're jsut set at function init?

[ehildenb]

I took a quick look at this, and seems like more trouble than it's worth at the moment. Will consider it in my local tree, see if I can find a solution.

[tothtamas28]

You mean as helpers so we're not re-computing them over and again

Re-computing the values is fine. The point is to have a single definition of these expressions so that e.g. the folder layout can be easily reconfigured.

[tothtamas28]

Let's create an issue to mark that there is duplicated functionality between kevm_pyk and ksummarize that eventually should be factored out.

[ehildenb]

I don't think this duplicated functionality will be long-lived. Plan to remove calls to sanitize_config once we have execute endpoint working (in my local branch, but not pushed up yet).

[ehildenb]

@qian-hu thanks for the more detail. I've added a test that this does not happen, and fixed this bug you found in the state saving.