Add fast summarization for Kontrol proofs

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

@@ -0,0 +1,79 @@
+// 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_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_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 skipped because `KontrolDeployment` doesn't initialize
+    ///         the L2OutputOracle
+    function test_simple_isOutputFinalized_succeeds() external override {
+        vm.skip(true);
+    }
+
+    /// @notice This test is skipped because `KontrolDeployment` doesn't initialize
+    ///         the L2OutputOracle
+    function test_isOutputFinalized_succeeds() external override {
+        vm.skip(true);
+    }
+}

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();
@@ -75,6 +77,7 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     )
         external
     {
+        setUpInlined();
         bytes memory _data = freshBigBytes(320);
 
         Types.WithdrawalTransaction memory _tx =

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,27 +180,36 @@ 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);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         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,14 +269,20 @@ 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";
         vm.store(OptimismPortalProxyAddress, slot, value);
         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);