Assertions between opcodes

[pirapira]

In ethereum/solidity#1178 there is a plan to export annotated opcodes from the Solidity compiler.

This issue keeps track of performing an experiment of verifying a program snippet with interleaved static assertions. See the proposed syntax in ethereum/solidity#1178.

[pirapira]

This has been done in the Isabelle/HOL repository.