From 7059e812d69d4474eb93f32bfa6c3b5571510715 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Fri, 3 May 2024 16:26:38 -0300
Subject: [PATCH 1/9] Migrate configuration from Echidna wiki

---
 SUMMARY.md                                |   1 +
 program-analysis/echidna/configuration.md | 247 ++++++++++++++++++++++
 2 files changed, 248 insertions(+)
 create mode 100644 program-analysis/echidna/configuration.md

diff --git a/SUMMARY.md b/SUMMARY.md
index 83b39023..67a6edd3 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -96,6 +96,7 @@
       - [Interacting with off-chain data via FFI cheatcode](./program-analysis/echidna/advanced/interacting-with-offchain-data-via-ffi.md)
     - [Fuzzing tips](./program-analysis/echidna/fuzzing_tips.md)
     - [Frequently Asked Questions](./program-analysis/echidna/frequently_asked_questions.md)
+    - [Configuration options](./program-analysis/echidna/configuration.md)
     - [Exercises](./program-analysis/echidna/exercises/README.md)
       - [Exercise 1](./program-analysis/echidna/exercises/Exercise-1.md)
       - [Exercise 2](./program-analysis/echidna/exercises/Exercise-2.md)
diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
new file mode 100644
index 00000000..e071b4c7
--- /dev/null
+++ b/program-analysis/echidna/configuration.md
@@ -0,0 +1,247 @@
+# Configuration options
+
+<style>table {margin: 0}</style>
+
+The following is a list of all the options that may be provided in the Echidna configuration file.
+
+## `testMode`
+
+Type | Default | Available in
+-----|---------|-------------
+String | `"property"` | *
+
+The test mode to run. It should be one of the following items:
+
+* `"property"`: Run user-defined property tests.
+* `"assertion"`: Detect assertion failures (previously `checkAsserts`).
+* `"optimization"`: Find the maximum value for a function.
+* `"overflow"`: Detect integer overflows (only available in Solidity 0.8.0 or greater).
+* `"exploration"`: Run contract code without executing any tests.
+
+## `testLimit`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `50000` | *
+
+Number of sequences of transactions to generate during testing.
+
+## `seqLen`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `100`   | *
+
+Number of transactions to generate during testing.
+
+## `shrinkLimit`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `5000`  | *
+
+Number of attempts to shrink a failing sequence of transactions.
+
+## `contractAddr`
+
+Type | Default | Available in
+-----|---------|-------------
+Address | `"0x00a329c0648769a73afac7f9381e08fb43dbea72"` | *
+
+Address to deploy the contract to test.
+
+## `coverage`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `true`  | *
+
+Enable the use of coverage-guided fuzzing and corpus collection.
+
+## `corpusDir`
+
+Type | Default | Available in
+-----|---------|-------------
+String | `null` | *
+
+Directory to save the corpus collected (requires coverage enabled).
+
+## `deployer`
+
+Type | Default | Available in
+-----|---------|-------------
+Address | `"0x30000"` | *
+
+Address of the deployer of the contract to test.
+
+## `deployContracts`
+
+Type | Default | Available in
+-----|---------|-------------
+[⁠[⁠Address, String⁠]⁠] | `[]` | *
+
+Addresses and contract names to deploy using the available source code. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
+
+## `deployBytecodes`
+
+Type | Default | Available in
+-----|---------|-------------
+[⁠[⁠Address, String⁠]⁠] | `[]` | *
+
+Addresses and bytecodes to deploy. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
+
+## `sender`
+
+Type | Default | Available in
+-----|---------|-------------
+[Address] | `["0x10000", "0x20000", "0x30000"]` | *
+
+List of addresses to (randomly) use for the transactions sent during testing.
+
+## `psender`
+
+Type | Default | Available in
+-----|---------|-------------
+Address | `"0x10000"` | *
+
+Address of the sender of the property to test.
+
+## `prefix`
+
+Type | Default | Available in
+-----|---------|-------------
+String | `"echidna_"` | *
+
+Prefix of the function names used as properties in the contract to test.
+
+## `propMaxGas`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `12500000` (current max gas per block) | *
+
+Maximum amount of gas to consume when running function properties.
+
+## `testMaxGas`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `12500000` (current max gas per block) | *
+
+Maximum amount of gas to consume when running random transactions.
+
+## `maxGasprice`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `0`     | *
+
+Maximum amount of gas price to randomly use in transactions. Do not change it unless you absolutely need it.
+
+## `maxTimeDelay`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `604800`  (one week) | *
+
+Maximum amount of seconds of delay between transactions.
+
+## `maxBlockDelay`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `60480` | *
+
+Maximum amount of block numbers between transactions.
+
+## `solcArgs`
+
+Type | Default | Available in
+-----|---------|-------------
+String | `""` | *
+
+Additional arguments to use in `solc` for compiling the contract to test.
+
+## `cryticArgs`
+
+Type | Default | Available in
+-----|---------|-------------
+[String] | `[]` | *
+
+Additional arguments to use in `crytic-compile` for compiling the contract to test.
+
+## `quiet`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `false` | *
+
+Hide `solc` stderr output and additional information during the testing.
+
+## `format`
+
+Type | Default | Available in
+-----|---------|-------------
+String | `null` | *
+
+Select a textual output format. By default, interactive TUI is run or text if a terminal is absent.
+
+* `"text"`: simple textual interface.
+* `"json"`: JSON output.
+* `"none"`: no output.
+
+## `balanceContract`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `0`     | *
+
+Initial Ether balance of `contractAddr`.
+
+## `balanceAddr`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `0xffffffff` | *
+
+Initial Ether balance of `deployer` and each of the `sender` accounts.
+
+## `maxValue`
+
+Type | Default | Available in
+-----|---------|-------------
+Int | `100000000000000000000` (100 ETH) | *
+
+Max amount of value in each randomly generated transaction.
+
+## `testDestruction`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `false` | *
+
+Add a special test that fails if a contract is self-destructed.
+
+## `stopOnFail`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `false` | *
+
+Stops the fuzzing campaign when the first test fails.
+
+## `allContracts`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `false` | *
+
+Makes Echidna fuzz the provided test contracts and any other deployed contract whose ABI is known at runtime.
+
+## `allowFFI`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `false` | 2.1.0+
+
+Allows the use of the HEVM `ffi` cheatcode.

