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