From 82009aad322335ea98ef3c56d00f2fb4186a2d1d Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 4 Nov 2024 21:42:59 +0700 Subject: [PATCH 1/4] Init `kontrol.toml` without `workers`, `match-test` --- packages/contracts-bedrock/kontrol.toml | 53 +++++++++++++++++++ .../test/kontrol/scripts/run-kontrol.sh | 52 +----------------- 2 files changed, 55 insertions(+), 50 deletions(-) create mode 100644 packages/contracts-bedrock/kontrol.toml diff --git a/packages/contracts-bedrock/kontrol.toml b/packages/contracts-bedrock/kontrol.toml new file mode 100644 index 000000000000..dcc51dae162a --- /dev/null +++ b/packages/contracts-bedrock/kontrol.toml @@ -0,0 +1,53 @@ +[build.default] +foundry-project-root = '.' +regen = true +rekompile = true +verbose = false +debug = false +require = 'test/kontrol/pausability-lemmas.md' +module-import = 'OptimismPortalKontrol:PAUSABILITY' +no-metadata = true +# auxiliary-lemmas = true +# o2 = true + +[prove.default] +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 +# 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 diff --git a/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh b/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh index 935f6e3b4903..e64df4b7d14b 100755 --- a/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh +++ b/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh @@ -15,12 +15,7 @@ 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 $? } @@ -28,24 +23,8 @@ 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 # From 9147872bfbdc35be315e34cd3c18dc49fa3cf541 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 4 Nov 2024 22:43:31 +0700 Subject: [PATCH 2/4] Add `match-test` to `kontrol.toml` --- packages/contracts-bedrock/kontrol.toml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/packages/contracts-bedrock/kontrol.toml b/packages/contracts-bedrock/kontrol.toml index dcc51dae162a..b4309d195695 100644 --- a/packages/contracts-bedrock/kontrol.toml +++ b/packages/contracts-bedrock/kontrol.toml @@ -5,7 +5,7 @@ rekompile = true verbose = false debug = false require = 'test/kontrol/pausability-lemmas.md' -module-import = 'OptimismPortalKontrol:PAUSABILITY' +module-import = 'OptimismPortalKontrol:PAUSABILITY-LEMMAS' no-metadata = true # auxiliary-lemmas = true # o2 = true @@ -40,6 +40,22 @@ 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] From 2777a7c8d84a9e48243b3e06f0dd92a056c76aa4 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Tue, 5 Nov 2024 20:21:45 +0700 Subject: [PATCH 3/4] Rename `kprove` to `kontrol-properties` --- packages/contracts-bedrock/foundry.toml | 2 +- packages/contracts-bedrock/test/kontrol/README.md | 6 +++--- .../contracts-bedrock/test/kontrol/scripts/run-kontrol.sh | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 59b16410f3a4..25c527211c4b 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -94,7 +94,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' diff --git a/packages/contracts-bedrock/test/kontrol/README.md b/packages/contracts-bedrock/test/kontrol/README.md index 7e4dc5a2809a..b05ca3f1a6ba 100644 --- a/packages/contracts-bedrock/test/kontrol/README.md +++ b/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. diff --git a/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh b/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh index e64df4b7d14b..7ed75f24a253 100755 --- a/packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh +++ b/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 From 1a559e1fb2e9bf40594a8c145f6911b3710fd855 Mon Sep 17 00:00:00 2001 From: Juan C Date: Thu, 5 Dec 2024 13:13:09 +0100 Subject: [PATCH 4/4] `kontrol.toml`: change `default` profile to `kontrol-properties` --- packages/contracts-bedrock/kontrol.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/packages/contracts-bedrock/kontrol.toml b/packages/contracts-bedrock/kontrol.toml index b4309d195695..b1495c41febf 100644 --- a/packages/contracts-bedrock/kontrol.toml +++ b/packages/contracts-bedrock/kontrol.toml @@ -1,4 +1,4 @@ -[build.default] +[build.kontrol-properties] foundry-project-root = '.' regen = true rekompile = true @@ -10,7 +10,7 @@ no-metadata = true # auxiliary-lemmas = true # o2 = true -[prove.default] +[prove.kontrol-properties] foundry-project-root = '.' verbose = false debug = false