From d633fb36e6cdba40a0c3eb913c99cd40254ed12c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Fri, 3 May 2024 17:13:13 -0300
Subject: [PATCH 2/9] Add CLI equivalent flags and version information

---
 program-analysis/echidna/configuration.md | 76 +++++++++++------------
 1 file changed, 38 insertions(+), 38 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index e071b4c7..d9f33688 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -6,9 +6,9 @@ The following is a list of all the options that may be provided in the Echidna c
 
 ## `testMode`
 
-Type | Default | Available in
------|---------|-------------
-String | `"property"` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+String | `"property"` | * | `--test-mode MODE`
 
 The test mode to run. It should be one of the following items:
 
@@ -20,33 +20,33 @@ The test mode to run. It should be one of the following items:
 
 ## `testLimit`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `50000` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | `50000` | *            | `--test-limit N`
 
 Number of sequences of transactions to generate during testing.
 
 ## `seqLen`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `100`   | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | `100`   | *            | `--seq-len N`
 
 Number of transactions to generate during testing.
 
 ## `shrinkLimit`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `5000`  | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | `5000`  | *            | `-shrink-limit N`
 
 Number of attempts to shrink a failing sequence of transactions.
 
 ## `contractAddr`
 
-Type | Default | Available in
------|---------|-------------
-Address | `"0x00a329c0648769a73afac7f9381e08fb43dbea72"` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Address | `"0x00a329c0648769a73af` `ac7f9381e08fb43dbea72"` | * | `--contract-addr ADDR`
 
 Address to deploy the contract to test.
 
@@ -60,17 +60,17 @@ Enable the use of coverage-guided fuzzing and corpus collection.
 
 ## `corpusDir`
 
-Type | Default | Available in
------|---------|-------------
-String | `null` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+String | `null` | * | `--corpus-dir PATH`
 
 Directory to save the corpus collected (requires coverage enabled).
 
 ## `deployer`
 
-Type | Default | Available in
------|---------|-------------
-Address | `"0x30000"` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Address | `"0x30000"` | * | `--deployer`
 
 Address of the deployer of the contract to test.
 
@@ -78,7 +78,7 @@ Address of the deployer of the contract to test.
 
 Type | Default | Available in
 -----|---------|-------------
-[⁠[⁠Address, String⁠]⁠] | `[]` | *
+[⁠[⁠Address, String⁠]⁠] | `[]` | 2.0.2+
 
 Addresses and contract names to deploy using the available source code. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
 
@@ -86,15 +86,15 @@ Addresses and contract names to deploy using the available source code. The depl
 
 Type | Default | Available in
 -----|---------|-------------
-[⁠[⁠Address, String⁠]⁠] | `[]` | *
+[⁠[⁠Address, String⁠]⁠] | `[]` | 2.0.2+
 
 Addresses and bytecodes to deploy. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
 
 ## `sender`
 
-Type | Default | Available in
------|---------|-------------
-[Address] | `["0x10000", "0x20000", "0x30000"]` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+[Address] | `["0x10000", "0x20000", "0x30000"]` | * | `--sender`
 
 List of addresses to (randomly) use for the transactions sent during testing.
 
@@ -156,17 +156,17 @@ Maximum amount of block numbers between transactions.
 
 ## `solcArgs`
 
-Type | Default | Available in
------|---------|-------------
-String | `""` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+String | `""` | * | `--solc-args ARGS`
 
 Additional arguments to use in `solc` for compiling the contract to test.
 
 ## `cryticArgs`
 
-Type | Default | Available in
------|---------|-------------
-[String] | `[]` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+[String] | `[]` | * | `--crytic-args ARGS`
 
 Additional arguments to use in `crytic-compile` for compiling the contract to test.
 
@@ -180,9 +180,9 @@ Hide `solc` stderr output and additional information during the testing.
 
 ## `format`
 
-Type | Default | Available in
------|---------|-------------
-String | `null` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+String | `null` | * | `--format FORMAT`
 
 Select a textual output format. By default, interactive TUI is run or text if a terminal is absent.
 
@@ -232,9 +232,9 @@ Stops the fuzzing campaign when the first test fails.
 
 ## `allContracts`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `false` | *
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Bool | `false` | 2.1.0+ (previously `multi-abi`) | `--all-contracts`
 
 Makes Echidna fuzz the provided test contracts and any other deployed contract whose ABI is known at runtime.
 

From 489ad0a89a0bd739e820d0fb9553c8846655d54b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Fri, 3 May 2024 17:14:50 -0300
Subject: [PATCH 3/9] Document recent config additions

---
 program-analysis/echidna/configuration.md | 94 +++++++++++++++++++++++
 1 file changed, 94 insertions(+)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index d9f33688..ab42d6bf 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -245,3 +245,97 @@ Type | Default | Available in
 Bool | `false` | 2.1.0+
 
 Allows the use of the HEVM `ffi` cheatcode.
+
+## `rpcUrl`
+
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+String | `null` | 2.2.0+ | `--rpc-url URL`
+
+URL to fetch contracts over RPC.
+
+## `rpcBlock`
+
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+String | `null` | 2.2.0+ | `--rpc-block N`
+
+Block number to use when fetching over RPC.
+
+## `coverageFormats`
+
+Type | Default | Available in
+-----|---------|-------------
+[String] | `["txt","html","lcov"]` | 2.2.0+
+
+List of file formats to save coverage reports in; default is all possible
+formats.
+
+## `workers`
+
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | `1`     | 2.2.0+       | `--workers`
+
+Number of workers.
+
+## `server`
+
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | `null`  | 2.2.2+       | `--server PORT`
+
+Run events server on the given port.
+
+## `symExec`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `false` | 2.2.4+
+
+Whether to add an additional symbolic execution worker.
+
+## `symExecConcolic`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `true`  | 2.2.4+
+
+Whether symbolic execution will be concolic (vs full symbolic execution). Only
+relevant if `symExec` is true.
+
+## `symExecNSolvers`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `1`     | 2.2.4+
+
+Number of SMT solvers used in symbolic execution. Only relevant if `symExec` is
+true.
+
+## `symExecTimeout`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `30`    | 2.2.4+
+
+Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true.
+
+## `symExecMaxIters`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `10`    | 2.2.4+
+
+Number of times we may revisit a particular branching point. Only relevant if
+`symExec` is true and `symExecConcolic` is false.
+
+## `symExecAskSMTIters`
+
+Type | Default | Available in
+-----|---------|-------------
+Int  | `1`     | 2.2.4+
+
+Number of times we may revisit a particular branching point before we consult
+the smt solver to check reachability. Only relevant if `symExec` is true and
+`symExecConcolic` is false.

