Booster not detecting that branching condition is implied by existing side condition

[lucasmt]

@qian-hu and I are having another issue when using the booster that is causing the execution to branch when it shouldn't. I have created an evm-semantics branch here with a simple test that reproduces the problem:

contract MyContract {
    uint256 public value;
}

contract ArrayTest is Test, KEVMCheats {
    function testArrayInitialization() public {
        kevm.infiniteGas();

        MyContract myContract = new MyContract();
        kevm.symbolicStorage(address(myContract));

        vm.assume(myContract.value() == 3);

        bytes32[] memory array = new bytes32[](2 ** myContract.value());

        assertEq(array.length, 8);
    }
}

This test can be run with no additional lemmas by running the reproduce1.sh script. The result is an execution that branches on the following condition:

chop ( 1 <<Int #lookup ( STORAGE:Map , 0 ) ) <=Int maxUInt64

Here, #lookup ( STORAGE:Map , 0 ) corresponds to the storage variable value, so this condition essentially translates to 2 ** value <= type(uint64).max. This happens because of the new bytes32[](2 ** myContract.value()) line, since Solidity requires that the length of an array must fit in a 64-bit integer.

The problem is that, since we have the line vm.assume(myContract.value() == 3), the configuration includes the side condition #lookup ( STORAGE:Map , 0 ) ==Int 3, which implies the branching condition above. This can be confirmed by running the run-claim.sh script, which runs a claim proving this implication. So I don't think we should be getting a branch on this condition in the first place, since the SMT solver should be able to tell that it's always true.

Additionally, if we try to simplify this expression down to a constant by adding the lemma

    rule #lookup ( STORAGE , I ) => 3
        requires #lookup ( STORAGE , I ) ==Int 3
        [simplification]

the call to kevm foundry-prove seems to hang in the simplify step for the initial node. This can be reproduced by running the reproduce2.sh script. I'm not sure why this happens either.

Finally, if we instead add the lemma

    rule 1 <<Int X => 1 <<Int 3
        requires X ==Int 3
        [simplification]

then the proof passes (this can be reproduced by running the reproduce3.sh script). However, this is less than ideal, because it means that we need to add a specific lemma for every expression where this happens (for example, we are getting a similar problem with an expression of the form 32 *Int #lookup ( STORAGE , I )).

Here are bug reports corresponding respectively to the execution of reproduce1.sh and reproduce2.sh: bug_report1.zip bug_report2.zip

[ehildenb]

@lucasmt is this problem solved if you add --simplify-after-execute flag to the booster invocation? If so, maybe we should make that option default. https://github.com/runtimeverification/hs-backend-booster/pull/249

[goodlyrottenapple]

@ehildenb the reproduce1.sh script uses this flag, so I don't think this solves the issue

[ehildenb]

How about with a lemma rule X ==Int Y => { X #Equals Y } [simplification], and that flag?

[ehildenb]

The old backend should be able to simplify this one, because it treats equalities as substitutions.

[geo2a]

While trying out different options of applying old backend's simplifications within kore-rpc-booster, I've discovered that adding the lemma:

    rule B ==Bool true => B [simplification]

makes the proof pass with the current kore-rpc-booster even without --simplify-after-exec.

It seems that the backend cannot figure out this system of constraints:

{ #lookup ( ?STORAGE:Map , 0 ) <=Int maxUInt8 #Equals true }
{ 3 ==Int #lookup ( ?STORAGE:Map , 0 ) ==Bool true #Equals true }

and branches, no matter if I simplify the state with the old-backend or not. Introducing the lemma above strips the ==Bool true bit.

I've pushed reproduce4.sh which produces a passing proof with the current kore-rpc-booster from main.

BTW, it seems like @PetarMax has already come up with a body of Bool-related lemmas that includes the one above. We should upstream them to evm-semantics.

[lucasmt]

We are no longer having this problem, so I believe the lemmas that @PetarMax added are working. As @geo2a said, we should make sure that these lemmas are upstreamed into evm-semantics.

[palinatolmach]

@PetarMax could you please confirm if the lemmas proposed here https://github.com/runtimeverification/evm-semantics/pull/2037 fix this issue? Do you think we can close this task?

[PetarMax]

I can confirm that this issue is no longer happening, both due to the lemmas (which are currently only in the engagement repo but will be upstreamed soon) and to the changes made to the booster backend.