CSE: manually specified preconditions

[palinatolmach]

We should add the ability to manually specify range constraints (e.g., that all values representing times are less than 2 ^Int 40) to remove various chops — this would require extending the natspec annotation mechanism.

The annotations should support at least basic boolean operations on variables including input and storage ones and having different types (e.g., mapping elements should be translated to lookups).

One example of preconditions we want to support is

`(_sharesAmount * totalPooledEther) / totalPooledEther == _sharesAmount`

[PetarMax]

Slightly more generally, we should be able to give the user the ability to specify arbitrary pre-conditions.