Add kontrol.toml for CI Kontrol tests

packages/contracts-bedrock/foundry.toml

@@ -95,7 +95,7 @@ optimizer = false
 ################################################################
 # See test/kontrol/README.md for an explanation of how the profiles are configured
 
-[profile.kprove]
+[profile.kontrol-properties]
 src = 'test/kontrol/proofs'
 out = 'kout-proofs'
 test = 'test/kontrol/proofs'

packages/contracts-bedrock/kontrol.toml

@@ -0,0 +1,69 @@
+[build.kontrol-properties]
+foundry-project-root       = '.'
+regen                      = true
+rekompile                  = true
+verbose                    = false
+debug                      = false
+require                    = 'test/kontrol/pausability-lemmas.md'
+module-import              = 'OptimismPortalKontrol:PAUSABILITY-LEMMAS'
+no-metadata                = true
+# auxiliary-lemmas         = true
+# o2                       = true
+
+[prove.kontrol-properties]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 10000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 16
+maintenance-rate           = 16
+assume-defined             = true
+no-log-rewrites            = true
+no-stack-checks            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify --equation-max-recursion 100 --equation-max-iterations 1000'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+run-constructor            = false
+symbolic-immutables        = false
+init-node-from-diff        = './snapshots/state-diff/Kontrol-31337.json'
+xml-test-report            = true
+match-test                 = ['OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused0',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused1(',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused2',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused3',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused4',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused5',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused6',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused7',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused8',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused9',
+                              'OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused10',
+                              'OptimismPortal2Kontrol.prove_finalizeWithdrawalTransaction_paused',
+                              'L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused',
+                              'L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused',
+                              'L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused',
+                              'L1CrossDomainMessengerKontrol.prove_relayMessage_paused']
+# max-frontier-parallel    = 6
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+use-hex-encoding           = false
+
+[view-kcfg.default]
+foundry-project-root       = '.'
+use-hex-encoding           = true

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

@@ -117,7 +117,7 @@ Once new deployment steps have been added to `runKontrolDeployment` the state-di
 
 #### 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.
+Write your proof in a `.k.sol` file in the [`proofs`](./proofs/) folder, which is the `test` directory used by the `kontrol-properties` 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:
 
@@ -164,12 +164,12 @@ This provides a significant reduction in proof execution time, as it avoids the
 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.:
+This project uses two different [`foundry.toml` profiles](../../foundry.toml), `kdeploy` and `kontrol-properties`, 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`](./scripts/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.
+- `kontrol-properties`: Used by the [`run-kontrol.sh`](./scripts/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.

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

@@ -1,7 +1,7 @@
 #!/bin/bash
 set -euo pipefail
 
-export FOUNDRY_PROFILE=kprove
+export FOUNDRY_PROFILE=kontrol-properties
 
 SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 # shellcheck source=/dev/null
@@ -15,37 +15,16 @@ parse_args "$@"
 kontrol_build() {
   notif "Kontrol Build"
   # shellcheck disable=SC2086
-  run kontrol build \
-    --require $lemmas \
-    --module-import $module \
-    --no-metadata \
-    ${rekompile} \
-    ${regen}
+  run kontrol build
   return $?
 }
 
 kontrol_prove() {
   notif "Kontrol Prove"
   # shellcheck disable=SC2086
   run kontrol prove \
-    --max-depth $max_depth \
-    --max-iterations $max_iterations \
-    --smt-timeout $smt_timeout \
     --workers $workers \
-    $reinit \
-    $bug_report \
-    $break_on_calls \
-    $break_every_step \
-    $tests \
-    --init-node-from-diff $state_diff \
-    --kore-rpc-command 'kore-rpc-booster --no-post-exec-simplify --equation-max-recursion 100 --equation-max-iterations 1000' \
-    --xml-test-report \
-    --maintenance-rate 16 \
-    --assume-defined \
-    --no-log-rewrites \
-    --smt-timeout 16000 \
-    --smt-retry-limit 0 \
-    --no-stack-checks
+    $tests
   return $?
 }
 
@@ -103,21 +82,6 @@ on_failure() {
   exit 1
 }
 
-#########################
-# kontrol build options #
-#########################
-# NOTE: This script has a recurring pattern of setting and unsetting variables,
-# 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.md
-base_module=PAUSABILITY-LEMMAS
-module=OptimismPortalKontrol:$base_module
-rekompile=--rekompile
-# rekompile=
-regen=--regen
-# regen=
-
 #################################
 # Tests to symbolically execute #
 #################################
@@ -165,9 +129,6 @@ done
 #########################
 # kontrol prove options #
 #########################
-max_depth=10000
-max_iterations=10000
-smt_timeout=100000
 max_workers=16 # Set to 16 since there are 16 proofs to run
 # workers is the minimum between max_workers and the length of test_list unless
 # no test arguments are provided, in which case we default to max_workers
@@ -176,15 +137,6 @@ if [ "$CUSTOM_TESTS" == 0 ] && [ "$SCRIPT_TESTS" == false ]; then
 else
   workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]}))
 fi
-reinit=--reinit
-reinit=
-break_on_calls=--break-on-calls
-break_on_calls=
-break_every_step=--break-every-step
-break_every_step=
-bug_report=--bug-report
-bug_report=
-state_diff="./snapshots/state-diff/Kontrol-31337.json"
 
 #############
 # RUN TESTS #