Changes introduced in CVL 2
CVL 2.0 is a major overhaul to the type system of CVL. Many of the changes are internal, but we also wanted to take this opportunity to introduce a few improvements to the syntax. The general goal of these changes is to make the behavior of CVL more explicit and predictable, and to bring the syntax more in line with Solidity’s syntax.
This document summarizes the changes to CVL syntax introduced by CVL 2.0.
Contents
Superficial syntax changes
There are several simple changes to the syntax to make specs more uniform and consistent, and to reduce the superficial differences with Solidity.
function
and ;
required for methods block entries
In CVL 2, methods block entries must now start with function
and end with
;
(semicolons were optional in CVL 1). For example:
balanceOf(address) returns(uint) envfree
will become
function balanceOf(address) external returns(uint) envfree;
(note also the addition of external
, described below).
This is also true for entries with summaries:
_setManagedBalance(address,uint256) => NONDET
will become
function _setManagedBalance(address,uint256) internal => NONDET;
Required ;
in more places
using
, import
, use
, and invariant
statements all require a ;
at the
end. For example,
using C as c
becomes
using C as c;
use
statements do not require (and may not have) a semicolon if they
are followed by a preserved
or filtered
block. For example:
use rule poolSolvency filtered {
f -> !isEmergencyWithdrawal(f)
}
Method literals require sig:
In some places in CVL, you can refer to a contract method by its name and argument types. For example, you might write
require f.selector == balanceOf(address).selector;
In this example, balanceOf(address)
is a method literal. In CVL 2,
these methods literals must now start with sig:
. For example, the above
would become:
require f.selector == sig:balanceOf(address).selector;
Use of contract name instead of using
variable
In CVL 1, the only way to refer to a contract in the scene was to first
introduce a contract instance variable with a using
statement, and then use
that variable. For example, to access a struct type S
defined in
Example.sol
, you would need to write
using Example as c;
rule example {
c.S x = getAnS();
}
In CVL 2, you must now use the name of the contract, rather than the instance variable, when referring to user-defined types. The above example would now be written
rule example {
Example.S x = getAnS();
}
There is no need for a using
statement in this example.
Calling methods on secondary contracts still requires using a contract instance variable:
using Example as c;
rule example {
...
c.balanceOf(a);
...
}
Entries in the methods
block may use either the contract name or an instance
variable:
using Example as c;
methods {
//// both are valid:
function c.balanceOf(address) external returns(uint) envfree;
function Example.transfer(address,uint) external envfree;
}
Using the contract name in the methods block currently has the same effect as using an instance variable; this may change in future versions of CVL.
Rules must start with rule
In CVL 1, you could omit the keyword rule
when writing rules:
onlyOwnerCanDecrease() {
...
}
In CVL 2, the rule
keyword is no longer optional:
rule onlyOwnerCanDecrease() {
...
}
Changes to methods block entries
In addition to the superficial changes listed above, there are some changes to
the way that methods block entries can be written (there are also a
few instances where the meanings of entries has
changed). In CVL 1, methods
block entries often had several different
functions and meanings:
They were used to indicate targets for summarization
They were used to write generic specs that could apply to contracts with missing methods
They were used to declare targets
envfree
The changes described in this section make these different uses more explicit:
Most Solidity types allowed as arguments
CVL 1 had some restrictions on the types of arguments allowed in methods
block
entries. For example, user-defined types (such as enums and structs) were not
fully supported.
CVL 2 methods
block entries may use any Solidity types for arguments and
return values, except for function types and contract or
interface types.
To work around the missing types, CVL 1 allowed users to encode some
user-defined types as primitive types in the methods
block; these workarounds
are no longer allowed in CVL 2. For example, consider the following solidity
function:
contract Example {
enum Permission { READ, WRITE };
function f(Permission p) internal { ... }
}
In CVL 1, a methods block entry for f
would need to declare that it takes a
uint8
argument:
methods {
f(uint8 permission) => NONDET
}
In CVL 2, the methods block entry should use the same type as the Solidity implementations, except for function types and contract or interface types:
methods {
function f(Example.Permission p) internal => NONDET;
}
The method can be called from CVL as follows:
rule example {
f(Example.Permission.READ);
}
Contract functions that take or return contract or interface types should
instead use address
in the methods
block declaration. For example, if the
contract contains the following function:
function listToken(IERC20 token) internal { ... }
the methods
block should use address
for the token
argument:
methods {
function listToken(address token) internal;
}
Contract functions that take or return function types are not currently supported. Users can use munging to work around this limitation.
Required internal
or external
annotation
Every methods block entry must be marked either internal
or external
. The
annotation must come after the argument list and before the returns
clause.
If a function is declared public
in Solidity, then the Solidity compiler
creates an internal implementation method, and an external wrapper method that
calls the internal implementation. Therefore, you can summarize a public
method by marking the summarization internal
.
Warning
The behavior of internal
vs. external
summarization for public methods can
be confusing, especially because functions called directly from CVL are not
summarized.
Consider a public function f
. Suppose we provide an internal
summary for
f
:
Calls from CVL to
f
will effectively be summarized, because CVL will call the external function, which will then call the internal implementation, and the internal implementation will be summarized.Calls from another contract to
f
(or calls tothis.f
fromf
’s contract) will effectively be summarized, again because the external function immediately calls the summarized internal implementation.Internal calls to
f
will be summarized.
On the other hand, suppose we provide an external
summary for f
. In this
case:
Calls from CVL to
f
will not be summarized, because direct calls from CVL to contract functions do not use summaries.Internal calls to
f
will not be summarized - they will use the original implementation.External calls to
f
(from Solidity code that callsthis.f
orc.f
) will be summarized
In most cases, public functions should use an internal
summary, since this
effectively summarizes both internal and external calls to the function.
If the rare case that you want to summarize the internal implementation and the
external wrapper differently, you can add two separate entries to the methods
block.
optional
methods block entries
In CVL 1, you could write an entry in the methods block for a method that does not exist in the contract; rules that would call the non-existent method were skipped during verification.
This behavior can lead to confusion, because typos or name changes could silently cause a rule to be skipped.
In CVL 2, this behavior is still available, but the methods entry must contain
the keyword optional
somewhere after the returns
clause and before the
summarization (if any).
library
annotations
In CVL 2, contract functions declared as library functions must be annotated
with library
in the methods
block.
Required calldata
, memory
, or storage
annotations for reference types
In CVL 2, methods block entries for internal functions must contain either calldata
,
memory
, or storage
annotations for all arguments with reference types (such
as arrays).
Summaries only apply to one contract by default
In CVL 1, a summary in the methods
block applied to all methods with the
given signature.
In CVL 2, summaries only apply to a single contract, unless the old behavior is
explicitly requested by using _
as the receiver. If no contract is specified,
the default is currentContract
.
Entries that use _
as the receiver are called wildcard entries, summaries
that do not are called exact entries.
Consider the following example:
using C as c;
methods {
function f(uint) internal => NONDET;
function c.g(uint) internal => ALWAYS(4);
function h(uint) internal => ALWAYS(1);
function _.h(uint) internal => NONDET;
}
In this example, the internal function currentContract.f
has a NONDET
summary, c.g
has an ALWAYS
summary, a call to currentContact.h
has an
ALWAYS
summary and a call to h(uint)
on any other contract will use a
NONDET
summary.
Summaries for specific contract methods (including the default
currentContract
) always override wildcard summaries.
Wildcard entries cannot be declared optional
or envfree
, since these
annotations only make sense for specific contract methods.
Warning
The meaning of your summarizations will change from CVL 1 to CVL 2. In CVL 2,
any entry without an _
will only apply to a single contract!
Requirements on returns
In CVL 1, the returns
clause on methods block entries was optional.
CVL 2 has stricter requirements on the declared return types.
Entries that apply to specific contracts (i.e. those that don’t use the
_.f
syntax) must include a returns
clause if the
contract method returns a value. A specific-contract entry may only omit the
returns
clause if the contract method does not return a value.
The Prover will report an error if the contract method’s return type differs
from the type declared in the methods
block entry.
Wildcard entries must not declare return types, because they may apply to multiple methods that return different types.
If a wildcard entry has a ghost or function summary, the user must explicitly
provide an expect
clause to the summary. The expect
clause tells the
Prover how to interpret the value returned by the summary. For example:
methods {
function _.foo() external => fooImpl() expect uint256 ALL;
}
This entry will replace any call to any external function foo()
with a call to
the CVL function fooImpl()
and will interpret the output of fooImpl
as a
uint256
.
If a function does not return any value, the summary should be declared with
expect void
.
Warning
You must check that your expect
clauses are correct.
The Prover cannot always check that the return type declared in the expect
clause matches the return type that the contract expects. Continuing the above
example, suppose the contract being verified declared a method foo()
that
returns a type other than uint256
:
function foo() external returns(address) {
...
}
function bar() internal {
address x = y.foo();
}
In this case, the Prover would encode the value returned by fooImpl()
as a
uint256
, and the bar
method would then attempt to decode this value as an
address
. This will cause undefined behavior, and in some cases the Prover
will not be able to detect the error.
Changes to integer types
In CVL 1, the rules for casting between integer types were complex; CVL 2 simplifies them.
The general rule of thumb is that you should use mathint
whenever possible;
only use uint
or int
types for data that will be passed as input to
contract functions.
It is now impossible for CVL math expressions to cause overflow - all integer operations are exact. The remainder of this section describes the changes in detail.
Mathematical operations return mathint
In CVL 2, the results of all arithmetic operators have type mathint
,
regardless of the input types. Arithmetic operators include +
,
*
, -
, /
, ^
, and %
, but not bitwise operators like <<
, xor
, and |
(changes to bitwise operators are described below).
The primary impact of this change is that you may need to declare more of your
variables as mathint
instead of uint
. If you are passing the results of
arithmetic operations to contract functions, you will need to be more explicit
about the overflow behavior by using the new casting operators.
Comparisons require identical types
When comparing two integers using ==
, <=
, <
, >
, or >=
, CVL 2 will
require both sides of the equation to have identical types, and implicit casts will not be used. Comparisons with number literals (e.g.
0
or 1
) are allowed for any integer type.
If you do not have identical types (and cannot change one of your variables to
a mathint
), the best solution is to use the special
to_mathint
operator to convert both sides to mathint
. For example:
assert to_mathint(balanceOf(user)) == initial + deposit;
Note that in this example, we do not need to cast the right hand side, since
the result of +
is always of type mathint
.
Note
When should you not simply cast to mathint
? We have one example: consider the
following code:
ghost uint256 sum;
hook ... {
havoc sum assuming sum@new == sum@old + newBalance - oldBalance;
}
Simply casting to mathint
will turn overflows into vacuity.
In this particular example, the right solution is to declare sum
to be a
mathint
instead of a uint
. Note that with the more recent update syntax,
this problem will correctly be reported as an error. For example, if you
mistakenly write the following:
ghost uint256 sum;
hook ... {
sum = sum + newBalance - oldBalance;
}
then the Prover will again report a type error, but the only available solutions
are to change sum
to a mathint
(which would prevent the vacuity) or write
an explicit assert
or require
cast (which would make the vacuity explicit).
Implicit and explicit casting
If every number that can be represented by one type can also be represented by another type, then we say that the first type is a subtype of the second type.
For example, a uint8
variable could have any value between 0
and 2^8-1
,
and all of these values can be stored in a uint16
variable, so uint8
is a
subtype of uint16
. An int16
can also store any value between 0
and
2^8-1
, so uint8
is also a subtype of int16
.
All integer types are subtypes of mathint
, since any integer can be
represented by a mathint
.
In CVL 1, the rules for converting between supertypes and subtypes were complicated; they depended not only on the types involved, but on the context in which the conversion happened. CVL 2 simplifies these rules and improves the clarity and predictability of casts.
In CVL 2, with one exception, you can always use a subtype whenever the
supertype is accepted. For example, you can always use a uint8
where an
int16
is expected. We say that the subtype can be “implicitly cast” to the
supertype.
The one exception is comparison operators; as mentioned above, you must add an
explicit conversion if you want to compare two numbers with different types.
The to_mathint
operator exists solely for this purpose; in all other contexts
you can simply use any number when a mathint
is expected (since all integer
types are subtypes of mathint
).
In order to convert from a supertype to a subtype, you must use an explicit
cast. In CVL 1, only a few casting operators (such as to_uint256
) were
supported.
CVL 2 replaces these casting operators with two new casting operators: assert casts
such as assert_uint8(x)
or assert_int256(x)
, and require casts such as require_uint8(x)
or require_int256(x)
.
Each of these casts checks that the value is in range; the assert
cast will
report a counterexample if the value is out of range, while the require
cast
will ignore counterexamples where the cast value is out of range.
Warning
As with normal require
statements, require casts can cause vacuity and should
be used with care.
CVL 2 supports assert and require casts on all numeric types.
Casts between address
, bytes1
…bytes32
, and integer types are not
supported.
require
and assert
casts are not allowed anywhere inside of a
quantified statement. You can work around this limitation
by adding a second variable. For example, the following axiom is invalid
because x+1
is not a uint
:
ghost mapping(uint => uint) a {
axiom forall uint x . a[x+1] == 0
}
However, it can be replaced with the following:
ghost mapping(uint => uint) a {
axiom forall uint x . forall uint y . (to_mathint(y) == x + 1) => a[y] == 0
}
Modulo operator %
returns negative values for negative inputs
As in Solidity, if n < 0
then n % k == -(-n % k)
.
Support for bytes1
…bytes32
CVL 2 supports the types bytes1
, bytes2
, …, bytes32
, as in Solidity.
Number literals must be explicitly cast to these types using to_bytesN
; for
example:
bytes32 x = to_bytes32(0);
Unlike Solidity, bytes1
…bytes32
literals do not need to be written in hex
or padded to the correct length.
There is no way to convert between these types and integer types (except for literals as just mentioned).
Changes for bitwise operations
In CVL1, the exact details for bitwise operations (such as &
, |
, and <<
) were not
completely specified, especially for negative integers.
In CVL 2, all bitwise operations (&
, |
, ~
, >>
, >>>
, <<
, and xor
)
on integer types first convert to a 256 bit word, then perform the operations
on the full 256-bit word, then convert back to the expected type. Signed
integer types use twos-complement encoding.
The two right-shifts differ in how they treat signed integers. >>
is an
arithmetic shift; it preserves the sign bit. >>>
is a logical shift; it pads
the shifted word with zero.
Bitwise operations cannot be performed on mathint
values.
Note
By default, bitwise operators are overapproximated (in both CVL 1 and CVL 2), so you may see counterexamples that incorrectly compute the results of bitwise operations. The approximations are still sound: the Prover will not report a rule as verified if the original code does not satisfy the rule.
The --settings -useBitVectorTheory flag makes the Prover’s reasoning about bitwise operations more precise, but this flag is experimental in CVL 2.
Changes to the fallback function
In CVL 1, you could determine whether a method
object was the fallback function
by comparing its selector to certorafallback().selector
:
assert f.selector == certorafallback().selector,
"f must be the fallback";
In CVL 2, certorafallback()
is no longer valid. Instead, you can use the new
field f.isFallback
to detect the fallback method:
assert f.isFallback,
"f must be the fallback";
Removed features
As part of the transition to CVL 2.0, we have removed several language features that are no longer used.
We have removed these features because we think they are no longer used and no longer useful. If you find that you do need one of these features, contact Certora support.
Methods entries for sighashes
In CVL 1, you could write a sighash instead of a method identifier in the
methods
block. This feature is no longer supported. You will need to have
the name and argument types of the called method in order to provide an entry.
invoke
, sinvoke
, and call
Older versions of CVL had special syntax for calling contract and CVL functions:
invoke f(args);
should be replaced withf@withrevert(args);
.sinvoke f(args);
should be replaced withf(args);
.call f(args)
should be replaced withf(args)
.
static_assert
and static_require
These deprecated aliases for assert
and require
are being removed; replace
them with assert
and require
respectively.
invoke_fallback
and certorafallback()
The invoke_fallback
syntax is no longer supported; there is no longer a way
to directly invoke the fallback method. You can work around this limitation by
writing a parametric rule and filtering on f.isFallback
. See
Changes to the fallback function.
invoke_whole
The invoke_whole
keyword is no longer supported.
Havocing local variables
In CVL 1, you could write the following:
calldataarg args; env e;
f(e, args);
havoc args;
g(e, args);
In CVL 2, you can only havoc
ghost variables and ghost functions. Instead of
havocing a local variable, replace the havoced variable with a new variable. For
example, you should replace the above with
calldataarg args; env e;
f(e,args);
calldataarg args2;
g(e,args2);
Destructuring syntax for struct returns
In CVL 1, if a contract function returned a struct, you could use a destructuring syntax to get the return value in your spec. For example, consider the following contract:
contract Example {
struct S {
uint firstField;
uint secondField;
bool thirdField;
}
function f() returns(S) { ... }
function g() returns(uint, uint) { ... }
}
To access the return value of f
in CVL 1, you could write the following:
uint x; uint y; bool z;
x, y, z = f();
This syntax is no longer supported. Instead, you should declare a variable with the struct type:
Example.S result = f();
uint x = result.firstField;
Destructuring assignments are still allowed for functions that return multiple values; the following is valid:
uint x; uint y;
x, y = g();
bytes[]
and string[]
In CVL 1, you could declare variables of type string[]
and bytes[]
. You can
no longer use these types in CVL.
You can still declare contract methods that use these types in the methods
block. However, you can only call methods that take one of these types as an
argument by passing a calldataarg
variable, and you cannot access the return
value of a method that returns one of these types.
pragma
CVL 1 had a pragma
command for specifying the CVL version, but this feature
was not used. It has been removed in CVL 2.
events
CVL 1 had syntax for an events
block, but it did nothing and has been removed.