From 1d1af8d0c8414589b2bc2e82f09492e97837537c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Fri, 3 May 2024 18:08:19 -0300
Subject: [PATCH 4/9] Document further missing options

---
 program-analysis/echidna/configuration.md | 44 +++++++++++++++++++++--
 1 file changed, 42 insertions(+), 2 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index ab42d6bf..e5581fa2 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -1,8 +1,12 @@
 # Configuration options
 
+<!-- To left align the tables -->
 <style>table {margin: 0}</style>
-
-The following is a list of all the options that may be provided in the Echidna configuration file.
+The following is a list of all the options that may be provided in the Echidna
+configuration file. Whenever an option can also be set via the command line, the
+CLI equivalent flag is provided as a reference. Some flags are relatively new
+and only available on recent Echidna builds; in those cases, the minimum Echidna
+version required to use the feature is indicated in the table.
 
 ## `testMode`
 
@@ -34,6 +38,22 @@ Int  | `100`   | *            | `--seq-len N`
 
 Number of transactions to generate during testing.
 
+## `timeout`
+
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | `null`  | *            | `--timeout N`
+
+Campaign timeout, in seconds. By default it is not time-limited.
+
+## `seed`
+
+Type | Default | Available in | CLI equivalent
+-----|---------|--------------|---------------
+Int  | random  | *            | `--seed N`
+
+Seed used for random value generation. By default it is a random integer.
+
 ## `shrinkLimit`
 
 Type | Default | Available in | CLI equivalent
@@ -238,6 +258,26 @@ Bool | `false` | 2.1.0+ (previously `multi-abi`) | `--all-contracts`
 
 Makes Echidna fuzz the provided test contracts and any other deployed contract whose ABI is known at runtime.
 
+## `filterBlacklist`
+
+Type | Default | Available in
+-----|---------|-------------
+Bool | `true`  | *
+
+Allows Echidna to avoid calling (when set to true) or only call (when set to
+false) a set of functions. The function allowlist or denylist should be provided
+in `filterFunctions`.
+
+## `filterFunctions`
+
+Type | Default | Available in
+-----|---------|-------------
+[String] | `[]` | *
+
+Configures the function allowlist or denylist from `filterBlacklist`. The list
+should contain strings in the format of
+`"Contract.functionName(uint256,uint256)"` following the signature convention.
+
 ## `allowFFI`
 
 Type | Default | Available in

From 62df2584718023b70d9dd64054309564d64f8c38 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Fri, 3 May 2024 18:15:15 -0300
Subject: [PATCH 5/9] Lint changes

---
 program-analysis/echidna/configuration.md | 281 +++++++++++-----------
 1 file changed, 141 insertions(+), 140 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index e5581fa2..f031fb84 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -2,6 +2,7 @@
 
 <!-- To left align the tables -->
 <style>table {margin: 0}</style>
+
 The following is a list of all the options that may be provided in the Echidna
 configuration file. Whenever an option can also be set via the command line, the
 CLI equivalent flag is provided as a reference. Some flags are relatively new
@@ -10,259 +11,259 @@ version required to use the feature is indicated in the table.
 
 ## `testMode`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-String | `"property"` | * | `--test-mode MODE`
+| Type   | Default      | Available in | CLI equivalent     |
+| ------ | ------------ | ------------ | ------------------ |
+| String | `"property"` | \*           | `--test-mode MODE` |
 
 The test mode to run. It should be one of the following items:
 
-* `"property"`: Run user-defined property tests.
-* `"assertion"`: Detect assertion failures (previously `checkAsserts`).
-* `"optimization"`: Find the maximum value for a function.
-* `"overflow"`: Detect integer overflows (only available in Solidity 0.8.0 or greater).
-* `"exploration"`: Run contract code without executing any tests.
+- `"property"`: Run user-defined property tests.
+- `"assertion"`: Detect assertion failures (previously `checkAsserts`).
+- `"optimization"`: Find the maximum value for a function.
+- `"overflow"`: Detect integer overflows (only available in Solidity 0.8.0 or greater).
+- `"exploration"`: Run contract code without executing any tests.
 
 ## `testLimit`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | `50000` | *            | `--test-limit N`
+| Type | Default | Available in | CLI equivalent   |
+| ---- | ------- | ------------ | ---------------- |
+| Int  | `50000` | \*           | `--test-limit N` |
 
 Number of sequences of transactions to generate during testing.
 
 ## `seqLen`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | `100`   | *            | `--seq-len N`
+| Type | Default | Available in | CLI equivalent |
+| ---- | ------- | ------------ | -------------- |
+| Int  | `100`   | \*           | `--seq-len N`  |
 
 Number of transactions to generate during testing.
 
 ## `timeout`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | `null`  | *            | `--timeout N`
+| Type | Default | Available in | CLI equivalent |
+| ---- | ------- | ------------ | -------------- |
+| Int  | `null`  | \*           | `--timeout N`  |
 
 Campaign timeout, in seconds. By default it is not time-limited.
 
 ## `seed`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | random  | *            | `--seed N`
+| Type | Default | Available in | CLI equivalent |
+| ---- | ------- | ------------ | -------------- |
+| Int  | random  | \*           | `--seed N`     |
 
 Seed used for random value generation. By default it is a random integer.
 
 ## `shrinkLimit`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | `5000`  | *            | `-shrink-limit N`
