CSE: Symbolic storage

In compositional symbolic execution, the storage of all of the involved contracts should be symbolic enough so that the generated claims are general enough, while also being structured enough so that the execution does not branch infeasibly. The non-exhaustive list of challenges, based by the type of data in storage, is as follows, in order of priority:

• Value types (bool, int, uint)
  • Structure: We can either choose to not make any structural changes, or put the values in storage explicitly. The former means that we will be reasoning on more complex terms (#lookup(STORAGE, SLOT)). The latter means the we might not catch cases in which the values have not been initialised, due to the partiality of K maps.
  • Values: The values should be appropriately bounded. This information should exist in the storage layout provided by the compiler. For example,, if a bool is stored in slot SLOT, we should have #rangeBool(#lookup(STORAGE, SLOT)), etc.
• Contracts: For any contract in storage of the executing contract, we should create a corresponding account with the appropriate bytecode and recursively format its storage as well. For the first version, we should assume non-aliasing.
• Mappings: Mappings with value types in their co-domain should not require structural changes. The reasoning, however, will require bringing back the unsound-in-principle-but-necessary keccak-related lemmas. Mappings with more complex types in their co-domain could be difficult to handle symbolically since we only know the inspected elements at runtime and it is not possible at the moment to have a sufficiently general rule that would infer additional structure.
• Strings and bytes: These have a length-dependent representation as described here.
• Dynamic arrays: As per the documentation, dynamic arrays should be easier to handle than mappings since their layout in storage appears to be contiguous.
• Interfaces: This cannot be handled in general given its higher-order nature, but can be handled for specific contracts satisfying the interface using the approach for contracts.