Update Kontrol from `0.1.316` to `1.0.53` (#12289)

* versions.json: update Kontrol from `0.1.316` to `1.0.37`

* Remove `kdeploy` profile

* Update kontrol commands

* Run Fault Proofs summary by default

* Update non fault proofs summaries

* Update fault proofs summaries

* Remove `deployment` folder

* Exclude `proveWithdrawalTransaction` proofs

* Revert "Exclude `proveWithdrawalTransaction` proofs"

This reverts commit 5dd0f0393ff654fa46c7ca7d5cd02e03ffd12b79.

* `run-kontrol.sh`: add `--bmc-depth 1`

* foundry.toml: remove `kdeploy` profile

* .gitignore: remove `kout-deployment`

* Update summaries

* `common.sh`: account for `FOUNDRY_PROFILE` being `default`

* Remove `check-kontrol-deployment.sh`

Since now the Kontrol snapshot is taken from the `Deploy.s.sol` script, there is
no need to check that the custom Kontrol deployment is unmodified. Plus, the
custom Kontrol deployment process was removed previously on this PR

* justfile: remove `kontrol-deployment-check` from running checks

* config.yml: remove `kontrol-deployment-check`

* moving to Kontrol v1.0.50, invariant operational

* always rekompile and regen

* workers correction

* moving to Kontrol v1.0.51

* run-kontrol.sh: shellcheck typos

* run-kontrol.sh: add `verbose` and flags for `rekompile` and `regen`

* run-kontrol.sh: remove `--verbose` for `kontrol prove`

* Update `DeploymentSummaryFault` code

* Update `DeploymentSummary`

* Update Kontrol to version `1.0.53`

---------
Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>

.circleci/config.yml

@@ -692,8 +692,6 @@ jobs:
           command: gas-snapshot-check
       - run-contracts-check:
           command: snapshots-check-no-build
-      - run-contracts-check:
-          command: kontrol-deployment-check
       - run-contracts-check:
           command: interfaces-check-no-build
       - run-contracts-check:

packages/contracts-bedrock/.gitignore

@@ -3,7 +3,6 @@ artifacts
 forge-artifacts
 cache
 broadcast
-kout-deployment
 kout-proofs
 test/kontrol/logs
 

packages/contracts-bedrock/foundry.toml

@@ -93,12 +93,6 @@ optimizer = false
 ################################################################
 # See test/kontrol/README.md for an explanation of how the profiles are configured
 
-[profile.kdeploy]
-src = 'src'
-out = 'kout-deployment'
-test = 'test/kontrol'
-script = 'scripts-kontrol'
-
 [profile.kprove]
 src = 'test/kontrol/proofs'
 out = 'kout-proofs'

packages/contracts-bedrock/justfile

@@ -126,10 +126,6 @@ gas-snapshot-check-no-build:
 # Checks that the gas snapshot is up to date.
 gas-snapshot-check: build-go-ffi gas-snapshot-check-no-build
 
-# Checks that the Kontrol deployment script has not changed.
-kontrol-deployment-check:
-  ./scripts/checks/check-kontrol-deployment.sh
-
 # Checks if the snapshots are up to date without building.
 snapshots-check-no-build:
   ./scripts/checks/check-snapshots.sh --no-build
@@ -202,7 +198,6 @@ semgrep:
 check:
   @just gas-snapshot-check-no-build \
   unused-imports-check-no-build \
-  kontrol-deployment-check \
   snapshots-check-no-build \
   lint-check \
   semver-diff-check-no-build \

packages/contracts-bedrock/scripts/checks/check-kontrol-deployment.sh

-#!/usr/bin/env bash
-set -euo pipefail
-
-# This script checks if the KontrolDeployment.sol file has changed. Removal of
-# the DeploymentSummary.t.sol test file means that our primary risk vector for
-# KontrolDeployment.sol is an *accidental* change to the file. Changes must
-# therefore be explicitly acknowledged by bumping the hash below.
-
-# Get relevant directories
-SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
-CONTRACTS_BASE=$(dirname "$(dirname "$SCRIPT_DIR")")
-
-# Generate the SHA-512 hash using OpenSSL (very portable)
-generated_hash=$(openssl dgst -sha512 "${CONTRACTS_BASE}/test/kontrol/deployment/KontrolDeployment.sol" | awk '{print $2}')
-
-# Define the known hash
-known_hash="1664d9c22266b55b43086fa03c0e9d0447b092abc86cba79b86ad36c49167062c2b58a78757a20a5fd257d307599edce8f8f604cc6b2ee86715144015a8c977d"
-
-# Compare the generated hash with the known hash
-if [ "$generated_hash" = "$known_hash" ]; then
-    echo "KontrolDeployment.sol matches the known hash."
-else
-    echo "KontrolDeployment.sol does not match the known hash. Please update the known hash."
-    echo "Old hash: $known_hash"
-    echo "New hash: $generated_hash"
-    exit 1
-fi

packages/contracts-bedrock/test/kontrol/deployment/KontrolDeployment.sol

-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.0;
-
-import { Deploy } from "scripts/deploy/Deploy.s.sol";
-
-contract KontrolDeployment is Deploy {
-    function runKontrolDeployment() public {
-        runWithStateDiff();
-    }
-
-    function runKontrolDeploymentFaultProofs() public {
-        cfg.setUseFaultProofs(true);
-        runWithStateDiff();
-    }
-}

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

@@ -202,17 +202,17 @@ The summary lemma is as follows, with commentary inlined:
        // 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.
-       andThenBool 0 <=Int PCOUNT
-       andThenBool 0 <=Int LENGTH andThenBool LENGTH <Int maxBytesLength
-       andThenBool 0 <=Int SRC    andThenBool SRC    <Int maxBytesLength
-       andThenBool 0 <=Int DEST   andThenBool DEST   <Int maxBytesLength
-       andThenBool #sizeWordStack(WS) <=Int 1015
-       andThenBool SRC +Int LENGTH <=Int DEST // No overlap between source and destination
-       andThenBool DEST <=Int lengthBytes(LM) // Destination starts within current memory
-       andThenBool PCOUNT +Int 51 <Int lengthBytes(JUMPDESTS) // We're not look outside of the JUMPDESTs bytearray
+       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
+       andBool PCOUNT +Int 51 <Int lengthBytes(JUMPDESTS) // We are not looking outside of the JUMPDESTs bytearray
        // All JUMPDESTs in the program are valid
-       andThenBool JUMPDESTS[PCOUNT +Int 2] ==Int 1 andThenBool JUMPDESTS[PCOUNT +Int 32] ==Int 1 andThenBool JUMPDESTS[PCOUNT +Int 51] ==Int 1
-       andThenBool PCOUNT +Int 51 <Int 2 ^Int 16  // and fit into two bytes
+       andBool JUMPDESTS[PCOUNT +Int 2] ==Int 1 andBool JUMPDESTS[PCOUNT +Int 32] ==Int 1 andBool JUMPDESTS[PCOUNT +Int 51] ==Int 1
+       andBool PCOUNT +Int 51 <Int 2 ^Int 24  // and fit into three bytes
       [priority(30), concrete(JUMPDESTS, PROGRAM, PCOUNT), preserves-definedness]
 
 endmodule

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

 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.13;
 
-import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
+import { DeploymentSummaryFaultProofs } from "./utils/DeploymentSummaryFaultProofs.sol";
 import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { IL1CrossDomainMessenger as L1CrossDomainMessenger } from "src/L1/interfaces/IL1CrossDomainMessenger.sol";
 import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
 
-contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
+contract L1CrossDomainMessengerKontrol is DeploymentSummaryFaultProofs, KontrolUtils {
     L1CrossDomainMessenger l1CrossDomainMessenger;
     SuperchainConfig superchainConfig;
 

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

 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.13;
 
-import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
+import { DeploymentSummaryFaultProofs } from "./utils/DeploymentSummaryFaultProofs.sol";
 import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { IL1ERC721Bridge as L1ERC721Bridge } from "src/L1/interfaces/IL1ERC721Bridge.sol";
 import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
 import { ICrossDomainMessenger as CrossDomainMessenger } from "src/universal/interfaces/ICrossDomainMessenger.sol";
 
-contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
+contract L1ERC721BridgeKontrol is DeploymentSummaryFaultProofs, KontrolUtils {
     L1ERC721Bridge l1ERC721Bridge;
     SuperchainConfig superchainConfig;
 

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

 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.13;
 
-import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
+import { DeploymentSummaryFaultProofs } from "./utils/DeploymentSummaryFaultProofs.sol";
 import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { IL1StandardBridge as L1StandardBridge } from "src/L1/interfaces/IL1StandardBridge.sol";
 import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
 import { ICrossDomainMessenger as CrossDomainMessenger } from "src/universal/interfaces/ICrossDomainMessenger.sol";
 
-contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
+contract L1StandardBridgeKontrol is DeploymentSummaryFaultProofs, KontrolUtils {
     L1StandardBridge l1standardBridge;
     SuperchainConfig superchainConfig;
 

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

@@ -155,7 +155,7 @@ start_docker () {
     --rm \
     --interactive \
     --detach \
-    --env FOUNDRY_PROFILE="$FOUNDRY_PROFILE" \
+    --env FOUNDRY_PROFILE="${FOUNDRY_PROFILE-default}" \
     --workdir /home/user/workspace \
     runtimeverificationinc/kontrol:ubuntu-jammy-"$KONTROL_RELEASE"
 

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

 #!/bin/bash
 set -euo pipefail
 
-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"
@@ -50,10 +48,8 @@ fi
 conditionally_start_docker
 
 CONTRACT_NAMES=deployments/kontrol.json
-SCRIPT_SIG="runKontrolDeployment()"
 if [ "$KONTROL_FP_DEPLOYMENT" = true ]; then
   CONTRACT_NAMES=deployments/kontrol-fp.json
-  SCRIPT_SIG="runKontrolDeploymentFaultProofs()"
 fi
 
 # Sender just needs to be anything but the default sender (0x1804c8AB1F12E6bbf3894d4083f33e07309d1f38)
@@ -61,7 +57,7 @@ fi
 # Conflicts with other stuff that happens inside of Kontrol and leads to errors that are hard to debug
 DEPLOY_CONFIG_PATH=deploy-config/hardhat.json \
 DEPLOYMENT_OUTFILE="$CONTRACT_NAMES" \
-  forge script --sender 0xf39Fd6e51aad88F6F4ce6aB8827279cffFb92266 -vvv test/kontrol/deployment/KontrolDeployment.sol:KontrolDeployment --sig $SCRIPT_SIG
+  forge script --sender 0xf39Fd6e51aad88F6F4ce6aB8827279cffFb92266 -vvv scripts/deploy/Deploy.s.sol:Deploy --sig runWithStateDiff
 echo "Created state diff json"
 
 # Clean and store the state diff json in snapshots/state-diff/Kontrol-Deploy.json
@@ -85,7 +81,7 @@ if [ "$KONTROL_FP_DEPLOYMENT" = true ]; then
 fi
 
 copy_to_docker # Copy the newly generated files to the docker container
-run kontrol load-state-diff $SUMMARY_NAME snapshots/state-diff/$STATEDIFF --contract-names $CONTRACT_NAMES --output-dir $SUMMARY_DIR --license $LICENSE
+run kontrol load-state --from-state-diff $SUMMARY_NAME snapshots/state-diff/$STATEDIFF --contract-names $CONTRACT_NAMES --output-dir $SUMMARY_DIR --license $LICENSE
 if [ "$LOCAL" = false ]; then
     # Sync Snapshot updates to the host
     docker cp "$CONTAINER_NAME:/home/user/workspace/$SUMMARY_DIR" "$WORKSPACE_DIR/$SUMMARY_DIR/.."

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

@@ -16,10 +16,11 @@ kontrol_build() {
   notif "Kontrol Build"
   # shellcheck disable=SC2086
   run kontrol build \
-    --verbose \
     --require $lemmas \
     --module-import $module \
-    $rekompile
+    --no-metadata \
+    ${rekompile} \
+    ${regen}
   return $?
 }
 
@@ -36,9 +37,15 @@ kontrol_prove() {
     $break_on_calls \
     $break_every_step \
     $tests \
-    --init-node-from $state_diff \
-    --kore-rpc-command 'kore-rpc-booster --equation-max-recursion 100' \
-    --xml-test-report
+    --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
   return $?
 }
 
@@ -107,10 +114,9 @@ lemmas=test/kontrol/pausability-lemmas.md
 base_module=PAUSABILITY-LEMMAS
 module=OptimismPortalKontrol:$base_module
 rekompile=--rekompile
-rekompile=
+# rekompile=
 regen=--regen
-# shellcheck disable=SC2034
-regen=
+# regen=
 
 #################################
 # Tests to symbolically execute #

versions.json

@@ -7,7 +7,7 @@
   "eth2_testnet_genesis": "v0.10.0",
   "nvm": "v20.9.0",
   "slither": "0.10.2",
-  "kontrol": "0.1.316",
+  "kontrol": "1.0.53",
   "just": "1.34.0",
   "binary_signer": "1.0.4",
   "semgrep": "1.90.0"