Add more technical Echidna documentation #357
Conversation
| # Configuration options | ||
|
|
||
| <!-- To left align the tables --> | ||
| <style>table {margin: 0}</style> |
There was a problem hiding this comment.
This line is visible in the md, for some reason 🤔
There was a problem hiding this comment.
I'll see if there's any neater way in mdbook to apply css to just one page
There was a problem hiding this comment.
I did a trick there to keep the CSS out of the markdown.
| | ---- | ------- | ------------ | ---------------- | | ||
| | Int | `50000` | \* | `--test-limit N` | | ||
|
|
||
| Number of sequences of transactions to generate during testing. |
There was a problem hiding this comment.
I think these are transactions, not sequences of transactions.
| | ---- | ------- | ------------ | -------------- | | ||
| | Int | `100` | \* | `--seq-len N` | | ||
|
|
||
| Number of transactions to generate during testing. |
There was a problem hiding this comment.
This needs a better explanation: we need to explain that every N transaction, the VM is reset to the state after contract deployment. This also limits the size of each sequence in the corpus.
| | ---- | ------- | ------------ | -------------- | | ||
| | Int | `null` | \* | `--timeout N` | | ||
|
|
||
| Campaign timeout, in seconds. By default it is not time-limited. |
There was a problem hiding this comment.
Explain how testLimit and timeout interacts.
| | --------- | ----------------------------------- | ------------ | -------------- | | ||
| | [Address] | `["0x10000", "0x20000", "0x30000"]` | \* | `--sender` | | ||
|
|
||
| List of addresses to (randomly) use for the transactions sent during testing. |
There was a problem hiding this comment.
Explain how the sender is used for normal transactions / assertions, instead of properties.
| | ------- | ----------- | ------------ | | ||
| | Address | `"0x10000"` | \* | | ||
|
|
||
| Address of the sender of the property to test. |
| | ---- | -------------------------------------- | ------------ | | ||
| | Int | `12500000` (current max gas per block) | \* | | ||
|
|
||
| Maximum amount of gas to consume when running function properties. |
There was a problem hiding this comment.
Explain that out of gas will cause the property to fail
| | ---- | -------------------------------------- | ------------ | | ||
| | Int | `12500000` (current max gas per block) | \* | | ||
|
|
||
| Maximum amount of gas to consume when running random transactions. |
There was a problem hiding this comment.
Explain that out of gas will NOT cause assertions to fail.
| | ---- | ------- | ------------ | | ||
| | Int | `30` | 2.2.4+ | | ||
|
|
||
| Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true. |
There was a problem hiding this comment.
If using z3, this timeout is not global, but per query (and this is a very important detail 😆)
| | ---- | ------- | ------------ | | ||
| | Int | `1` | 2.2.4+ | | ||
|
|
||
| Number of SMT solvers used in symbolic execution. Only relevant if `symExec` is |
There was a problem hiding this comment.
Clarify that there is only a single symexec worker, but we can have multiple threads to solve queries.
| | ------ | ------- | ------------ | --------------- | | ||
| | String | `null` | 2.2.0+ | `--rpc-block N` | | ||
|
|
||
| Block number to use when fetching over RPC. |
There was a problem hiding this comment.
Add alternative ENV variable?
| | ------ | ------- | ------------ | --------------- | | ||
| | String | `null` | 2.2.0+ | `--rpc-url URL` | | ||
|
|
||
| URL to fetch contracts over RPC. |
There was a problem hiding this comment.
Add alternative ENV variable?
| | ---- | ------- | ------------ | | ||
| | Int | `0` | \* | | ||
|
|
||
| Initial Ether balance of `contractAddr`. |
There was a problem hiding this comment.
Link the tutorial on the handling of ether
The initial set of configuration parameters was taken from https://github.com/crytic/echidna/wiki/Config