+| Type | Default | Available in | CLI equivalent    |
+| ---- | ------- | ------------ | ----------------- |
+| Int  | `5000`  | \*           | `-shrink-limit N` |
 
 Number of attempts to shrink a failing sequence of transactions.
 
 ## `contractAddr`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Address | `"0x00a329c0648769a73af` `ac7f9381e08fb43dbea72"` | * | `--contract-addr ADDR`
+| Type    | Default                                           | Available in | CLI equivalent         |
+| ------- | ------------------------------------------------- | ------------ | ---------------------- |
+| Address | `"0x00a329c0648769a73af` `ac7f9381e08fb43dbea72"` | \*           | `--contract-addr ADDR` |
 
 Address to deploy the contract to test.
 
 ## `coverage`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `true`  | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `true`  | \*           |
 
 Enable the use of coverage-guided fuzzing and corpus collection.
 
 ## `corpusDir`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-String | `null` | * | `--corpus-dir PATH`
+| Type   | Default | Available in | CLI equivalent      |
+| ------ | ------- | ------------ | ------------------- |
+| String | `null`  | \*           | `--corpus-dir PATH` |
 
 Directory to save the corpus collected (requires coverage enabled).
 
 ## `deployer`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Address | `"0x30000"` | * | `--deployer`
+| Type    | Default     | Available in | CLI equivalent |
+| ------- | ----------- | ------------ | -------------- |
+| Address | `"0x30000"` | \*           | `--deployer`   |
 
 Address of the deployer of the contract to test.
 
 ## `deployContracts`
 
-Type | Default | Available in
------|---------|-------------
-[⁠[⁠Address, String⁠]⁠] | `[]` | 2.0.2+
+| Type                    | Default | Available in |
+| ----------------------- | ------- | ------------ |
+| [⁠[⁠Address, String⁠]⁠] | `[]`    | 2.0.2+       |
 
 Addresses and contract names to deploy using the available source code. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
 
 ## `deployBytecodes`
 
-Type | Default | Available in
------|---------|-------------
-[⁠[⁠Address, String⁠]⁠] | `[]` | 2.0.2+
+| Type                    | Default | Available in |
+| ----------------------- | ------- | ------------ |
+| [⁠[⁠Address, String⁠]⁠] | `[]`    | 2.0.2+       |
 
 Addresses and bytecodes to deploy. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
 
 ## `sender`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-[Address] | `["0x10000", "0x20000", "0x30000"]` | * | `--sender`
+| Type      | Default                             | Available in | CLI equivalent |
+| --------- | ----------------------------------- | ------------ | -------------- |
+| [Address] | `["0x10000", "0x20000", "0x30000"]` | \*           | `--sender`     |
 
 List of addresses to (randomly) use for the transactions sent during testing.
 
 ## `psender`
 
-Type | Default | Available in
------|---------|-------------
-Address | `"0x10000"` | *
+| Type    | Default     | Available in |
+| ------- | ----------- | ------------ |
+| Address | `"0x10000"` | \*           |
 
 Address of the sender of the property to test.
 
 ## `prefix`
 
-Type | Default | Available in
------|---------|-------------
-String | `"echidna_"` | *
+| Type   | Default      | Available in |
+| ------ | ------------ | ------------ |
+| String | `"echidna_"` | \*           |
 
 Prefix of the function names used as properties in the contract to test.
 
 ## `propMaxGas`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `12500000` (current max gas per block) | *
+| Type | Default                                | Available in |
+| ---- | -------------------------------------- | ------------ |
+| Int  | `12500000` (current max gas per block) | \*           |
 
 Maximum amount of gas to consume when running function properties.
 
 ## `testMaxGas`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `12500000` (current max gas per block) | *
+| Type | Default                                | Available in |
+| ---- | -------------------------------------- | ------------ |
+| Int  | `12500000` (current max gas per block) | \*           |
 
 Maximum amount of gas to consume when running random transactions.
 
 ## `maxGasprice`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `0`     | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `0`     | \*           |
 
 Maximum amount of gas price to randomly use in transactions. Do not change it unless you absolutely need it.
 
 ## `maxTimeDelay`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `604800`  (one week) | *
+| Type | Default             | Available in |
+| ---- | ------------------- | ------------ |
+| Int  | `604800` (one week) | \*           |
 
 Maximum amount of seconds of delay between transactions.
 
 ## `maxBlockDelay`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `60480` | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `60480` | \*           |
 
 Maximum amount of block numbers between transactions.
 
 ## `solcArgs`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-String | `""` | * | `--solc-args ARGS`
+| Type   | Default | Available in | CLI equivalent     |
+| ------ | ------- | ------------ | ------------------ |
+| String | `""`    | \*           | `--solc-args ARGS` |
 
 Additional arguments to use in `solc` for compiling the contract to test.
 
 ## `cryticArgs`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-[String] | `[]` | * | `--crytic-args ARGS`
+| Type     | Default | Available in | CLI equivalent       |
+| -------- | ------- | ------------ | -------------------- |
+| [String] | `[]`    | \*           | `--crytic-args ARGS` |
 
 Additional arguments to use in `crytic-compile` for compiling the contract to test.
 
 ## `quiet`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `false` | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `false` | \*           |
 
 Hide `solc` stderr output and additional information during the testing.
 
 ## `format`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-String | `null` | * | `--format FORMAT`
+| Type   | Default | Available in | CLI equivalent    |
+| ------ | ------- | ------------ | ----------------- |
+| String | `null`  | \*           | `--format FORMAT` |
 
 Select a textual output format. By default, interactive TUI is run or text if a terminal is absent.
 
-* `"text"`: simple textual interface.
-* `"json"`: JSON output.
-* `"none"`: no output.
+- `"text"`: simple textual interface.
+- `"json"`: JSON output.
+- `"none"`: no output.
 
 ## `balanceContract`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `0`     | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `0`     | \*           |
 
 Initial Ether balance of `contractAddr`.
 
 ## `balanceAddr`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `0xffffffff` | *
+| Type | Default      | Available in |
+| ---- | ------------ | ------------ |
+| Int  | `0xffffffff` | \*           |
 
 Initial Ether balance of `deployer` and each of the `sender` accounts.
 
 ## `maxValue`
 
