Expressions
A CVL expression is anything that represents a value. This page documents all possible expressions in CVL and explains how they are evaluated.
Contents
Syntax
The syntax for CVL expressions is given by the following EBNF grammar:
expr ::= literal
| unop expr
| expr binop expr
| "(" exprs ")"
| expr "?" expr ":" expr
| [ "forall" | "exists" ] type id "." expr
| expr "." id
| id [ "[" expr "]" { "[" expr "]" } ]
| id "(" types ")"
| function_call
| expr "in" id
function_call ::=
| [ id "." ] id
[ "@" ( "norevert" | "withrevert" | "dontsummarize" ) ]
"(" exprs ")"
[ "at" id ]
literal ::= "true" | "false" | number | string
unop ::= "~" | "!" | "-"
binop ::= "+" | "-" | "*" | "/" | "%" | "^"
| ">" | "<" | "==" | "!=" | ">=" | "<="
| "&" | "|" | "<<" | ">>" | "&&" | "||"
| "=>" | "<=>" | "xor" | ">>>"
specials_fields ::=
| "block" "." [ "number" | "timestamp" ]
| "msg" "." [ "address" | "sender" | "value" ]
| "tx" "." [ "origin" ]
| "length"
| "selector" | "isPure" | "isView" | "numberOfArguments" | "isFallback"
special_vars ::=
| "lastReverted" | "lastHasThrown"
| "lastStorage"
| "allContracts"
| "lastMsgSig"
| "_"
| "max_uint" | "max_address" | "max_uint8" | ... | "max_uint256"
| "nativeBalances"
| "calledContract"
cast_functions ::=
| require_functions | to_functions | assert_functions
require_functions ::=
| "require_uint8" | ... | "require_uint256" | "require_int8" | ... | "require_int256"
to_functions ::=
| "to_mathint" | "to_bytes1" | ... | "to_bytes32"
assert_functions ::=
| "assert_uint8" | ... | "assert_uint256" | "assert_int8" | ... | "assert_int256"
contract ::= id | "currentContract"
See Basic Syntax for the id
, number
, and string
productions.
See Types for the type
production.
Basic operations
CVL provides the same basic arithmetic, comparison, bitwise, and logical operations for basic types that solidity does, with a few differences listed in this section and the next. The precedence and associativity rules are standard.
Caution
One significant difference between CVL and Solidity is that in Solidity, ^
denotes bitwise exclusive or and **
denotes exponentiation, whereas in CVL,
^
denotes exponentiation and xor
denotes exclusive or.
Todo
The >>>
operator is currently undocumented.
See Changes to integer types for more information about the interaction between mathematical types and the meaning of mathematical operations.
String interpolation
String literals that appear in assertion messages or rule descriptions can
contain placeholders that are replaced by explicit values in the verification
report. A variable can be included by prefixing it with a $
, while more
complex expressions can be included by surrounding them with ${...}
.
For example:
rule example(method f, uint x)
description "$f should output 0 on $x with ${e.msg.sender}"
{
env e;
assert f(e,x) == 0, "failed with timestamp ${e.block.timestamp}";
}
Extended logical operations
CVL also adds several useful logical operations:
Like
&&
or||
, an implication expressionexpr1 => expr2
requiresexpr1
andexpr2
to be boolean expressions and is itself a boolean expression.expr1 => expr2
evaluates tofalse
if and only ifexpr1
evaluates totrue
andexpr2
evaluates tofalse
.expr1 => expr2
is equivalent to!expr1 || expr2
.For example, the statement
assert initialized => x > 0;
will only report counterexamples whereinitialized
is true butx
is not positive.
Todo
Whether implications (and other boolean connectors) are short-circuiting is currently undocumented.
Similarly, an if and only if expression (also called a bidirectional implication)
expr1 <=> expr2
requiresexpr1
andexpr2
to be boolean expressions and is itself a boolean expression.expr1 <=> expr2
evaluates totrue
ifexpr1
andexpr2
evaluate to the same boolean value.For example, the statement
assert balanceA > 0 <=> balanceB > 0;
will report a violation if exactly one ofbalanceA
andbalanceB
is positive.An if-then-else (ITE) expression of the form
cond ? expr1 : expr2
requirescond
to be a boolean expression and requiresexpr1
andexpr2
to have the same type; the entire if-then-else expression has the same type asexpr1
andexpr2
. The expressioncond ? expr1 : expr2
should be read “ifcond
thenexpr1
elseexpr2
. Ifcond
evaluates totrue
then the entire expression evaluates toexpr1
; otherwise the entire expression evaluates toexpr2
.For example, the expression
uint balance = address == owner ? ownerBalance() : userBalance(address);
will set
balance
toownerBalance()
ifaddress
isowner
, and will set it touserBalance(address)
otherwise.Conditional expressions are short-circuiting: if
expr1
orexpr2
have side-effects (such as updating a ghost variable), only the side-effects of the expression that is chosen are performed.A universal expression of the form
forall t v . expr
requirest
to be a type (such asuint256
oraddress
) andv
to be a variable name;expr
should be a boolean expression and may refer to the identifierv
. The expression evaluates totrue
if every possible value of the variablev
causesexpr
to evaluate totrue
.For example, the statement
require (forall address user . balance(user) <= balance(biggestUser));
will ensure that every other user has a balance that is less than or equal to the balance of
biggestUser
.Like a universal expression, an existential expression of the form
exists t v . expr
requirest
to be a type andv
to be a variable name;expr
should be a boolean expression and may refer to the variablev
. The expression evaluates totrue
if there is any possible value of the variablev
that causesexpr
to evaluate totrue
.For example, the statement
require (exists uint t . priceAtTime(t) != 0);
will ensure that there is some time for which the price is nonzero.
Note
The symbols forall
and exist
are sometimes referred to as quantifiers,
and expressions of the form forall type v . e
and exist type v . e
are
referred to as quantified expressions.
Caution
forall
and exists
expressions are powerful and elegant ways to express rules
and invariants, but they require the Prover to consider all possible values of
a given type. In some cases they can cause significant slowdowns for the
Prover.
If you have rules or invariants using exists
that are running slowly or
timing out, you can remove the exists
by manually computing the value that
exists. For example, you might replace
require (exists uint t . priceAtTime(t) != 0);
with
require priceAtTime(startTime) != 0;
Accessing fields and arrays
One can access the special fields of built-in types, fields of user-defined
struct
types, and members of user-defined enum
types using the normal
expr.field
notation. Note that as described in User-defined types,
access to user-defined types must be qualified by a contract name.
Access to arrays also uses the same syntax as Solidity.
Contracts, method signatures and their properties
Writing the ABI signature for a contract method produces a method
object,
which can be used to access the method fields.
For example,
method m;
require m.selector == sig:balanceOf(address).selector
|| m.selector == sig:transfer(address, uint256).selector;
will constrain m
to be either the balanceOf
or the transfer
method.
One can determine whether a contract has a particular method using the s in c
where s
is a method selector and c
is a contract (either currentContract
or a contract introduced with a using statement. For
example, the statement
if (burnFrom(address,uint256).selector in currentContract) {
...
}
will check that the current contract supports the optional burnFrom
method.
Special variables and fields
Several of the CVL types have special fields; see Types (particularly The env type, The method and calldataarg types, and Array access).
There are also several built-in variables:
bool lastReverted
andbool lastHasThrown
are boolean values that indicate whether the most recent contract function reverted or threw an exception.Caution
The variables
lastReverted
andlastHasThrown
are updated after each contract call, even those called without@withrevert
(see Calling contract functions). This is a common source of errors. For example, the following rule is vacuous:rule revert_if_paused() { withdraw@withrevert(); assert isPaused() => lastReverted; }
In this rule, the call to
isPaused
will updatelastReverted
totrue
, overwriting the value set bywithdraw
.lastStorage
refers to the most recent state of the EVM storage. See The storage type for more details.You can use the variable
_
as a placeholder for a value you are not interested in.The maximum values for the different integer types are available as the variables
max_uint
,max_address
,max_uint8
,max_uint16
etc.nativeBalances
is a mapping of the native token balances, i.e. ETH for Ethereum. The balance of anaddress a
can be expressed usingnativeBalances[a]
.calledContract
is only available in function summaries. It refers to the receiver contract of a summarized method call.
CVL also has several built-in functions for converting between numeric types. See Basic operations for details.
Calling contract functions
There are many kinds of function-like things that can be called from CVL:
Contract functions
There are several additional features that can be used when calling contract functions (including calling them through method variables).
The method name can optionally be prefixed by a contract name. If a contract is
not explicitly named, the method will be called with currentContract
as the
receiver.
It is possible for multiple contract methods to match the method call. This can happen in two ways:
The method to be called is a method variable
The method to be called is overloaded in the contract (i.e. there are two methods of the same name), and the method is called with a calldataarg argument.
In either case, the Prover will consider every possible resolution of the method while verifying the rule, and will provide a separate verification report for each checked method. Rules that use this feature are referred to as parametric rules.
After the function name, but before the arguments, you can write an optional
method tag, one of @norevert
, @withrevert
, or @dontsummarize
.
@norevert
indicates that examples where the method revert should not be considered. This is the default behavior if no tag is provided@withrevert
indicates that examples that would revert should still be considered. In this case, the method will set thelastReverted
andlastHasThrown
variables totrue
in case the called method reverts or throws an exception.Todo
The
@dontsummarize
tag is currently undocumented.
After the method tag, the method arguments are provided. Unless the method is declared envfree, the first argument must be an environment value. The remaining arguments must either be a single calldataarg value, or the same types of arguments that would normally be passed to the contract method.
After the method arguments, a method invocation can optionally include at s
where s
is a storage variable. This indicates that
before the method is executed, the EVM state should be restored to the saved
state s
.
Type restrictions
When calling a contract function, the Prover must convert the arguments and return values from their Solidity types to their CVL types and vice-versa. There are some restrictions on the types that can be converted. See Conversions between CVL and Solidity types for more details.
Comparing storage
As described in the documentation on storage types, CVL represents the entirety of the EVM and its
ghost state
in variables with storage
type. Variables of this type can be checked for equality and inequality.
The basic form of this expression is s1 == s2
, where s1
and s2
are variables of type storage
.
This expression compares the states represented by s1
and s2
; that is, it checks equality of the following:
The values in storage for all contracts,
The balances of all contracts,
The state of all ghost variables and functions
Thus, if any field in any contract’s storage differs between s1
and s2
, the expression will return false
.
The expression s1 != s2
is shorthand for !(s1 == s2)
.
Storage comparisons also support narrowing the scope of comparison to specific components of the global
state represented by storage
variables. This syntax is s1[r] == s2[r]
or s1[r] != s2[r]
, where r
is a “storage comparison basis”,
and s1
and s2
are variables of type storage
. The valid bases of comparison are:
The name of a contract imported with a using statement,
The keyword
nativeBalances
, orThe name of a ghost variable or function
It is an error to use different bases on different sides of the comparison operator, and it is also an error to use a comparison basis on one side and not the other. The application of the basis restricts the comparison to only consider the portion of global state identified by the basis.
If the qualifier is a contract identifier
imported via using
, then the comparison operation will only consider the storage fields of that contract. For example:
using MyContract as c;
using OtherContract as o;
rule compare_state_of_c(env e) {
storage init = lastStorage;
o.mutateOtherState(e); // changes `o` but not `c`
assert lastStorage[c] == init[c];
}
will pass verification whereas:
using MyContract as c;
using OtherContract as o;
rule compare_state_of_c(env e) {
storage init = lastStorage;
c.mutateContractState(e); // changes `c`
assert lastStorage[c] == init[c];
}
will not.
Note
Comparing contract’s state using this method will not compare the balance of the contract between the two states.
If the qualifier is the identifier nativeBalances
, then the account balances
of all contracts are compared between the two storage states.
Finally, if the basis is the name of a ghost function or variable, the values of that
function/variable are compared between storage states.
Two ghost functions are considered equal if they have the same outputs for all input arguments.
Warning
The default behavior of the Prover on unresolved external calls is to pessimistically havoc contract state and balances. This behavior will render most storage comparisons that incorporate such state useless. Care should be taken (using summarization) to ensure that rules that compare storage do not encounter this behavior.
Warning
The grammar admits storage comparisons for both equality and inequality
that occur arbitrarily nested within expressions. However, support within the Prover for
these comparisons is primarily aimed at assertions of storage equality, e.g., assert s1 == s2
.
Support for storage inequality as well as nesting comparisons within other expressions is considered
experimental.
Warning
The storage comparison checks for exact equality between every single slot of storage which can
lead to surprising failures of storage equality assertions.
In particular, these failures can happen if an uninitialized storage slot is
written and then later cleared by Solidity (via the pop()
function or the delete
keyword). After the
clear operation the slot will definitely hold 0, but the Prover will not make any assumptions
about the value of the uninitialized slot which means they can be considered different.