This project is an effort by several groups working on formal methods for Ethereum smart contracts, aiming at creating a simple but effective language to write formal specification. It extends on the previous Act project.
Some general features it hopes to achieve are:
- Simple structure and logic.
- Support writing properties on a high level (closer to Solidity/Vyper) as well as on the machine level.
- Cross-tool communication: Different tools might be able to generate different knowledge and use the specification language to exchange information.
- No attachment to a particular logic. If a tool wishes to support certain expressions, extensions can be written.
Everyone is encouraged to join/start discussions on issues and pull requests.
Act specifications are functional descriptions of the behaviour of a smart contract. Take the following toy state machine written in Solidity as an example:
contract StateMachine {
uint x;
function f() public {
if (x == 0)
x = 1;
}
function g() public {
if (x == 1)
x = 0;
}
}
The initial state is x = 0
, and x
can toggle between 1 and 0 by calling
functions f
and g
, respectively.
A simple specification for the program above could be the following Act:
constructor of StateMachine
interface constructor()
creates
uint256 x := 0
invariants
x <= 1
behaviour f of StateMachine
interface f()
case x == 0:
storage
x => 1
ensures
(x == 0) or (x == 1)
behaviour g of StateMachine
interface g()
case x == 1:
storage
x => 0
ensures
(x == 1) or (x == 0)
The case
s of a behaviour
specify how storage changes as a result of calling
the function, and its return argument, if present. They make up the lowest
level description of the specification. Functions pre and post conditions are
described in the iff
and ensures
sections, respectively. Contract
invariants specify relations between its storage variables that should remain
true for the entire lifetime of the contract.
More examples can be found in the examples
directory.
Act is designed to enable modular verification. Instead of checking properties that might be too hard to prove from the bytecode, such as contract invariants, we hope that it is easier to do that via multiple easier steps:
- Given a
behaviour
, show that implementation bytecode results in storage updates and return values as specified. - Given a
behaviour
, prove that thepost condition
described in theensures
section holds, assuming thepre condition
described in theiff
section. - Given a set of
behaviour
s, prove contract invariants. - Given
(transition system = "CONTRACT")
, show that arbitrary properties hold.
Note that steps 2, 3 and 4 can be done over Act only, without interaction with
the source code/bytecode. Reasoning about higher level properties outside the
source code/bytecode also makes it easier to apply different tools, which we
here refer to as proof backends
.
We are currently working on three different proof backends:
- Coq definitions
- K specs
- SMT theorems
The types of proofs that can be performed by the various backends can be understood in the following table:
Proof type \ Backend | HEVM | KEVM | SMT | Coq |
---|---|---|---|---|
Bytecode (with unknown calls) | Planned | ? | ||
Bytecode | Planned | WIP | ||
Poststate => postcondition | WIP | |||
Source level | Planned | |||
Contract level invariant | Done | WIP | ||
General higher properties | WIP |
The grammar for the specification language is in the src
repository. This
is the front end parsing of the language. Given a set of act
behaviours
(transitions), one can generate a set of proof obligations as a JSON object.
For example, take the following simplified Token contract:
contract Token {
uint8 constant public decimals = 18;
string public name;
string public symbol;
mapping (address => uint) public balanceOf;
function mint(uint value) public {
balanceOf[msg.sender] += value;
}
}
The behaviour of function mint
can be specified as the following Act:
behaviour mint of Token
interface mint(uint value)
storage
balanceOf[CALLER] => balanceOf[CALLER] + value
Parsing the Act gives us the generated proof obligations:
[
{
"stateUpdates": {
"Token": [
{
"location": {
"arity": 2,
"args": [
"balanceOf",
"CALLER"
],
"symbol": "lookup"
},
"value": {
"arity": 2,
"args": [
{
"arity": 2,
"args": [
"balanceOf",
"CALLER"
],
"symbol": "lookup"
},
"value"
],
"symbol": "+"
}
}
]
},
"name": "mint",
"preConditions": [],
"contract": "Token",
"interface": "mint(uint256 value)",
"returns": null
}
]
Different proof backends can make use of this single JSON output without the need to parse an Act, and apply its own techniques to try and answer the proof obligations.
With nix:
nix build -f default.nix exe
Enter a nix-shell to get the dependencies of the project:
nix-shell
this gives all the necessary prerequisites for recompiling:
make compiler
or entering a ghci
REPL:
make repl
To update the project dependencies run:
nix-shell --command niv update