-Type | Default | Available in
------|---------|-------------
-Int | `100000000000000000000` (100 ETH) | *
+| Type | Default                           | Available in |
+| ---- | --------------------------------- | ------------ |
+| Int  | `100000000000000000000` (100 ETH) | \*           |
 
 Max amount of value in each randomly generated transaction.
 
 ## `testDestruction`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `false` | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `false` | \*           |
 
 Add a special test that fails if a contract is self-destructed.
 
 ## `stopOnFail`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `false` | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `false` | \*           |
 
 Stops the fuzzing campaign when the first test fails.
 
 ## `allContracts`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Bool | `false` | 2.1.0+ (previously `multi-abi`) | `--all-contracts`
+| Type | Default | Available in                    | CLI equivalent    |
+| ---- | ------- | ------------------------------- | ----------------- |
+| Bool | `false` | 2.1.0+ (previously `multi-abi`) | `--all-contracts` |
 
 Makes Echidna fuzz the provided test contracts and any other deployed contract whose ABI is known at runtime.
 
 ## `filterBlacklist`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `true`  | *
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `true`  | \*           |
 
 Allows Echidna to avoid calling (when set to true) or only call (when set to
 false) a set of functions. The function allowlist or denylist should be provided
@@ -270,9 +271,9 @@ in `filterFunctions`.
 
 ## `filterFunctions`
 
-Type | Default | Available in
------|---------|-------------
-[String] | `[]` | *
+| Type     | Default | Available in |
+| -------- | ------- | ------------ |
+| [String] | `[]`    | \*           |
 
 Configures the function allowlist or denylist from `filterBlacklist`. The list
 should contain strings in the format of
@@ -280,101 +281,101 @@ should contain strings in the format of
 
 ## `allowFFI`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `false` | 2.1.0+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `false` | 2.1.0+       |
 
 Allows the use of the HEVM `ffi` cheatcode.
 
 ## `rpcUrl`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-String | `null` | 2.2.0+ | `--rpc-url URL`
+| Type   | Default | Available in | CLI equivalent  |
+| ------ | ------- | ------------ | --------------- |
+| String | `null`  | 2.2.0+       | `--rpc-url URL` |
 
 URL to fetch contracts over RPC.
 
 ## `rpcBlock`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-String | `null` | 2.2.0+ | `--rpc-block N`
+| Type   | Default | Available in | CLI equivalent  |
+| ------ | ------- | ------------ | --------------- |
+| String | `null`  | 2.2.0+       | `--rpc-block N` |
 
 Block number to use when fetching over RPC.
 
 ## `coverageFormats`
 
-Type | Default | Available in
------|---------|-------------
-[String] | `["txt","html","lcov"]` | 2.2.0+
+| Type     | Default                 | Available in |
+| -------- | ----------------------- | ------------ |
+| [String] | `["txt","html","lcov"]` | 2.2.0+       |
 
 List of file formats to save coverage reports in; default is all possible
 formats.
 
 ## `workers`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | `1`     | 2.2.0+       | `--workers`
+| Type | Default | Available in | CLI equivalent |
+| ---- | ------- | ------------ | -------------- |
+| Int  | `1`     | 2.2.0+       | `--workers`    |
 
 Number of workers.
 
 ## `server`
 
-Type | Default | Available in | CLI equivalent
------|---------|--------------|---------------
-Int  | `null`  | 2.2.2+       | `--server PORT`
+| Type | Default | Available in | CLI equivalent  |
+| ---- | ------- | ------------ | --------------- |
+| Int  | `null`  | 2.2.2+       | `--server PORT` |
 
 Run events server on the given port.
 
 ## `symExec`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `false` | 2.2.4+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `false` | 2.2.4+       |
 
 Whether to add an additional symbolic execution worker.
 
 ## `symExecConcolic`
 
-Type | Default | Available in
------|---------|-------------
-Bool | `true`  | 2.2.4+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Bool | `true`  | 2.2.4+       |
 
 Whether symbolic execution will be concolic (vs full symbolic execution). Only
 relevant if `symExec` is true.
 
 ## `symExecNSolvers`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `1`     | 2.2.4+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `1`     | 2.2.4+       |
 
 Number of SMT solvers used in symbolic execution. Only relevant if `symExec` is
 true.
 
 ## `symExecTimeout`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `30`    | 2.2.4+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `30`    | 2.2.4+       |
 
 Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true.
 
 ## `symExecMaxIters`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `10`    | 2.2.4+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `10`    | 2.2.4+       |
 
 Number of times we may revisit a particular branching point. Only relevant if
 `symExec` is true and `symExecConcolic` is false.
 
 ## `symExecAskSMTIters`
 
-Type | Default | Available in
------|---------|-------------
-Int  | `1`     | 2.2.4+
+| Type | Default | Available in |
+| ---- | ------- | ------------ |
+| Int  | `1`     | 2.2.4+       |
 
 Number of times we may revisit a particular branching point before we consult
 the smt solver to check reachability. Only relevant if `symExec` is true and

From 2d9e871d8c305fffa3d4d13594ee7ceb7a495f98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Tue, 14 May 2024 14:54:52 -0300
Subject: [PATCH 6/9] Apply changes from Gustavo's review

---
 program-analysis/echidna/configuration.md | 47 ++++++++++++++---------
 1 file changed, 28 insertions(+), 19 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index f031fb84..910b250b 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -23,13 +23,15 @@ The test mode to run. It should be one of the following items:
 - `"overflow"`: Detect integer overflows (only available in Solidity 0.8.0 or greater).
 - `"exploration"`: Run contract code without executing any tests.
 
+Review the [testing modes tutorial](./basic/testing-modes.md) to select the one most suitable to your project.
+
 ## `testLimit`
 
 | Type | Default | Available in | CLI equivalent   |
 | ---- | ------- | ------------ | ---------------- |
 | Int  | `50000` | \*           | `--test-limit N` |
 
-Number of sequences of transactions to generate during testing.
+Number of transactions to generate during testing. The campaign will stop when the `testLimit` is reached or if a `timeout` is set and the execution time exceeds it.
 
 ## `seqLen`
 
