Formalize verification of contracts

[lerno]

In order to separate capabilities for compilers, introducing formal verification levels of contracts could be useful. A simple example:

V0: Contracts are only semantically checked.
V1: @require may be compiled into asserts inside of the function. Compile time violations detected through constant folding should not compile.
V2: As V1, but @ensures is also checked.
V3: @require and @ensures are added at the caller side as well. Compile time violations detected through constant folding should not compile.
V4: Detected compile time violations also includes range checks.
V5: Something else