Skip to content

Commit 01009ef

Browse files
msoosethmsooseth
committed
Update
Update Better summary Update Update Should be equivalent More docs update
1 parent 07bc1b2 commit 01009ef

File tree

4 files changed

+196
-194
lines changed

4 files changed

+196
-194
lines changed

‎doc/src/equivalence.md

+137-42
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,148 @@
11
# `hevm equivalence`
22

3-
```
4-
Usage: hevm equivalence --code-a TEXT --code-b TEXT [--sig TEXT]
5-
[--arg STRING]... [--calldata TEXT]
6-
[--smttimeout NATURAL] [--max-iterations INTEGER]
7-
[--solver TEXT] [--smtoutput] [--smtdebug] [--debug]
8-
[--trace] [--ask-smt-iterations INTEGER]
9-
[--num-cex-fuzz INTEGER]
10-
[--loop-detection-heuristic LOOPHEURISTIC]
11-
[--abstract-arithmetic] [--abstract-memory]
12-
13-
Available options:
14-
-h,--help Show this help text
15-
--code-a TEXT Bytecode of the first program
16-
--code-b TEXT Bytecode of the second program
17-
--sig TEXT Signature of types to decode / encode
18-
--arg STRING Values to encode
19-
--calldata TEXT Tx: calldata
20-
--smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300)
21-
--max-iterations INTEGER Number of times we may revisit a particular branching
22-
point. Default is 5. Setting to -1 allows infinite looping
23-
--solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla
24-
--smtoutput Print verbose smt output
25-
--smtdebug Print smt queries sent to the solver
26-
--debug Debug printing of internal behaviour
27-
--trace Dump trace
28-
--ask-smt-iterations INTEGER
29-
Number of times we may revisit a particular branching
30-
point before we consult the smt solver to check
31-
reachability (default: 1) (default: 1)
32-
--num-cex-fuzz INTEGER Number of fuzzing tries to do to generate a
33-
counterexample (default: 3) (default: 3)
34-
--loop-detection-heuristic LOOPHEURISTIC
35-
Which heuristic should be used to determine if we are
36-
in a loop: StackBased (default) or Naive
37-
(default: StackBased)
3+
```plain
4+
Usage: hevm equivalence [--code-a TEXT] [--code-b TEXT] [--code-a-file STRING]
5+
[--code-b-file STRING] [--sig TEXT] [--arg STRING]...
6+
[--calldata TEXT] [--smttimeout NATURAL]
7+
[--max-iterations INTEGER] [--solver TEXT]
8+
[--num-solvers NATURAL] ...
389
```
3910

4011
Symbolically execute both the code given in `--code-a` and `--code-b` and try
41-
to prove equivalence between their outputs and storages. Extracting bytecode
42-
from solidity contracts can be done via, e.g.:
12+
to prove equivalence between their outputs and storages.
4313

14+
## Simple example usage
15+
16+
```shell
17+
$ solc --bin-runtime "contract1.sol" | tail -n1 > a.bin
18+
$ solc --bin-runtime "contract2.sol" | tail -n1 > b.bin
19+
$ hevm equivalence --code-a-file a.txt --code-b-file b.txt
4420
```
45-
hevm equivalence \
46-
--code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
47-
--code-b $(solc --bin-runtime "contract2.sol" | tail -n1)
48-
```
21+
22+
## Calldata size limits
23+
4924
If `--sig` is given, calldata is assumed to take the form of the function
5025
given. If `--calldata` is provided, a specific, concrete calldata is used. If
5126
neither is provided, a fully abstract calldata of at most `2**64` byte is
5227
assumed. Note that a `2**64` byte calldata would go over the gas limit, and
53-
hence should cover all meaningful cases.
28+
hence should cover all meaningful cases. You can limit the buffer size via
29+
`--max-buf-size`, which sets the exponent of the size, i.e. 10 would limit the
30+
calldata to `2**10` bytes.
31+
32+
## What constitutes equivalence
33+
34+
The equivalence checker considers two contracts equivalent if given the
35+
same calldata they:
36+
- return the same value
37+
- have the same storage
38+
- match on the success/failure of the execution
39+
Importantly, logs are *not* considered in the equivalence check. Hence,
40+
it is possible that two contracts are considered equivalent by `hevm equivalence` but
41+
they emit different log items.
42+
43+
For example, two contracts that are:
44+
45+
```
46+
PUSH1 3
47+
```
48+
49+
And
50+
51+
```
52+
PUSH1 4
53+
```
54+
55+
Are considered *equivalent*, because they don't put anything in the return
56+
data, are not different in their success/fail attribute, and don't touch
57+
storage. However, these two are considered different:
58+
59+
```
60+
PUSH1 3
61+
PUSH1 0x20
62+
MSTORE
63+
PUSH1 0x40
64+
PUSH1 0x00
65+
RETURN
66+
```
67+
68+
and:
69+
70+
71+
```
72+
PUSH1 4
73+
PUSH1 0x20
74+
MSTORE
75+
PUSH1 0x40
76+
PUSH1 0x00
77+
RETURN
78+
```
79+
80+
Since one of them returns a 3 and the other a 4. We also consider contracts different when
81+
they differ in success/fail. So these two contracts:
82+
83+
```
84+
PUSH1 0x00
85+
PUSH1 0x00
86+
RETURN
87+
```
88+
89+
and:
90+
91+
```
92+
PUSH1 0x00
93+
PUSH1 0x00
94+
REVERT
95+
```
96+
97+
Are considered different, as one of them reverts (i.e. fails) and the other
98+
succeeds.
99+
100+
## Creation code equivalence
101+
102+
If you want to check the equivalence of not just the runtime code, but also the
103+
creation code of two contracts, you can use the `--creation` flag. For example
104+
these two contracts:
105+
106+
```solidity
107+
contract C {
108+
uint private immutable NUMBER;
109+
constructor(uint a) {
110+
NUMBER = 2;
111+
}
112+
function stuff(uint b) public returns (uint256) {
113+
unchecked{return 2+NUMBER+b;}
114+
}
115+
}
116+
```
117+
118+
And:
119+
120+
```solidity
121+
contract C {
122+
uint private immutable NUMBER;
123+
constructor(uint a) {
124+
NUMBER = 4;
125+
}
126+
function stuff(uint b) public returns (uint256) {
127+
unchecked {return NUMBER+b;}
128+
}
129+
}
130+
```
131+
132+
Will compare equal when compared with `--create` flag:
133+
134+
```shell
135+
solc --bin a.sol | tail -n1 > a.bin
136+
solc --bin b.sol | tail -n1 > b.bin
137+
cabal run exe:hevm equivalence -- --code-a-file a.bin --code-b-file b.bin --create
138+
```
139+
140+
Notice that we used `--bin` and not `--bin-runtime` for solc here. Also note that
141+
in case `NUMBER` is declared `public`, the two contracts will not be considered
142+
equivalent, since solidity will generate a getter for `NUMBER`, which will
143+
return 2/4 respectively.
144+
145+
## Further reading
146+
147+
For a tutorial on how to use `hevm equivalence`, see the [equivalence checking
148+
tutorial](symbolic-execution-tutorial.html).