@@ -37,7 +39,7 @@ Number of sequences of transactions to generate during testing.
 | ---- | ------- | ------------ | -------------- |
 | Int  | `100`   | \*           | `--seq-len N`  |
 
-Number of transactions to generate during testing.
+Number of transactions that a transaction sequence will have during testing, and maximum length of transaction sequences in the corpus. After every N transactions, Echidna will reset the EVM to the initial post-deployment state.
 
 ## `timeout`
 
@@ -45,7 +47,7 @@ Number of transactions to generate during testing.
 | ---- | ------- | ------------ | -------------- |
 | Int  | `null`  | \*           | `--timeout N`  |
 
-Campaign timeout, in seconds. By default it is not time-limited.
+Campaign timeout, in seconds. By default it is not time-limited. If a value is set, the campaign will stop when the time is exhausted or the `testLimit` is reached, whichever happens first.
 
 ## `seed`
 
@@ -53,7 +55,7 @@ Campaign timeout, in seconds. By default it is not time-limited.
 | ---- | ------- | ------------ | -------------- |
 | Int  | random  | \*           | `--seed N`     |
 
-Seed used for random value generation. By default it is a random integer.
+Seed used for random value generation. By default it is a random integer. The seed may not guarantee reproducibility if multiple `workers` are used, as the operating system thread scheduling may introduce additional randomness into the process.
 
 ## `shrinkLimit`
 
@@ -77,7 +79,7 @@ Address to deploy the contract to test.
 | ---- | ------- | ------------ |
 | Bool | `true`  | \*           |
 
-Enable the use of coverage-guided fuzzing and corpus collection.
+Enable the use of coverage-guided fuzzing and corpus collection. We recommend keeping this enabled.
 
 ## `corpusDir`
 
@@ -141,7 +143,7 @@ Prefix of the function names used as properties in the contract to test.
 | ---- | -------------------------------------- | ------------ |
 | Int  | `12500000` (current max gas per block) | \*           |
 
-Maximum amount of gas to consume when running function properties.
+Maximum amount of gas to consume when running function properties. If a property runs out of gas, it will be considered as a failure.
 
 ## `testMaxGas`
 
@@ -149,7 +151,7 @@ Maximum amount of gas to consume when running function properties.
 | ---- | -------------------------------------- | ------------ |
 | Int  | `12500000` (current max gas per block) | \*           |
 
-Maximum amount of gas to consume when running random transactions.
+Maximum amount of gas to consume when running random transactions. A non-property transaction that runs out of gas (e.g. a transaction in assertion mode) will not be considered a failure.
 
 ## `maxGasprice`
 
@@ -217,7 +219,7 @@ Select a textual output format. By default, interactive TUI is run or text if a
 | ---- | ------- | ------------ |
 | Int  | `0`     | \*           |
 
-Initial Ether balance of `contractAddr`.
+Initial Ether balance of `contractAddr`. See our tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
 
 ## `balanceAddr`
 
@@ -225,7 +227,7 @@ Initial Ether balance of `contractAddr`.
 | ---- | ------------ | ------------ |
 | Int  | `0xffffffff` | \*           |
 
-Initial Ether balance of `deployer` and each of the `sender` accounts.
+Initial Ether balance of `deployer` and each of the `sender` accounts. See our tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
 
 ## `maxValue`
 
@@ -233,7 +235,7 @@ Initial Ether balance of `deployer` and each of the `sender` accounts.
 | ---- | --------------------------------- | ------------ |
 | Int  | `100000000000000000000` (100 ETH) | \*           |
 
-Max amount of value in each randomly generated transaction.
+Max amount of value in each randomly generated transaction. See our tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
 
 ## `testDestruction`
 
@@ -289,20 +291,28 @@ Allows the use of the HEVM `ffi` cheatcode.
 
 ## `rpcUrl`
 
-| Type   | Default | Available in | CLI equivalent  |
-| ------ | ------- | ------------ | --------------- |
-| String | `null`  | 2.2.0+       | `--rpc-url URL` |
+| Type   | Default | Available in                                | CLI equivalent  | Env. variable equivalent |
+| ------ | ------- | ------------------------------------------- | --------------- | ------------------------ |
+| String | `null`  | 2.1.0+ (env), 2.2.0+ (config), 2.2.3+ (cli) | `--rpc-url URL` | `ECHIDNA_RPC_URL`        |
 
 URL to fetch contracts over RPC.
 
 ## `rpcBlock`
 
-| Type   | Default | Available in | CLI equivalent  |
-| ------ | ------- | ------------ | --------------- |
-| String | `null`  | 2.2.0+       | `--rpc-block N` |
+| Type   | Default | Available in                                | CLI equivalent  | Env. variable equivalent |
+| ------ | ------- | ------------------------------------------- | --------------- | ------------------------ |
+| String | `null`  | 2.1.0+ (env), 2.2.0+ (config), 2.2.3+ (cli) | `--rpc-block N` | `ECHIDNA_RPC_BLOCK`      |
 
 Block number to use when fetching over RPC.
 
+## `etherscanApiKey`
+
+| Type   | Default | Available in                  | Env. variable equivalent |
+| ------ | ------- | ----------------------------- | ------------------------ |
+| String | `null`  | 2.1.0+ (env), 2.2.4+ (config) | `ETHERSCAN_API_KEY`      |
+
+Etherscan API key used to fetch contract code.
+
 ## `coverageFormats`
 
 | Type     | Default                 | Available in |
@@ -351,8 +361,7 @@ relevant if `symExec` is true.
 | ---- | ------- | ------------ |
 | Int  | `1`     | 2.2.4+       |
 
-Number of SMT solvers used in symbolic execution. Only relevant if `symExec` is
-true.
+Number of SMT solvers used in symbolic execution. While there is a single symExec worker, N threads may be used to solve SMT queries. Only relevant if `symExec` is true.
 
 ## `symExecTimeout`
 
@@ -360,7 +369,7 @@ true.
 | ---- | ------- | ------------ |
 | Int  | `30`    | 2.2.4+       |
 
-Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true.
+Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true. When the SMT solver used is Z3, this timeout applies per query, and is not global.
 
 ## `symExecMaxIters`
 

From 642afa5fc12e5b9f33e1e1374eff8a0841beb75c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Tue, 14 May 2024 14:56:39 -0300
Subject: [PATCH 7/9] Lint and text wrap

---
 program-analysis/echidna/configuration.md | 66 ++++++++++++++++-------
 1 file changed, 47 insertions(+), 19 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index 910b250b..a55d7a61 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -23,7 +23,8 @@ The test mode to run. It should be one of the following items:
 - `"overflow"`: Detect integer overflows (only available in Solidity 0.8.0 or greater).
 - `"exploration"`: Run contract code without executing any tests.
 
-Review the [testing modes tutorial](./basic/testing-modes.md) to select the one most suitable to your project.
+Review the [testing modes tutorial](./basic/testing-modes.md) to select the one
+most suitable to your project.
 
 ## `testLimit`
 
@@ -31,7 +32,9 @@ Review the [testing modes tutorial](./basic/testing-modes.md) to select the one
 | ---- | ------- | ------------ | ---------------- |
 | Int  | `50000` | \*           | `--test-limit N` |
 
-Number of transactions to generate during testing. The campaign will stop when the `testLimit` is reached or if a `timeout` is set and the execution time exceeds it.
+Number of transactions to generate during testing. The campaign will stop when
+the `testLimit` is reached or if a `timeout` is set and the execution time
+exceeds it.
 
 ## `seqLen`
 
@@ -39,7 +42,9 @@ Number of transactions to generate during testing. The campaign will stop when t
 | ---- | ------- | ------------ | -------------- |
 | Int  | `100`   | \*           | `--seq-len N`  |
 
-Number of transactions that a transaction sequence will have during testing, and maximum length of transaction sequences in the corpus. After every N transactions, Echidna will reset the EVM to the initial post-deployment state.
+Number of transactions that a transaction sequence will have during testing, and
+maximum length of transaction sequences in the corpus. After every N
+transactions, Echidna will reset the EVM to the initial post-deployment state.
 
 ## `timeout`
 
@@ -47,7 +52,9 @@ Number of transactions that a transaction sequence will have during testing, and
 | ---- | ------- | ------------ | -------------- |
 | Int  | `null`  | \*           | `--timeout N`  |
 
-Campaign timeout, in seconds. By default it is not time-limited. If a value is set, the campaign will stop when the time is exhausted or the `testLimit` is reached, whichever happens first.
+Campaign timeout, in seconds. By default it is not time-limited. If a value is
+set, the campaign will stop when the time is exhausted or the `testLimit` is
+reached, whichever happens first.
 
 ## `seed`
 
@@ -55,7 +62,10 @@ Campaign timeout, in seconds. By default it is not time-limited. If a value is s
 | ---- | ------- | ------------ | -------------- |
 | Int  | random  | \*           | `--seed N`     |
 
-Seed used for random value generation. By default it is a random integer. The seed may not guarantee reproducibility if multiple `workers` are used, as the operating system thread scheduling may introduce additional randomness into the process.
+Seed used for random value generation. By default it is a random integer. The
+seed may not guarantee reproducibility if multiple `workers` are used, as the
+operating system thread scheduling may introduce additional randomness into the
+process.
 
 ## `shrinkLimit`
 
@@ -79,7 +89,8 @@ Address to deploy the contract to test.
 | ---- | ------- | ------------ |
 | Bool | `true`  | \*           |
 
-Enable the use of coverage-guided fuzzing and corpus collection. We recommend keeping this enabled.
+Enable the use of coverage-guided fuzzing and corpus collection. We recommend
+keeping this enabled.
 
 ## `corpusDir`
 
@@ -103,7 +114,9 @@ Address of the deployer of the contract to test.
 | ----------------------- | ------- | ------------ |
 | [⁠[⁠Address, String⁠]⁠] | `[]`    | 2.0.2+       |
 
-Addresses and contract names to deploy using the available source code. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
+Addresses and contract names to deploy using the available source code. The
+deployer address is the same as the contract to test. Echidna will error if the
+deployment fails.
 
 ## `deployBytecodes`
 
@@ -111,7 +124,8 @@ Addresses and contract names to deploy using the available source code. The depl
 | ----------------------- | ------- | ------------ |
 | [⁠[⁠Address, String⁠]⁠] | `[]`    | 2.0.2+       |
 
-Addresses and bytecodes to deploy. The deployer address is the same as the contract to test. Echidna will error if the deployment fails.
+Addresses and bytecodes to deploy. The deployer address is the same as the
+contract to test. Echidna will error if the deployment fails.
 
 ## `sender`
 
@@ -143,7 +157,8 @@ Prefix of the function names used as properties in the contract to test.
 | ---- | -------------------------------------- | ------------ |
 | Int  | `12500000` (current max gas per block) | \*           |
 
-Maximum amount of gas to consume when running function properties. If a property runs out of gas, it will be considered as a failure.
+Maximum amount of gas to consume when running function properties. If a property
+runs out of gas, it will be considered as a failure.
 
 ## `testMaxGas`
 
@@ -151,7 +166,9 @@ Maximum amount of gas to consume when running function properties. If a property
 | ---- | -------------------------------------- | ------------ |
 | Int  | `12500000` (current max gas per block) | \*           |
 
-Maximum amount of gas to consume when running random transactions. A non-property transaction that runs out of gas (e.g. a transaction in assertion mode) will not be considered a failure.
+Maximum amount of gas to consume when running random transactions. A
+non-property transaction that runs out of gas (e.g. a transaction in assertion
+mode) will not be considered a failure.
 
 ## `maxGasprice`
 
@@ -159,7 +176,8 @@ Maximum amount of gas to consume when running random transactions. A non-propert
 | ---- | ------- | ------------ |
 | Int  | `0`     | \*           |
 
-Maximum amount of gas price to randomly use in transactions. Do not change it unless you absolutely need it.
+Maximum amount of gas price to randomly use in transactions. Do not change it
+unless you absolutely need it.
 
 ## `maxTimeDelay`
 
