Contracts and storage layouts in CSE executions

[PetarMax]

All contracts relevant to a CSE execution need to be present in the storage explicitly, and their storage layout needs to be made explicit as well. Consider the (contrived, but representative) example from #356 of Double.applyOp:

contract Double is UIntUnaryOp {

    Identity iv;

    function applyOp(uint256 x) external view returns (uint256) {
        return iv.applyOp(x) + iv.applyOp(x);
    }
}

which holds an instance of an Identity contract in its storage and calls the applyOp function from it. There are two issues with the current generality of the CSE initial state:

1. The <accessedStorage> cell is fully symbolic, resulting in branching on whether or not various slots of various contracts have previously been accessed, together with an infinite branching similar to that reported in this KEVM issue due to the lack of full coverage of the <accessedStorage> update rules. This can be seen, for example, in nodes 4, 5, and 6, of the attached KCFG, which, respectively have the path conditions:

{ true #Equals ( notBool CONTRACT_ID:Int in_keys ( ACCESSEDSTORAGE_CELL:Map ) ) }

and

{ ACCESSEDSTORAGE_CELL:Map #Equals ( ( CONTRACT_ID:Int |-> TS:Set ) _DotVar7:Map ) }

and

{ true #Equals CONTRACT_ID:Int in_keys ( ACCESSEDSTORAGE_CELL:Map ) }
#And #Not ( #Exists _DotVar7:Map . #Exists TS:Set . ( { false #Equals CONTRACT_ID:Int in_keys ( _DotVar7:Map ) }
#And { ACCESSEDSTORAGE_CELL:Map #Equals ( ( CONTRACT_ID:Int |-> TS:Set )
_DotVar7:Map ) } ) )

2. The storage is fully symbolic, meaning that the knowledge that iv is an Identity contract is lost, and the execution cannot figure out which function corresponds to applyOp.

The KCFG can be obtained by running

kontrol build --require src/cse/lemmas.k --module-import CSETest:CSE-LEMMAS --verbose --regen --rekompile
kontrol prove --verbose --match-test 'Double.applyOp'

from the src/tests/integration/test-data/foundry folder of Kontrol using the petar/cse-exploration branch of PR #355.

Double.applyOp.txt