Kontrol documentation and cleanup (#9254)

* docs: change directory structure format

* build: add kontrol installation commands

* chore: simpler kprove profile

* chore: update help text in run-kontrol.sh

* docs: refactor and clarify README content

* chore: fix typo in test name

* ci: check kontrol state diff in snapshot checks

* feat: cleanup even when forge script fails

* perf: improve assumptions and better document them

* doc: more docs

* doc: update description of make-summary-deployment.sh
Co-authored-by: Juan C. <38925412+JuanCoRo@users.noreply.github.com>

* perf: revert back to the 320 byte assumption for now

* doc: clarify optionality of build step

* fix: add output directory to shellcheck ignored dirs

* fix/refactor: snapshots job needs kontrol via docker in CI

* fix: shellcheck lints

* docs: fix links and add brief summary of adding new proofs

* fix: remove shift, which cause early exit

we only have 1 input param so don't need shift: when shift fails
it would cause the script to exit early due to set -e

* fix: run in proper environment

* fix: start docker when needed

* chore: cleanup docker

* fix: another fix from shell script refactor

* ci: add docker to bedrock tests

* fix(ci): move remote docker from contracts-bedrock-tests to contracts-bedrock-checks

* ci: maybe docker setup needs to come earlier

* fix: various changes so make-summary-deployment works in docker

- avoid copying node_modules to container, which caused a symlink error
- fix which script commands are run in docker
- restore order of setup_remote_docker step

* fix: bind mount instead of copy into docker

* style: remove unneded braces

* fix: -v to create dir on docker, restore file copying

* fix: copy new files

* fix permissions error

---------
Co-authored-by: Juan C. <38925412+JuanCoRo@users.noreply.github.com>

.circleci/config.yml

@@ -397,6 +397,8 @@ jobs:
       - attach_workspace: { at: "." }
       - check-changed:
           patterns: contracts-bedrock,op-node
+      - setup_remote_docker:
+          docker_layer_caching: true
       # populate node modules from the cache
       - run:
           name: Install dependencies

package.json

@@ -21,7 +21,7 @@
     "lint:ts:check": "npx nx run-many --target=lint:ts:check",
     "lint:check": "npx nx run-many --target=lint:check",
     "lint:fix": "npx nx run-many --target=lint:fix",
-    "lint:shellcheck": "find . -type f -name '*.sh' -not -path '*/node_modules/*' -not -path './packages/contracts-bedrock/lib/*' -not -path './.husky/_/husky.sh' -exec sh -c 'echo \"Checking $1\"; shellcheck \"$1\"' _ {} \\;",
+    "lint:shellcheck": "find . -type f -name '*.sh' -not -path '*/node_modules/*' -not -path './packages/contracts-bedrock/lib/*' -not -path './packages/contracts-bedrock/kout*/*' -not -path './.husky/_/husky.sh' -exec sh -c 'echo \"Checking $1\"; shellcheck \"$1\"' _ {} \\;",
     "preinstall": "npx only-allow pnpm",
     "ready": "pnpm lint && pnpm test",
     "prepare": "husky install",
@@ -31,6 +31,8 @@
     "release:version": "changeset version && pnpm install --lockfile-only",
     "install:foundry": "curl -L https://foundry.paradigm.xyz | bash && pnpm update:foundry",
     "update:foundry": "bash ./ops/scripts/install-foundry.sh",
+    "install:kontrol": "curl -L https://kframework.org/install | bash && pnpm update:kontrol",
+    "update:kontrol": "kup install kontrol --version v$(jq -r .kontrol < versions.json)",
     "install:abigen": "go install github.com/ethereum/go-ethereum/cmd/abigen@$(jq -r .abigen < versions.json)",
     "print:abigen": "abigen --version | sed -e 's/[^0-9]/ /g' -e 's/^ *//g' -e 's/ *$//g' -e 's/ /./g' -e 's/^/v/'",
     "check:abigen": "[[ $(pnpm -s print:abigen) = $(cat versions.json | jq -r '.abigen') ]] && echo '✓ abigen versions match' || (echo '✗ abigen version mismatch. Run `pnpm upgrade:abigen` to upgrade.' && exit 1)",

packages/contracts-bedrock/foundry.toml

@@ -86,4 +86,4 @@ script = 'scripts-kontrol'
 src = 'test/kontrol/proofs'
 out = 'kout-proofs'
 test = 'test/kontrol/proofs'
-script = 'scripts-kontrol'
+script = 'test/kontrol/proofs'

packages/contracts-bedrock/package.json

@@ -27,7 +27,7 @@
     "gas-snapshot:no-build": "forge snapshot --match-contract GasBenchMark",
     "statediff": "./scripts/statediff.sh && git diff --exit-code",
     "gas-snapshot": "pnpm build:go-ffi && pnpm gas-snapshot:no-build",
-    "snapshots": "npx tsx scripts/generate-snapshots.ts",
+    "snapshots": "npx tsx scripts/generate-snapshots.ts && ./test/kontrol/scripts/make-summary-deployment.sh",
     "snapshots:check": "./scripts/check-snapshots.sh",
     "slither": "./scripts/slither.sh",
     "slither:check": "pnpm slither && git diff --exit-code",

packages/contracts-bedrock/test/kontrol/README.md

 # Kontrol Verification
 
-This folder contains Kontrol symbolic property tests.
+<!-- START doctoc generated TOC please keep comment here to allow auto update -->
+<!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-## Directory structure
+- [Getting Started](#getting-started)
+  - [Overview](#overview)
+  - [Directory structure](#directory-structure)
+  - [Installation](#installation)
+- [Usage](#usage)
+  - [Build Deployment Summary](#build-deployment-summary)
+  - [Execute Proofs](#execute-proofs)
+  - [Add New Proofs](#add-new-proofs)
+- [Implementation Details](#implementation-details)
+  - [Assumptions](#assumptions)
+  - [Deployment Summary Process](#deployment-summary-process)
 
-The directory is structured as follows
+<!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
-```tree
-test/kontrol
-├── deployment
-│   ├── DeploymentSummary.t.sol
-│   └── KontrolDeployment.sol
-├── pausability-lemmas.k
-├── proofs
-│   ├── interfaces
-│   │   └── KontrolInterfaces.sol
-│   ├── L1CrossDomainMessenger.k.sol
-│   ├── L1ERC721Bridge.k.sol
-│   ├── L1StandardBridge.k.sol
-│   ├── OptimismPortal.k.sol
-│   └── utils
-│       ├── DeploymentSummaryCode.sol
-│       ├── DeploymentSummary.sol
-│       └── KontrolUtils.sol
-├── README.md
-└── scripts
-    ├── json
-    │   ├── clean_json.py
-    │   └── reverse_key_values.py
-    ├── make-summary-deployment.sh
-    └── run-kontrol.sh
-```
+## Getting Started
+
+### Overview
 
-### Root folder
+[Kontrol](https://github.com/runtimeverification/kontrol) is a tool by [Runtime Verification](https://runtimeverification.com/) (RV) that enables formal verification of Ethereum smart contracts. Quoting from the Kontrol [docs](https://docs.runtimeverification.com/kontrol/overview/readme):
 
-- [`pausability-lemmas.k`](./pausability-lemmas.k): File containing the necessary lemmas for this project
-- [`deployment`](./deployment): Custom deploy sequence for Kontrol proofs and tests for its summarization
-- [`proofs`](./proofs): Where the proofs of the project live
-- [`scripts`](./scripts): Where the scripts of the projects live
+> Kontrol combines [KEVM](https://github.com/runtimeverification/evm-semantics) and [Foundry](https://book.getfoundry.sh/) to grant developers the ability to perform [formal verification](https://en.wikipedia.org/wiki/Formal_verification) without learning a new language or tool. This is especially useful for those who are not verification engineers. Additionally, developers can leverage Foundry test suites they have already developed and use symbolic execution to increase the level of confidence.
+>
+> KEVM is a tool that enables formal verification of smart contracts on the Ethereum blockchain. It provides a mathematical foundation for specifying and implementing smart contracts. Developers can use KEVM to rigorously reason about the behavior of their smart contracts, ensuring correctness and reducing the likelihood of vulnerabilities in the contract code.
 
-### [`deployment`](./deployment) folder
+This document details the Kontrol setup used in this repo to run various proofs against the contracts in the [`contracts-bedrock`](../../) directory.
+
+### Directory structure
+
+The directory is structured as follows
 
-- [`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol): Simplified deployment sequence for Kontrol proofs
-- [`DeploymentSummary.t.sol`](./deployment/DeploymentSummary.t.sol): Tests for the summarization of custom deployment
+<pre>
+├── <a href="./pausability-lemmas.k">pausability-lemmas.k</a>: File containing the necessary lemmas for this project
+├── <a href="./deployment">deployment</a>: Custom deploy sequence for Kontrol proofs and tests for its <a href="https://github.com/runtimeverification/kontrol/pull/271">fast summarization</a>
+│   ├── <a href="./deployment/KontrolDeployment.sol">KontrolDeployment.sol</a>: Simplified deployment sequence for Kontrol proofs
+│   └── <a href="./deployment/DeploymentSummary.t.sol">DeploymentSummary.t.sol</a>: Tests for the summarization of custom deployment
+├── <a href="./proofs">proofs</a>: Where the proofs (tests) themselves live
+│   ├── *.k.sol</a>: Symbolic property tests for contracts
+│   ├── <a href="./proofs/interfaces">interfaces</a>: Interface files for src contracts, to avoid unnecessary compilation of contracts
+│   └── <a href="./proofs/utils">utils</a>: Proof dependencies, including the autogenerated deployment summary contracts
+└── <a href="./scripts">scripts</a>: Where the scripts of the projects live
+    ├── <a href="./scripts/json">json</a>: Data cleaning scripts for the output of <a href="./deployment/KontrolDeployment.sol">KontrolDeployment.sol</a>
+    ├── <a href="./scripts/make-summary-deployment.sh">make-summary-deployment.sh</a>: Executes <a href="./deployment/KontrolDeployment.sol">KontrolDeployment.sol</a>, curates the result and writes the summary deployment contract
+    └── <a href="./scripts/run-kontrol.sh">run-kontrol.sh</a>: Wrapper around the kontrol CLI to run the proofs
+</pre>
 
-### [`proofs`](./proofs) folder
+### Installation
 
-- [`L1CrossDomainMessenger.k.sol`](./proofs/L1CrossDomainMessenger.k.sol): Symbolic property tests for [`L1CrossDomainMessenger`](../../src/L1/L1CrossDomainMessenger.sol)
-- [`L1ERC721Bridge.k.sol`](./proofs/L1ERC721Bridge.k.sol): Symbolic property tests for [`L1ERC721Bridge`](../../src/L1/L1ERC721Bridge.sol)
-- [`L1StandardBridge.k.sol`](./proofs/L1StandardBridge.k.sol): Symbolic property tests for [`L1StandardBridge`](../../src/L1/L1StandardBridge.sol)
-- [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol): Symbolic property tests for [`OptimismPortal`](../../src/L1/OptimismPortal.sol)
-- [`interfaces`](./proofs/interfaces): Files with the signature of the functions involved in the verification effort
-- [`utils`](./proofs/utils): Proof dependencies, including the summary contracts
+1. `cd` to the root of this repo.
+2. Install Foundry by running `pnpm install:foundry`. This installs `foundryup`, the foundry toolchain installer, then installs the required foundry version.
+3. Install Kontrol by running `pnpm install:kontrol`. This installs `kup`, the package manager for RV tools, then installs the required kontrol version.
+4. Install Docker.
 
-### [`scripts`](./scripts) folder
+## Usage
 
-- [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh): Executes [`KontrolDeployment.sol`](./KontrolDeployment.sol), curates the result and writes the summary deployment contract
-- [`run-kontrol.sh`](./scrpts/run-kontrol.sh): Proof execution script
-- [`json`](./scripts/json): Data cleaning scripts for the output of [`KontrolDeployment.sol`](./KontrolDeployment.sol)
+Verifying proofs has two steps: build, and execute.
 
-## Verification execution
+### Build Deployment Summary
 
-The verification execution consists of two steps, although the first step may be omitted to use the committed version. There's one script to run per step. These scripts should be run from the [`contracts-bedrock`](../../) directory.
+First, generate a deployment summary contract from the deploy script in [`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol) by running the following command:
 
-1. Generate a deployment summary contract from [`KontrolDeployment.sol`](./KontrolDeployment.sol)
 ```bash
-  ./test/kontrol/scripts/make-summary-deployment.sh
+./test/kontrol/scripts/make-summary-deployment.sh
 ```
-This step is optional. The default summary can be found [here](./proofs/utils/DeploymentSummary.sol), which is the summarization of the [`KontrolDeployment.sol`](./KontrolDeployment.sol) script.
 
-2. Execute the tests in [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol)
-```bash
-  ./test/kontrol/scripts/run-kontrol.sh $option
+[`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol) contains the minimal deployment sequence required by the proofs.
+The [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) script will generate a JSON state diff. This state diff is used in two ways by Kontrol.
+First, Kontrol generates a summary contract recreating the state diffs recorded in the JSON. This contract is used to test that the information contained in the generated JSON is correct and aids in the specification of the symbolic property tests. The generation of this contract is also handled by the `make-summary-deployment.sh` script.
+Second, the state diff JSON is used to load the post-deployment state directly into Kontrol when running the proofs.
+
+This step is optional if an up-to-date summary contract already exists, which will be the case until the `KontrolDeployment` contract changes, or any of the source contracts under test change.
+See the [Implementation Details](#implementation-details) section for more information, and to learn about the CI check that ensures the committed autogenerated files from this step are up-to-date.
+
+The summary contract can be found in [`DeploymentSummary.sol`](./proofs/utils/DeploymentSummary.sol), which is summarization (state changes) of the [`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol) contract.
+
+### Execute Proofs
+
+Use the [`run-kontrol.sh`](./scripts/run-kontrol.sh) script to runs the proofs in all `*.k.sol` files.
+
+```
+./test/kontrol/scripts/run-kontrol.sh [container|local|dev]
 ```
-See below for further documentation on `run-kontrol.sh`.
 
-### `run-kontrol.sh` script
-The `run-kontrol.sh` script handles all modes of proof execution. The modes, corresponding to the available arguments of the script, are the following:
-- `container`: Run the proofs in the same docker image used in CI. The intended use case is CI debugging. This is the default execution mode, meaning that if no arguments are provided, the proofs will be executed in this mode.
-- `local`: Run the proofs with your local Kontrol install, enforcing the version to be the same as the one used in CI. The intended use case is running the proofs without risking discrepancies because of different Kontrol versions.
+The `run-kontrol.sh` script supports three modes of proof execution:
+
+- `container`: Runs the proofs using the same Docker image used in CI. This is the default execution mode—if no arguments are provided, the proofs will be executed in this mode.
+- `local`: Runs the proofs with your local Kontrol install, and enforces that the Kontrol version matches the one used in CI, which is specified in [`versions.json`](../../../../versions.json).
 - `dev`: Run the proofs with your local Kontrol install, without enforcing any version in particular. The intended use case is proof development and related matters.
 
 For a similar description of the options run `run-kontrol.sh --help`.
 
-## Kontrol Foundry profiles
+### Add New Proofs
+
+More details on best practices for writing and adding new proofs will be added here in the future.
+The summary is:
+
+1. Update the deployment summary and its tests as needed.
+2. Write the proofs in an appropriate `*.k.sol` file in the `proofs` folder.
+3. Add the proof name to the `test_list` array in the [`run-kontrol.sh`](./scripts/run-kontrol.sh) script.
+
+## Implementation Details
+
+### Assumptions
+
+1. A critical invariant of the `KontrolDeployment.sol` contract is that it stays in sync with the original `Deploy.s.sol` contract.
+   Currently, this is partly enforced by running some of the standard post-`setUp` deployment assertions in `DeploymentSummary.t.sol`.
+   A more rigorous approach may be to leverage the `ChainAssertions` library, but more investigation is required to determine if this is feasible without large changes to the deploy script.
+
+2. Until symbolic bytes are natively supported in Kontrol, we must make assumptions about the length of `bytes` parameters.
+   All current assumptions can be found by searching for `// ASSUME:` comments in the files.
+   Some of this assumptions can be lifted once [symbolic bytes](https://github.com/runtimeverification/kontrol/issues/272) are supported in Kontrol.
+
+### Deployment Summary Process
+
+As mentioned above, a deployment summary contract is first generated before executing the proofs.
+This is because the proof execution leverages Kontrol's [fast summarization](https://github.com/runtimeverification/kontrol/pull/271) feature, which allows loading the post-`setUp` state directly into Kontrol.
+This provides a significant reduction in proof execution time, as it avoids the need to execute the deployment script every time the proofs are run.
 
-This project uses two different [Foundry profiles](../../foundry.toml), `kdeploy` and `kprove`.
+All code executed in Kontrol—even when execution is concrete and not symbolic—is significantly slower than in Foundry, due to the mathematical representation of the EVM in Kontrol.
+Therefore we want to minimize the amount of code executed in Kontrol, and the fast summarization feature allows us to reduce `setUp` execution time.
 
-- `kdeploy`: This profile is used to generate a summary contract from the execution of the [`KontrolDeployment.sol`](./KontrolDeployment.sol) script. In particular, the `kdeploy` profile is used by the [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) script to generate the [deployment summary contract](./proofs/utils/DeploymentSummary.sol). The summary contract is then used with the `kprove` profile to load the post-setUp state directly into Kontrol. We don't need the output artifacts from this step, so we save them to the `kout-deployment` directory, which is not used anywhere else. We also point the script path to the `scripts-kontrol` directory, which does not exist, to avoid compiling scripts we don't need, which reduces execution time.
+This project uses two different [`foundry.toml` profiles](../../foundry.toml), `kdeploy` and `kprove`, to facilitate usage of this fast summarization feature.:
 
-- `kprove`: This profile is used by the [`run-kontrol.sh`](./scrpts/run-kontrol.sh) script, which needs to be run after executing [`./test/kontrol/script/make-summary-deployment`](./scripts/make-summary-deployment.sh) (this last script uses the `kdeploy` profile). The proofs are executed using the `kprove` profile. The `src` directory points to a test folder because we only want to compile what is in the `test/kontrol/proofs` folder since it contains all the deployed bytecode and the proofs. We similarly point the script path to a non-existent directory for the same reason as above. The `out` folder for this profile is `kout-proofs`.
+- `kdeploy`: Used by [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) to generate the `DeploymentSummary.sol` contract based on execution of the `KontrolDeployment.sol` contract using Foundry's state diff recording cheatcodes.
+  This is where all necessary [`src/L1`](../../src/L1) files are compiled with their bytecode saved into the `DeploymentSummaryCode.sol` file, which is inherited by `DeploymentSummary`.
 
-Note that the compilation of the necessary `src/L1` files is done with the `kdeploy` profile, and the results are saved into [`test/kontrol/proofs/utils/DeploymentSummary.sol`](./proofs/utils/DeploymentSummary.sol). So, when running the `kprove` profile, the deployed bytecode of the `src/L1` files are recorded in the automatically generated file `test/kontrol/proofs/utils/DeploymentSummaryCode.sol`.
+- `kprove`: Used by the [`run-kontrol.sh`](./scrpts/run-kontrol.sh) script to execute proofs, which can be run once a `DeploymentSummary.sol` contract is present. This profile's `src` and `script` paths point to a test folder because we only want to compile what is in the `test/kontrol/proofs` folder, since that folder contains all bytecode and proofs.
 
-## References
+The `make-summary-deployment.sh` scripts saves off the generated JSON state diff to `snapshots/state-diff/Kontrol-Deploy.json`, and is run as part of the `snapshots` script in `package.json`.
+Therefore, the snapshots CI check will fail if the committed Kontrol state diff is out of sync.
+Note that the CI check only compares the JSON state diff, not the generated `DeploymentSummary.sol` or `DeploymentSummaryCode` contracts.
+This is for simplicity, as those three files will be in sync upon successful execution of the `make-summary-deployment.sh` script.
+We commit the `DeploymentSummary.sol` and `DeploymentSummaryCode.sol` contracts, because forge fails to build if those contracts are not present—it is simpler to commit these autogenerated files than to workaround their absence in forge builds.
 
-[Kontrol docs](https://docs.runtimeverification.com/kontrol/overview/readme)
+During `make-summary-deployment.sh`, the `mustGetAddress` usage in `Deploy.s.sol` is temporarily replaced by `getAddress`—the former reverts if the deployed contract does not exist, while the latter returns the zero address.
+This is required because the deploy script in `KontrolDeployment.sol` is does not fully reproduce all deployments in `Deploy.s.sol`, so the `mustGetAddress` usage would cause the script to revert since some contracts are not deployed.
+`KontrolDeployment.sol` is a simplified, minimal deployment sequence for Kontrol proofs, and is not intended to be a full deployment sequence for the contracts in `contracts-bedrock`.

packages/contracts-bedrock/test/kontrol/proofs/L1CrossDomainMessenger.k.sol

@@ -33,7 +33,9 @@ contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
     {
         setUpInlined();
 
-        // ASSUME: conservative upper bound on the `_message` length
+        // ASSUME: Conservative upper bound on the `_message` length. Most contract calls will have
+        // a message length less than 600 bytes. This assumption can be removed once Kontrol
+        // supports symbolic `bytes`: https://github.com/runtimeverification/kontrol/issues/272
         bytes memory _message = freshBigBytes(600);
 
         // Pause System

packages/contracts-bedrock/test/kontrol/proofs/L1ERC721Bridge.k.sol

@@ -21,7 +21,7 @@ contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
     /// TODO: Replace symbolic workarounds with the appropriate
     /// types once Kontrol supports symbolic `bytes` and `bytes[]`
     /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
-    function prove_finalizeBridgeERC21_paused(
+    function prove_finalizeBridgeERC721_paused(
         address _localToken,
         address _remoteToken,
         address _from,
@@ -41,8 +41,10 @@ contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
             bytes32(uint256(uint160(address(l1ERC721Bridge.otherBridge()))))
         );
 
-        // ASSUME: conservative upper bound on the `_extraData` length
-        bytes memory _extraData = freshBigBytes(320);
+        // ASSUME: Conservative upper bound on the `_extraData` length, since extra data is optional
+        // for convenience of off-chain tooling. This assumption can be removed once Kontrol
+        // supports symbolic `bytes`: https://github.com/runtimeverification/kontrol/issues/272
+        bytes memory _extraData = freshBigBytes(64);
 
         // Pause Standard Bridge
         vm.prank(superchainConfig.guardian());

packages/contracts-bedrock/test/kontrol/proofs/L1StandardBridge.k.sol

@@ -41,8 +41,11 @@ contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
             bytes32(uint256(uint160(address(l1standardBridge.otherBridge()))))
         );
 
-        // ASSUME: conservative upper bound on the `_extraData` length
-        bytes memory _extraData = freshBigBytes(320);
+        // ASSUME: Upper bound on the `_extraData` length, since extra data is optional for
+        // for convenience of off-chain tooling, and should not affect execution  This assumption
+        // can be removed once Kontrol supports symbolic `bytes`:
+        // https://github.com/runtimeverification/kontrol/issues/272
+        bytes memory _extraData = freshBigBytes(32);
 
         // Pause Standard Bridge
         vm.prank(superchainConfig.guardian());
@@ -71,8 +74,11 @@ contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
             bytes32(uint256(uint160(address(l1standardBridge.otherBridge()))))
         );
 
-        // ASSUME: conservative upper bound on the `_extraData` length
-        bytes memory _extraData = freshBigBytes(320);
+        // ASSUME: Upper bound on the `_extraData` length, since extra data is optional for
+        // for convenience of off-chain tooling, and should not affect execution  This assumption
+        // can be removed once Kontrol supports symbolic `bytes`:
+        // https://github.com/runtimeverification/kontrol/issues/272
+        bytes memory _extraData = freshBigBytes(32);
 
         // Pause Standard Bridge
         vm.prank(superchainConfig.guardian());

packages/contracts-bedrock/test/kontrol/proofs/OptimismPortal.k.sol

@@ -42,7 +42,11 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     {
         setUpInlined();
 
-        // ASSUME: conservative upper bound on the `_data` length
+        // ASSUME: This bound on the `_data` length is too low, and should be at least 1000 bytes.
+        // Kontrol currently hangs and fails with this value because of the resulting configuration
+        // size. For now we leave this as a low value to avoid the hang, but it should be increased
+        // once Kontrol is improved and supports symbolic `bytes`:
+        // https://github.com/runtimeverification/kontrol/issues/272
         bytes memory _data = freshBigBytes(320);
         bytes[] memory _withdrawalProof = freshWithdrawalProof();
 
@@ -74,7 +78,11 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     {
         setUpInlined();
 
-        // ASSUME: conservative upper bound on the `_data` length
+        // ASSUME: This bound on the `_data` length is too low, and should be at least 1000 bytes.
+        // Kontrol currently hangs and fails with this value because of the resulting configuration
+        // size. For now we leave this as a low value to avoid the hang, but it should be increased
+        // once Kontrol is improved and supports symbolic `bytes`:
+        // https://github.com/runtimeverification/kontrol/issues/272
         bytes memory _data = freshBigBytes(320);
 
         // Pause Optimism Portal

packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolUtils.sol

@@ -2,9 +2,10 @@
 pragma solidity 0.8.15;
 
 import { Vm } from "forge-std/Vm.sol";
-import { Types } from "src/libraries/Types.sol";
 import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol";
 
+// The GhostBytes contracts are a workaround to create a symbolic bytes array. This is slow, but
+// required until symbolic bytes are supported in Kontrol: https://github.com/runtimeverification/kontrol/issues/272
 contract GhostBytes {
     bytes public ghostBytes;
 }
@@ -36,12 +37,9 @@ contract GhostBytes10 {
     }
 }
 
-/// @notice tests inheriting this contract cannot be run with forge
+/// @notice Tests inheriting this contract cannot be run with forge
 abstract contract KontrolUtils is KontrolCheats {
-    /// @dev we only care about the vm signature
-    // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D.
-    address internal constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
-    Vm internal constant vm = Vm(VM_ADDRESS);
+    Vm internal constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code")))));
 
     /// @dev Creates a fresh bytes with length greater than 31
     /// @param bytesLength: Length of the fresh bytes. Should be concrete
@@ -65,55 +63,18 @@ abstract contract KontrolUtils is KontrolCheats {
         sBytes = ghostBytes.ghostBytes();
     }
 
-    /// @dev Creates a bounded symbolic bytes[] memory representing a withdrawal proof
-    /// Each element is 17 * 32 = 544 bytes long, plus ~10% margin for RLP encoding: each element is 600 bytes
-    /// The length of the array to 10 or fewer elements
+    /// @dev Creates a bounded symbolic bytes[] memory representing a withdrawal proof.
     function freshWithdrawalProof() public returns (bytes[] memory withdrawalProof) {
-        // Assume arrayLength = 2 for faster proof speeds
-        // TODO: have the array length range between 0 and 10 elements
+        // ASSUME: Withdrawal proofs do not currently exceed 6 elements in length. This can be
+        // shrank to 2 for faster proof speeds during testing and development.
+        // TODO: Allow the array length range between 0 and 10 elements. This can be done once
+        // symbolic bytes are supported in Kontrol: https://github.com/runtimeverification/kontrol/issues/272
         uint256 arrayLength = 6;
-
         withdrawalProof = new bytes[](arrayLength);
 
-        // Deploy ghost contract
-        // GhostBytes10 ghostBytes10 = new GhostBytes10();
-
-        // Make the storage of the ghost contract symbolic
-        // kevm.symbolicStorage(address(ghostBytes10));
-
-        // Each bytes element will have a length of 600
-        // uint256 bytesSlotValue = 600 * 2 + 1;
-
-        // Load the size encoding into the first slot of ghostBytes
-        // vm.store(address(ghostBytes10), bytes32(uint256(0)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(1)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(2)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(3)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(4)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(5)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(6)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(7)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(8)), bytes32(bytesSlotValue));
-        // vm.store(address(ghostBytes10), bytes32(uint256(9)), bytes32(bytesSlotValue));
-
-        // withdrawalProof = ghostBytes10.getGhostBytesArray();
-
-        // Second approach
-
-        // withdrawalProof[0] = ghostBytes10.ghostBytes0();
-        // withdrawalProof[1] = ghostBytes10.ghostBytes1();
-        // withdrawalProof[2] = ghostBytes10.ghostBytes2();
-        // withdrawalProof[3] = ghostBytes10.ghostBytes3();
-        // withdrawalProof[4] = ghostBytes10.ghostBytes4();
-        // withdrawalProof[5] = ghostBytes10.ghostBytes5();
-        // withdrawalProof[6] = ghostBytes10.ghostBytes6();
-        // withdrawalProof[7] = ghostBytes10.ghostBytes7();
-        // withdrawalProof[8] = ghostBytes10.ghostBytes8();
-        // withdrawalProof[9] = ghostBytes10.ghostBytes9();
-
-        // First approach
-
         for (uint256 i = 0; i < withdrawalProof.length; ++i) {
+            // ASSUME: Each element is 600 bytes. Proof elements are 17 * 32 = 544 bytes long, plus
+            // ~10% margin for RLP encoding:, giving us the 600 byte assumption.
             withdrawalProof[i] = freshBigBytes(600);
         }
     }

packages/contracts-bedrock/test/kontrol/scripts/common.sh

+#!/bin/bash
+# Common functions and variables for run-kontrol.sh and make-summary-deployment.sh
+
+notif() { echo "== $0: $*" >&2 ; }
+usage() {
+  echo "Usage: $0 [-h|--help] [container|local|dev]" 1>&2
+  echo "Options:" 1>&2
+  echo "  -h, --help         Display this help message." 1>&2
+  echo "  container          Run in docker container. Reproduce CI execution. (Default)" 1>&2
+  echo "  local              Run locally, enforces registered versions.json version for better reproducibility. (Recommended)" 1>&2
+  echo "  dev                Run locally, does NOT enforce registered version. (Useful for developing with new versions and features)" 1>&2
+  exit 0
+}
+
+# Set Run Directory <root>/packages/contracts-bedrock
+WORKSPACE_DIR=$( cd "$SCRIPT_HOME/../../.." >/dev/null 2>&1 && pwd )
+
+# Variables
+export CONTAINER_NAME=kontrol-tests
+KONTROLRC=$(jq -r .kontrol < "$WORKSPACE_DIR/../../versions.json")
+export KONTROL_RELEASE=$KONTROLRC
+export LOCAL=false
+
+# Argument Parsing
+parse_args() {
+  if [ $# -gt 1 ]; then
+    usage
+  elif [ $# -eq 0 ] || [ "$1" == "container" ]; then
+    notif "Running in docker container (DEFAULT)"
+    export LOCAL=false
+  elif [ "$1" == "-h" ] || [ "$1" == "--help" ]; then
+    usage
+  elif [ "$1" == "local" ]; then
+    notif "Running with LOCAL install, .kontrolrc CI version ENFORCED"
+    check_kontrol_version
+  elif [ "$1" == "dev" ]; then
+    notif "Running with LOCAL install, IGNORING .kontrolrc version"
+    export LOCAL=true
+    pushd "$WORKSPACE_DIR" > /dev/null || exit
+  else
+    usage
+  fi
+}
+
+check_kontrol_version() {
+  if [ "$(kontrol version | awk -F': ' '{print$2}')" == "$KONTROLRC" ]; then
+    notif "Kontrol version matches $KONTROLRC"
+    export LOCAL=true
+    pushd "$WORKSPACE_DIR" > /dev/null || exit
+  else
+    notif "Kontrol version does NOT match $KONTROLRC"
+    notif "Please run 'kup install kontrol --version v$KONTROLRC'"
+    exit 1
+  fi
+}
+
+conditionally_start_docker() {
+  if [ "$LOCAL" == false ]; then
+    # Is old docker container running?
+    if [ "$(docker ps -q -f name="$CONTAINER_NAME")" ]; then
+        # Stop old docker container
+        notif "Stopping old docker container"
+        clean_docker
+    fi
+    start_docker
+  fi
+}
+
+start_docker () {
+  docker run \
+    --name "$CONTAINER_NAME" \
+    --rm \
+    --interactive \
+    --detach \
+    --env FOUNDRY_PROFILE="$FOUNDRY_PROFILE" \
+    --workdir /home/user/workspace \
+    -v "$WORKSPACE_DIR":/home/user/workspace \
+    runtimeverificationinc/kontrol:ubuntu-jammy-"$KONTROL_RELEASE"
+
+  copy_to_docker
+}
+
+copy_to_docker() {
+  # Copy test content to container. We need to avoid copying node_modules because
+  # it results in the below error, so we copy the workspace to a temp directory
+  # and then copy it to the container.
+  #   Error response from daemon: invalid symlink "/home/user/workspace/node_modules/@typescript-eslint/eslint-plugin" -> "../../../../node_modules/.pnpm/@typescript-eslint+eslint-plugin@6.19.1_@typescript-eslint+parser@6.19.1_eslint@8.56.0_typescript@5.3.3/node_modules/@typescript-eslint/eslint-plugin"
+  # Even though we use a bind mount, we still need to copy the files to the
+  # container because we are running Docker on a remote host.
+  TMP_DIR=$(mktemp -d)
+  cp -r "$WORKSPACE_DIR/." "$TMP_DIR"
+  rm -rf "$TMP_DIR/node_modules"
+  docker cp --follow-link "$TMP_DIR/." $CONTAINER_NAME:/home/user/workspace
+  rm -rf "$TMP_DIR"
+
+  docker exec --user root "$CONTAINER_NAME" chown -R user:user /home/user
+}
+
+clean_docker(){
+  notif "Stopping Docker Container"
+  docker stop "$CONTAINER_NAME"
+}
+
+
+docker_exec () {
+  docker exec --user user --workdir /home/user/workspace $CONTAINER_NAME "${@}"
+}
+
+run () {
+  if [ "$LOCAL" = true ]; then
+    notif "Running local"
+    # shellcheck disable=SC2086
+    "${@}"
+  else
+    notif "Running in docker"
+    docker_exec "${@}"
+  fi
+}

packages/contracts-bedrock/test/kontrol/scripts/make-summary-deployment.sh

 #!/bin/bash
 set -euo pipefail
 
+export FOUNDRY_PROFILE=kdeploy
+
+SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+# shellcheck source=/dev/null
+source "$SCRIPT_HOME/common.sh"
+parse_args "$@"
+
+cleanup() {
+  # Restore the original script from the backup
+  if [ -f "$DEPLOY_SCRIPT.bak" ]; then
+    cp "$DEPLOY_SCRIPT.bak" "$DEPLOY_SCRIPT"
+    rm "$DEPLOY_SCRIPT.bak"
+  fi
+
+  if [ -f "snapshots/state-diff/Deploy.json" ]; then
+    rm "snapshots/state-diff/Deploy.json"
+  fi
+
+  if [ "$LOCAL" = false ]; then
+    clean_docker
+  fi
+}
+
+# Set trap to call cleanup function on exit
+trap cleanup EXIT
+
 # create deployments/hardhat/.deploy and snapshots/state-diff/Deploy.json if necessary
 if [ ! -d "deployments/hardhat" ]; then
   mkdir deployments/hardhat;
@@ -16,40 +42,39 @@ if [ ! -f "snapshots/state-diff/Deploy.json" ]; then
 fi
 
 DEPLOY_SCRIPT="./scripts/Deploy.s.sol"
+conditionally_start_docker
 
 # Create a backup
-cp ${DEPLOY_SCRIPT} ${DEPLOY_SCRIPT}.bak
+cp $DEPLOY_SCRIPT $DEPLOY_SCRIPT.bak
 
 # Replace mustGetAddress by getAddress in Deploy.s.sol
 # This is needed because the Kontrol deployment is only a partial
 # version of the full Optimism deployment. Since not all the components
 # of the system are deployed, we'd get some reverts on the `mustGetAddress` functions
-awk '{gsub(/mustGetAddress/, "getAddress")}1' ${DEPLOY_SCRIPT} > temp && mv temp ${DEPLOY_SCRIPT}
+awk '{gsub(/mustGetAddress/, "getAddress")}1' $DEPLOY_SCRIPT > temp && mv temp $DEPLOY_SCRIPT
 
-FOUNDRY_PROFILE=kdeploy forge script -vvv test/kontrol/deployment/KontrolDeployment.sol:KontrolDeployment --sig 'runKontrolDeployment()'
+forge script -vvv test/kontrol/deployment/KontrolDeployment.sol:KontrolDeployment --sig 'runKontrolDeployment()'
 echo "Created state diff json"
 
-# Restore the file from the backup
-cp ${DEPLOY_SCRIPT}.bak ${DEPLOY_SCRIPT}
-rm ${DEPLOY_SCRIPT}.bak
-
 # Clean and store the state diff json in snapshots/state-diff/Kontrol-Deploy.json
 JSON_SCRIPTS=test/kontrol/scripts/json
 GENERATED_STATEDIFF=Deploy.json # Name of the statediff json produced by the deployment script
-STATEDIFF=Kontrol-${GENERATED_STATEDIFF} # Name of the Kontrol statediff
-mv snapshots/state-diff/${GENERATED_STATEDIFF} snapshots/state-diff/${STATEDIFF}
-python3 ${JSON_SCRIPTS}/clean_json.py snapshots/state-diff/${STATEDIFF}
-jq . snapshots/state-diff/${STATEDIFF} > temp && mv temp snapshots/state-diff/${STATEDIFF} # Prettify json
+STATEDIFF=Kontrol-$GENERATED_STATEDIFF # Name of the Kontrol statediff
+mv snapshots/state-diff/$GENERATED_STATEDIFF snapshots/state-diff/$STATEDIFF
+python3 $JSON_SCRIPTS/clean_json.py snapshots/state-diff/$STATEDIFF
+jq . snapshots/state-diff/$STATEDIFF > temp && mv temp snapshots/state-diff/$STATEDIFF # Prettify json
 echo "Cleaned state diff json"
 
 CONTRACT_NAMES=deployments/hardhat/.deploy
-python3 ${JSON_SCRIPTS}/reverse_key_values.py ${CONTRACT_NAMES} ${CONTRACT_NAMES}Reversed
+python3 $JSON_SCRIPTS/reverse_key_values.py $CONTRACT_NAMES ${CONTRACT_NAMES}Reversed
 CONTRACT_NAMES=${CONTRACT_NAMES}Reversed
 
 SUMMARY_DIR=test/kontrol/proofs/utils
 SUMMARY_NAME=DeploymentSummary
 LICENSE=MIT
-kontrol summary ${SUMMARY_NAME} snapshots/state-diff/${STATEDIFF} --contract-names ${CONTRACT_NAMES} --output-dir ${SUMMARY_DIR} --license ${LICENSE}
-forge fmt ${SUMMARY_DIR}/${SUMMARY_NAME}.sol
-forge fmt ${SUMMARY_DIR}/${SUMMARY_NAME}Code.sol
-echo "Added state updates to ${SUMMARY_DIR}/${SUMMARY_NAME}.sol"
+
+copy_to_docker # Copy the newly generated files to the docker container
+run kontrol summary $SUMMARY_NAME snapshots/state-diff/$STATEDIFF --contract-names $CONTRACT_NAMES --output-dir $SUMMARY_DIR --license $LICENSE
+forge fmt $SUMMARY_DIR/$SUMMARY_NAME.sol
+forge fmt $SUMMARY_DIR/${SUMMARY_NAME}Code.sol
+echo "Added state updates to $SUMMARY_DIR/$SUMMARY_NAME.sol"

packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh

 #!/bin/bash
 set -euo pipefail
 
-#####################
-# Support Functions #
-#####################
-blank_line() { echo '' >&2 ; }
-notif() { echo "== $0: $*" >&2 ; }
-usage() {
-  echo "Usage: $0 [-h|--help] [container|local|dev]" 1>&2
-  echo "Options:" 1>&2
-  echo "  -h, --help         Display this help message." 1>&2
-  echo "  container          Run tests in docker container. Reproduce CI execution. (Default)" 1>&2
-  echo "  local              Run locally, enforces CI Registered .kontrolrc Kontrol version for better reproducibility. (Recommended)" 1>&2
-  echo "  dev                Run locally, do NOT enforce CI registered Kontrol version (Recomended w/ greater kup & kontrol experience)" 1>&2
-  exit 0
-}
-
-#############
-# Variables #
-#############
-# Set Script Directory Variables <root>/packages/contracts-bedrock/test/kontrol
-SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
-notif "Script Home: $SCRIPT_HOME"
-blank_line
-
-# Set Run Directory <root>/packages/contracts-bedrock
-WORKSPACE_DIR=$( cd "${SCRIPT_HOME}/../../.." >/dev/null 2>&1 && pwd )
-notif "Run Directory: ${WORKSPACE_DIR}"
-blank_line
-
 export FOUNDRY_PROFILE=kprove
-export CONTAINER_NAME=kontrol-tests
-KONTROLRC=$(jq -r .kontrol < "${WORKSPACE_DIR}/../../versions.json")
-export KONTROL_RELEASE=${KONTROLRC}
-export LOCAL=false
 
-#######################
-# Check for arguments #
-#######################
-if [ $# -gt 1 ]; then
-  usage
-else
-  if [ $# -eq 0 ] || [ "$1" == "container" ]; then
-    notif "Running in docker container (DEFAULT)"
-    blank_line
-    export LOCAL=false
-    [ $# -gt 1 ] && shift
-  elif [ "$1" == "-h" ] || [ "$1" == "--help" ]; then
-    usage
-  elif [ "$1" == "local" ]; then
-    notif "Running with LOCAL install, .kontrolrc CI version ENFORCED"
-    if [ "$(kontrol version | awk -F': ' '{print$2}')" == "${KONTROLRC}" ]; then
-      notif "Kontrol version matches ${KONTROLRC}"
-      blank_line
-      export LOCAL=true
-      shift
-      pushd "${WORKSPACE_DIR}" > /dev/null
-    else
-      notif "Kontrol version does NOT match ${KONTROLRC}"
-      notif "Please run 'kup install kontrol --version v${KONTROLRC}'"
-      blank_line
-      exit 1
-    fi
-  elif [ "$1" == "dev" ]; then
-    notif "Running with LOCAL install, IGNORING .kontrolrc version"
-    blank_line
-    export LOCAL=true
-    shift
-    pushd "${WORKSPACE_DIR}" > /dev/null
-  else
-    # Unexpected argument passed
-    usage
-  fi
-fi
+SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+# shellcheck source=/dev/null
+source "$SCRIPT_HOME/common.sh"
+parse_args "$@"
 
 #############
 # Functions #
@@ -82,110 +16,70 @@ kontrol_build() {
   # shellcheck disable=SC2086
   run kontrol build \
     --verbose \
-                        --require ${lemmas}         \
-                        --module-import ${module}   \
-                        ${rekompile}
-            }
+    --require $lemmas \
+    --module-import $module \
+    $rekompile
+}
 
 kontrol_prove() {
   notif "Kontrol Prove"
   # shellcheck disable=SC2086
   run kontrol prove \
-                        --max-depth ${max_depth}           \
-                        --max-iterations ${max_iterations} \
-                        --smt-timeout ${smt_timeout}       \
-                        --workers ${workers}               \
-                        ${reinit}                          \
-                        ${bug_report}                      \
-                        ${break_on_calls}                  \
-                        ${auto_abstract}                   \
-                        ${tests}                           \
-                        ${use_booster}                     \
-                        --init-node-from ${state_diff}
-}
-
-start_docker () {
-    docker run                                    \
-      --name "${CONTAINER_NAME}"                  \
-      --rm                                        \
-      --interactive                               \
-      --detach                                    \
-      --env FOUNDRY_PROFILE="${FOUNDRY_PROFILE}"  \
-      --workdir /home/user/workspace              \
-    runtimeverificationinc/kontrol:ubuntu-jammy-"${KONTROL_RELEASE}"
-
-    # Copy test content to container
-    docker cp --follow-link "${WORKSPACE_DIR}/." ${CONTAINER_NAME}:/home/user/workspace
-    docker exec --user root ${CONTAINER_NAME} chown -R user:user /home/user
-}
-
-docker_exec () {
-    docker exec --user user --workdir /home/user/workspace ${CONTAINER_NAME} "${@}"
-}
-
-run () {
-  if [ "${LOCAL}" = true ]; then
-    notif "Running local"
-    # shellcheck disable=SC2086
-    "${@}"
-  else
-  notif "Running in docker"
-    docker_exec "${@}"
-  fi
+    --max-depth $max_depth \
+    --max-iterations $max_iterations \
+    --smt-timeout $smt_timeout \
+    --workers $workers \
+    $reinit \
+    $bug_report \
+    $break_on_calls \
+    $auto_abstract \
+    $tests \
+    $use_booster \
+    --init-node-from $state_diff
 }
 
 dump_log_results(){
   trap clean_docker ERR
     RESULTS_FILE="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
     LOG_PATH="test/kontrol/logs"
-    RESULTS_LOG="${LOG_PATH}/${RESULTS_FILE}"
+    RESULTS_LOG="$LOG_PATH/$RESULTS_FILE"
 
-    if [ ! -d ${LOG_PATH} ]; then
-      mkdir ${LOG_PATH}
+    if [ ! -d $LOG_PATH ]; then
+      mkdir $LOG_PATH
     fi
 
-    notif "Generating Results Log: ${LOG_PATH}"
-    blank_line
+    notif "Generating Results Log: $LOG_PATH"
 
     run tar -czvf results.tar.gz kout-proofs/ > /dev/null 2>&1
-    if [ "${LOCAL}" = true ]; then
-      mv results.tar.gz "${RESULTS_LOG}"
+    if [ "$LOCAL" = true ]; then
+      mv results.tar.gz "$RESULTS_LOG"
     else
-      docker cp ${CONTAINER_NAME}:/home/user/workspace/results.tar.gz "${RESULTS_LOG}"
+      docker cp "$CONTAINER_NAME:/home/user/workspace/results.tar.gz" "$RESULTS_LOG"
     fi
-    if [ -f "${RESULTS_LOG}" ]; then
-      cp "${RESULTS_LOG}" "${LOG_PATH}/kontrol-results_latest.tar.gz"
+    if [ -f "$RESULTS_LOG" ]; then
+      cp "$RESULTS_LOG" "$LOG_PATH/kontrol-results_latest.tar.gz"
     else
-      notif "Results Log: ${RESULTS_LOG} not found, skipping.."
-      blank_line
+      notif "Results Log: $RESULTS_LOG not found, skipping.."
     fi
     # Report where the file was generated and placed
-    notif "Results Log: $(dirname "${RESULTS_LOG}") generated"
+    notif "Results Log: $(dirname "$RESULTS_LOG") generated"
 
-    if [ "${LOCAL}" = false ]; then
-      notif "Results Log: ${RESULTS_LOG} generated"
-      blank_line
+    if [ "$LOCAL" = false ]; then
+      notif "Results Log: $RESULTS_LOG generated"
       RUN_LOG="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log"
-      docker logs ${CONTAINER_NAME} > "${LOG_PATH}/${RUN_LOG}"
+      docker logs "$CONTAINER_NAME" > "$LOG_PATH/$RUN_LOG"
     fi
 }
 
-clean_docker(){
-    notif "Stopping Docker Container"
-    docker stop ${CONTAINER_NAME}
-    blank_line
-}
-
 # Define the function to run on failure
 on_failure() {
   dump_log_results
 
-    if [ "${LOCAL}" = false ]; then
+  if [ "$LOCAL" = false ]; then
     clean_docker
   fi
 
   notif "Cleanup complete."
-    blank_line
   exit 1
 }
 
@@ -201,7 +95,7 @@ trap on_failure ERR INT
 # empty assignment to activate/deactivate the corresponding flag
 lemmas=test/kontrol/pausability-lemmas.k
 base_module=PAUSABILITY-LEMMAS
-module=OptimismPortalKontrol:${base_module}
+module=OptimismPortalKontrol:$base_module
 rekompile=--rekompile
 rekompile=
 regen=--regen
@@ -215,7 +109,7 @@ regen=
 test_list=( "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
             "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
             "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
-            "L1ERC721BridgeKontrol.prove_finalizeBridgeERC21_paused" \
+            "L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused" \
             "L1CrossDomainMessengerKontrol.prove_relayMessage_paused"
           )
 tests=""
@@ -247,27 +141,16 @@ state_diff="./snapshots/state-diff/Kontrol-Deploy.json"
 #############
 # RUN TESTS #
 #############
-if [ "${LOCAL}" == false ]; then
-  # Is old docker container running?
-  if [ "$(docker ps -q -f name=${CONTAINER_NAME})" ]; then
-      # Stop old docker container
-      notif "Stopping old docker container"
-      clean_docker
-      blank_line
-  fi
-  start_docker
-fi
+conditionally_start_docker
 
 kontrol_build
 kontrol_prove
 
 dump_log_results
 
-if [ "${LOCAL}" == false ]; then
+if [ "$LOCAL" == false ]; then
     notif "Stopping docker container"
     clean_docker
 fi
 
-blank_line
 notif "DONE"
-blank_line