Add fast summarization for Kontrol proofs (#9092)

* KontrolDeployment: move to `deployment` folder

* Add `DeploymentSummary.t.sol`

* `DeploymentSummary`: `vm` visivility from `internal` to `private`

* KontrolUtils: `vm` visivility form `private` to `internal`

* Add fast summarization; run `finalizeWithdrawalTransaction` proof

* Delete dummy proofs

* README.md: Reflect `deployment` folder & deletion of `proofs/tests`

* `run-kontrol.sh`: fix path for `Kontrol-Deploy.json`

* `OptimismPortal_Test`: set `virtual` functions to override in Kontrol summary test

* `DeploymentSummary_Test`: Tidy up & remove innecessary code

* `versions.json`: bump Kontrol from `0.1.117` to `0.1.121`

* Update `Kontrol-Deploy.json`

* `run-kontrol.sh`: remove `bmc` proving mode

* `OptimismPortalKontrol`: inline `setUp` function

* `OptimismPortal_Test`: fix typo in comments

* Prettify `snapshots/state-diff/Kontrol-Deploy.json`

* `run-kontrol.sh`: add logs to `test/kontrol/logs` instead of root

* Update Kontrol deployment summary

* `DeploymentSummary_Test`: Update `test_constructor_suceeds`; add `test_initialize_succeeds`

* `DeploymentSummary_Test`: fix typos

* `DeploymentSummary_Test`: remove `vm.skip(true)`

* `OptimismPortalKontrol`: simplify test logic

packages/contracts-bedrock/test/L1/OptimismPortal.t.sol

@@ -25,13 +25,17 @@ import { OptimismPortal } from "src/L1/OptimismPortal.sol";
 contract OptimismPortal_Test is CommonTest {
     address depositor;
 
-    function setUp() public override {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function setUp() public virtual override {
         super.setUp();
         depositor = makeAddr("depositor");
     }
 
     /// @dev Tests that the constructor sets the correct values.
-    function test_constructor_succeeds() external {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_constructor_succeeds() external virtual {
         OptimismPortal opImpl = OptimismPortal(payable(deploy.mustGetAddress("OptimismPortal")));
         assertEq(address(opImpl.L2_ORACLE()), address(0));
         assertEq(address(opImpl.l2Oracle()), address(0));
@@ -42,7 +46,9 @@ contract OptimismPortal_Test is CommonTest {
     }
 
     /// @dev Tests that the initializer sets the correct values.
-    function test_initialize_succeeds() external {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_initialize_succeeds() external virtual {
         address guardian = deploy.cfg().superchainConfigGuardian();
         assertEq(address(optimismPortal.L2_ORACLE()), address(l2OutputOracle));
         assertEq(address(optimismPortal.l2Oracle()), address(l2OutputOracle));
@@ -282,7 +288,9 @@ contract OptimismPortal_Test is CommonTest {
     }
 
     /// @dev Tests that `isOutputFinalized` succeeds for an EOA depositing a tx with ETH and data.
-    function test_simple_isOutputFinalized_succeeds() external {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_simple_isOutputFinalized_succeeds() external virtual {
         uint256 startingBlockNumber = deploy.cfg().l2OutputOracleStartingBlockNumber();
 
         uint256 ts = block.timestamp;
@@ -302,7 +310,9 @@ contract OptimismPortal_Test is CommonTest {
     }
 
     /// @dev Tests `isOutputFinalized` for a finalized output.
-    function test_isOutputFinalized_succeeds() external {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_isOutputFinalized_succeeds() external virtual {
         uint256 checkpoint = l2OutputOracle.nextBlockNumber();
         uint256 nextOutputIndex = l2OutputOracle.nextOutputIndex();
         vm.roll(checkpoint);

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

@@ -8,15 +8,14 @@ The directory is structured as follows
 
 ```tree
 test/kontrol
-├── KontrolDeployment.sol
+├── deployment
+│   ├── DeploymentSummary.t.sol
+│   └── KontrolDeployment.sol
 ├── pausability-lemmas.k
 ├── proofs
 │   ├── interfaces
 │   │   └── KontrolInterfaces.sol
 │   ├── OptimismPortal.k.sol
-│   ├── tests
-│   │   ├── Counter.sol
-│   │   └── Counter.t.sol
 │   └── utils
 │       ├── DeploymentSummaryCode.sol
 │       ├── DeploymentSummary.sol
@@ -32,11 +31,16 @@ test/kontrol
 
 ### Root folder
 
-- [`KontrolDeployment.sol`](./KontrolDeployment.sol): Reduced deployment to generate the summary contract
 - [`pausability-lemmas.k`](./pausability-lemmas.k): File containing the necessary lemmas for this project
+- [`deployment`](./deployment): Custom deploy sequence for Kontrol proofs and tests for its summarization
 - [`proofs`](./proofs): Where the proofs of the project live
 - [`scripts`](./scripts): Where the scripts of the projects live
 
+### [`deployment`](./deployment) folder
+
+- [`KontrolDeployment.sol`](./deployment/KontrolDeployment.sol): Simplified deployment sequence for Kontrol proofs
+- [`DeploymentSummary.t.sol`](./deployment/DeploymentSummary.t.sol): Tests for the summarization of custom deployment
+
 ### [`proofs`](./proofs) folder
 
 - [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol): Symbolic property tests

packages/contracts-bedrock/test/kontrol/deployment/DeploymentSummary.t.sol

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+// Libraries
+import { Constants } from "src/libraries/Constants.sol";
+
+// Target contract dependencies
+import { L2OutputOracle } from "src/L1/L2OutputOracle.sol";
+import { SystemConfig } from "src/L1/SystemConfig.sol";
+import { SuperchainConfig } from "src/L1/SuperchainConfig.sol";
+import { OptimismPortal } from "src/L1/OptimismPortal.sol";
+import { DeploymentSummary } from "../proofs/utils/DeploymentSummary.sol";
+import { OptimismPortal_Test } from "test/L1/OptimismPortal.t.sol";
+
+/// @dev Contract testing the deployment summary correctness
+contract DeploymentSummary_Test is DeploymentSummary, OptimismPortal_Test {
+    /// @notice super.setUp is not called on purpose
+    function setUp() public override {
+        // Recreate Deployment Summary state changes
+        DeploymentSummary deploymentSummary = new DeploymentSummary();
+        deploymentSummary.recreateDeployment();
+
+        // Set summary addresses
+        optimismPortal = OptimismPortal(payable(OptimismPortalProxyAddress));
+        superchainConfig = SuperchainConfig(SuperchainConfigProxyAddress);
+        l2OutputOracle = L2OutputOracle(L2OutputOracleProxyAddress);
+        systemConfig = SystemConfig(SystemConfigProxyAddress);
+
+        // Set up utilized addresses
+        depositor = makeAddr("depositor");
+        alice = makeAddr("alice");
+        bob = makeAddr("bob");
+        vm.deal(alice, 10000 ether);
+        vm.deal(bob, 10000 ether);
+    }
+
+    /// @dev Skips the first line of `super.test_constructor_succeeds` because
+    ///      we're not exercising the `Deploy` logic in these tests. However,
+    ///      the remaining assertions of the test are important to check
+    function test_constructor_succeeds() external override {
+        // OptimismPortal opImpl = OptimismPortal(payable(deploy.mustGetAddress("OptimismPortal")));
+        OptimismPortal opImpl = OptimismPortal(payable(OptimismPortalAddress));
+        assertEq(address(opImpl.L2_ORACLE()), address(0));
+        assertEq(address(opImpl.l2Oracle()), address(0));
+        assertEq(address(opImpl.SYSTEM_CONFIG()), address(0));
+        assertEq(address(opImpl.systemConfig()), address(0));
+        assertEq(address(opImpl.superchainConfig()), address(0));
+        assertEq(opImpl.l2Sender(), Constants.DEFAULT_L2_SENDER);
+    }
+
+    /// @dev Skips the first line of `super.test_initialize_succeeds` because
+    ///      we're not exercising the `Deploy` logic in these tests. However,
+    ///      the remaining assertions of the test are important to check
+    function test_initialize_succeeds() external override {
+        // address guardian = deploy.cfg().superchainConfigGuardian();
+        address guardian = superchainConfig.guardian();
+        assertEq(address(optimismPortal.L2_ORACLE()), address(l2OutputOracle));
+        assertEq(address(optimismPortal.l2Oracle()), address(l2OutputOracle));
+        assertEq(address(optimismPortal.SYSTEM_CONFIG()), address(systemConfig));
+        assertEq(address(optimismPortal.systemConfig()), address(systemConfig));
+        assertEq(optimismPortal.GUARDIAN(), guardian);
+        assertEq(optimismPortal.guardian(), guardian);
+        assertEq(address(optimismPortal.superchainConfig()), address(superchainConfig));
+        assertEq(optimismPortal.l2Sender(), Constants.DEFAULT_L2_SENDER);
+        assertEq(optimismPortal.paused(), false);
+    }
+
+    /// @notice This test is overridden because `KontrolDeployment` doesn't initialize
+    ///         the L2OutputOracle, which is needed in this test
+    function test_simple_isOutputFinalized_succeeds() external override { }
+
+    /// @notice This test is overridden because `KontrolDeployment` doesn't initialize
+    ///         the L2OutputOracle, which is needed in this test
+    function test_isOutputFinalized_succeeds() external override { }
+}

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

@@ -13,8 +13,9 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     OptimismPortal optimismPortal;
     SuperchainConfig superchainConfig;
 
-    function setUp() public {
-        recreateDeployment();
+    /// @dev Inlined setUp function for faster Kontrol performance
+    ///      Tracking issue: https://github.com/runtimeverification/kontrol/issues/282
+    function setUpInlined() public {
         optimismPortal = OptimismPortal(payable(OptimismPortalProxyAddress));
         superchainConfig = SuperchainConfig(SuperchainConfigProxyAddress);
     }
@@ -39,6 +40,7 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     )
         external
     {
+        setUpInlined();
         bytes memory _data = freshBigBytes(320);
 
         bytes[] memory _withdrawalProof = freshWithdrawalProof();
@@ -48,16 +50,10 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
         Types.OutputRootProof memory _outputRootProof =
             Types.OutputRootProof(_outputRootProof0, _outputRootProof1, _outputRootProof2, _outputRootProof3);
 
-        // After deployment, Optimism portal is enabled
-        require(optimismPortal.paused() == false, "Portal should not be paused");
-
         // Pause Optimism Portal
         vm.prank(optimismPortal.GUARDIAN());
         superchainConfig.pause("identifier");
 
-        // Portal is now paused
-        require(optimismPortal.paused(), "Portal should be paused");
-
         // No one can call proveWithdrawalTransaction
         vm.expectRevert("OptimismPortal: paused");
         optimismPortal.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
@@ -75,21 +71,16 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     )
         external
     {
+        setUpInlined();
         bytes memory _data = freshBigBytes(320);
 
         Types.WithdrawalTransaction memory _tx =
             Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data);
 
-        // After deployment, Optimism portal is enabled
-        require(optimismPortal.paused() == false, "Portal should not be paused");
-
         // Pause Optimism Portal
         vm.prank(optimismPortal.GUARDIAN());
         superchainConfig.pause("identifier");
 
-        // Portal is now paused
-        require(optimismPortal.paused(), "Portal should be paused");
-
         vm.expectRevert("OptimismPortal: paused");
         optimismPortal.finalizeWithdrawalTransaction(_tx);
     }

packages/contracts-bedrock/test/kontrol/proofs/tests/Counter.sol

-// SPDX-License-Identifier: UNLICENSED
-pragma solidity ^0.8.13;
-
-contract Counter {
-    uint256 public number;
-
-    function setNumber(uint256 newNumber) public {
-        number = newNumber;
-    }
-}

packages/contracts-bedrock/test/kontrol/proofs/tests/Counter.t.sol

-// SPDX-License-Identifier: UNLICENSED
-pragma solidity ^0.8.13;
-
-import { Counter } from "./Counter.sol";
-
-contract CounterTest {
-    Counter counter;
-
-    function setUp() public {
-        counter = new Counter();
-    }
-
-    function test_SetNumber(uint256 x) public {
-        counter.setNumber(x);
-        require(counter.number() == x, "Not equal");
-    }
-}

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

@@ -9,13 +9,13 @@ import { DeploymentSummaryCode } from "./DeploymentSummaryCode.sol";
 
 contract DeploymentSummary is DeploymentSummaryCode {
     // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D
-    address internal constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
-    Vm internal constant vm = Vm(VM_ADDRESS);
+    address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
+    Vm private constant vm = Vm(VM_ADDRESS);
 
     address internal constant AddressManagerAddress = 0xBb2180ebd78ce97360503434eD37fcf4a1Df61c3;
-    address internal constant L2OutputOracleAddress = 0x1B9F0e648A0A4780120A6Cd07B952F76560c8F8b;
+    address internal constant L2OutputOracleAddress = 0x19652082F846171168Daf378C4fD3ee85a0D4A60;
     address internal constant L2OutputOracleProxyAddress = 0x8B71b41D4dBEb2b6821d44692d3fACAAf77480Bb;
-    address internal constant OptimismPortalAddress = 0x94eA1235778aDc02FD93c242e6A23Ef5C8c3CE44;
+    address internal constant OptimismPortalAddress = 0x8887E7568E81405c4E0D4cAaabdda949e3B9d4E4;
     address internal constant OptimismPortalProxyAddress = 0x978e3286EB805934215a88694d80b09aDed68D90;
     address internal constant ProtocolVersionsAddress = 0xfbfD64a6C0257F613feFCe050Aa30ecC3E3d7C3F;
     address internal constant ProtocolVersionsProxyAddress = 0x416C42991d05b31E9A6dC209e91AD22b79D87Ae6;
@@ -24,7 +24,7 @@ contract DeploymentSummary is DeploymentSummaryCode {
     address internal constant SafeSingletonAddress = 0x90193C961A926261B756D1E5bb255e67ff9498A1;
     address internal constant SuperchainConfigAddress = 0x068E44eB31e111028c41598E4535be7468674D0A;
     address internal constant SuperchainConfigProxyAddress = 0xDEb1E9a6Be7Baf84208BB6E10aC9F9bbE1D70809;
-    address internal constant SystemConfigAddress = 0xc7B87b2b892EA5C3CfF47168881FE168C00377FB;
+    address internal constant SystemConfigAddress = 0xffbA8944650e26653823658d76A122946F27e2f2;
     address internal constant SystemConfigProxyAddress = 0x1c23A6d89F95ef3148BCDA8E242cAb145bf9c0E4;
     address internal constant SystemOwnerSafeAddress = 0x2601573C28B77dea6C8B73385c25024A28a00C3F;
 
@@ -180,10 +180,19 @@ contract DeploymentSummary is DeploymentSummaryCode {
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000101";
         vm.store(L2OutputOracleAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000004";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(L2OutputOracleAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(L2OutputOracleAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000001";
         vm.store(L2OutputOracleAddress, slot, value);
         vm.etch(SystemConfigAddress, SystemConfigCode);
+        slot = hex"a11ee3ab75b40e88a0105e935d17cd36c8faee0138320d776c411291bdbbb19f";
+        value = hex"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff";
+        vm.store(SystemConfigAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000001";
         vm.store(SystemConfigAddress, slot, value);
@@ -191,16 +200,16 @@ contract DeploymentSummary is DeploymentSummaryCode {
         value = hex"0000000000000000000000000000000000000000000000000000000000000101";
         vm.store(SystemConfigAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
-        value = hex"0000000000000000000000001804c8ab1f12e6bbf3894d4083f33e07309d1f38";
+        value = hex"0000000000000000000000004e59b44847b379578588920ca78fbf26c0b4956c";
         vm.store(SystemConfigAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
         value = hex"000000000000000000000000000000000000000000000000000000000000dead";
         vm.store(SystemConfigAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000068";
-        value = hex"0000000000000000000000000000000000000000000000000000000001406f40";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
         vm.store(SystemConfigAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000069";
-        value = hex"0000ffffffffffffffffffffffffffffffff000f42403b9aca00080a01312d00";
+        value = hex"0000000000000000000000000000000000000000000000000000020100000001";
         vm.store(SystemConfigAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000001";
@@ -209,7 +218,7 @@ contract DeploymentSummary is DeploymentSummaryCode {
         value = hex"0000000000000000000000000000000000000000000000000000000000000003";
         vm.store(SystemOwnerSafeAddress, slot, value);
         slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
-        value = hex"000000000000000000000000c7b87b2b892ea5c3cff47168881fe168c00377fb";
+        value = hex"000000000000000000000000ffba8944650e26653823658d76a122946f27e2f2";
         vm.store(SystemConfigProxyAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000001";
@@ -238,6 +247,18 @@ contract DeploymentSummary is DeploymentSummaryCode {
         slot = hex"65a7ed542fb37fe237fdfbdd70b31598523fe5b32879e307bae27a0bd9581c08";
         value = hex"0000000000000000000000009965507d1a55bcc2695c58ba16fb37d819b0a4dc";
         vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"71ac12829d66ee73d8d95bff50b3589745ce57edae70a3fb111a2342464dc597";
+        value = hex"000000000000000000000000ff00000000000000000000000000000000000000";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"e52a667f71ec761b9b381c7b76ca9b852adf7e8905da0e0ad49986a0a6871815";
+        value = hex"0000000000000000000000008b71b41d4dbeb2b6821d44692d3facaaf77480bb";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"4b6c74f9e688cb39801f2112c14a8c57232a3fc5202e1444126d4bce86eb19ac";
+        value = hex"000000000000000000000000978e3286eb805934215a88694d80b09aded68d90";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"a11ee3ab75b40e88a0105e935d17cd36c8faee0138320d776c411291bdbbb19f";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemConfigProxyAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000069";
         value = hex"0000ffffffffffffffffffffffffffffffff000f42403b9aca00080a01312d00";
         vm.store(SystemConfigProxyAddress, slot, value);
@@ -248,7 +269,7 @@ contract DeploymentSummary is DeploymentSummaryCode {
         value = hex"0000000000000000000000000000000000000000000000000000000000000004";
         vm.store(SystemOwnerSafeAddress, slot, value);
         slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
-        value = hex"00000000000000000000000094ea1235778adc02fd93c242e6a23ef5c8c3ce44";
+        value = hex"0000000000000000000000008887e7568e81405c4e0d4caaabdda949e3b9d4e4";
         vm.store(OptimismPortalProxyAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000001";
@@ -256,6 +277,12 @@ contract DeploymentSummary is DeploymentSummaryCode {
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000101";
         vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000036";
+        value = hex"0000000000000000000000008b71b41d4dbeb2b6821d44692d3facaaf77480bb";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000037";
+        value = hex"0000000000000000000000001c23a6d89f95ef3148bcda8e242cab145bf9c0e4";
+        vm.store(OptimismPortalProxyAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000035";
         value = hex"0000000000000000000000deb1e9a6be7baf84208bb6e10ac9f9bbe1d7080900";
         vm.store(OptimismPortalProxyAddress, slot, value);

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

@@ -40,8 +40,8 @@ contract GhostBytes10 {
 abstract contract KontrolUtils is KontrolCheats {
     /// @dev we only care about the vm signature
     // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D.
-    address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
-    Vm private constant vm = Vm(VM_ADDRESS);
+    address internal constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
+    Vm internal constant vm = Vm(VM_ADDRESS);
 
     /// @dev Creates a fresh bytes with length greater than 31
     /// @param bytesLength: Length of the fresh bytes. Should be concrete

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

@@ -26,7 +26,7 @@ cp ${DEPLOY_SCRIPT} ${DEPLOY_SCRIPT}.bak
 # of the system are deployed, we'd get some reverts on the `mustGetAddress` functions
 awk '{gsub(/mustGetAddress/, "getAddress")}1' ${DEPLOY_SCRIPT} > temp && mv temp ${DEPLOY_SCRIPT}
 
-FOUNDRY_PROFILE=kdeploy forge script -vvv test/kontrol/KontrolDeployment.sol:KontrolDeployment --sig 'runKontrolDeployment()'
+FOUNDRY_PROFILE=kdeploy forge script -vvv test/kontrol/deployment/KontrolDeployment.sol:KontrolDeployment --sig 'runKontrolDeployment()'
 echo "Created state diff json"
 
 # Restore the file from the backup
@@ -39,6 +39,7 @@ GENERATED_STATEDIFF=Deploy.json # Name of the statediff json produced by the dep
 STATEDIFF=Kontrol-${GENERATED_STATEDIFF} # Name of the Kontrol statediff
 mv snapshots/state-diff/${GENERATED_STATEDIFF} snapshots/state-diff/${STATEDIFF}
 python3 ${JSON_SCRIPTS}/clean_json.py snapshots/state-diff/${STATEDIFF}
+jq . snapshots/state-diff/${STATEDIFF} > temp && mv temp snapshots/state-diff/${STATEDIFF} # Prettify json
 echo "Cleaned state diff json"
 
 CONTRACT_NAMES=deployments/hardhat/.deploy

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

@@ -94,14 +94,14 @@ kontrol_prove() {
                         --max-depth ${max_depth}           \
                         --max-iterations ${max_iterations} \
                         --smt-timeout ${smt_timeout}       \
-                        --bmc-depth ${bmc_depth}           \
                         --workers ${workers}               \
                         ${reinit}                          \
                         ${bug_report}                      \
                         ${break_on_calls}                  \
                         ${auto_abstract}                   \
                         ${tests}                           \
-                        ${use_booster}
+                        ${use_booster}                     \
+                        --init-node-from ${state_diff}
 }
 
 start_docker () {
@@ -135,20 +135,26 @@ run () {
 }
 
 dump_log_results(){
-    trap clean_docker ERR
-    RESULTS_LOG="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
+  trap clean_docker ERR
+    RESULTS_FILE="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
+    LOG_PATH="test/kontrol/logs"
+    RESULTS_LOG="${LOG_PATH}/${RESULTS_FILE}"
 
-    notif "Generating Results Log: ${RESULTS_LOG}"
+    if [ ! -d ${LOG_PATH} ]; then
+      mkdir ${LOG_PATH}
+    fi
+
+    notif "Generating Results Log: ${LOG_PATH}"
     blank_line
 
     run tar -czvf results.tar.gz kout-proofs/ > /dev/null 2>&1
     if [ "${LOCAL}" = true ]; then
-      cp results.tar.gz "${RESULTS_LOG}"
+      mv results.tar.gz "${RESULTS_LOG}"
     else
       docker cp ${CONTAINER_NAME}:/home/user/workspace/results.tar.gz "${RESULTS_LOG}"
     fi
     if [ -f "${RESULTS_LOG}" ]; then
-      cp "${RESULTS_LOG}" kontrol-results_latest.tar.gz
+      cp "${RESULTS_LOG}" "${LOG_PATH}/kontrol-results_latest.tar.gz"
     else
       notif "Results Log: ${RESULTS_LOG} not found, skipping.."
       blank_line
@@ -160,7 +166,7 @@ dump_log_results(){
       notif "Results Log: ${RESULTS_LOG} generated"
       blank_line
       RUN_LOG="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log"
-      docker logs ${CONTAINER_NAME} > "${RUN_LOG}"
+      docker logs ${CONTAINER_NAME} > "${LOG_PATH}/${RUN_LOG}"
     fi
 }
 
@@ -208,7 +214,6 @@ regen=
 max_depth=1000000
 max_iterations=1000000
 smt_timeout=100000
-bmc_depth=10
 workers=1
 reinit=--reinit
 reinit=
@@ -220,14 +225,14 @@ bug_report=--bug-report
 bug_report=
 use_booster=--use-booster
 # use_booster=
+state_diff="./snapshots/state-diff/Kontrol-Deploy.json"
 
 #########################################
 # List of tests to symbolically execute #
 #########################################
 tests=""
-tests+="--match-test CounterTest.test_SetNumber "
 #tests+="--match-test OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused "
-#tests+="--match-test OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused "
+tests+="--match-test OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused "
 
 #############
 # RUN TESTS #

versions.json

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