Refactor cterm_execute

[tothtamas28]

• Extract class CTermExecute to represent the return value
• Assert some properties on the RPC response and simplify logic

[ehildenb]

What is the purpose of this change?

cterm_execute currently loses a lot of information that the RPC call actually returns, re-inferring it based on things like the number of next states. If anything, we should be propagating more of that logic up, and dealing directly with the ExecuteResult that we already have:

pyk/src/pyk/kore/rpc.py

Line 502 in b5c15a2

class ExecuteResult(ABC): # noqa: B024

Part of the reason that we should deal with that result directly is because of changes like this, where we want to add more information to the returned response and be able to propagate that up to the KCFGExplore as well.

[tothtamas28]

What is the purpose of this change?

It's a clean-up:

1. Replaces a five-tuple return value by a class
2. Eliminates some unreachable branches and asserts the corresponding conditions (tested in evm-semantics and kontrol)

If anything, we should be propagating more of that logic up, and dealing directly with the ExecuteResult

I agree, the more complexity we can eliminate the better, we could replace the return type by a wrapper on ExecuteResult for example. But I don't see how this PR would prevent that, in fact I think we can be more confident in the correctness of such a change after this PR has been merged, as it replaces

if len(next_states) == 1 and len(next_states) < len(_next_states):
    return ...
elif len(next_states) == 1:
    if er.reason == StopReason.CUT_POINT_RULE:
        return ...
    else:
        next_states = []
return ...

by

return ...

[ehildenb]

Sounds good, thank you for the explanation!

[geo2a]

Great clean-up!