Exploit the opaque modifier

[DavePearce]

This modifier can be used to improve stability, as discussed in the paper "Improving the Stability of Type Safety Proofs in Dafny". Challenges:

1. Decide which functions should be marked opaque and which should not.
2. Generally want potentially expensive functions to be marked opaque.
3. Need to play around with being able to reveal them.

A good class of functions which could be revealed separately would be those related to gas. These are not needed for the majority of verification tasks. Otherwise, might include things like memory expansion and/or precompiles?

[DavePearce]

Observe we currently have the following functions already marked as opaque:

function {:opaque} Call(address: u160, data: Array<u8>) : Option<(Array<u8>,nat)> 

function {:opaque} Sha3(data: Array<u8>) : u256

opaque function Copy<T>(src: seq<T>, dst: seq<T>, start: nat) : (result:seq<T>)

In particular, the last one is significant I think.