Implement kevm.forgetBranch cheatcode

[anvacaru]

blocked on: #903
blocked on: runtimeverification/kontrol-cheatcodes#15
blocked on: runtimeverification/evm-semantics#2662
blocked on: runtimeverification/k#4700

Changes in this PR:

• a new cheatcode forgetBranch(uint256,uint8,uint256):
  • when called, should remove a constraint from the set of path constraints.
  • It puts a #forget Int Int Int production at the top of the K Cell. The #forget rule is set as a cut-rule.
• Creating a new class, FOUNDRYSemantics(KEVMSemantics), that is inheriting the KEVMSemantics.
• Two new functions are added to FOUNDRYSemantics:
  • _check_forget_pattern(self, cterm: CTerm) -> bool: checks if the forget cut-rule is at the top of the K Cell
  • _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult:
    1. reads the values from the #forget K production and reconstructs the constraint.
    2. It simplifies the constraint using the CTermSymbolic.simplify endpoint and a CTerm created from an empty configuration.
    3. If the simplified constraint is part of the current path constraints, it gets removed, and a new Step is returned; otherwise, None is returned.
• overwrites can_make_custom_step and custom_step to check and run the forget pattern.

Usage example:

function test_forgetBranch(uint256 x) public {
    uint256 y;

    vm.assume(x > 200);
    kevm.forgetBranch(x, KontrolCheatsBase.ComparisonOperator.GreaterThan, 200);
    if(x > 200){
        y = 21;
    } else {
        y = 42;
    }
}

[ehildenb]

I think this should be implemented as a custom kontrol forget-constraint ... command, or kontrol abstract-constraint ... command, not as a cheatcode. I think as a cheatcode, teh workflow for the verification engineers is worse actually, because tehy will have to

• Run the test the first time, and see that there is a branch they want to forget.
• Modify the code to insert the correc branch forgetting. This requires the rather clunky feeling system of "kinda specifying the condition to forget".
• Rebuild, and rerun the entire proof from the beginning. You don't know if your cheatcode implementation worked until ti reaches the same point it reached before, and if it does not work (you got the condition wrong), you start over completely.

As a separate custom command, it's instead looks like:

• Run the test the first time, and see that there is a branch to forget.
• Prune the KCFG after the branching points (very fast).
• Run the command to remove the constraints you care about, passing in exactly the unparsed text of the constraints you want ot remove (fast and precise, no guessing).
• Inspect the KCFG to see that it's what you want.
• Resume the proof from taht point.

In the second approach, iterating on removing the desired constraints is a very tight loop of commands that never even need to load a haskell backend up (inspecting kcfg, pruning nodes, and forgetting constraints), and you can resume the proof directly from the spot that you left off, instead of returning all the way to the beginning to even see if your change worked.

[Stevengre]

I think we can have both. Custom command is a debugging method with quick response, cheatcode is a fixed proof for CI?

[PetarMax]

After having read through, I think we should definitely have both, because the separate custom command allows for quick debugging and then the Solidity-level forgetting allows for a continuous proof.

[PetarMax]

Here are my thoughts, starting from:

• branch forgetting is an advanced technique that should be used only if there is no other recourse

From the point of understanding and debugging whether or not removing or abstracting a constraint will work, I 100% agree with @ehildenb that we should have a separate kontrol _______ command.

From the point of understanding what are the constraints that can be removed, those are all already present and clearly visible in the Solidity code, and using a cheatcode to remove them would ideally be straightforward. However, there are two snags:

1. The less complicated one, in which the test does not have immediate access to the parts of the state on which the branching is happening. This one is handled by writing auxiliary functions that get to that part of the state and then using that information in the test. In the test that I needed it for, all of these functions except one were already in place, as reasoning about those parts of the state was needed by the test setup.
2. The much more complicated one, caused by the backend simplifications, which will simplify any constraint that is part of the path constraints to true. This means, for example, that if a branching on a < b occurred and if we try to pass a < b directly to the forgetBranch cheatcode, the condition will be wrapped into a bool2Word, and will simplify to true. To the best of my knowledge, there is no way to either not wrap the condition into a bool2Word as all data is Word or disallow backend simplification at this specific point. This is why we have the unfortunate and truly UX-unpleasant forgetBranch(LHS, OP, RHS). Perhaps we could have two forgetBranch functions, one with just the condition and the other with it separated, and then do a pre-processing pass on the Solidity code that would transform the former into the latter.

When it comes to custom_step using simplify, I see custom_step is a free-for-all that takes us out of executing the semantics into Python, where we might as well use whatever is available to us. Having said that, it is much more complicated than the other custom steps that we've had so far.

[lucasmt]

The cheatcode seems to be working on our tests, so I'm approving this and we can revisit it later to revise the implementation/add a command-line version.