Improve docs #690
+255
−195
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,50 @@ | ||
| # Common options | ||
|
|
||
| The subcommands of hevm present a number | ||
| of common options. Here, we document these options in detail. | ||
|
|
||
| ## Maximum Buffer Size, ``--max-buf-size`` | ||
|
|
||
| The buffers in hevm are limited to a maximum size of 2^N bytes, where N is by | ||
| default 64, but adjustable via the `--max-buf-size` flag. This helps to prevent | ||
| the system from creating buffers that are too large and would exceed the gas | ||
| limit. Limiting this value further to e.g. 20 can help to force the system to | ||
| generate counterexamples that are easier to examine and understand. | ||
|
|
||
| ## Choice of Solver, ``--solver`` | ||
|
|
||
| hevm can use any SMT solver that supports the AUFBV theory and incremental | ||
| solving. Currently, z3, cvc5, and bitwuzla's interfaces are implemented. While | ||
| any of these solvers work, we recommend using bitwuzla as it is in general | ||
| extremely fast, almost always significantly faster than e.g. z3. | ||
|
|
||
| ## Number of Solvers, ``--num-solvers`` | ||
|
|
||
| hevm can run multiple solvers in parallel and will run as many solvers as it | ||
| detects the number of CPU cores on the machine. However, in some cases, that | ||
| may lead to memory outs, in case the solver happens to get queries that are | ||
| memory-intensive. In these cases, the number of solvers can be limited to a a | ||
| specific (low) number via the `--num-solvers` flag. | ||
|
|
||
| ## Promising no reentrancy, ``--promise-no-reent`` | ||
|
|
||
| hevm can be instructed to assume that no reentrancy will occur during the | ||
| execution of the contract. This is currently neccessary to fully explore | ||
| certain contracts. This is because value transfer is usually done via a `CALL`, | ||
| which can be reentrant. By promising no reentrancy, the system can assume that | ||
| no reentrancy will occur and can explore the contract more fully. | ||
|
|
||
| ## Timeout for SMT queries, ``--smttimeout`` | ||
|
|
||
| Some queries take too long. With a timeout, we ensure that hevm eventually | ||
| terminates. However, endstates where the timeout was reached are considered | ||
| inditerminate, and will lead to a `WARNING` in the output. It is worthwhile | ||
| trying to switch to a different SMT solver such as bitwuzla, or increasing the | ||
| timeout if this happens. | ||
|
|
||
| ## Loop Iteration Limit, ``--ask-smt-iterations`` | ||
|
|
||
| Loops in the code cause a challenge to symbolic execution framework. In order | ||
| to not run indefinitely, hevm will only explore a certain number of iterations | ||
| of a loop before consideing abandoning the exploration of that branch. This | ||
| number can be set via the `--ask-smt-iterations` flag. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,53 +1,152 @@ | ||
| # `hevm equivalence` | ||
|
|
||
| ```plain | ||
| Usage: hevm equivalence [--code-a TEXT] [--code-b TEXT] [--code-a-file STRING] | ||
| [--code-b-file STRING] [--sig TEXT] [--arg STRING]... | ||
| [--calldata TEXT] [--smttimeout NATURAL] | ||
| [--max-iterations INTEGER] [--solver TEXT] | ||
| [--num-solvers NATURAL] ... | ||
| ``` | ||
|
|
||
| Symbolically execute both the code given in `--code-a` and `--code-b` and try | ||
| to prove equivalence between their outputs and storages. For a full listing of | ||
| options, see `hevm equivalence --help`. For common options, see | ||
| [here](./common-options.md). | ||
|
|
||
| ## Simple example usage | ||
|
|
||
| ```shell | ||
| $ solc --bin-runtime "contract1.sol" | tail -n1 > a.bin | ||
| $ solc --bin-runtime "contract2.sol" | tail -n1 > b.bin | ||
| $ hevm equivalence --code-a-file a.bin --code-b-file b.bin | ||
| ``` | ||
|
|
||
| ## Calldata size limits | ||
|
|
||
| If `--sig` is given, calldata is assumed to take the form of the function | ||
| given. If `--calldata` is provided, a specific, concrete calldata is used. If | ||
| neither is provided, a fully abstract calldata of at most `2**64` byte is | ||
| assumed. Note that a `2**64` byte calldata would go over the gas limit, and | ||
| hence should cover all meaningful cases. You can limit the buffer size via | ||
| `--max-buf-size`, which sets the exponent of the size, i.e. 10 would limit the | ||
|
There was a problem hiding this comment. Should we call this option There was a problem hiding this comment. Good point! Yes, we should. Fixing. There was a problem hiding this comment. Ah wait... this actually applies to other buffers too, like here: symCalldata :: App m => Text -> [AbiType] -> [String] -> Expr Buf -> m (Expr Buf, [Prop])
symCalldata sig typesignature concreteArgs base = do
conf <- readConfig
let
args = concreteArgs <> replicate (length typesignature - length concreteArgs) "<symbolic>"
mkArg :: AbiType -> String -> Int -> CalldataFragment
mkArg typ "<symbolic>" n = symAbiArg (T.pack $ "arg" <> show n) typ
mkArg typ arg _ =
case makeAbiValue typ arg of
AbiUInt _ w -> St [] . Lit . into $ w
AbiInt _ w -> St [] . Lit . unsafeInto $ w
AbiAddress w -> St [] . Lit . into $ w
AbiBool w -> St [] . Lit $ if w then 1 else 0
_ -> internalError "TODO"
calldatas = zipWith3 mkArg typesignature args [1..]
(cdBuf, props) = combineFragments calldatas base
withSelector = writeSelector cdBuf sig
sizeConstraints
= (Expr.bufLength withSelector .>= cdLen calldatas)
.&& (Expr.bufLength withSelector .< (Lit (2 ^ conf.maxBufSize)))and also the data that an unknown contract sends back to us. We should explain this... There was a problem hiding this comment. OK, I am gonna talk about this more in the docs and try to give a better explanation in the |
||
| calldata to `2**10` bytes. | ||
|
|
||
| ## What constitutes equivalence | ||
|
|
||
| The equivalence checker considers two contracts equivalent if given the | ||
| same calldata they: | ||
| - return the same value | ||
| - have the same storage | ||
| - match on the success/failure of the execution | ||
| Importantly, logs are *not* considered in the equivalence check. Hence, | ||
| it is possible that two contracts are considered equivalent by `hevm equivalence` but | ||
| they emit different log items. Furthermore, gas is explicitly not considered, | ||
| as in many cases, the point of the equivalence check is to ensure that the | ||
| contracts are functionally equivalent, but one of them is more gas efficient. | ||
|
|
||
| For example, two contracts that are: | ||
|
|
||
| ``` | ||
| PUSH1 3 | ||
| ``` | ||
|
|
||
| And | ||
|
|
||
| ``` | ||
| PUSH1 4 | ||
| ``` | ||
|
|
||
| Are considered *equivalent*, because they don't put anything in the return | ||
| data, are not different in their success/fail attribute, and don't touch | ||
| storage. However, these two are considered different: | ||
|
|
||
| ``` | ||
| PUSH1 3 | ||
| PUSH1 0x20 | ||
| MSTORE | ||
| PUSH1 0x40 | ||
| PUSH1 0x00 | ||
| RETURN | ||
| ``` | ||
|
|
||
| and: | ||
|
|
||
|
|
||
| ``` | ||
| PUSH1 4 | ||
| PUSH1 0x20 | ||
| MSTORE | ||
| PUSH1 0x40 | ||
| PUSH1 0x00 | ||
| RETURN | ||
| ``` | ||
|
|
||
| Since one of them returns a 3 and the other a 4. We also consider contracts different when | ||
| they differ in success/fail. So these two contracts: | ||
|
|
||
| ``` | ||
| PUSH1 0x00 | ||
| PUSH1 0x00 | ||
| RETURN | ||
| ``` | ||
|
|
||
| and: | ||
|
|
||
| ``` | ||
| PUSH1 0x00 | ||
| PUSH1 0x00 | ||
| REVERT | ||
| ``` | ||
|
|
||
| Are considered different, as one of them reverts (i.e. fails) and the other | ||
| succeeds. | ||
|
|
||
| ## Creation code equivalence | ||
|
|
||
| If you want to check the equivalence of not just the runtime code, but also the | ||
| creation code of two contracts, you can use the `--creation` flag. For example | ||
| these two contracts: | ||
|
|
||
| ```solidity | ||
| contract C { | ||
| uint private immutable NUMBER; | ||
| constructor(uint a) { | ||
| NUMBER = 2; | ||
| } | ||
| function stuff(uint b) public returns (uint256) { | ||
| unchecked{return 2+NUMBER+b;} | ||
| } | ||
| } | ||
| ``` | ||
|
|
||
| And: | ||
|
|
||
| ```solidity | ||
| contract C { | ||
| uint private immutable NUMBER; | ||
| constructor(uint a) { | ||
| NUMBER = 4; | ||
| } | ||
| function stuff(uint b) public returns (uint256) { | ||
| unchecked {return NUMBER+b;} | ||
| } | ||
| } | ||
| ``` | ||
|
|
||
| Will compare equal when compared with `--create` flag: | ||
|
|
||
| ```shell | ||
| solc --bin a.sol | tail -n1 > a.bin | ||
| solc --bin b.sol | tail -n1 > b.bin | ||
| cabal run exe:hevm equivalence -- --code-a-file a.bin --code-b-file b.bin --create | ||
| ``` | ||
|
|
||
| Notice that we used `--bin` and not `--bin-runtime` for solc here. Also note that | ||
| in case `NUMBER` is declared `public`, the two contracts will not be considered | ||
| equivalent, since solidity will generate a getter for `NUMBER`, which will | ||
| return 2/4 respectively. | ||
|
|
||
| ## Further reading | ||
|
|
||
| For a tutorial on how to use `hevm equivalence`, see the [equivalence checking | ||
| tutorial](symbolic-execution-tutorial.html). | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What does
...mean here?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was trying to imply that there are more options... maybe I should remove? I don't want to list them all, I think it's not that useful? What do you think?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not document all the options?
It seems unusual to omit some of them.
Unless you can argue they belong to separate categories, like "for users" and "for developers"?
And you want to list only those important for the users.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, we keep adding some and then not documenting them in the MD docs. I am wondering what' the best thing to do here. Of course I can run
--helpand copy-paste but I'm not sure that's the best. I am trying to improve the documentation, not make it perfect :D Currently, it's quite out of date. I am not sure what's best. The full--helpis also way too verbose and I don't think it's too helpful. They can always run it themselves. What do you think? Should I just copy-paste the--helpand then explain the options as it is now (with common-options.md to explain the common ones)?