Loop invariants

@wilcoxjay and I talked today, and he suggested the idea of also expressing loop invariants in the spec.

The challenge there is that loops don't have an interface, so how can we talk about them inside a function in the spec such that they represent loop behavior in different levels, eg, Solidity / bytecode?

One use case is, for example, a tool that runs on the Solidity level inferring loop invariants and trying to communicate these properties to tools that target bytecode.

An idea would be to have the basic spec level of abstraction similar to the ABI, and have extensions to that, such as spec that can also reason about bytecode.

The issue does not name files, tests, or an entry point. Begin by resolving how loop invariants should be represented within a function specification across Solidity and bytecode abstraction levels; done would be an agreed specification design that supports the stated cross-level communication use case.

Written by the indexing model from the issue text.