Final version for Kontrol pausability proofs (#9530)

* Update tests to native symbolic `bytes` and `bytes[]`

* adding lemmas

* `run-kontrol.sh`: add more sensible parameters

* Change `startPrank` by `prank`

* Replace `mockCall` workaround with `vm.mockCall`

* Make `bytes` length symbolic

* `KontrolUtils`: remove symbolic workarounds

* `run-kontrol.sh`: add `prove_proveWithdrawalTransaction_paused`

* `forge fmt`

* `versions.json`: bump Kontrol from `0.1.127` to `0.1.156`

* Remove `ASSUME` comments

* ci: run kontrol on develop and allow manual dispatch

* ci: rename parameter

* `OptimismPortalKontrol`: add remaining ranges for `_withdrawalProof`

* Add forge-like UX to `run-kontrol.sh`

* `pausability-lemmas.k`: clean file

* general tests, further lemmas, summary claim

* Address shellcheck failures

* Change `pausability-lemmas.k` to `pausability-lemmas.md`

* `versions.json`: bump `kontrol` from `0.1.156` to `0.1.178`

* `OptimismPortalKontrol`: update `kontrol` natspec to version 0.1.178

* `pausability-lemmas.md`: remove unused `Lemmas` header

* Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* `pausability-lemmas.md`: fix spelling typo

* `pausability-lemmas.md`: fix typo `bytearrays` to `byte arrays`

* `run-kontrol.sh`: correctly format temorarily unexecuted lemmas

* `common.sh`: execute `copy_to_docker` only when in docker mode

* `make-summary-deployment.sh`: add argument check before parsing

* Reflect `kontrol summary` change to `kontrol load-state-diff`

From version `0.1.162`, `kontrol summary` has been renamed to `kontrol
load-state-diff`.
The reason of this renaming is that `kontrol summary` will be
used by kontrol's compositional symbolic execution.
Also, changing the name to `load-state-diff` makes more explicit what the
command does.
Related PR: https://github.com/runtimeverification/kontrol/pull/374

* `pausability-lemmas.md`: remove upstreamed lemmas

* fix: writing typos

* lemma text pass

* paragraph about summary maintainability

* README.md: include latest changes

* pausability-lemmas.md: markdown link typo

* KontrolUtils: add documentation comment

* pausability-lemmas.md: fix markdown typo vol2

* pausability-lemmas.md: fix markdown typo vol3

* Add specialized usage functions

* `README.md`: remove `bash` in `make-summary-deployment.sh` description

* `README.md`: complete `Add New Proofs` section

* versions.json: bump kontrol from 0.1.178 to 0.1.196

* run-kontrol.sh: add `--xml-test-report` flag

* .gitignore: add `kontrol_prove_report.xml`

* foundry.toml: set `ast = true` in `kprove` profile

* config.yml: set correct path for kontrol `store_artifacts`

* config.yml: add `store_test_results` step to `kontrol-tests` job

* package.json: execute `run-kontrol.sh` with `script` option

We run `run-kontrol.sh` with the `script` option to avoid executing all proofs

* run-kontrol.sh: remove proof with 10 elements in favor of 0 and 1

The longer the `_withdrawalProof` array the longer the execution time
Adding the lengths 0 and 1 fits within the max cpus and won't take as long to run

* chore: typos and formatting

* ci: fix kontrol trigger

* README.md: minor typo

---------
Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

.circleci/config.yml

@@ -23,6 +23,9 @@ parameters:
   fault_proofs_dispatch:
     type: boolean
     default: false
+  kontrol_dispatch:
+    type: boolean
+    default: false
 
 orbs:
   go: circleci/go@1.8.0
@@ -1485,7 +1488,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:
@@ -2078,9 +2083,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.
 

packages/contracts-bedrock/test/kontrol/pausability-lemmas.k

-requires "evm.md"
-requires "foundry.md"
-
-module PAUSABILITY-LEMMAS
-    imports BOOL
-    imports FOUNDRY
-    imports INFINITE-GAS
-    imports INT-SYMBOLIC
-
-// Your lemmas go here
-
-endmodule

packages/contracts-bedrock/test/kontrol/pausability-lemmas.md

+Kontrol Lemmas
+==============
+
+Lemmas are K rewrite rules that enhance the reasoning power of Kontrol. For more information on lemmas, please consult [this section](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs) of the Kontrol documentation.
+
+This file contains the lemmas required to run the proofs included in the [proofs](./proofs) folder. Some of these lemmas are general enough to likely be incorporated into future versions of Kontrol, while others are specific to the challenges presented by the proofs.
+
+Similarly to other files such as [`cheatcodes.md`](https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/cheatcodes.md), we use the idiomatic way of programming in Kontrol, which is [literate programming](https://en.wikipedia.org/wiki/Literate_programming), allowing for better documentation of the code.
+
+## Imports
+
+For writing the lemmas, we use the [`foundry.md`](https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md) file. This file contains and imports all of the definitions from KEVM and Kontrol on top of which we write the lemmas.
+
+```k
+requires "foundry.md"
+
+module PAUSABILITY-LEMMAS
+    imports BOOL
+    imports FOUNDRY
+    imports INT-SYMBOLIC
+```
+
+## Arithmetic
+
+Lemmas on arithmetic reasoning. Specifically, on: cancellativity, inequalites in which the two sides are of different signs; and the rounding-up mechanism of the Solidity compiler (expressed through `notMaxUInt5 &Int ( X +Int 31 )`, which rounds up `X` to the nearest multiple of 32).
+
+```k
+    // Cancellativity #1
+    rule A +Int ( (B -Int A) +Int C ) => B +Int C [simplification]
+
+    // Cancellativity #2
+    rule (A -Int B) -Int (C -Int B) => A -Int C [simplification]
+
+    // Cancellativity #3
+    rule A -Int (A +Int B) => 0 -Int B [simplification]
+
+    // Various inequalities
+    rule X  <Int A &Int B => true requires X <Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification]
+    rule X  <Int A +Int B => true requires X <Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification]
+    rule X <=Int A +Int B => true requires X <Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification]
+
+    // Upper bound on (pow256 - 32) &Int lengthBytes(X)
+    rule notMaxUInt5 &Int Y <=Int Y => true
+      requires 0 <=Int Y
+      [simplification]
+
+    // Bounds on notMaxUInt5 &Int ( X +Int 31 )
+    rule X <=Int   notMaxUInt5 &Int ( X +Int 31 )          => true requires 0 <=Int X                   [simplification]
+    rule X <=Int   notMaxUInt5 &Int ( Y +Int 31 )          => true requires X <=Int 0 andBool 0 <=Int Y [simplification, concrete(X)]
+    rule X <=Int ( notMaxUInt5 &Int ( X +Int 31 ) ) +Int Y => true requires 0 <=Int X andBool 0 <=Int Y [simplification, concrete(Y)]
+
+    rule notMaxUInt5 &Int X +Int 31 <Int Y => true requires 0 <=Int X andBool X +Int 32 <=Int Y [simplification, concrete(Y)]
+
+    rule notMaxUInt5 &Int X +Int 31 <Int X +Int 32 => true requires 0 <=Int X [simplification]
+```
+
+## `#asWord`
+
+Lemmas about [`#asWord`](https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md#bytes-helper-functions). `#asWord(B)` interprets the byte array `B` as a single word (with MSB first).
+
+```k
+    // Move to function parameters
+    rule { #asWord ( BA1 ) #Equals #asWord ( BA2 ) } => #Top
+      requires BA1 ==K BA2
+      [simplification]
+
+    // #asWord ignores leading zeros
+    rule #asWord ( BA1 +Bytes BA2 ) => #asWord ( BA2 )
+      requires #asInteger(BA1) ==Int 0
+      [simplification, concrete(BA1)]
+
+    // `#asWord` of a byte array cannot equal a number that cannot fit within the byte array
+    rule #asWord ( BA ) ==Int Y => false
+        requires lengthBytes(BA) <=Int 32
+         andBool (2 ^Int (8 *Int lengthBytes(BA))) <=Int Y
+        [concrete(Y), simplification]
+```
+
+## `#asInteger`
+
+Lemmas about [`#asInteger`](https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md#bytes-helper-functions). `#asInteger(X)` interprets the byte array `X` as a single arbitrary-precision integer (with MSB first).
+
+```k
+    // Conversion from bytes always yields a non-negative integer
+    rule 0 <=Int #asInteger ( _ ) => true [simplification]
+```
+
+## `#padRightToWidth`
+
+Lemmas about [`#padRightToWidth`](https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md#bytes-helper-functions). `#padRightToWidth(W, BA)` right-pads the byte array `BA` with zeros so that the resulting byte array has length `W`.
+
+```k
+    // Definitional expansion
+    rule #padRightToWidth (W, BA) => BA +Bytes #buf(W -Int lengthBytes(BA), 0)
+      [concrete(W), simplification]
+```
+
+## `#range(BA, START, WIDTH)`
+
+Lemmas about [`#range(BA, START, WIDTH)`](https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md#bytes-helper-functions). `#range(BA, START, WIDTH)` returns the range of `BA` from index `START` of width `WIDTH`.
+
+```k
+    // Parameter equality
+    rule { #range (BA, S, W1) #Equals #range (BA, S, W2) } => #Top
+      requires W1 ==Int W2
+      [simplification]
+```
+
+## Byte array indexing and update
+
+Lemmas about [`BA [ I ]` and `BA1 [ S := BA2 ]`](https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md#element-access). `BA [ I ]` returns the integer representation of the `I`-th byte of byte array `BA`. `BA1 [ S := BA2 ]` updates the byte array `BA1` with byte array `BA2` from index `S`.
+
+
+```k
+    // Byte indexing in terms of #asWord
+    rule BA [ X ] => #asWord ( #range (BA, X, 1) )
+      requires X <=Int lengthBytes(BA)
+      [simplification(40)]
+
+    // Empty update has no effect
+    rule BA [ START := b"" ] => BA
+      requires 0 <=Int START andBool START <=Int lengthBytes(BA)
+      [simplification]
+
+    // Update passes to right operand of concat if start position is beyond the left operand
+    rule ( BA1 +Bytes BA2 ) [ S := BA ] => BA1 +Bytes ( BA2 [ S -Int lengthBytes(BA1) := BA ] )
+      requires lengthBytes(BA1) <=Int S
+      [simplification]
+
+    // Consecutive quasi-contiguous byte-array update
+    rule BA [ S1 := BA1 ] [ S2 := BA2 ] => BA [ S1 := #range(BA1, 0, S2 -Int S1) +Bytes BA2 ]
+      requires 0 <=Int S1 andBool S1 <=Int S2 andBool S2 <=Int S1 +Int lengthBytes(BA1)
+      [simplification]
+
+    // Parameter equality: byte-array update
+    rule { BA1:Bytes [ S1 := BA2 ] #Equals BA3:Bytes [ S2 := BA4 ] } => #Top
+      requires BA1 ==K BA3 andBool S1 ==Int S2 andBool BA2 ==K BA4
+      [simplification]
+```
+
+Summaries
+---------
+
+Functions summaries are rewrite rules that capture (summarize) the effects of executing a function. Such rules allow Kontrol to, instead of executing the function itself, just apply the summary rule.
+
+## `copy_memory_to_memory` summary
+
+The following rule summarises the behavior of the `copy_memory_to_memory` function. This function is automatically generated by the Solidity compiler. In its Yul form, it is as follows:
+
+```solidity
+function copy_memory_to_memory(src, dst, length) {
+  let i := 0
+  for { } lt(i, length) { i := add(i, 32) }
+  {
+    mstore(add(dst, i), mload(add(src, i)))
+  }
+  if gt(i, length)
+  {
+    // clear end
+    mstore(add(dst, length), 0)
+  }
+}
+```
+
+It is used to copy `length` bytes of memory from index `src` to index `dest`, doing so in steps of 32 bytes, and right-padding with zeros to a multiple of 32.
+
+Following the compiler constraints, we enforce a limit on the length of byte arrays and indices into byte arrays.
+
+```k
+    syntax Int ::= "maxBytesLength" [alias]
+    rule maxBytesLength => 9223372036854775808
+```
+
+The summary lemma is as follows, with commentary inlined:
+
+```k
+    rule [copy-memory-to-memory-summary]:
+      <k> #execute ... </k>
+      <useGas> false </useGas>
+      <schedule> SHANGHAI </schedule>
+      <jumpDests> JUMPDESTS </jumpDests>
+      // The program and program counter are symbolic, focusing on the part we will be executing (CP)
+      <program> PROGRAM </program>
+      <pc> PCOUNT => PCOUNT +Int 53 </pc>
+      // The word stack has the appropriate form, as per the compiled code
+      <wordStack> LENGTH : _ : SRC : DEST : WS </wordStack>
+      // The program copies LENGTH bytes of memory from SRC +Int 32 to DEST +Int OFFSET,
+      // padded with 32 zeros in case LENGTH is not divisible by 32
+      <localMem>
+        LM => LM [ DEST +Int 32 := #range ( LM, SRC +Int 32, LENGTH ) +Bytes
+                                   #buf ( ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) , 0 ) +Bytes
+                                   #buf ( ( ( ( 32 -Int ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) ) ) modInt 32 ), 0 ) ]
+      </localMem>
+      requires
+       // The current program we are executing differs from the original one only in the hardcoded jump addresses,
+       // which are now relative to PCOUNT, and the hardcoded offset, which is now symbolic.
+               #range(PROGRAM, PCOUNT, 53) ==K b"`\x00[\x81\x81\x10\x15b\x00\x81`W` \x81\x85\x01\x81\x01Q\x86\x83\x01\x82\x01R\x01b\x00\x81BV[\x81\x81\x11\x15b\x00\x81sW`\x00` \x83\x87\x01\x01R[P"
+                                               [ 08 := #buf(3, PCOUNT +Int 32) ]
+                                               [ 28 := #buf(3, PCOUNT +Int  2) ]
+                                               [ 38 := #buf(3, PCOUNT +Int 51) ]
+
+       // Various well-formedness constraints. In particular, the maxBytesLength-related ones are present to
+       // remove various chops that would otherwise creep into the execution, and are reasonable since byte
+       // arrays in actual programs would never reach that size.
+       andBool 0 <=Int PCOUNT
+       andBool 0 <=Int LENGTH andBool LENGTH <Int maxBytesLength
+       andBool 0 <=Int SRC    andBool SRC    <Int maxBytesLength
+       andBool 0 <=Int DEST   andBool DEST   <Int maxBytesLength
+       andBool #sizeWordStack(WS) <=Int 1015
+
+       andBool SRC +Int LENGTH <=Int DEST // No overlap between source and destination
+       andBool DEST <=Int lengthBytes(LM) // Destination starts within current memory
+       // All JUMPDESTs in the program are valid
+       andBool (PCOUNT +Int 2) in JUMPDESTS andBool (PCOUNT +Int 32) in JUMPDESTS andBool (PCOUNT +Int 51) in JUMPDESTS
+       andBool PCOUNT +Int 51 <Int 2 ^Int 16  // and fit into two bytes
+      [priority(30), concrete(JUMPDESTS, PROGRAM, PCOUNT), preserves-definedness]
+
+endmodule
+```
+
+This summary is required to enable reasoning about byte arrays or arbitrary (symbolic) length. Otherwise, we would have to deal with a loop as the Solidity compiler copies memory to memory in chunks of 32 bytes at a time, and as this loop would have a symbolic bound, the symbolic execution would either have to be bounded or would not terminate.
+
+Unfortunately, the Solidity compiler optimizes the compiled bytecode in unpredictable ways, meaning that changes in the test suite can affect the compilation of `copy_memory_to_memory`. In light of this, and in order to be able to use our summary, we opt against using the `Test` contract of `forge-std`.
+
+The looping issue has been recognized as such by the Solidity developers, and starting from version [0.8.24](https://soliditylang.org/blog/2024/01/26/solidity-0.8.24-release-announcement/) EVM comes with an `MCOPY` instruction ([EIP-5656](https://eips.ethereum.org/EIPS/eip-5656)), which copies a part of memory to another part of memory as an atomic action. If the development were to move to this (or higher) version of the compiler, there would be no need for this summary.

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

@@ -19,25 +19,18 @@ contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
         superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
     }
 
-    /// TODO: Replace struct parameters and workarounds with the appropriate
-    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
-    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
     function prove_relayMessage_paused(
         uint256 _nonce,
         address _sender,
         address _target,
         uint256 _value,
-        uint256 _gas
+        uint256 _gas,
+        bytes calldata _message
     )
         external
     {
         setUpInlined();
 
-        // 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
         vm.prank(superchainConfig.guardian());
         superchainConfig.pause("identifier");

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

@@ -6,6 +6,7 @@ import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { Types } from "src/libraries/Types.sol";
 import {
     IL1ERC721Bridge as L1ERC721Bridge,
+    IL1CrossDomainMessenger as CrossDomainMessenger,
     ISuperchainConfig as SuperchainConfig
 } from "./interfaces/KontrolInterfaces.sol";
 
@@ -18,43 +19,30 @@ contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
         superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
     }
 
-    /// 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_finalizeBridgeERC721_paused(
         address _localToken,
         address _remoteToken,
         address _from,
         address _to,
-        uint256 _amount
+        uint256 _amount,
+        bytes calldata _extraData
     )
         public
     {
         setUpInlined();
 
-        // Current workaround to be replaced with `vm.mockCall`, once the cheatcode is implemented in Kontrol
-        // This overrides the storage slot read by `CrossDomainMessenger::xDomainMessageSender`
-        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/285
-        vm.store(
-            l1CrossDomainMessengerProxyAddress,
-            hex"00000000000000000000000000000000000000000000000000000000000000cc",
-            bytes32(uint256(uint160(address(l1ERC721Bridge.otherBridge()))))
-        );
-
-        // 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());
         superchainConfig.pause("identifier");
 
-        // Pranking with `vm.prank` instead will result in failure from Kontrol
-        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/316
-        vm.startPrank(address(l1ERC721Bridge.messenger()));
+        vm.mockCall(
+            address(l1ERC721Bridge.messenger()),
+            abi.encodeWithSelector(CrossDomainMessenger.xDomainMessageSender.selector),
+            abi.encode(address(l1ERC721Bridge.otherBridge()))
+        );
+
+        vm.prank(address(l1ERC721Bridge.messenger()));
         vm.expectRevert("L1ERC721Bridge: paused");
         l1ERC721Bridge.finalizeBridgeERC721(_localToken, _remoteToken, _from, _to, _amount, _extraData);
-        vm.stopPrank();
     }
 }

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

@@ -6,6 +6,7 @@ import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { Types } from "src/libraries/Types.sol";
 import {
     IL1StandardBridge as L1StandardBridge,
+    IL1CrossDomainMessenger as CrossDomainMessenger,
     ISuperchainConfig as SuperchainConfig
 } from "./interfaces/KontrolInterfaces.sol";
 
@@ -18,77 +19,55 @@ contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
         superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
     }
 
-    /// 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_finalizeBridgeERC20_paused(
         address _localToken,
         address _remoteToken,
         address _from,
         address _to,
-        uint256 _amount
+        uint256 _amount,
+        bytes calldata _extraData
     )
         public
     {
         setUpInlined();
 
-        // Current workaround to be replaced with `vm.mockCall`, once the cheatcode is implemented in Kontrol
-        // This overrides the storage slot read by `CrossDomainMessenger::xDomainMessageSender`
-        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/285
-        vm.store(
-            l1CrossDomainMessengerProxyAddress,
-            hex"00000000000000000000000000000000000000000000000000000000000000cc",
-            bytes32(uint256(uint160(address(l1standardBridge.otherBridge()))))
-        );
-
-        // 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());
         superchainConfig.pause("identifier");
 
-        // Pranking with `vm.prank` instead will result in failure from Kontrol
-        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/316
-        vm.startPrank(address(l1standardBridge.messenger()));
+        vm.mockCall(
+            address(l1standardBridge.messenger()),
+            abi.encodeWithSelector(CrossDomainMessenger.xDomainMessageSender.selector),
+            abi.encode(address(l1standardBridge.otherBridge()))
+        );
+
+        vm.prank(address(l1standardBridge.messenger()));
         vm.expectRevert("StandardBridge: paused");
         l1standardBridge.finalizeBridgeERC20(_localToken, _remoteToken, _from, _to, _amount, _extraData);
-        vm.stopPrank();
     }
 
-    /// 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_finalizeBridgeETH_paused(address _from, address _to, uint256 _amount) public {
+    function prove_finalizeBridgeETH_paused(
+        address _from,
+        address _to,
+        uint256 _amount,
+        bytes calldata _extraData
+    )
+        public
+    {
         setUpInlined();
 
-        // Current workaround to be replaced with `vm.mockCall`, once the cheatcode is implemented in Kontrol
-        // This overrides the storage slot read by `CrossDomainMessenger::xDomainMessageSender`
-        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/285
-        vm.store(
-            l1CrossDomainMessengerProxyAddress,
-            hex"00000000000000000000000000000000000000000000000000000000000000cc",
-            bytes32(uint256(uint160(address(l1standardBridge.otherBridge()))))
-        );
-
-        // 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());
         superchainConfig.pause("identifier");
 
-        // Pranking with `vm.prank` instead will result in failure from Kontrol
-        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/316
-        vm.startPrank(address(l1standardBridge.messenger()));
+        vm.mockCall(
+            address(l1standardBridge.messenger()),
+            abi.encodeWithSelector(CrossDomainMessenger.xDomainMessageSender.selector),
+            abi.encode(address(l1standardBridge.otherBridge()))
+        );
+
+        vm.prank(address(l1standardBridge.messenger()));
         vm.expectRevert("StandardBridge: paused");
         l1standardBridge.finalizeBridgeETH(_from, _to, _amount, _extraData);
-        vm.stopPrank();
     }
 }

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

@@ -20,78 +20,176 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
         superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
     }
 
-    /// TODO: Replace struct parameters and workarounds with the appropriate
-    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
-    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
-    function prove_proveWithdrawalTransaction_paused(
-        // WithdrawalTransaction args
-        uint256 _nonce,
-        address _sender,
-        address _target,
-        uint256 _value,
-        uint256 _gasLimit,
-        // bytes   memory _data,
+    function prove_finalizeWithdrawalTransaction_paused(Types.WithdrawalTransaction calldata _tx) external {
+        setUpInlined();
+
+        // Pause Optimism Portal
+        vm.prank(optimismPortal.guardian());
+        superchainConfig.pause("identifier");
+
+        vm.expectRevert("OptimismPortal: paused");
+        optimismPortal.finalizeWithdrawalTransaction(_tx);
+    }
+
+    /// @dev Function containing the logic for prove_proveWithdrawalTransaction_paused
+    ///      The reason for this is that we want the _withdrawalProof to range in size from
+    ///      0 to 10. These 11 proofs will exercise the same logic, which is contained in this function
+    function prove_proveWithdrawalTransaction_paused_internal(
+        Types.WithdrawalTransaction memory _tx,
         uint256 _l2OutputIndex,
-        // OutputRootProof args
-        bytes32 _outputRootProof0,
-        bytes32 _outputRootProof1,
-        bytes32 _outputRootProof2,
-        bytes32 _outputRootProof3
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] memory _withdrawalProof
     )
-        external
+        internal
     {
         setUpInlined();
 
-        // 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();
-
-        Types.WithdrawalTransaction memory _tx =
-            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data);
-        Types.OutputRootProof memory _outputRootProof =
-            Types.OutputRootProof(_outputRootProof0, _outputRootProof1, _outputRootProof2, _outputRootProof3);
-
         // Pause Optimism Portal
         vm.prank(optimismPortal.guardian());
         superchainConfig.pause("identifier");
 
-        // No one can call proveWithdrawalTransaction
         vm.expectRevert("OptimismPortal: paused");
         optimismPortal.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
     }
 
-    /// TODO: Replace struct parameters and workarounds with the appropriate
-    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
-    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
-    function prove_finalizeWithdrawalTransaction_paused(
-        uint256 _nonce,
-        address _sender,
-        address _target,
-        uint256 _value,
-        uint256 _gasLimit
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 10,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused10(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
     )
         external
     {
-        setUpInlined();
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 9,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused9(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
 
-        // 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);
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 8,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused8(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
 
-        // Pause Optimism Portal
-        vm.prank(optimismPortal.guardian());
-        superchainConfig.pause("identifier");
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 7,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused7(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
 
-        vm.expectRevert("OptimismPortal: paused");
-        optimismPortal.finalizeWithdrawalTransaction(
-            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data)
-        );
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 6,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused6(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 5,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused5(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 4,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused4(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 3,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused3(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 2,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused2(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 1,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 600,
+    function prove_proveWithdrawalTransaction_paused1(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    function prove_proveWithdrawalTransaction_paused0(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof
+    )
+        external
+    {
+        bytes[] memory _withdrawalProof = new bytes[](0);
+        prove_proveWithdrawalTransaction_paused_internal(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
     }
 }

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

 // SPDX-License-Identifier: MIT
-// This file was autogenerated by running `kontrol summary`. Do not edit this file manually.
+// This file was autogenerated by running `kontrol load-state-diff`. Do not edit this file manually.
 
 pragma solidity ^0.8.13;
 

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

 // SPDX-License-Identifier: MIT
-// This file was autogenerated by running `kontrol summary`. Do not edit this file manually.
+// This file was autogenerated by running `kontrol load-state-diff`. Do not edit this file manually.
 
 pragma solidity ^0.8.13;
 

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

 // SPDX-License-Identifier: MIT
+
+// This file exists to provide the `internal constant vm` on top of `KontrolCheats`.
+// The reason for explicitly defining `vm` here instead of inheriting Forge's `Test`
+// contract is the K summary of the `copy_memory_to_memory` function.
+// This summary dependent on the bytecode of the test contract, which means that if `Test`
+// was inherited, updating the version of `Test` could potentially imply having to adjust
+// said summary for the latest version, introducing a flakiness source.
+// Note that starting with version 0.8.24, the opcode `MCOPY` is introduced, removing the
+// need for the `copy_memory_to_memory` function and its summary, and thus this workaround.
+// For more information refer to the `copy_memory_to_memory` summary section of `pausability-lemmas.md`.
+
 pragma solidity 0.8.15;
 
 import { Vm } from "forge-std/Vm.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;
-}
-
-contract GhostBytes10 {
-    bytes public ghostBytes0;
-    bytes public ghostBytes1;
-    bytes public ghostBytes2;
-    bytes public ghostBytes3;
-    bytes public ghostBytes4;
-    bytes public ghostBytes5;
-    bytes public ghostBytes6;
-    bytes public ghostBytes7;
-    bytes public ghostBytes8;
-    bytes public ghostBytes9;
-
-    function getGhostBytesArray() public view returns (bytes[] memory _arr) {
-        _arr = new bytes[](10);
-        _arr[0] = ghostBytes0;
-        _arr[1] = ghostBytes1;
-        _arr[2] = ghostBytes2;
-        _arr[3] = ghostBytes3;
-        _arr[4] = ghostBytes4;
-        _arr[5] = ghostBytes5;
-        _arr[6] = ghostBytes6;
-        _arr[7] = ghostBytes7;
-        _arr[8] = ghostBytes8;
-        _arr[9] = ghostBytes9;
-    }
-}
-
 /// @notice Tests inheriting this contract cannot be run with forge
 abstract contract KontrolUtils is KontrolCheats {
     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
-    function freshBigBytes(uint256 bytesLength) internal returns (bytes memory sBytes) {
-        require(bytesLength >= 32, "Small bytes");
-
-        uint256 bytesSlotValue;
-        unchecked {
-            bytesSlotValue = bytesLength * 2 + 1;
-        }
-
-        // Deploy ghost contract
-        GhostBytes ghostBytes = new GhostBytes();
-
-        // Make the storage of the ghost contract symbolic
-        kevm.symbolicStorage(address(ghostBytes));
-
-        // Load the size encoding into the first slot of ghostBytes
-        vm.store(address(ghostBytes), bytes32(uint256(0)), bytes32(bytesSlotValue));
-
-        sBytes = ghostBytes.ghostBytes();
-    }
-
-    /// @dev Creates a bounded symbolic bytes[] memory representing a withdrawal proof.
-    function freshWithdrawalProof() public returns (bytes[] memory withdrawalProof) {
-        // 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);
-
-        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

@@ -2,10 +2,31 @@
 # Common functions and variables for run-kontrol.sh and make-summary-deployment.sh
 
 notif() { echo "== $0: $*" >&2 ; }
-usage() {
+
+# usage function for the run-kontrol.sh script
+usage_run_kontrol() {
+  echo "Usage: $0 [-h|--help] [container|local|dev] [script|tests]" 1>&2
+  echo "" 1>&2
+  echo "  -h, --help         Display this help message." 1>&2
+  echo "" 1>&2
+  echo "Execution modes:"
+  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
+  echo "" 1>&2
+  echo "Tests executed:"
+  echo "  script             Execute the tests recorded in run-kontrol.sh" 1>&2
+  echo "  tests              Execute the tests provided as arguments" 1>&2
+  exit 0
+}
+
+# usage function for the make-summary-deployment.sh script
+usage_make_summary() {
   echo "Usage: $0 [-h|--help] [container|local|dev]" 1>&2
-  echo "Options:" 1>&2
+  echo "" 1>&2
   echo "  -h, --help         Display this help message." 1>&2
+  echo "" 1>&2
+  echo "Execution modes:"
   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
@@ -20,25 +41,84 @@ export CONTAINER_NAME=kontrol-tests
 KONTROLRC=$(jq -r .kontrol < "$WORKSPACE_DIR/../../versions.json")
 export KONTROL_RELEASE=$KONTROLRC
 export LOCAL=false
+export SCRIPT_TESTS=false
+SCRIPT_OPTION=false
+export CUSTOM_TESTS=0 # Store the position where custom tests start, interpreting 0 as no tests
+CUSTOM_OPTION=0
+export RUN_KONTROL=false # true if any functions are called from run-kontrol.sh
+
+# General usage function, which discerns from which script is being called and displays the appropriate message
+usage() {
+  if [ "$RUN_KONTROL" = "true" ]; then
+    usage_run_kontrol
+  else
+    usage_make_summary
+  fi
+}
+
 
 # Argument Parsing
+# The logic behind argument parsing is the following (in order):
+# - Execution mode argument: container (or empty), local, dev
+# - Tests arguments (first if execution mode empty): script, specific test names
 parse_args() {
-  if [ $# -gt 1 ]; then
+  if [ $# -eq 0 ]; then
+    export LOCAL=false
+    export SCRIPT_TESTS=false
+    export CUSTOM_TESTS=0
+  # `script` argument caps the total possible arguments to its position
+  elif { [ $# -gt 1 ] && [ "$1" == "script" ]; } || { [ $# -gt 2 ] && [ "$2" == "script" ]; }; then
     usage
-  elif [ $# -eq 0 ] || [ "$1" == "container" ]; then
+  elif [ $# -eq 1 ]; then
+    SCRIPT_OPTION=false
+    CUSTOM_OPTION=0
+    parse_first_arg "$1"
+  elif [ $# -eq 2 ] && [ "$2" == "script" ]; then
+    if [ "$1" != "container" ] && [ "$1" != "local" ] && [ "$1" != "dev" ]; then
+      notif "Invalid first argument. Must be \`container\`, \`local\` or \`dev\`"
+      exit 1
+    fi
+    SCRIPT_OPTION=true
+    CUSTOM_OPTION=0
+    parse_first_arg "$1"
+  else
+    SCRIPT_OPTION=false
+    CUSTOM_OPTION=2
+    parse_first_arg "$1"
+  fi
+}
+
+# Parse the first argument passed to `run-kontrol.sh`
+parse_first_arg() {
+  if [ "$1" == "container" ]; then
     notif "Running in docker container (DEFAULT)"
     export LOCAL=false
+    export SCRIPT_TESTS=$SCRIPT_OPTION
+    export CUSTOM_TESTS=$CUSTOM_OPTION
   elif [ "$1" == "-h" ] || [ "$1" == "--help" ]; then
     usage
   elif [ "$1" == "local" ]; then
     notif "Running with LOCAL install, .kontrolrc CI version ENFORCED"
+    export SCRIPT_TESTS=$SCRIPT_OPTION
+    export CUSTOM_TESTS=$CUSTOM_OPTION
     check_kontrol_version
   elif [ "$1" == "dev" ]; then
     notif "Running with LOCAL install, IGNORING .kontrolrc version"
     export LOCAL=true
+    export SCRIPT_TESTS=$SCRIPT_OPTION
+    export CUSTOM_TESTS=$CUSTOM_OPTION
     pushd "$WORKSPACE_DIR" > /dev/null || exit
+  elif [ "$1" == "script" ]; then
+    notif "Running in docker container (DEFAULT)"
+    export LOCAL=false
+    NEGATED_SCRIPT_TESTS=$([[ "${SCRIPT_OPTION}" == "true" ]] && echo false || echo true)
+    export SCRIPT_TESTS=$NEGATED_SCRIPT_TESTS
+    export CUSTOM_TESTS=$CUSTOM_OPTION
   else
-    usage
+    notif "Running in docker container (DEFAULT)"
+    export LOCAL=false
+    export SCRIPT_TESTS=$SCRIPT_OPTION
+    export CUSTOM_TESTS=1 # Store the position where custom tests start
   fi
 }
 
@@ -87,13 +167,15 @@ copy_to_docker() {
   #   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"
+  if [ "$LOCAL" == false ]; then
+    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
+    docker exec --user root "$CONTAINER_NAME" chown -R user:user /home/user
+  fi
 }
 
 clean_docker(){

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

@@ -6,7 +6,18 @@ 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 "$@"
+# Sanity check on arguments
+if [ $# -gt 1 ]; then
+  echo "At most one argument can be provided. Instead $# were provided" 1>&2
+  exit 1
+elif [ $# -eq 1 ]; then
+  if [ "$1" != "-h" ] && [ "$1" != "--help" ] && [ "$1" != "container" ] && [ "$1" != "local" ] && [ "$1" != "dev" ]; then
+    notif "Invalid argument. Must be \`container\`, \`local\`, \`dev\`, \`-h\` or \`--help\`"
+    exit 1
+  else
+    parse_first_arg "$@"
+  fi
+fi
 
 cleanup() {
   # Restore the original script from the backup
@@ -74,7 +85,7 @@ SUMMARY_NAME=DeploymentSummary
 LICENSE=MIT
 
 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
+run kontrol load-state-diff $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

@@ -6,6 +6,7 @@ export FOUNDRY_PROFILE=kprove
 SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 # shellcheck source=/dev/null
 source "$SCRIPT_HOME/common.sh"
+export RUN_KONTROL=true
 parse_args "$@"
 
 #############
@@ -32,10 +33,12 @@ kontrol_prove() {
     $reinit \
     $bug_report \
     $break_on_calls \
+    $break_every_step \
     $auto_abstract \
     $tests \
     $use_booster \
-    --init-node-from $state_diff
+    --init-node-from $state_diff \
+    --xml-test-report
 }
 
 dump_log_results(){
@@ -93,7 +96,7 @@ trap on_failure ERR INT
 # such as `rekompile`. Such a pattern is intended for easy use while locally
 # developing and executing the proofs via this script. Comment/uncomment the
 # empty assignment to activate/deactivate the corresponding flag
-lemmas=test/kontrol/pausability-lemmas.k
+lemmas=test/kontrol/pausability-lemmas.md
 base_module=PAUSABILITY-LEMMAS
 module=OptimismPortalKontrol:$base_module
 rekompile=--rekompile
@@ -105,13 +108,33 @@ regen=
 #################################
 # Tests to symbolically execute #
 #################################
-# Missing: OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused
-test_list=( "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
-            "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
-            "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
-            "L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused" \
-            "L1CrossDomainMessengerKontrol.prove_relayMessage_paused"
-          )
+
+# Temporarily unexecuted tests
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused0" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused1" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused2" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused3" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused4" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused5" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused6" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused7" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused8" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused9" \
+# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused10" \
+
+test_list=()
+if [ "$SCRIPT_TESTS" == true ]; then
+  test_list=( "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused0" \
+              "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused1" \
+              "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
+              "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
+              "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
+              "L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused" \
+              "L1CrossDomainMessengerKontrol.prove_relayMessage_paused"
+  )
+elif [ "$CUSTOM_TESTS" != 0 ]; then
+  test_list=( "${@:${CUSTOM_TESTS}}" )
+fi
 tests=""
 for test_name in "${test_list[@]}"; do
   tests+="--match-test $test_name "
@@ -120,18 +143,25 @@ done
 #########################
 # kontrol prove options #
 #########################
-max_depth=1000000
-max_iterations=1000000
+max_depth=10000
+max_iterations=10000
 smt_timeout=100000
 max_workers=7 # Set to 7 since the CI machine has 8 CPUs
 # workers is the minimum between max_workers and the length of test_list
-workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]}))
+# unless no test arguments are provided, in which case we default to max_workers
+if [ "$CUSTOM_TESTS" == 0 ] && [ "$SCRIPT_TESTS" == false ]; then
+  workers=${max_workers}
+else
+  workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]}))
+fi
 reinit=--reinit
 reinit=
 break_on_calls=--no-break-on-calls
 # break_on_calls=
+break_every_step=--break-every-step
+break_every_step=
 auto_abstract=--auto-abstract-gas
-# auto_abstract=
+auto_abstract=
 bug_report=--bug-report
 bug_report=
 use_booster=--use-booster

versions.json

@@ -4,5 +4,5 @@
   "geth": "v1.13.4",
   "nvm": "v20.9.0",
   "slither": "0.10.0",
-  "kontrol": "0.1.127"
+  "kontrol": "0.1.196"
 }