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
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 ] ";"
| "satisfy" 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.
Variable declarations
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.
satisfy
statements
A satisfy
statement is used to check that the rule can be executed in such a
way that the satisfy
statement is true. A rule with a satisfy
statement is
describing a scenario and must not contain assert
statements. We require that
each rule ends with either a satisfy
statement or an assert
statement.
See Producing Positive Examples for an example demonstrating the satisfy
command.
For each satisfy
statement, the Certora verifier will produce a witness for a
valid execution of the rule. It will show an execution trace containing values
for each input variable and each state variable where all require
and satisfy
statements are executed successfully. In case there is no such execution, for
example if the require
statements are already inconsistent or if a solidity
function always reverts, an error is reported.
If the rule contains multiple satisfy
statements, then all executed satisfy
statements must hold. However, a satisfy
statement on a conditional branch
that is not executed does not need to hold.
If at least one satisfy
statement is not satisfiable an error is reported.
If all satisfy
statements can be fulfilled on at least one path, the rule
succeeds.
Note
A success only guarantees that there is some satisfying execution starting in some arbitrary state. It is not possible to check that every possible starting state has an execution that satisfies the condition.
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.
Solidity-like statements
Todo
This feature is currently undocumented.
Function calls
Todo
This feature is currently undocumented. See Calling contract functions for partial information.
havoc
statements
Todo
This section is currently incomplete. See ghosts and Two State Context for the old documentation.
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.