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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,53 +1,149 @@ | ||
| # `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`. | ||
|
|
||
| ## 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.txt --code-b-file b.txt | ||
msooseth marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| ``` | ||
|
|
||
| ## 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. | ||
|
|
||
| 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
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)?