@@ -191,7 +209,8 @@ Additional arguments to use in `solc` for compiling the contract to test.
 | -------- | ------- | ------------ | -------------------- |
 | [String] | `[]`    | \*           | `--crytic-args ARGS` |
 
-Additional arguments to use in `crytic-compile` for compiling the contract to test.
+Additional arguments to use in `crytic-compile` for compiling the contract to
+test.
 
 ## `quiet`
 
@@ -207,7 +226,8 @@ Hide `solc` stderr output and additional information during the testing.
 | ------ | ------- | ------------ | ----------------- |
 | String | `null`  | \*           | `--format FORMAT` |
 
-Select a textual output format. By default, interactive TUI is run or text if a terminal is absent.
+Select a textual output format. By default, interactive TUI is run or text if a
+terminal is absent.
 
 - `"text"`: simple textual interface.
 - `"json"`: JSON output.
@@ -219,7 +239,8 @@ Select a textual output format. By default, interactive TUI is run or text if a
 | ---- | ------- | ------------ |
 | Int  | `0`     | \*           |
 
-Initial Ether balance of `contractAddr`. See our tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
+Initial Ether balance of `contractAddr`. See our tutorial on [working with
+ETH](./basic/working-with-eth.md) for more details.
 
 ## `balanceAddr`
 
@@ -227,7 +248,8 @@ Initial Ether balance of `contractAddr`. See our tutorial on [working with ETH](
 | ---- | ------------ | ------------ |
 | Int  | `0xffffffff` | \*           |
 
-Initial Ether balance of `deployer` and each of the `sender` accounts. See our tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
+Initial Ether balance of `deployer` and each of the `sender` accounts. See our
+tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
 
 ## `maxValue`
 
@@ -235,7 +257,8 @@ Initial Ether balance of `deployer` and each of the `sender` accounts. See our t
 | ---- | --------------------------------- | ------------ |
 | Int  | `100000000000000000000` (100 ETH) | \*           |
 
-Max amount of value in each randomly generated transaction. See our tutorial on [working with ETH](./basic/working-with-eth.md) for more details.
+Max amount of value in each randomly generated transaction. See our tutorial on
+[working with ETH](./basic/working-with-eth.md) for more details.
 
 ## `testDestruction`
 
@@ -259,7 +282,8 @@ Stops the fuzzing campaign when the first test fails.
 | ---- | ------- | ------------------------------- | ----------------- |
 | Bool | `false` | 2.1.0+ (previously `multi-abi`) | `--all-contracts` |
 
-Makes Echidna fuzz the provided test contracts and any other deployed contract whose ABI is known at runtime.
+Makes Echidna fuzz the provided test contracts and any other deployed contract
+whose ABI is known at runtime.
 
 ## `filterBlacklist`
 
@@ -361,7 +385,9 @@ relevant if `symExec` is true.
 | ---- | ------- | ------------ |
 | Int  | `1`     | 2.2.4+       |
 
-Number of SMT solvers used in symbolic execution. While there is a single symExec worker, N threads may be used to solve SMT queries. Only relevant if `symExec` is true.
+Number of SMT solvers used in symbolic execution. While there is a single
+symExec worker, N threads may be used to solve SMT queries. Only relevant if
+`symExec` is true.
 
 ## `symExecTimeout`
 
@@ -369,7 +395,9 @@ Number of SMT solvers used in symbolic execution. While there is a single symExe
 | ---- | ------- | ------------ |
 | Int  | `30`    | 2.2.4+       |
 
-Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true. When the SMT solver used is Z3, this timeout applies per query, and is not global.
+Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true.
+When the SMT solver used is Z3, this timeout applies per query, and is not
+global.
 
 ## `symExecMaxIters`
 

From 43096f24122aaf94bf731611ecd8b471bc06be98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Tue, 14 May 2024 15:47:52 -0300
Subject: [PATCH 8/9] Move CSS out of md file

---
 program-analysis/echidna/configuration.md | 3 ---
 static/custom.css                         | 5 +++++
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index a55d7a61..b8dcfd02 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -1,8 +1,5 @@
 # Configuration options
 
-<!-- To left align the tables -->
-<style>table {margin: 0}</style>
-
 The following is a list of all the options that may be provided in the Echidna
 configuration file. Whenever an option can also be set via the command line, the
 CLI equivalent flag is provided as a reference. Some flags are relatively new
diff --git a/static/custom.css b/static/custom.css
index b1365ced..5d27c1cd 100644
--- a/static/custom.css
+++ b/static/custom.css
@@ -5,3 +5,8 @@
   width: 50%;
   max-width: max-content;
 }
+
+/* program-analysis/echidna/configuration.md */
+h1#configuration-options ~ div > table {
+  margin: 0;
+}

From 8b36faa2408a6246e9d585b658140e90e92b6062 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Tue, 14 May 2024 15:52:21 -0300
Subject: [PATCH 9/9] Document sender, psender

---
 program-analysis/echidna/configuration.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/program-analysis/echidna/configuration.md b/program-analysis/echidna/configuration.md
index b8dcfd02..0643212f 100644
--- a/program-analysis/echidna/configuration.md
+++ b/program-analysis/echidna/configuration.md
@@ -130,7 +130,10 @@ contract to test. Echidna will error if the deployment fails.
 | --------- | ----------------------------------- | ------------ | -------------- |
 | [Address] | `["0x10000", "0x20000", "0x30000"]` | \*           | `--sender`     |
 
-List of addresses to (randomly) use for the transactions sent during testing.
+List of addresses to (randomly) use as `msg.sender` for the transactions sent
+during testing. These addresses are used as the sender for all transactions
+produced by Echidna, except for property evaluation in `property` mode (see
+`psender` below).
 
 ## `psender`
 
@@ -138,7 +141,9 @@ List of addresses to (randomly) use for the transactions sent during testing.
 | ------- | ----------- | ------------ |
 | Address | `"0x10000"` | \*           |
 
-Address of the sender of the property to test.
+Address of `msg.sender` to use for property evaluation. This address is only
+used to evaluate properties (functions with the configured `prefix`) while
+executing Echidna in `property` mode.
 
 ## `prefix`