Final version for Kontrol pausability proofs

.circleci/config.yml

@@ -23,6 +23,9 @@ parameters:
   fault_proofs_dispatch:
     type: boolean
     default: false
+  kontrol_dispatch:
+    type: boolean
+    default: false
 
 orbs:
   go: circleci/[email protected]
@@ -1470,7 +1473,9 @@ jobs:
           command: pnpm test:kontrol
           working_directory: ./packages/contracts-bedrock
       - store_artifacts:
-          path: ./packages/contracts-bedrock/kontrol-results_latest.tar.gz
+          path: ./packages/contracts-bedrock/test/kontrol/logs/kontrol-results_latest.tar.gz
+      - store_test_results:
+          path: ./packages/contracts-bedrock/kontrol_prove_report.xml
       - notify-failures-on-develop
 
 workflows:
@@ -2063,9 +2068,14 @@ workflows:
           context:
             - slack
 
-  scheduled-kontrol-tests:
+  develop-kontrol-tests:
     when:
-      equal: [ build_four_hours, <<pipeline.schedule.name>> ]
+      and:
+        - or:
+          - equal: [ "develop", <<pipeline.git.branch>> ]
+          - equal: [ true, <<pipeline.parameters.kontrol_dispatch>> ]
+        - not:
+           equal: [ scheduled_pipeline, << pipeline.trigger_source >> ]
     jobs:
       - kontrol-tests:
           context:

packages/contracts-bedrock/.gitignore

@@ -13,6 +13,7 @@ coverage.out
 
 # Testing State
 .testdata
+kontrol_prove_report.xml
 
 # Scripts
 scripts/go-ffi/go-ffi

packages/contracts-bedrock/foundry.toml

@@ -87,3 +87,4 @@ src = 'test/kontrol/proofs'
 out = 'kout-proofs'
 test = 'test/kontrol/proofs'
 script = 'test/kontrol/proofs'
+ast = true

packages/contracts-bedrock/package.json

@@ -19,7 +19,7 @@
     "build:go-ffi": "(cd scripts/go-ffi && go build)",
     "autogen:invariant-docs": "npx tsx scripts/autogen/generate-invariant-docs.ts",
     "test": "pnpm build:go-ffi && forge test",
-    "test:kontrol": "./test/kontrol/scripts/run-kontrol.sh",
+    "test:kontrol": "./test/kontrol/scripts/run-kontrol.sh script",
     "genesis": "./scripts/generate-l2-genesis.sh",
     "coverage": "pnpm build:go-ffi && forge coverage",
     "coverage:lcov": "pnpm build:go-ffi && forge coverage --report lcov",

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

@@ -34,7 +34,7 @@ This document details the Kontrol setup used in this repo to run various proofs
 The directory is structured as follows
 
 <pre>
-├── <a href="./pausability-lemmas.k">pausability-lemmas.k</a>: File containing the necessary lemmas for this project
+├── <a href="./pausability-lemmas.md">pausability-lemmas.md</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
@@ -63,9 +63,11 @@ Verifying proofs has two steps: build, and execute.
 
 First, generate a deployment summary contract from the deploy script in [`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol) by running the following command:
 
-```bash
-./test/kontrol/scripts/make-summary-deployment.sh
 ```
+./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.
@@ -82,7 +84,7 @@ The summary contract can be found in [`DeploymentSummary.sol`](./proofs/utils/De
 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]
+./test/kontrol/scripts/run-kontrol.sh [container|local|dev] [script|tests]
 ```
 
 The `run-kontrol.sh` script supports three modes of proof execution:
@@ -91,16 +93,66 @@ The `run-kontrol.sh` script supports three modes of proof execution:
 - `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
 
-More details on best practices for writing and adding new proofs will be added here in the future.
-The summary is:
+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)
 
-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.
+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
 
@@ -110,9 +162,10 @@ The summary is:
    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.
+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
 
@@ -125,8 +178,8 @@ Therefore we want to minimize the amount of code executed in Kontrol, and the fa
 
 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` 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`.
+- `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.