Abstracted storage representation for Solidity smart contracts

An idea from @geo2a about having our storage representation change to allow for more abstract reasoning at the level of solidity data structures. Other tools (like Halmos) do this, which costs generality in terms of handling arbitrary EVM bytecode, but gains in speed/efficiency.

• Change the <storage> cell in KEVM to be of new type Storage, which is super-sort of Map. Change #lookup to handle this as input and add a new #write which writes it (and adjust all lemmas to be over these new constructs). Was attempted:
  • https://github.com/runtimeverification/evm-semantics/pull/1549
  • https://github.com/runtimeverification/evm-semantics/pull/1550
  • https://github.com/runtimeverification/evm-semantics/pull/1598
• In Kontrol, extnend the Storage sort with new SolidityStorage subsort, which accomodates Solidity contract fields. The field names can be the first keys in the overall map, and the second keys can be mapping indices, or struct member names, etc...
• In Kontrol, where we generate storage-layout lemmas, instead generate ones that go the "other direction". Basically, they should look at storage reads/writes (SSTORE and SLOAD), and "reverse" the keccak expressions being passed into them to find their high-level Solidity counterparts. These reversing rules can be generated automatically in the same way we generate the sugar rules now (which are not used), by just reversing the rules we generate.

This will provide:

• Better looking storage layouts by default, easier to map back to Solidity storage values.
• Perhaps simpler reasoning than having these massive keccak expressions that are passed around a bunch? This may also simplify and speed up the backend.

Start by reviewing the attempted changes in PRs #1549, #1550, and #1598, then trace the KEVM cell, #lookup, and the proposed #write constructs. Next, inspect Kontrol's storage-layout lemma generation around SLOAD and SSTORE. Done means the KEVM storage abstraction, SolidityStorage representation, and generated reverse storage-layout rules work together and improve storage reasoning as described.