maint(ci): remove autogenerated invariant docs (#11988)

Removes autogenerated invariant docs from the contracts package.
These autogenerated docs create confusion about where invariants
should be defined (the answer is in the specs) and no one actually
looks at them anyway. Just adds an additional step into CI for
minimal benefit.

.circleci/config.yml

@@ -689,8 +689,6 @@ jobs:
           command: lint
       - run-contracts-check:
           command: gas-snapshot-check
-      - run-contracts-check:
-          command: autogen-invariant-docs
       - run-contracts-check:
           command: snapshots-check-no-build
       - run-contracts-check:

packages/contracts-bedrock/CONTRIBUTING.md

@@ -68,7 +68,6 @@ You can run `just -l` to list them all, some of the key ones are:
 1  `just gas-snapshot` Generates the gas snapshot for the smart contracts.
 1. `just semver-lock` Generates the semver lockfile.
 1. `just snapshots` Generates the storage and ABI snapshots.
-1. `just autogen-invariant-docs` Generates the invariant test documentation.
 1. `just clean` Removes all build artifacts for `forge` and `go` compilations.
 1. `just validate-spacers` Validates the positions of the storage slot spacers.
 1. `just validate-deploy-configs` Validates the deployment configurations in `deploy-config`

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

-# `AddressAliasHelper` Invariants
-
-## Address aliases are always able to be undone.
-**Test:** [`AddressAliasHelper.t.sol#L48`](../test/invariants/AddressAliasHelper.t.sol#L48)
-
-Asserts that an address that has been aliased with `applyL1ToL2Alias` can always be unaliased with `undoL1ToL2Alias`. 
\ No newline at end of file

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

-# `Burn.Eth` Invariants
-
-## `eth(uint256)` always burns the exact amount of eth passed.
-**Test:** [`Burn.Eth.t.sol#L66`](../test/invariants/Burn.Eth.t.sol#L66)
-
-Asserts that when `Burn.eth(uint256)` is called, it always burns the exact amount of ETH passed to the function. 
\ No newline at end of file

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

-# `Burn.Gas` Invariants
-
-## `gas(uint256)` always burns at least the amount of gas passed.
-**Test:** [`Burn.Gas.t.sol#L66`](../test/invariants/Burn.Gas.t.sol#L66)
-
-Asserts that when `Burn.gas(uint256)` is called, it always burns at least the amount of gas passed to the function. 
\ No newline at end of file

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

-# `CrossDomainMessenger` Invariants
-
-## A call to `relayMessage` should succeed if at least the minimum gas limit can be supplied to the target context, there is enough gas to complete execution of `relayMessage` after the target context's execution is finished, and the target context did not revert.
-**Test:** [`CrossDomainMessenger.t.sol#L143`](../test/invariants/CrossDomainMessenger.t.sol#L143)
-
-There are two minimum gas limits here: 
-- The outer min gas limit is for the call from the `OptimismPortal` to the `L1CrossDomainMessenger`,  and it can be retrieved by calling the xdm's `baseGas` function with the `message` and inner limit. 
-- The inner min gas limit is for the call from the `L1CrossDomainMessenger` to the target contract. 
-
-## A call to `relayMessage` should assign the message hash to the `failedMessages` mapping if not enough gas is supplied to forward `minGasLimit` to the target context or if there is not enough gas to complete execution of `relayMessage` after the target context's execution is finished.
-**Test:** [`CrossDomainMessenger.t.sol#L176`](../test/invariants/CrossDomainMessenger.t.sol#L176)
-
-There are two minimum gas limits here: 
-- The outer min gas limit is for the call from the `OptimismPortal` to the `L1CrossDomainMessenger`,  and it can be retrieved by calling the xdm's `baseGas` function with the `message` and inner limit. 
-- The inner min gas limit is for the call from the `L1CrossDomainMessenger` to the target contract. 
\ No newline at end of file

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

-# `ETHLiquidity` Invariants
-
-## Calls to mint/burn repeatedly should never cause the actor's balance to increase beyond the starting balance.
-**Test:** [`ETHLiquidity.t.sol#L86`](../test/invariants/ETHLiquidity.t.sol#L86)
-

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

-# `Encoding` Invariants
-
-## `convertRoundTripAToB` never fails.
-**Test:** [`Encoding.t.sol#L73`](../test/invariants/Encoding.t.sol#L73)
-
-Asserts that a raw versioned nonce can be encoded / decoded to reach the same raw value. 
-
-## `convertRoundTripBToA` never fails.
-**Test:** [`Encoding.t.sol#L82`](../test/invariants/Encoding.t.sol#L82)
-
-Asserts that an encoded versioned nonce can always be decoded / re-encoded to reach the same encoded value. 
\ No newline at end of file

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

-# `FaultDisputeGame` Invariants
-
-## FaultDisputeGame always returns all ETH on total resolution
-**Test:** [`FaultDisputeGame.t.sol#L33`](../test/invariants/FaultDisputeGame.t.sol#L33)
-
-The FaultDisputeGame contract should always return all ETH in the contract to the correct recipients upon resolution of all outstanding claims. There may never be any ETH left in the contract after a full resolution. 
\ No newline at end of file

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

-# `Hashing` Invariants
-
-## `hashCrossDomainMessage` reverts if `version` is > `1`.
-**Test:** [`Hashing.t.sol#L119`](../test/invariants/Hashing.t.sol#L119)
-
-The `hashCrossDomainMessage` function should always revert if the `version` passed is > `1`. 
-
-## `version` = `0`: `hashCrossDomainMessage` and `hashCrossDomainMessageV0` are equivalent.
-**Test:** [`Hashing.t.sol#L129`](../test/invariants/Hashing.t.sol#L129)
-
-If the version passed is 0, `hashCrossDomainMessage` and `hashCrossDomainMessageV0` should be equivalent. 
-
-## `version` = `1`: `hashCrossDomainMessage` and `hashCrossDomainMessageV1` are equivalent.
-**Test:** [`Hashing.t.sol#L140`](../test/invariants/Hashing.t.sol#L140)
-
-If the version passed is 1, `hashCrossDomainMessage` and `hashCrossDomainMessageV1` should be equivalent. 
\ No newline at end of file

packages/contracts-bedrock/invariant-docs/InvariantTest.sol.md

-# `InvariantTest.sol` Invariants
-

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

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

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

-# `OptimismPortal` Invariants
-
-## Deposits of any value should always succeed unless `_to` = `address(0)` or `_isCreation` = `true`.
-**Test:** [`OptimismPortal.t.sol#L151`](../test/invariants/OptimismPortal.t.sol#L151)
-
-All deposits, barring creation transactions and transactions sent to `address(0)`, should always succeed. 
-
-## `finalizeWithdrawalTransaction` should revert if the finalization period has not elapsed.
-**Test:** [`OptimismPortal.t.sol#L174`](../test/invariants/OptimismPortal.t.sol#L174)
-
-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#L204`](../test/invariants/OptimismPortal.t.sol#L204)
-
-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#L233`](../test/invariants/OptimismPortal.t.sol#L233)
-
-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. 
\ No newline at end of file

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

-# `OptimismPortal2` Invariants
-
-## Deposits of any value should always succeed unless `_to` = `address(0)` or `_isCreation` = `true`.
-**Test:** [`OptimismPortal2.t.sol#L163`](../test/invariants/OptimismPortal2.t.sol#L163)
-
-All deposits, barring creation transactions and transactions sent to `address(0)`, should always succeed. 
-
-## `finalizeWithdrawalTransaction` should revert if the proof maturity period has not elapsed.
-**Test:** [`OptimismPortal2.t.sol#L185`](../test/invariants/OptimismPortal2.t.sol#L185)
-
-A withdrawal that has been proven should not be able to be finalized until after the proof maturity period has elapsed. 
-
-## `finalizeWithdrawalTransaction` should revert if the withdrawal has already been finalized.
-**Test:** [`OptimismPortal2.t.sol#L214`](../test/invariants/OptimismPortal2.t.sol#L214)
-
-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 `PROOF_MATURITY_DELAY_SECONDS` after it was successfully proven, if the game has resolved and passed the air-gap.
-**Test:** [`OptimismPortal2.t.sol#L242`](../test/invariants/OptimismPortal2.t.sol#L242)
-
-This invariant asserts that there is no chain of calls that can be made that will prevent a withdrawal from being finalized exactly `PROOF_MATURITY_DELAY_SECONDS` after it was successfully proven and the game has resolved and passed the air-gap. 
\ No newline at end of file

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

-# `OptimismSuperchainERC20` Invariants
-
-## sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)
-**Test:** [`OptimismSuperchainERC20#L36`](../test/invariants/OptimismSuperchainERC20#L36)
-
-
-
-## sum of supertoken total supply across all chains is equal to convert(legacy, super)- convert(super, legacy) when all when all cross-chain messages are processed
-**Test:** [`OptimismSuperchainERC20#L57`](../test/invariants/OptimismSuperchainERC20#L57)
-
-
-
-## many other assertion mode invariants are also defined  under `test/invariants/OptimismSuperchainERC20/fuzz/` .
-**Test:** [`OptimismSuperchainERC20#L80`](../test/invariants/OptimismSuperchainERC20#L80)
-
-since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the handler for assertion test failures 
\ No newline at end of file

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 `pnpm autogen:invariant-docs` -->
-<!-- START autoTOC -->
-
-## Table of Contents
-- [AddressAliasHelper](./AddressAliasHelper.md)
-- [Burn.Eth](./Burn.Eth.md)
-- [Burn.Gas](./Burn.Gas.md)
-- [CrossDomainMessenger](./CrossDomainMessenger.md)
-- [ETHLiquidity](./ETHLiquidity.md)
-- [Encoding](./Encoding.md)
-- [FaultDisputeGame](./FaultDisputeGame.md)
-- [Hashing](./Hashing.md)
-- [InvariantTest.sol](./InvariantTest.sol.md)
-- [L2OutputOracle](./L2OutputOracle.md)
-- [OptimismPortal](./OptimismPortal.md)
-- [OptimismPortal2](./OptimismPortal2.md)
-- [OptimismSuperchainERC20](./OptimismSuperchainERC20.md)
-- [ResourceMetering](./ResourceMetering.md)
-- [SafeCall](./SafeCall.md)
-- [SuperchainWETH](./SuperchainWETH.md)
-- [SystemConfig](./SystemConfig.md)
-<!-- END autoTOC -->
-
-## Usage
-
-To auto-generate documentation for invariant tests, run `just autogen-invariant-docs`.
-
-## Documentation Standard
-
-In order for an invariant test file to be picked up by the [docgen script](../scripts/autogen/generate-invariant-docs.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 {
-    // ...
-}
-```

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:** [`ResourceMetering.t.sol#L166`](../test/invariants/ResourceMetering.t.sol#L166)
-
-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:** [`ResourceMetering.t.sol#L175`](../test/invariants/ResourceMetering.t.sol#L175)
-
-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:** [`ResourceMetering.t.sol#L183`](../test/invariants/ResourceMetering.t.sol#L183)
-
-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:** [`ResourceMetering.t.sol#L191`](../test/invariants/ResourceMetering.t.sol#L191)
-
-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:** [`ResourceMetering.t.sol#L201`](../test/invariants/ResourceMetering.t.sol#L201)
-
-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:** [`ResourceMetering.t.sol#L211`](../test/invariants/ResourceMetering.t.sol#L211)
-
-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:** [`ResourceMetering.t.sol#L220`](../test/invariants/ResourceMetering.t.sol#L220)
-
-When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation should never be allowed to underflow. 
\ No newline at end of file

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

-# `SafeCall` Invariants
-
-## If `callWithMinGas` performs a call, then it must always provide at least the specified minimum gas limit to the subcontext.
-**Test:** [`SafeCall.t.sol#L33`](../test/invariants/SafeCall.t.sol#L33)
-
-If the check for remaining gas in `SafeCall.callWithMinGas` passes, the subcontext of the call below it must be provided at least `minGas` gas. 
-
-## `callWithMinGas` reverts if there is not enough gas to pass to the subcontext.
-**Test:** [`SafeCall.t.sol#L66`](../test/invariants/SafeCall.t.sol#L66)
-
-If there is not enough gas in the callframe to ensure that `callWithMinGas` can provide the specified minimum gas limit to the subcontext of the call, then `callWithMinGas` must revert. 
\ No newline at end of file

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

-# `SuperchainWETH` Invariants
-
-## Calls to sendERC20 should always succeed as long as the actor has less than uint248 wei which is much greater than the total ETH supply. Actor's balance should also not increase out of nowhere.
-**Test:** [`SuperchainWETH.t.sol#L184`](../test/invariants/SuperchainWETH.t.sol#L184)
-

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

-# `SystemConfig` Invariants
-
-## Gas limit boundaries
-**Test:** [`SystemConfig.t.sol#L71`](../test/invariants/SystemConfig.t.sol#L71)
-
-The gas limit of the `SystemConfig` contract can never be lower than the hard-coded lower bound or higher than the hard-coded upper bound. The lower bound must never be higher than the upper bound. 
\ No newline at end of file

packages/contracts-bedrock/justfile

@@ -13,9 +13,6 @@ build: prebuild
 build-go-ffi:
   cd scripts/go-ffi && go build
 
-autogen-invariant-docs:
-  go run ./scripts/autogen/generate-invariant-docs .
-
 test: build-go-ffi
   forge test
 
@@ -133,7 +130,7 @@ clean:
   rm -rf ./artifacts ./forge-artifacts ./cache ./scripts/go-ffi/go-ffi ./deployments/hardhat/*
   find ./.testdata -mindepth 1 -not -name '.gitkeep' -delete
 
-pre-pr-no-build: gas-snapshot-no-build snapshots-no-build semver-lock autogen-invariant-docs lint
+pre-pr-no-build: gas-snapshot-no-build snapshots-no-build semver-lock lint
 
 pre-pr: clean build-go-ffi build pre-pr-no-build
 

packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go

-package main
-
-import (
-	"flag"
-	"fmt"
-	"os"
-	"path/filepath"
-	"slices"
-	"strings"
-)
-
-const (
-	NatspecInv         = "@custom:invariant"
-	BaseInvariantGhUrl = "../test/invariants/"
-)
-
-// Contract represents an invariant test contract
-type Contract struct {
-	Name     string
-	FileName string
-	Docs     []InvariantDoc
-}
-
-// InvariantDoc represents the documentation of an invariant
-type InvariantDoc struct {
-	Header string
-	Desc   string
-	LineNo int
-}
-
-var writtenFiles []string
-
-// Generate the docs
-func main() {
-	flag.Parse()
-	if flag.NArg() != 1 {
-		fmt.Println("Expected path of contracts-bedrock as CLI argument")
-		os.Exit(1)
-	}
-	rootDir := flag.Arg(0)
-
-	invariantsDir := filepath.Join(rootDir, "test/invariants")
-	fmt.Printf("invariants dir: %s\n", invariantsDir)
-	docsDir := filepath.Join(rootDir, "invariant-docs")
-	fmt.Printf("invariant docs dir: %s\n", docsDir)
-
-	// Forge
-	fmt.Println("Generating docs for forge invariants...")
-	if err := docGen(invariantsDir, docsDir); err != nil {
-		fmt.Printf("Failed to generate invariant docs: %v\n", err)
-		os.Exit(1)
-	}
-
-	fmt.Println("Generating table-of-contents...")
-	// Generate an updated table of contents
-	if err := tocGen(docsDir); err != nil {
-		fmt.Printf("Failed to generate TOC of docs: %v\n", err)
-		os.Exit(1)
-	}
-	fmt.Println("Done!")
-}
-
-// Lazy-parses all test files in the `test/invariants` directory
-// to generate documentation on all invariant tests.
-func docGen(invariantsDir, docsDir string) error {
-
-	// Grab all files within the invariants test dir
-	files, err := os.ReadDir(invariantsDir)
-	if err != nil {
-		return fmt.Errorf("error reading directory: %w", err)
-	}
-
-	// Array to store all found invariant documentation comments.
-	var docs []Contract
-
-	for _, file := range files {
-		// Read the contents of the invariant test file.
-		fileName := file.Name()
-		filePath := filepath.Join(invariantsDir, fileName)
-		// where invariants for a module have their own directory, interpret
-		// the test file with the same name as the directory as a 'main' of
-		// sorts, from where documentation is pulled
-		if file.IsDir() {
-			filePath = filepath.Join(filePath, strings.Join([]string{fileName, ".t.sol"}, ""))
-		}
-		fileContents, err := os.ReadFile(filePath)
-		if err != nil {
-			return fmt.Errorf("error reading file %q: %w", filePath, err)
-		}
-
-		// Split the file into individual lines and trim whitespace.
-		lines := strings.Split(string(fileContents), "\n")
-		for i, line := range lines {
-			lines[i] = strings.TrimSpace(line)
-		}
-
-		// Create an object to store all invariant test docs for the current contract
-		name := strings.Replace(fileName, ".t.sol", "", 1)
-		contract := Contract{Name: name, FileName: fileName}
-
-		var currentDoc InvariantDoc
-
-		// Loop through all lines to find comments.
-		for i := 0; i < len(lines); i++ {
-			line := lines[i]
-
-			// We have an invariant doc
-			if strings.HasPrefix(line, "/// "+NatspecInv) {
-				// Assign the header of the invariant doc.
-				currentDoc = InvariantDoc{
-					Header: strings.TrimSpace(strings.Replace(line, "/// "+NatspecInv, "", 1)),
-					Desc:   "",
-				}
-				i++
-
-				// If the header is multi-line, continue appending to the `currentDoc`'s header.
-				for {
-					if i >= len(lines) {
-						break
-					}
-					line = lines[i]
-					i++
-					if !(strings.HasPrefix(line, "///") && strings.TrimSpace(line) != "///") {
-						break
-					}
-					currentDoc.Header += " " + strings.TrimSpace(strings.Replace(line, "///", "", 1))
-				}
-
-				// Process the description
-				for {
-					if i >= len(lines) {
-						break
-					}
-					line = lines[i]
-					i++
-					if !strings.HasPrefix(line, "///") {
-						break
-					}
-					line = strings.TrimSpace(strings.Replace(line, "///", "", 1))
-
-					// If the line has any contents, insert it into the desc.
-					// Otherwise, consider it a linebreak.
-					if len(line) > 0 {
-						currentDoc.Desc += line + " "
-					} else {
-						currentDoc.Desc += "\n"
-					}
-				}
-
-				// Set the line number of the test
-				currentDoc.LineNo = i
-
-				// Add the doc to the contract
-				contract.Docs = append(contract.Docs, currentDoc)
-			}
-		}
-
-		// Add the contract to the array of docs
-		docs = append(docs, contract)
-	}
-
-	for _, contract := range docs {
-		filePath := filepath.Join(docsDir, contract.Name+".md")
-		alreadyWritten := slices.Contains(writtenFiles, filePath)
-
-		// If the file has already been written, append the extra docs to the end.
-		// Otherwise, write the file from scratch.
-		var fileContent string
-		if alreadyWritten {
-			existingContent, err := os.ReadFile(filePath)
-			if err != nil {
-				return fmt.Errorf("error reading existing file %q: %w", filePath, err)
-			}
-			fileContent = string(existingContent) + "\n" + renderContractDoc(contract, false)
-		} else {
-			fileContent = renderContractDoc(contract, true)
-		}
-
-		err = os.WriteFile(filePath, []byte(fileContent), 0644)
-		if err != nil {
-			return fmt.Errorf("error writing file %q: %w", filePath, err)
-		}
-
-		if !alreadyWritten {
-			writtenFiles = append(writtenFiles, filePath)
-		}
-	}
-
-	_, _ = fmt.Fprintf(os.Stderr,
-		"Generated invariant test documentation for:\n"+
-			" - %d contracts\n"+
-			" - %d invariant tests\n"+
-			"successfully!\n",
-		len(docs),
-		func() int {
-			total := 0
-			for _, contract := range docs {
-				total += len(contract.Docs)
-			}
-			return total
-		}(),
-	)
-	return nil
-}
-
-// Generate a table of contents for all invariant docs and place it in the README.
-func tocGen(docsDir string) error {
-	autoTOCPrefix := "<!-- START autoTOC -->\n"
-	autoTOCPostfix := "<!-- END autoTOC -->\n"
-
-	files, err := os.ReadDir(docsDir)
-	if err != nil {
-		return fmt.Errorf("error reading directory %q: %w", docsDir, err)
-	}
-
-	// Generate a table of contents section.
-	var tocList []string
-	for _, file := range files {
-		fileName := file.Name()
-		if fileName != "README.md" {
-			tocList = append(tocList, fmt.Sprintf("- [%s](./%s)", strings.Replace(fileName, ".md", "", 1), fileName))
-		}
-	}
-	toc := fmt.Sprintf("%s\n## Table of Contents\n%s\n%s",
-		autoTOCPrefix, strings.Join(tocList, "\n"), autoTOCPostfix)
-
-	// Write the table of contents to the README.
-	readmePath := filepath.Join(docsDir, "README.md")
-	readmeContents, err := os.ReadFile(readmePath)
-	if err != nil {
-		return fmt.Errorf("error reading README file %q: %w", readmePath, err)
-	}
-	readmeParts := strings.Split(string(readmeContents), autoTOCPrefix)
-	above := readmeParts[0]
-	readmeParts = strings.Split(readmeParts[1], autoTOCPostfix)
-	below := readmeParts[1]
-	err = os.WriteFile(readmePath, []byte(above+toc+below), 0644)
-	if err != nil {
-		return fmt.Errorf("error writing README file %q: %w", readmePath, err)
-	}
-	return nil
-}
-
-// Render a `Contract` object into valid markdown.
-func renderContractDoc(contract Contract, header bool) string {
-	var sb strings.Builder
-
-	if header {
-		sb.WriteString(fmt.Sprintf("# `%s` Invariants\n", contract.Name))
-	}
-	sb.WriteString("\n")
-
-	for i, doc := range contract.Docs {
-		line := fmt.Sprintf("%s#L%d", contract.FileName, doc.LineNo)
-		sb.WriteString(fmt.Sprintf("## %s\n**Test:** [`%s`](%s%s)\n\n%s", doc.Header, line, BaseInvariantGhUrl, line, doc.Desc))
-		if i != len(contract.Docs)-1 {
-			sb.WriteString("\n\n")
-		}
-	}
-
-	return sb.String()
-}