‎doc/src/exec.md

+10-39
Original file line numberDiff line numberDiff line change
@@ -2,57 +2,28 @@
22

33
Run an EVM computation using specified parameters.
44

5-
```
5+
```plain
66
Usage: hevm exec [--code TEXT] [--calldata TEXT] [--address ADDR]
77
[--caller ADDR] [--origin ADDR] [--coinbase ADDR]
88
[--value W256] [--nonce WORD64] [--gas WORD64] [--number W256]
99
[--timestamp W256] [--basefee W256] [--priority-fee W256]
10-
[--gaslimit WORD64] [--gasprice W256] [--create]
10+
[--gaslimit WORD64] [--gasprice W256]
1111
[--maxcodesize W256] [--prev-randao W256] [--chainid W256]
12-
[--debug] [--trace] [--rpc TEXT] [--block W256] [--root STRING]
13-
[--project-type PROJECTTYPE]
14-
15-
Available options:
16-
-h,--help Show this help text
17-
--code TEXT Program bytecode
18-
--calldata TEXT Tx: calldata
19-
--address ADDR Tx: address
20-
--caller ADDR Tx: caller
21-
--origin ADDR Tx: origin
22-
--coinbase ADDR Block: coinbase
23-
--value W256 Tx: Eth amount
24-
--nonce WORD64 Nonce of origin
25-
--gas WORD64 Tx: gas amount
26-
--number W256 Block: number
27-
--timestamp W256 Block: timestamp
28-
--basefee W256 Block: base fee
29-
--priority-fee W256 Tx: priority fee
30-
--gaslimit WORD64 Tx: gas limit
31-
--gasprice W256 Tx: gas price
32-
--create Tx: creation
33-
--maxcodesize W256 Block: max code size
34-
--prev-randao W256 Block: prevRandao
35-
--chainid W256 Env: chainId
36-
--debug Debug printing of internal behaviour
37-
--trace Dump trace
38-
--rpc TEXT Fetch state from a remote node
39-
--block W256 Block state is be fetched from
40-
--root STRING Path to project root directory (default: . )
41-
--project-type PROJ Foundry or CombinedJSON project (default: Foundry)
42-
--assertion-type ASSERT Assertions as per Forge or DSTest (default: Forge)
12+
[--trace] [--rpc TEXT] [--block W256] ...
4313
```
4414

45-
Minimum required flags: either you must provide `--code` or you must both pass
46-
`--rpc` and `--address`.
15+
Concretely execute a given EVM bytecode with the specified parameters. Minimum
16+
required flags: either you must provide `--code` or you must both pass `--rpc`
17+
and `--address`. For a full listing of options, see `hevm exec --help`.
4718

4819
If the execution returns an output, it will be written
4920
to stdout. Exit code indicates whether the execution was successful or
5021
errored/reverted.
5122

52-
Simple example usage:
23+
## Simple example usage
5324

54-
```
55-
hevm exec --code 0x647175696e6550383480393834f3 --gas 0xff
25+
```shell
26+
$ hevm exec --code 0x647175696e6550383480393834f3 --gas 0xff
5627
"Return: 0x647175696e6550383480393834f3"
5728
```
5829

