feat(ctb): Invariant docgen (#4574)

* Begin simple invariant docgen script

* Support Echidna tests in invariant docgen

* Use custom natspec tags for invariant doc comments

* Handle multi-line headers for linting purposes

* Restack

* Upstack

* New doc

* New doc

* Add test file name to link in docgen script

* Relative URL path

* Use `path.join`

* Add task to `contracts-bedrock` workflow to check diff of `invariant-docs`

* Generate a table of contents for invariant docs

.circleci/config.yml

@@ -263,6 +263,10 @@ jobs:
           name: storage snapshot
           command: yarn storage-snapshot && git diff --exit-code .storage-layout
           working_directory: packages/contracts-bedrock
+      - run:
+          name: invariant docs
+          command: yarn autogen:invariant-docs && git diff --exit-code ./invariant-docs/*.md
+          working_directory: packages/contracts-bedrock
 
   bedrock-echidna-build:
     docker:

packages/contracts-bedrock/contracts/echidna/FuzzAddressAliasing.sol

@@ -24,7 +24,10 @@ contract EchidnaFuzzAddressAliasing {
     }
 
     /**
-     * @notice Verifies that testRoundTrip(...) did not ever fail.
+     * @custom:invariant Address aliases are always able to be undone.
+     *
+     * Asserts that an address that has been aliased with `applyL1ToL2Alias` can always
+     * be unaliased with `undoL1ToL2Alias`.
      */
     function echidna_round_trip_aliasing() public view returns (bool) {
         // ASSERTION: The round trip aliasing done in testRoundTrip(...) should never fail.

packages/contracts-bedrock/contracts/echidna/FuzzBurn.sol

@@ -26,6 +26,12 @@ contract EchidnaFuzzBurnEth is StdUtils {
         }
     }
 
+    /**
+     * @custom:invariant `eth(uint256)` always burns the exact amount of eth passed.
+     *
+     * Asserts that when `Burn.eth(uint256)` is called, it always burns the exact amount
+     * of ETH passed to the function.
+     */
     function echidna_burn_eth() public view returns (bool) {
         // ASSERTION: The amount burned should always match the amount passed exactly
         return !failedEthBurn;
@@ -62,6 +68,12 @@ contract EchidnaFuzzBurnGas is StdUtils {
         }
     }
 
+    /**
+     * @custom:invariant `gas(uint256)` always burns at least the amount of gas passed.
+     *
+     * Asserts that when `Burn.gas(uint256)` is called, it always burns at least the amount
+     * of gas passed to the function.
+     */
     function echidna_burn_gas() public view returns (bool) {
         // ASSERTION: The amount of gas burned should be strictly greater than the
         // the amount passed as _value (minimum _value + whatever minor overhead to

packages/contracts-bedrock/contracts/echidna/FuzzEncoding.sol

@@ -49,7 +49,9 @@ contract EchidnaFuzzEncoding {
     }
 
     /**
-     * @notice Verifies that testRoundTripAToB did not ever fail.
+     * @custom:invariant `testRoundTripAToB` never fails.
+     *
+     * Asserts that a raw versioned nonce can be encoded / decoded to reach the same raw value.
      */
     function echidna_round_trip_encoding_AToB() public view returns (bool) {
         // ASSERTION: The round trip encoding done in testRoundTripAToB(...)
@@ -57,7 +59,10 @@ contract EchidnaFuzzEncoding {
     }
 
     /**
-     * @notice Verifies that testRoundTripBToA did not ever fail.
+     * @custom:invariant `testRoundTripBToA` never fails.
+     *
+     * Asserts that an encoded versioned nonce can always be decoded / re-encoded to reach
+     * the same encoded value.
      */
     function echidna_round_trip_encoding_BToA() public view returns (bool) {
         // ASSERTION: The round trip encoding done in testRoundTripBToA should never

packages/contracts-bedrock/contracts/echidna/FuzzHashing.sol

@@ -112,17 +112,36 @@ contract EchidnaFuzzHashing {
         }
     }
 
+    /**
+     * @custom:invariant `hashCrossDomainMessage` reverts if `version` is > `1`.
+     *
+     * The `hashCrossDomainMessage` function should always revert if the `version` passed is > `1`.
+     */
     function echidna_hash_xdomain_msg_high_version() public view returns (bool) {
         // ASSERTION: A call to hashCrossDomainMessage will never succeed for a version > 1
         return !failedCrossDomainHashHighVersion;
     }
 
+    /**
+     * @custom:invariant `version` = `0`: `hashCrossDomainMessage` and `hashCrossDomainMessageV0`
+     * are equivalent.
+     *
+     * If the version passed is 0, `hashCrossDomainMessage` and `hashCrossDomainMessageV0` should be
+     * equivalent.
+     */
     function echidna_hash_xdomain_msg_0() public view returns (bool) {
         // ASSERTION: A call to hashCrossDomainMessage and hashCrossDomainMessageV0
         // should always match when the version passed is 0
         return !failedCrossDomainHashV0;
     }
 
+    /**
+     * @custom:invariant `version` = `1`: `hashCrossDomainMessage` and `hashCrossDomainMessageV1`
+     * are equivalent.
+     *
+     * If the version passed is 1, `hashCrossDomainMessage` and `hashCrossDomainMessageV1` should be
+     * equivalent.
+     */
     function echidna_hash_xdomain_msg_1() public view returns (bool) {
         // ASSERTION: A call to hashCrossDomainMessage and hashCrossDomainMessageV1
         // should always match when the version passed is 1

packages/contracts-bedrock/contracts/echidna/FuzzOptimismPortal.sol

@@ -27,6 +27,13 @@ contract EchidnaFuzzOptimismPortal {
         failedToComplete = false;
     }
 
+    /**
+     * @custom:invariant Deposits of any value should always succeed unless
+     * `_to` = `address(0)` or `_isCreation` = `true`.
+     *
+     * All deposits, barring creation transactions and transactions sent to `address(0)`,
+     * should always succeed.
+     */
     function echidna_deposit_completes() public view returns (bool) {
         return !failedToComplete;
     }

packages/contracts-bedrock/contracts/echidna/FuzzResourceMetering.sol

@@ -78,7 +78,7 @@ contract EchidnaFuzzResourceMetering is ResourceMetering, StdUtils {
                 ((uint256(params.prevBaseFee) - cachedPrevBaseFee) < maxBaseFeeChange);
         }
 
-        // If the last blocked used less than the target amount of gas, (or was empty),
+        // If the last block used less than the target amount of gas, (or was empty),
         // ensure that: this block's baseFee was decreased, but not by more than the max amount
         if (
             (cachedPrevBoughtGas < uint256(TARGET_RESOURCE_LIMIT)) ||
@@ -128,30 +128,78 @@ contract EchidnaFuzzResourceMetering is ResourceMetering, StdUtils {
 
     function _burnInternal(uint64 _gasToBurn) private metered(_gasToBurn) {}
 
+    /**
+     * @custom:invariant The base fee should increase if the last block used more
+     * than the target amount of gas
+     *
+     * If the last block used more than the target amount of gas (and there were no
+     * empty blocks in between), ensure this block's baseFee increased, but not by
+     * more than the max amount per block.
+     */
     function echidna_high_usage_raise_baseFee() public view returns (bool) {
         return !failedRaiseBaseFee;
     }
 
+    /**
+     * @custom:invariant The base fee should decrease if the last block used less
+     * than the target amount of gas
+     *
+     * If the previous block used less than the target amount of gas, the base fee should decrease,
+     * but not more than the max amount.
+     */
     function echidna_low_usage_lower_baseFee() public view returns (bool) {
         return !failedLowerBaseFee;
     }
 
+    /**
+     * @custom:invariant A block's base fee should never be below `MINIMUM_BASE_FEE`
+     *
+     * This test asserts that a block's base fee can never drop below the
+     * `MINIMUM_BASE_FEE` threshold.
+     */
     function echidna_never_below_min_baseFee() public view returns (bool) {
         return !failedNeverBelowMinBaseFee;
     }
 
+    /**
+     * @custom:invariant A block can never consume more than `MAX_RESOURCE_LIMIT` gas.
+     *
+     * This test asserts that a block can never consume more than the `MAX_RESOURCE_LIMIT`
+     * gas threshold.
+     */
     function echidna_never_above_max_gas_limit() public view returns (bool) {
         return !failedMaxGasPerBlock;
     }
 
+    /**
+     * @custom:invariant The base fee can never be raised more than the max base fee change.
+     *
+     * After a block consumes more gas than the target gas, the base fee cannot be raised
+     * more than the maximum amount allowed. The max base fee change (per-block) is derived
+     * as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR`
+     */
     function echidna_never_exceed_max_increase() public view returns (bool) {
         return !failedMaxRaiseBaseFeePerBlock;
     }
 
+    /**
+     * @custom:invariant The base fee can never be lowered more than the max base fee change.
+     *
+     * After a block consumes less than the target gas, the base fee cannot be lowered more
+     * than the maximum amount allowed. The max base fee change (per-block) is derived as
+     *follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR`
+     */
     function echidna_never_exceed_max_decrease() public view returns (bool) {
         return !failedMaxLowerBaseFeePerBlock;
     }
 
+    /**
+     * @custom:invariant The `maxBaseFeeChange` calculation over multiple blocks can never
+     * underflow.
+     *
+     * When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation
+     * should never be allowed to underflow.
+     */
     function echidna_underflow() public view returns (bool) {
         return !underflow;
     }

packages/contracts-bedrock/invariant-docs/AddressAliasing.md

+# `AddressAliasing` Invariants
+
+## Address aliases are always able to be undone.
+**Test:** [`FuzzAddressAliasing.sol#L32`](../contracts/echidna/FuzzAddressAliasing.sol#L32)
+
+Asserts that an address that has been aliased with `applyL1ToL2Alias` can always be unaliased with `undoL1ToL2Alias`. 

packages/contracts-bedrock/invariant-docs/Burn.md

+# `Burn` Invariants
+
+## `eth(uint256)` always burns the exact amount of eth passed.
+**Test:** [`FuzzBurn.sol#L35`](../contracts/echidna/FuzzBurn.sol#L35)
+
+Asserts that when `Burn.eth(uint256)` is called, it always burns the exact amount of ETH passed to the function. 
+
+
+## `gas(uint256)` always burns at least the amount of gas passed.
+**Test:** [`FuzzBurn.sol#L77`](../contracts/echidna/FuzzBurn.sol#L77)
+
+Asserts that when `Burn.gas(uint256)` is called, it always burns at least the amount of gas passed to the function. 

packages/contracts-bedrock/invariant-docs/Encoding.md

+# `Encoding` Invariants
+
+## `testRoundTripAToB` never fails.
+**Test:** [`FuzzEncoding.sol#L56`](../contracts/echidna/FuzzEncoding.sol#L56)
+
+Asserts that a raw versioned nonce can be encoded / decoded to reach the same raw value. 
+
+
+## `testRoundTripBToA` never fails.
+**Test:** [`FuzzEncoding.sol#L67`](../contracts/echidna/FuzzEncoding.sol#L67)
+
+Asserts that an encoded versioned nonce can always be decoded / re-encoded to reach the same encoded value. 

packages/contracts-bedrock/invariant-docs/Hashing.md

+# `Hashing` Invariants
+
+## `hashCrossDomainMessage` reverts if `version` is > `1`.
+**Test:** [`FuzzHashing.sol#L120`](../contracts/echidna/FuzzHashing.sol#L120)
+
+The `hashCrossDomainMessage` function should always revert if the `version` passed is > `1`. 
+
+
+## `version` = `0`: `hashCrossDomainMessage` and `hashCrossDomainMessageV0` are equivalent.
+**Test:** [`FuzzHashing.sol#L132`](../contracts/echidna/FuzzHashing.sol#L132)
+
+If the version passed is 0, `hashCrossDomainMessage` and `hashCrossDomainMessageV0` should be equivalent. 
+
+
+## `version` = `1`: `hashCrossDomainMessage` and `hashCrossDomainMessageV1` are equivalent.
+**Test:** [`FuzzHashing.sol#L145`](../contracts/echidna/FuzzHashing.sol#L145)
+
+If the version passed is 1, `hashCrossDomainMessage` and `hashCrossDomainMessageV1` should be equivalent. 

packages/contracts-bedrock/invariant-docs/L2OutputOracle.md

+# `L2OutputOracle` Invariants
+
+## The block number of the output root proposals should monotonically increase.
+**Test:** [`L2OutputOracle.t.sol#L36`](../contracts/test/invariants/L2OutputOracle.t.sol#L36)
+
+When a new output is submitted, it should never be allowed to correspond to a block number that is less than the current output. 

packages/contracts-bedrock/invariant-docs/OptimismPortal.md

+# `OptimismPortal` Invariants
+
+## `finalizeWithdrawalTransaction` should revert if the finalization period has not elapsed.
+**Test:** [`OptimismPortal.t.sol#L86`](../contracts/test/invariants/OptimismPortal.t.sol#L86)
+
+A withdrawal that has been proven should not be able to be finalized until after the finalization period has elapsed. 
+
+
+## `finalizeWithdrawalTransaction` should revert if the withdrawal has already been finalized.
+**Test:** [`OptimismPortal.t.sol#L123`](../contracts/test/invariants/OptimismPortal.t.sol#L123)
+
+Ensures that there is no chain of calls that can be made that allows a withdrawal to be finalized twice. 
+
+
+## A withdrawal should **always** be able to be finalized `FINALIZATION_PERIOD_SECONDS` after it was successfully proven.
+**Test:** [`OptimismPortal.t.sol#L158`](../contracts/test/invariants/OptimismPortal.t.sol#L158)
+
+This invariant asserts that there is no chain of calls that can be made that will prevent a withdrawal from being finalized exactly `FINALIZATION_PERIOD_SECONDS` after it was successfully proven. 
+
+
+## Deposits of any value should always succeed unless `_to` = `address(0)` or `_isCreation` = `true`.
+**Test:** [`FuzzOptimismPortal.sol#L37`](../contracts/echidna/FuzzOptimismPortal.sol#L37)
+
+All deposits, barring creation transactions and transactions sent to `address(0)`, should always succeed. 

packages/contracts-bedrock/invariant-docs/README.md

+# Invariant Docs
+
+This directory contains documentation for all defined invariant tests within `contracts-bedrock`.
+
+<!-- Do not modify the following section manually. It will be automatically generated on running `yarn autogen:invariant-docs` -->
+<!-- START autoTOC -->
+
+## Table of Contents
+- [AddressAliasing](./AddressAliasing.md)
+- [Burn](./Burn.md)
+- [Encoding](./Encoding.md)
+- [Hashing](./Hashing.md)
+- [L2OutputOracle](./L2OutputOracle.md)
+- [OptimismPortal](./OptimismPortal.md)
+- [ResourceMetering](./ResourceMetering.md)
+- [SystemConfig](./SystemConfig.md)
+<!-- END autoTOC -->
+
+## Usage
+
+To auto-generate documentation for invariant tests, run `yarn autogen:invariant-docs`.
+
+## Documentation Standard
+
+In order for an invariant test file to be picked up by the [docgen script](../scripts/invariant-doc-gen.ts), it must
+adhere to the following conventions:
+
+### Forge Invariants
+
+All `forge` invariant tests must exist within the `contracts/test/invariants` folder, and the file name should be
+`<ContractName>.t.sol`, where `<ContractName>` is the name of the contract that is being tested.
+
+All tests within `forge` invariant files should follow the convention:
+
+```solidity
+/**
+ * @custom:invariant <title>
+ *
+ * <longDescription>
+ */
+function invariant_<shortDescription>() external {
+    // ...
+}
+```
+
+### Echidna Invariants
+
+All `echidna` invariant tests must exist within the `contracts/echidna` folder, and the file name should be
+`Fuzz<ContractName>.sol`, where `<ContractName>` is the name of the contract that is being tested.
+
+All property tests within `echidna` invariant files should follow the convention:
+```solidity
+/**
+ * @custom:invariant <title>
+ *
+ * <longDescription>
+ */
+function echidna_<shortDescription>() external view returns (bool) {
+    // ...
+}
+```

packages/contracts-bedrock/invariant-docs/ResourceMetering.md

+# `ResourceMetering` Invariants
+
+## The base fee should increase if the last block used more than the target amount of gas
+**Test:** [`FuzzResourceMetering.sol#L139`](../contracts/echidna/FuzzResourceMetering.sol#L139)
+
+If the last block used more than the target amount of gas (and there were no empty blocks in between), ensure this block's baseFee increased, but not by more than the max amount per block. 
+
+
+## The base fee should decrease if the last block used less than the target amount of gas
+**Test:** [`FuzzResourceMetering.sol#L150`](../contracts/echidna/FuzzResourceMetering.sol#L150)
+
+If the previous block used less than the target amount of gas, the base fee should decrease, but not more than the max amount. 
+
+
+## A block's base fee should never be below `MINIMUM_BASE_FEE`
+**Test:** [`FuzzResourceMetering.sol#L160`](../contracts/echidna/FuzzResourceMetering.sol#L160)
+
+This test asserts that a block's base fee can never drop below the `MINIMUM_BASE_FEE` threshold. 
+
+
+## A block can never consume more than `MAX_RESOURCE_LIMIT` gas.
+**Test:** [`FuzzResourceMetering.sol#L170`](../contracts/echidna/FuzzResourceMetering.sol#L170)
+
+This test asserts that a block can never consume more than the `MAX_RESOURCE_LIMIT` gas threshold. 
+
+
+## The base fee can never be raised more than the max base fee change.
+**Test:** [`FuzzResourceMetering.sol#L181`](../contracts/echidna/FuzzResourceMetering.sol#L181)
+
+After a block consumes more gas than the target gas, the base fee cannot be raised more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR` 
+
+
+## The base fee can never be lowered more than the max base fee change.
+**Test:** [`FuzzResourceMetering.sol#L192`](../contracts/echidna/FuzzResourceMetering.sol#L192)
+
+After a block consumes less than the target gas, the base fee cannot be lowered more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR` 
+
+
+## The `maxBaseFeeChange` calculation over multiple blocks can never underflow.
+**Test:** [`FuzzResourceMetering.sol#L203`](../contracts/echidna/FuzzResourceMetering.sol#L203)
+
+When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation should never be allowed to underflow. 

packages/contracts-bedrock/invariant-docs/SystemConfig.md

+# `SystemConfig` Invariants
+
+## The gas limit of the `SystemConfig` contract can never be lower than the hard-coded lower bound.
+**Test:** [`SystemConfig.t.sol#L40`](../contracts/test/invariants/SystemConfig.t.sol#L40)
+

packages/contracts-bedrock/package.json

@@ -22,6 +22,7 @@
     "build": "hardhat compile && yarn autogen:artifacts && yarn build:ts && yarn typechain",
     "build:ts": "tsc -p tsconfig.build.json",
     "autogen:artifacts": "ts-node scripts/generate-artifacts.ts",
+    "autogen:invariant-docs": "ts-node scripts/invariant-doc-gen.ts",
     "deploy": "hardhat deploy",
     "test": "yarn build:differential && yarn build:fuzz && forge test",
     "coverage": "yarn build:differential && yarn build:fuzz && forge coverage",

packages/contracts-bedrock/scripts/invariant-doc-gen.ts

+import fs from 'fs'
+import path from 'path'
+
+const BASE_INVARIANTS_DIR = path.join(
+  __dirname,
+  '..',
+  'contracts',
+  'test',
+  'invariants'
+)
+const BASE_ECHIDNA_DIR = path.join(__dirname, '..', 'contracts', 'echidna')
+const BASE_DOCS_DIR = path.join(__dirname, '..', 'invariant-docs')
+const BASE_ECHIDNA_GH_URL = '../contracts/echidna/'
+const BASE_INVARIANT_GH_URL = '../contracts/test/invariants/'
+const NATSPEC_INV = '@custom:invariant'
+const BLOCK_COMMENT_PREFIX_REGEX = /\*(\/)?/
+const BLOCK_COMMENT_HEADER_REGEX = /\*\s(.)+/
+
+// Represents an invariant test contract
+type Contract = {
+  name: string
+  fileName: string
+  isEchidna: boolean
+  docs: InvariantDoc[]
+}
+
+// Represents the documentation of an invariant
+type InvariantDoc = {
+  header?: string
+  desc?: string
+  lineNo?: number
+}
+
+const writtenFiles = []
+
+/**
+ * Lazy-parses all test files in the `contracts/test/invariants` directory to generate documentation
+ * on all invariant tests.
+ */
+const docGen = (dir: string): void => {
+  // Grab all files within the invariants test dir
+  const files = fs.readdirSync(dir)
+
+  // Array to store all found invariant documentation comments.
+  const docs: Contract[] = []
+
+  for (const fileName of files) {
+    // Read the contents of the invariant test file.
+    const fileContents = fs.readFileSync(path.join(dir, fileName)).toString()
+
+    // Split the file into individual lines and trim whitespace.
+    const lines = fileContents.split('\n').map((line: string) => line.trim())
+
+    // Create an object to store all invariant test docs for the current contract
+    const isEchidna = fileName.startsWith('Fuzz')
+    const name = isEchidna
+      ? fileName.replace('Fuzz', '').replace('.sol', '')
+      : fileName.replace('.t.sol', '')
+    const contract: Contract = { name, fileName, isEchidna, docs: [] }
+
+    let currentDoc: InvariantDoc
+
+    // Loop through all lines to find comments.
+    for (let i = 0; i < lines.length; i++) {
+      let line = lines[i]
+
+      if (line.startsWith('/**')) {
+        // We are at the beginning of a new doc comment. Reset the `currentDoc`.
+        currentDoc = {}
+
+        // Move on to the next line
+        line = lines[++i]
+
+        // We have an invariant doc
+        if (line.startsWith(`* ${NATSPEC_INV}`)) {
+          // Assign the header of the invariant doc.
+          // TODO: Handle ambiguous case for `INVARIANT: ` prefix.
+          // TODO: Handle multi-line headers.
+          currentDoc = {
+            header: line.replace(`* ${NATSPEC_INV}`, '').trim(),
+            desc: '',
+          }
+
+          // If the header is multi-line, continue appending to the `currentDoc`'s header.
+          while (BLOCK_COMMENT_HEADER_REGEX.test((line = lines[++i]))) {
+            currentDoc.header += ` ${line
+              .replace(BLOCK_COMMENT_PREFIX_REGEX, '')
+              .trim()}`
+          }
+
+          // Process the description
+          while ((line = lines[++i]).startsWith('*')) {
+            line = line.replace(BLOCK_COMMENT_PREFIX_REGEX, '').trim()
+
+            // If the line has any contents, insert it into the desc.
+            // Otherwise, consider it a linebreak.
+            currentDoc.desc += line.length > 0 ? `${line} ` : '\n'
+          }
+
+          // Set the line number of the test
+          currentDoc.lineNo = i + 1
+
+          // Add the doc to the contract
+          contract.docs.push(currentDoc)
+        }
+      }
+    }
+
+    // Add the contract to the array of docs
+    docs.push(contract)
+  }
+
+  for (const contract of docs) {
+    const fileName = path.join(BASE_DOCS_DIR, `${contract.name}.md`)
+    const alreadyWritten = writtenFiles.includes(fileName)
+
+    // If the file has already been written, append the extra docs to the end.
+    // Otherwise, write the file from scratch.
+    fs.writeFileSync(
+      fileName,
+      alreadyWritten
+        ? `${fs.readFileSync(fileName)}\n${renderContractDoc(contract, false)}`
+        : renderContractDoc(contract, true)
+    )
+
+    // If the file was just written for the first time, add it to the list of written files.
+    if (!alreadyWritten) {
+      writtenFiles.push(fileName)
+    }
+  }
+
+  console.log(
+    `Generated invariant test documentation for:\n - ${
+      docs.length
+    } contracts\n - ${docs.reduce(
+      (acc: number, contract: Contract) => acc + contract.docs.length,
+      0
+    )} invariant tests\nsuccessfully!`
+  )
+}
+
+/**
+ * Generate a table of contents for all invariant docs and place it in the README.
+ */
+const tocGen = (): void => {
+  const autoTOCPrefix = '<!-- START autoTOC -->\n'
+  const autoTOCPostfix = '<!-- END autoTOC -->\n'
+
+  // Grab the name of all markdown files in `BASE_DOCS_DIR` except for `README.md`.
+  const files = fs
+    .readdirSync(BASE_DOCS_DIR)
+    .filter((fileName: string) => fileName !== 'README.md')
+
+  // Generate a table of contents section.
+  const tocList = files
+    .map(
+      (fileName: string) => `- [${fileName.replace('.md', '')}](./${fileName})`
+    )
+    .join('\n')
+  const toc = `${autoTOCPrefix}\n## Table of Contents\n${tocList}\n${autoTOCPostfix}`
+
+  // Write the table of contents to the README.
+  const readmeContents = fs
+    .readFileSync(path.join(BASE_DOCS_DIR, 'README.md'))
+    .toString()
+  const above = readmeContents.split(autoTOCPrefix)[0]
+  const below = readmeContents.split(autoTOCPostfix)[1]
+  fs.writeFileSync(
+    path.join(BASE_DOCS_DIR, 'README.md'),
+    `${above}${toc}${below}`
+  )
+}
+
+/**
+ * Render a `Contract` object into valid markdown.
+ */
+const renderContractDoc = (contract: Contract, header: boolean): string => {
+  const _header = header ? `# \`${contract.name}\` Invariants\n` : ''
+  const docs = contract.docs
+    .map((doc: InvariantDoc) => {
+      const line = `${contract.fileName}#L${doc.lineNo}`
+      return `## ${doc.header}\n**Test:** [\`${line}\`](${getGithubBase(
+        contract
+      )}${line})\n\n${doc.desc}`
+    })
+    .join('\n\n')
+  return `${_header}\n${docs}`
+}
+
+/**
+ * Get the base URL for the test contract
+ */
+const getGithubBase = ({ isEchidna }: Contract): string =>
+  isEchidna ? BASE_ECHIDNA_GH_URL : BASE_INVARIANT_GH_URL
+
+// Generate the docs
+
+// Forge
+console.log('Generating docs for forge invariants...')
+docGen(BASE_INVARIANTS_DIR)
+
+// New line
+console.log()
+
+// Echidna
+console.log('Generating docs for echidna invariants...')
+docGen(BASE_ECHIDNA_DIR)
+
+// Generate an updated table of contents
+tocGen()