Handle CTerm bottom and top gracefully

[iFrostizz]

closes runtimeverification/kontrol#22
closes #13

We now check when instantiating a CTerm from_kast if the pattern is bottom or top and shortcut from the split early to return either a CTermBottom or a CTermTop.

[iFrostizz]

Actually shouldn't we also do the check in the __init__() ? I was scared that it would duplicate code

[ehildenb]

This looks good, but we should adjust the various methods in KCFGExplore to also handle the new cases correctly. I think in particular, KCFGExplore.cterm_simplify should return a CTerm now, not a KInner:

pyk/src/pyk/kcfg/explore.py

Line 104 in c292c46

def cterm_simplify(self, cterm: CTerm) -> tuple[KInner, tuple[LogEntry, ...]]:

[ehildenb]

Also, we should possibly remove these failure cases?

pyk/src/pyk/kcfg/explore.py

Line 273 in c292c46

if is_top(new_term):

[ehildenb]

Also, we should probably have KProve.prove return a list[CTerm] as well now.

pyk/src/pyk/ktool/kprove.py

Line 185 in c292c46

def prove(

(and prove_claim perhaps?), and prove_cterm

So for example, prove returns a KInner, which could be a #Or(...) of a bunch of states. So you could return:

return [CTerm.from_kast(disjunct) for disjunct in flatten_label('#Or', final_state)]

[ehildenb]

This is also a big change, so you need to check that it will work with KEVM locally:

• Make a new branch of KEVM, link it to this branch of pyk.
• Try running the proof that was triggering the original bug with this branch of pyk.
• Add any fixes needed to KEVM to make it work with this branch.
• Link to that new branch here.

[iFrostizz]

Trying to run the problematic code on this branch !

[ehildenb]

Looks great, thank you for the clean focused change! Once you have confirmed that this will work with KEVM, fele free to add automerge.

[iFrostizz]

@ehildenb I had to move away from the inheritance CTerm type matching because it wasn't playing well with instantiating the CTerm using the __init__ function. Also added a try_cell because top and bottom CTerm don't have those, so the interfacing code can just try to fetch the cell if it's not None. And it's now fixed on kevm! Asking again for review please

[iFrostizz]

runtimeverification/evm-semantics@master...kevm-graceful-res#diff-8ef99db40b2010c0b478f54603fda2b277c332347b8945df0e83bb686a6eafc1

As a bottom or top node does not have any cell, in the kcfg it looks like so: