Prove invariants with ensures

[MrChico]

When it comes to ensuring global properties of the system, we can by induction prove global "accounting invariants" using the ensures clause and requires clauses. I imagine a procedure that goes as follows:

For each contract, we make a spec with completely abstracted calldata (so that we can explore every execution path, this relates to #16), include the relevant storage variables and assume the desired invariant in the requires clause, and claim that however the storage updates, the invariant will hold in the ensures clause. Together with a proof that the invariant holds at contract creation, this proves by induction that the invariants hold.

We haven't really utilized the ensures clause thus far, but this seems like an excellent opportunity to do so.