# Kontrol Verification - [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) ## Getting Started ### Overview [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): > 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. 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 
├── pausability-lemmas.md: File containing the necessary lemmas for this project
├── deployment: Custom deploy sequence for Kontrol proofs and tests for its fast summarization
│   ├── KontrolDeployment.sol: Simplified deployment sequence for Kontrol proofs
│   └── DeploymentSummary.t.sol: Tests for the summarization of custom deployment
├── proofs: Where the proofs (tests) themselves live
│   ├── *.k.sol: Symbolic property tests for contracts
│   ├── interfaces: Interface files for src contracts, to avoid unnecessary compilation of contracts
│   └── utils: Proof dependencies, including the autogenerated deployment summary contracts
└── scripts: Where the scripts of the projects live
    ├── json: Data cleaning scripts for the output of KontrolDeployment.sol
    ├── make-summary-deployment.sh: Executes KontrolDeployment.sol, curates the result and writes the summary deployment contract
    └── run-kontrol.sh: Wrapper around the kontrol CLI to run the proofs
### Installation 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. ## Usage Verifying proofs has two steps: build, and execute. ### Build Deployment Summary First, generate a deployment summary contract from the deploy script in [`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol) by running the following command: ``` ./test/kontrol/scripts/make-summary-deployment.sh [container|local|dev] ``` The [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) supports the same execution modes as `run-kontrol.sh` below. [`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] [script|tests] ``` 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. It also supports two methods for specifying which tests to execute: - `script`: Runs the tests specified in the `test_list` variable - `tests`: Names of the tests to be executed. `tests` can have two forms: - `ContractName.testName`: e.g., `run-kontrol.sh ContractName.test1 ContractName.test2` - Empty, executing all the functions starting with `test`, `prove` or `check` present in the defined `out` directory. For instance, `./test/kontrol/scripts/run-kontrol.sh` will execute all `prove_*` functions in the [proofs](./proofs/) directory using the same Docker image as in CI. [Warning: executing all proofs in parallel is _very_ resource intensive] For a similar description of the options run `run-kontrol.sh --help`. ### Add New Proofs These are the instructions to add a new proof to this project. If all functions involved in the new proof are from a contract already deployed by [`KontrolDeployment`](./deployment/KontrolDeployment.sol) the first two steps can be skipped. #### Make Kontrol aware of the new contract being tested The `runKontrolDeployment` function of [`KontrolDeployment`](./deployment/KontrolDeployment.sol) partially reproduces the deployment process laid out in the `_run` function of [`Deploy.s.sol`](../../scripts/Deploy.s.sol). `runKontrolDeployment` has the `stateDiff` modifier to make use of [Foundry's state diff cheatcodes](https://book.getfoundry.sh/cheatcodes/start-state-diff-recording). Kontrol utilizes the JSON resulting from this modifier for two purposes: 1. Load all the state updates generated by `runKontrolDeployment` as the initial configuration for all proofs, effectively offloading the computation of the deployment process to `forge` and thus improving performance. 2. Produce the [`DeploymentSummary`](./proofs/utils/DeploymentSummary.sol) script contract to test that the produced JSON contains correct updates. Hence, in order to write a proof for a contract which is not present in `KontrolDeployment` it must be added there first. To add a new contract, properly inspect the above-mentioned `_run` function and place the corresponding deployment steps of the contract appropriately within the `runKontrolDeployment` function. Once new deployment steps have been added to `runKontrolDeployment` the state-diff files have to [be rebuilt](#build-deployment-summary). #### Include existing tests on the new state-diff recorded bytecode The next step is to include tests for the newly included state updates in [`DeploymentSummary.t.sol`](deployment/DeploymentSummary.t.sol). These tests inherit the tests from [`test`](../L1) of the contracts deployed by `runKontrolDeployment`. This ensures that deployment steps were implemented correctly and that the state updates are correct. It might be necessary to set some of the existing tests from [`test`](../L1) as virtual because they can't be executed as is. See [`DeploymentSummary.t.sol`](deployment/DeploymentSummary.t.sol) for more concrete examples. #### Add function signatures to [`KontrolInterfaces`](./proofs/interfaces/KontrolInterfaces.sol) So far we've got all the state updates ready to be added to the initial configuration of each proof, but we cannot yet write any proof about the function. We still need to add the relevant signatures into `KontrolInterfaces`. The reason for having `KontrolInterfaces` instead of using directly the contracts is to reduce the amount of compiled contracts by Kontrol. In the future there might interfaces for all contracts under `contracts-bedrock`, which would imply the removal of `KontrolInterfaces`. #### Write the proof Write your proof in a `.k.sol` file in the [`proofs`](./proofs/) folder, which is the `test` directory used by the `kprove` profile to run the proofs (see [Deployment Summary Process](#deployment-summary-process)). The name of the new proofs should start with `prove` (or `check`) instead of `test` to avoid `forge test` running them. The reason for this is that if Kontrol cheatcodes (see [Kontrol's own cheatcodes](https://github.com/runtimeverification/kontrol-cheatcodes/blob/master/src/KontrolCheats.sol)) are used in a test, it will not be runnable by `forge`. Currently, none of the tests are using custom Kontrol cheatcodes, but this is something to bear in mind. To reference the correct addresses for writing the tests, first import the signatures as in this example: ```solidity import { IOptimismPortal as OptimismPortal, ISuperchainConfig as SuperchainConfig } from "./interfaces/KontrolInterfaces.sol"; ``` Declare the correspondent variables and cast the correct signatures to the correct addresses: ```solidity OptimismPortal optimismPortal; SuperchainConfig superchainConfig; function setUp() public { optimismPortal = OptimismPortal(payable(optimismPortalProxyAddress)); superchainConfig = SuperchainConfig(superchainConfigProxyAddress); } ``` Note that the names of the addresses come from [`DeploymentSummary.t.sol`](deployment/DeploymentSummary.t.sol) and are automatically generated by the [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) script. #### Add your test to [`run-kontrol.sh`](./scripts/run-kontrol.sh) As described in [Execute Proofs](#execute-proofs), there's a `script` mode for specifying which proofs to run, and that is the mode used in CI. To run the new proofs with the `script` option, add `ContractName.prove_functionName_paused` to the variable `test_list` in the `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. Size of `bytes[]` arguments. In [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol), the `prove_proveWithdrawalTransaction_paused` proof is broken down into 11 different proofs, each corresponding to a different size of the `_withdrawalProof` argument, which is of type `bytes[]`. We execute the same logic for lengths of `_withdrawalProof` ranging from 0 to 10, setting the length of each symbolic `bytes` element to 600. - The reason for a max length of 10 is that it provides a conservative upper bound based on [historical data](https://dune.com/queries/3433954/5768623) for proof sizes. - The reason for choosing 600 as the length for the elements of `_withdrawalProof` is that each element is `17 * 32 = 544` bytes long, so adding a 10% margin for RLP encoding and rounding up yields 600 bytes. The same historical data confirms this is a valid bound. - All other symbolic `bytes` arguments that are not part of a `bytes` array have a symbolic length bounded by `2^63`. ### 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. 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. This project uses two different [`foundry.toml` profiles](../../foundry.toml), `kdeploy` and `kprove`, to facilitate usage of this fast summarization feature.: - `kdeploy`: Used by [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) to generate the [`DeploymentSummary.sol`](./proofs/utils/DeploymentSummary.sol) contract based on execution of the [`KontrolDeployment.sol`](./deployment/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`](./proofs/utils/DeploymentSummaryCode.sol) file, which is inherited by `DeploymentSummary`. - `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. 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. 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`.