@@ -61,7 +32,7 @@ Virtual Machine will put `0x647175696e6550383480393834f3` in the RETURNDATA.
6132

6233
To execute a mainnet transaction:
6334

64-
```
35+
```shell
6536
# install seth as per
6637
# https://github.com/makerdao/developerguides/blob/master/devtools/seth/seth-guide/seth-guide.md
6738
$ export ETH_RPC_URL=https://mainnet.infura.io/v3/YOUR_API_KEY_HERE

‎doc/src/symbolic.md

+22-67
Original file line numberDiff line numberDiff line change
@@ -1,83 +1,24 @@
11
# `hevm symbolic`
22

3-
```shell
3+
```plain
44
Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR]
55
[--caller ADDR] [--origin ADDR] [--coinbase ADDR]
66
[--value W256] [--nonce WORD64] [--gas WORD64]
7-
[--number W256] [--timestamp W256] [--basefee W256]
8-
[--priority-fee W256] [--gaslimit WORD64] [--gasprice W256]
9-
[--create] [--maxcodesize W256] [--prev-randao W256]
10-
[--chainid W256] [--rpc TEXT] [--block W256]
11-
[--root STRING] [--project-type PROJECTTYPE]
12-
[--initial-storage INITIALSTORAGE] [--sig TEXT]
13-
[--arg STRING]... [--get-models] [--show-tree]
14-
[--show-reachable-tree] [--smttimeout NATURAL]
15-
[--max-iterations INTEGER] [--solver TEXT] [--smtdebug]
16-
[--assertions [WORD256]] [--ask-smt-iterations INTEGER]
17-
[--num-solvers NATURAL]
18-
[--loop-detection-heuristic LOOPHEURISTIC]
19-
20-
Available options:
21-
-h,--help Show this help text
22-
--code TEXT Program bytecode
23-
--calldata TEXT Tx: calldata
24-
--address ADDR Tx: address
25-
--caller ADDR Tx: caller
26-
--origin ADDR Tx: origin
27-
--coinbase ADDR Block: coinbase
28-
--value W256 Tx: Eth amount
29-
--nonce WORD64 Nonce of origin
30-
--gas WORD64 Tx: gas amount
31-
--number W256 Block: number
32-
--timestamp W256 Block: timestamp
33-
--basefee W256 Block: base fee
34-
--priority-fee W256 Tx: priority fee
35-
--gaslimit WORD64 Tx: gas limit
36-
--gasprice W256 Tx: gas price
37-
--create Tx: creation
38-
--maxcodesize W256 Block: max code size
39-
--prev-randao W256 Block: prevRandao
40-
--chainid W256 Env: chainId
41-
--rpc TEXT Fetch state from a remote node
42-
--block W256 Block state is be fetched from
43-
--root STRING Path to project root directory (default: . )
44-
--project-type PROJECTTYPE Foundry or CombinedJSON project
45-
--initial-storage INITIALSTORAGE
46-
Starting state for storage: Empty, Abstract (default
47-
Abstract)
48-
--sig TEXT Signature of types to decode / encode
49-
--arg STRING Values to encode
50-
--get-models Print example testcase for each execution path
51-
--show-tree Print branches explored in tree view
52-
--show-reachable-tree Print only reachable branches explored in tree view
53-
--smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300)
54-
--max-iterations INTEGER Number of times we may revisit a particular branching
55-
point. Default is 5. Setting to -1 allows infinite looping
56-
--solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla
57-
--smtdebug Print smt queries sent to the solver
58-
--assertions [WORD256] Comma separated list of solc panic codes to check for
59-
(default: user defined assertion violations only)
60-
--ask-smt-iterations INTEGER
61-
Number of times we may revisit a particular branching
62-
point before we consult the smt solver to check
63-
reachability (default: 1) (default: 1)
64-
--num-solvers NATURAL Number of solver instances to use (default: number of
65-
cpu cores)
66-
--loop-detection-heuristic LOOPHEURISTIC
67-
Which heuristic should be used to determine if we are
68-
in a loop: StackBased (default) or Naive
69-
(default: StackBased)
7+
[--number W256] [--timestamp W256] [--basefee W256] ..
708
```
719

72-
Run a symbolic execution against the given parameters, searching for assertion violations.
10+
Run a symbolic execution against the given parameters, searching for assertion
11+
violations. For a full listing of options, see `hevm symbolic --help`.
7312

74-
Counterexamples will be returned for any reachable assertion violations. Where
13+
Counterexamples are returned for any reachable assertion violations. Where
7514
an assertion violation is defined as either an execution of the invalid opcode
7615
(`0xfe`), or a revert with a message of the form
7716
`abi.encodeWithSelector('Panic(uint256)', errCode)` with `errCode` being one of
7817
the predefined solc assertion codes defined
7918
[here](https://docs.soliditylang.org/en/latest/control-structures.html#panic-via-assert-and-error-via-require).
8019

20+
## Arithmetic overflow
21+
8122
By default hevm ignores assertion violations that result from arithmetic
8223
overflow (`Panic(0x11)`), although this behaviour can be customised via the
8324
`--assertions` flag. For example, the following will return counterexamples for
@@ -87,7 +28,10 @@ arithmetic overflow (`0x11`) and user defined assertions (`0x01`):
8728
hevm symbolic --code $CODE --assertions '[0x01, 0x11]'
8829
```
8930

