Address casting

[zoep]

This PR introduces the ability to cast addresses to contracts. Below are the key components of the new feature:

1. The specification language is extended with a new block, called pointers for constructor and behaviours. This block allows assumptions about variables of address type pointing to specific contract types. For example:

constructor of C
interface constructor(address x, address y)

pointers
  x |-> A
  y |-> B

Here, the variable x is assumed to be an address pointing to a contract of type A, and an address pointing to a contract of type B. Subsequently, in the rest of the specification, x and y can be treated as contracts of types A and B, respectively.

3. The internal Act contract type is removed, contracts are internally treated as integers. The representation is the same as address type.

4. Field selector and mapping syntax is now available for input variables, not just state variables. This allows for handling calldata variables that are addresses pointing to contracts as contracts.

5. Handling of state and calldata variables in the AST is unified. A phantom type is added to differentiate between calldata and storage entries. The downside of this is that it requires adding a singleton type which adds complexity. However, this approach allows us to avoid duplicate code while still enforcing that only storage variables are used in specific AST nodes (e.g., storage updates).

6. The translation to hevm's Expr is modified so that it creates an initial contract state that has all contracts that are assume to be alive when a constructor is called.

   • The initial contract state consists of the contract state of each contract in the points to block. This requires recursively creating the initial contract state of each one of these contracts and adding their state to the contract state.
   • Every time we add a new contract address to the state we have to check this it is not aliased with the addresses that are already present in the state. This restriction simplifies implementation as, otherwise, we would have to construct exponentially many contract states, to account for all possible aliasing cases. Given the rarity of address aliasing in smart contracts, this limitation is expected to have minimal practical impact

7. After each constructor or behavior state transition, a check ensures that the post-transition contract state is isomorphic to the pre-transition state. This ensures that the contract state shape is invariant in the contract. Without this invariant, equivalence would need to account for every potential contract state shape, which would increase computational complexity.

8. Several tests that involve casting are added.