Statements 

The bodies of rules, functions, and hooks in CVL are made up of statements. Statements describe the steps that are simulated by the Prover when evaluating a rule.

Statements in CVL are similar to statements in Solidity, although there are some differences; see Solidity-like statements. This document lists the available CVL commands.

Contents

Statements

Syntax 

The syntax for statements in CVL is given by the following EBNF grammar:

block ::= statement { statement }

statement ::= type id [ "=" expr ] ";"

            | "require" expr ";"
            | "static_require" expr ";"
            | "assert" expr [ "," string ] ";"
            | "static_assert" expr [ "," string ] ";"

            | "requireInvariant" id "(" exprs ")" ";"

            | lhs "=" expr ";"
            | "if" expr statement [ "else" statement ]
            | "{" block "}"
            | "return" [ expr ] ";"

            | function_call ";"
            | "call" id "(" exprs ")" ";"
            | "invoke_fallback" "(" exprs ")" ";"
            | "invoke_whole" "(" exprs ")" ";"
            | "reset_storage" expr ";"

            | "havoc" id [ "assuming" expr ] ";"

lhs ::= id [ "[" expr "]" ] [ "," lhs ]

See Basic Syntax for the id and string productions. See Types for the type production. See Expressions for the expr and function_call productions.

Unlike undefined variables in most programming languages, undefined variables in CVL are a centrally important language feature. If a variable is declared but not defined, the Prover will generate models with every possible value of the undefined variable.

Undefined variables in CVL behave the same way as rule parameters.

When the Prover reports a counterexample that violates a rule, the values of the variables declared in the rule are displayed in the report. Variables declared in CVL functions are not currently visible in the report.

`assert` and `require`

The assert and require commands are similar to the corresponding statements in Solidity. The require statement is used to specify the preconditions for a rule, while the assert statement is used to specify the expected behavior of contract functions.

During verification, the Prover will ignore any model that causes the require expressions to evaluate to false. Unlike Solidity, the require statement does not contain a descriptive message, because the Prover will never consider an example where the require statement evaluates to false.

The assert statements define the expected behavior of contract functions. If it is possible to generate a model that causes the assert expression to evaluate to false, the Prover will construct one of them and report a violation.

Assert conditions may be followed by a message string describing the condition; this message will be included in the reported violation. Assertion messages may use string interpolation to add information about the counterexamples to the message.

Note

Unlike Solidity’s assert and require, the CVL syntax for assert and require does not require parentheses around the expression and message.

`requireInvariant` statements 

Todo

This feature is currently undocumented.

Note

requireInvariant is always safe for invariants that have been proved, even in preserved blocks; see Invariants and induction for a detailed explanation.

Todo

Be sure to document @old and @new (two-state contexts). They are not documented in Expressions because I think havoc ... assuming ... is the only place that they are available.

Statements 

Syntax 

Variable declarations 

`assert` and `require`

`requireInvariant` statements 

Solidity-like statements 

Function calls 

`havoc` statements 