Specifying behaviour with calls to unknown code

A common occurrence in smart contracts are calls to contracts with unknown code, whether for executing a simple eth payment, proxy/multisig actions or delegating control for a flash loan.

Such behaviour is naturally hard to specify, since the entire point is that these functions admit unspecified behaviour. Nevertheless, we want to be able to specify exactly what these functions do with respect to **the domain for which their behaviour is defined**, and express that beyond this domain, anything is allowed.

As an example, if we have a function with a flash loan, we have a clear expectation on the poststate of the contract itself, expressing that the loan need be paid back, while allowing any other part of the world state to change in ways we do not know.

Here's a suggested syntax for making such claims:
```act
behaviour flash of A
interface flash(address flasher, uint amount)

iff in range uint256

token.balanceOf[A] + flashFee

storage A.token
balanceOf[A] => balanceOf[A] + A.flashFee

storage _
_
```

the meaning being that a call to `A.flash(flasher, amount)` will increment the `A.token` balance of `A` by whatever the storage variable `flashFee` is set to, and that, for any contract that isn't `A` or `A.token`, **arbitrary changes to storage may occur**.

In other words, the syntax
```
storage _
_
```
would be shorthand for something along the lines for "for all addresses `X` that are not the main contract of the spec nor any of the other contracts mentioned to in the spec, the storage contents of `X` can change arbitrarily".

Before I get to how to prove claims like this, let me say some things about the syntax.

First of all, I think we need a more general keyword than `storage`, since nonces and balances may also change, new addresses can be created, and so on. `state` is an obvious candidate that was also brought up before. Can every instance of `storage` be changed into `state`? Should `storage` be a subheader of `state`?

If we continue with the EVM opcodes in CAPS idea, then maybe just generalizing `storage` to `state` and allow for references to BALANCE and NONCE under this header could be nice:
```
behaviour f of A
interface f()

state
x => x + 1
BALANCE => BALANCE + 1
```

Second of all, it needs to clarified what a "contract mentioned in the spec" means. Every contract with a `storage`/`state` header present? In the current syntax, we can actually read and refer to variables of other contracts without introducing a `storage` header for them. Should we allow storage writes to read-only contracts? I'm don't think so... Can this be made clearer in the syntax?

Lastly, I would like to make a note on proving strategies for these types of specs. This is a crude write up and I apologize if it's hard to follow, but I needed to get this down. Refinements can come later.

In order to determine which branches to explore, we first need to establish a functional dependency for all of the specs of all of the "contracts mentioned in the spec" for which behaviour is defined. A spec `S` is functionally dependent on all the specs which can write to the reads of `S`.

Now, when encountering a call to an unknown contract, we branch and explore:

- The case in which the external call does not enter any of the "contracts mentioned in the spec", and we simply carry on with exploring the rest of the function after the call.
- For every "contract mentioned in the spec" and any spec which can modify state, apply the spec and notice which storage items can change (the `changeset`). We now branch again into
- - the case where the external call is done and we are back in the main function with all the storage items in the `changeset` set to arbitrary values.
- - explore any of the specs again, now with any storage item in the `changeset` set to an arbitrary value. If more variables can change, add them to the `changeset` and repeat. If the `changeset` has not grown, we do not need to continue looping here.

The issue names no files, tests, or entry points. Start by reviewing the current Act syntax and handling of calls to unknown contracts, then define the state wildcard semantics, which contracts are in scope, and the proof-branching rules; done means the syntax and semantics are agreed clearly enough to implement and test.

Written by the indexing model from the issue text.