Add support for views

[annenkov]

The view functionality allows for querying contracts in a synchronous way. This functionality makes it easier to implement contracts that require using some data from other contracts, for example, getting data from oracles. With only message passing, it could be implemented with callbacks. This is, however, awkward and error-prone.

The view mechanism guarantees that the state will not be changed, that's why it should be relatively unproblematic to add to ConCert: the execution model stays the same, we just need to add some additional data available to contracts during the receive function call.

We can extend ConCert to handle views:

• Add view function(s) to the Contract; it could be done by using a single function that dispatches on a special "view message" (however, the return type still might be different for different views).

• Pass around the extended state. Currently, the blockchain state available to the contracts (part of the contract's signature):

Record Chain :=
 build_chain {
   chain_height : nat;
   current_slot : nat;
   finalized_height : nat;
 }.

It could be extended with a field containing the whole Environment, or some restriction of it. In this case, one could access the contract's view functions (and, maybe, state?). Possibly, some of the infrastructure from the implementations of the execution layer can be used [LocalBlockchain](https://github.com/AU-COBRA/ConCert/blob/0399316dbc882e228e5e0c0daf98b51460dc760a/execution/theories/LocalBlockchain.v#L39]

• Introduce a view_call function that will fetch a view and, if it was successfully fetched, call it.