90-
The default value for `calldata` and `caller` are symbolic values, but can be specialized to concrete functions with their corresponding flags.
31+
The default value for `calldata` and `caller` are symbolic values, but can be
32+
specialized to concrete functions with their corresponding flags.
33+
34+
## Specializing calldata
9135

9236
One can also specialize specific arguments to a function signature, while
9337
leaving others abstract. If `--sig` is given, calldata is assumed to be of the
@@ -126,11 +70,15 @@ The default timeout for SMT queries is no timeout. If your program is taking
12670
longer than a couple of minutes to run, you can experiment with configuring the
12771
timeout to somewhere around 10s by doing `--smttimeout 10000`
12872

73+
## Storage
74+
12975
Storage can be initialized in two ways:
13076

13177
- `Empty`: all storage slots for all contracts are initialized to zero
13278
- `Abstract`: all storage slots are initialized as unconstrained abstract values
13379

80+
## Exploration strategy
81+
13482
`hevm` uses an eager approach for symbolic execution, meaning that it will
13583
first attempt to explore all branches in the program (without querying the smt
13684
solver to check if they are reachable or not). Once the full execution tree has
@@ -143,3 +91,10 @@ iterations (controlled by the `--ask-smt-iterations` flag), the solver will be
14391
invoked to check whether a given loop branch is reachable. In cases where the
14492
number of loop iterations is known in advance, you may be able to speed up
14593
execution by setting this flag to an appropriate value.
94+
95+
## Further reading
96+
97+
For a tutorial on symbolic execution with `hevm`, see the [the page
98+
here](symbolic-execution-tutorial.html).
99+
An older blog post on symbolic execution with `hevm` can be found
100+
[here](https://fv.ethereum.org/2020/07/28/symbolic-hevm-release).

0 commit comments

Comments
 (0)