Add Kontrol proofs for `L1StandardBridgeKontrol` and `L1ERC721BridgeKontrol` (#9183)

* OptimismPortal.k.sol: directly feed `WithdrawalTransaction` argument

* KontrolInterfaces: add interfaces for bridges

* KontrolDeployment: add deployment for L1 bridges

* run-kontrol.sh: add bridge proofs

* Update summaries

* Add `L1StandardBridge` proofs

* Add `L1ERC721Bridge` proof

* KontrolDeployment: remove typo import

* `kontrol-tests`: add remaining files to `check-changed`

* Fix spelling typo

* Document current `vm.mockCall` workaround

* Document symbolic bytes assumptions

* Supress upper case legacy naming

* Add summarization tests for `L1ERC721Bridge`

* Add summarization tests for `L1StandardBridge`

* run-kontrol.sh: set `workers` to `min(max_workers, #test_list)`

* README.md: add bridge proofs

* make `xDomainMessageSender` part of `IL1CrossDomainMessenger`

* Missed instances of `ICrossDomainMessenger`

* Document `vm.prank()` issue

* Improve assumption documentation

* run-kontrol.sh: improve style

* `kontrol-tests`: add remaining files to `check-changed`

* run-kontrol.sh: document `max_workers=7`

.circleci/config.yml

@@ -1332,7 +1332,7 @@ jobs:
           name: Checkout Submodule
           command: make submodules
       - check-changed:
-          patterns: contracts-bedrock/test/kontrol,contracts-bedrock/src/L1/OptimismPortal\.sol
+          patterns: contracts-bedrock/test/kontrol,contracts-bedrock/src/L1/OptimismPortal\.sol,contracts-bedrock/src/L1/L1CrossDomainMessenger\.sol,contracts-bedrock/src/L1/L1ERC721Bridge\.sol,contracts-bedrock/src/L1/L1StandardBridge\.sol,contracts-bedrock/src/L1/ResourceMetering\.sol,contracts-bedrock/src/universal/StandardBridge\.sol,contracts-bedrock/src/universal/ERC721Bridge\.sol,contracts-bedrock/src/universal/CrossDomainMessenger\.sol
       - setup_remote_docker:
           docker_layer_caching: true
       - run:

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

@@ -47,7 +47,9 @@ contract L1ERC721Bridge_Test is Bridge_Initializer {
     );
 
     /// @dev Sets up the testing environment.
-    function setUp() public override {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function setUp() public virtual override {
         super.setUp();
 
         localToken = new TestERC721();
@@ -62,7 +64,9 @@ contract L1ERC721Bridge_Test is Bridge_Initializer {
     }
 
     /// @dev Tests that the impl is created with the correct values.
-    function test_constructor_succeeds() public {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_constructor_succeeds() public virtual {
         L1ERC721Bridge impl = L1ERC721Bridge(deploy.mustGetAddress("L1ERC721Bridge"));
         assertEq(address(impl.MESSENGER()), address(0));
         assertEq(address(impl.messenger()), address(0));

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

@@ -33,7 +33,9 @@ contract L1StandardBridge_Getter_Test is Bridge_Initializer {
 
 contract L1StandardBridge_Initialize_Test is Bridge_Initializer {
     /// @dev Test 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 {
         L1StandardBridge impl = L1StandardBridge(deploy.mustGetAddress("L1StandardBridge"));
         assertEq(address(impl.superchainConfig()), address(0));
         assertEq(address(impl.MESSENGER()), address(0));

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

@@ -16,6 +16,8 @@ test/kontrol
 │   ├── interfaces
 │   │   └── KontrolInterfaces.sol
 │   ├── L1CrossDomainMessenger.k.sol
+│   ├── L1ERC721Bridge.k.sol
+│   ├── L1StandardBridge.k.sol
 │   ├── OptimismPortal.k.sol
 │   └── utils
 │       ├── DeploymentSummaryCode.sol
@@ -45,6 +47,8 @@ test/kontrol
 ### [`proofs`](./proofs) folder
 
 - [`L1CrossDomainMessenger.k.sol`](./proofs/L1CrossDomainMessenger.k.sol): Symbolic property tests for [`L1CrossDomainMessenger`](../../src/L1/L1CrossDomainMessenger.sol)
+- [`L1ERC721Bridge.k.sol`](./proofs/L1ERC721Bridge.k.sol): Symbolic property tests for [`L1ERC721Bridge`](../../src/L1/L1ERC721Bridge.sol)
+- [`L1StandardBridge.k.sol`](./proofs/L1StandardBridge.k.sol): Symbolic property tests for [`L1StandardBridge`](../../src/L1/L1StandardBridge.sol)
 - [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol): Symbolic property tests for [`OptimismPortal`](../../src/L1/OptimismPortal.sol)
 - [`interfaces`](./proofs/interfaces): Files with the signature of the functions involved in the verification effort
 - [`utils`](./proofs/utils): Proof dependencies, including the summary contracts

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

@@ -12,8 +12,20 @@ import { SuperchainConfig } from "src/L1/SuperchainConfig.sol";
 import { OptimismPortal } from "src/L1/OptimismPortal.sol";
 import { L1CrossDomainMessenger } from "src/L1/L1CrossDomainMessenger.sol";
 import { DeploymentSummary } from "../proofs/utils/DeploymentSummary.sol";
-import { OptimismPortal_Test } from "test/L1/OptimismPortal.t.sol";
+import { L1ERC721Bridge } from "src/L1/L1ERC721Bridge.sol";
+import { L1StandardBridge } from "src/L1/L1StandardBridge.sol";
+import { ERC20 } from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
+import { LegacyMintableERC20 } from "src/legacy/LegacyMintableERC20.sol";
+
+// Tests
 import { L1CrossDomainMessenger_Test } from "test/L1/L1CrossDomainMessenger.t.sol";
+import { OptimismPortal_Test } from "test/L1/OptimismPortal.t.sol";
+import { L1ERC721Bridge_Test, TestERC721 } from "test/L1/L1ERC721Bridge.t.sol";
+import {
+    L1StandardBridge_Getter_Test,
+    L1StandardBridge_Initialize_Test,
+    L1StandardBridge_Pause_Test
+} from "test/L1/L1StandardBridge.t.sol";
 
 /// @dev Contract testing the deployment summary correctness
 contract DeploymentSummary_TestOptimismPortal is DeploymentSummary, OptimismPortal_Test {
@@ -115,3 +127,133 @@ contract DeploymentSummary_TestL1CrossDomainMessenger is DeploymentSummary, L1Cr
     ///         L2CrossDomainMessenger, which is needed in this test
     function test_relayMessage_v2_reverts() external override { }
 }
+
+contract DeploymentSummary_TestL1ERC721Bridge is DeploymentSummary, L1ERC721Bridge_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);
+        l1CrossDomainMessenger = L1CrossDomainMessenger(l1CrossDomainMessengerProxyAddress);
+        l1ERC721Bridge = L1ERC721Bridge(l1ERC721BridgeProxyAddress);
+
+        // Set up utilized addresses
+        alice = makeAddr("alice");
+        bob = makeAddr("bob");
+        vm.deal(alice, 10000 ether);
+        vm.deal(bob, 10000 ether);
+
+        // Bridge_Initializer setUp
+        L1Token = new ERC20("Native L1 Token", "L1T");
+
+        LegacyL2Token = new LegacyMintableERC20({
+            _l2Bridge: address(l2StandardBridge),
+            _l1Token: address(L1Token),
+            _name: string.concat("LegacyL2-", L1Token.name()),
+            _symbol: string.concat("LegacyL2-", L1Token.symbol())
+        });
+        vm.label(address(LegacyL2Token), "LegacyMintableERC20");
+
+        // Deploy the L2 ERC20 now
+        // L2Token = OptimismMintableERC20(
+        //     l2OptimismMintableERC20Factory.createStandardL2Token(
+        //         address(L1Token),
+        //         string(abi.encodePacked("L2-", L1Token.name())),
+        //         string(abi.encodePacked("L2-", L1Token.symbol()))
+        //     )
+        // );
+
+        // BadL2Token = OptimismMintableERC20(
+        //     l2OptimismMintableERC20Factory.createStandardL2Token(
+        //         address(1),
+        //         string(abi.encodePacked("L2-", L1Token.name())),
+        //         string(abi.encodePacked("L2-", L1Token.symbol()))
+        //     )
+        // );
+
+        NativeL2Token = new ERC20("Native L2 Token", "L2T");
+
+        // RemoteL1Token = OptimismMintableERC20(
+        //     l1OptimismMintableERC20Factory.createStandardL2Token(
+        //         address(NativeL2Token),
+        //         string(abi.encodePacked("L1-", NativeL2Token.name())),
+        //         string(abi.encodePacked("L1-", NativeL2Token.symbol()))
+        //     )
+        // );
+
+        // BadL1Token = OptimismMintableERC20(
+        //     l1OptimismMintableERC20Factory.createStandardL2Token(
+        //         address(1),
+        //         string(abi.encodePacked("L1-", NativeL2Token.name())),
+        //         string(abi.encodePacked("L1-", NativeL2Token.symbol()))
+        //     )
+        // );
+
+        // L1ERC721Bridge_Test setUp
+        localToken = new TestERC721();
+        remoteToken = new TestERC721();
+
+        // Mint alice a token.
+        localToken.mint(alice, tokenId);
+
+        // Approve the bridge to transfer the token.
+        vm.prank(alice);
+        localToken.approve(address(l1ERC721Bridge), tokenId);
+    }
+
+    /// @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() public override {
+        // L1ERC721Bridge impl = L1ERC721Bridge(deploy.mustGetAddress("L1ERC721Bridge"));
+        L1ERC721Bridge impl = L1ERC721Bridge(l1ERC721BridgeAddress);
+        assertEq(address(impl.MESSENGER()), address(0));
+        assertEq(address(impl.messenger()), address(0));
+        assertEq(address(impl.OTHER_BRIDGE()), Predeploys.L2_ERC721_BRIDGE);
+        assertEq(address(impl.otherBridge()), Predeploys.L2_ERC721_BRIDGE);
+        assertEq(address(impl.superchainConfig()), address(0));
+    }
+}
+
+contract DeploymentSummary_TestL1StandardBridge is
+    DeploymentSummary,
+    L1StandardBridge_Getter_Test,
+    L1StandardBridge_Initialize_Test,
+    L1StandardBridge_Pause_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);
+        l1CrossDomainMessenger = L1CrossDomainMessenger(l1CrossDomainMessengerProxyAddress);
+        l1ERC721Bridge = L1ERC721Bridge(l1ERC721BridgeProxyAddress);
+        l1StandardBridge = L1StandardBridge(payable(l1StandardBridgeProxyAddress));
+    }
+
+    /// @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 {
+        // L1StandardBridge impl = L1StandardBridge(deploy.mustGetAddress("L1StandardBridge"));
+        L1StandardBridge impl = L1StandardBridge(payable(l1StandardBridgeAddress));
+        assertEq(address(impl.superchainConfig()), address(0));
+        assertEq(address(impl.MESSENGER()), address(0));
+        assertEq(address(impl.messenger()), address(0));
+        assertEq(address(impl.OTHER_BRIDGE()), Predeploys.L2_STANDARD_BRIDGE);
+        assertEq(address(impl.otherBridge()), Predeploys.L2_STANDARD_BRIDGE);
+        assertEq(address(l2StandardBridge), Predeploys.L2_STANDARD_BRIDGE);
+    }
+}

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

@@ -12,7 +12,9 @@ contract KontrolDeployment is Deploy {
         deployERC1967Proxy("OptimismPortalProxy");
         deployERC1967Proxy("L2OutputOracleProxy");
         deployERC1967Proxy("SystemConfigProxy");
+        deployL1StandardBridgeProxy();
         deployL1CrossDomainMessengerProxy();
+        deployERC1967Proxy("L1ERC721BridgeProxy");
         transferAddressManagerOwnership(); // to the ProxyAdmin
 
         // deployImplementations();
@@ -20,9 +22,13 @@ contract KontrolDeployment is Deploy {
         deployL1CrossDomainMessenger();
         deployL2OutputOracle();
         deploySystemConfig();
+        deployL1StandardBridge();
+        deployL1ERC721Bridge();
 
         // initializeImplementations();
         initializeSystemConfig();
+        initializeL1StandardBridge();
+        initializeL1ERC721Bridge();
         initializeL1CrossDomainMessenger();
         initializeOptimismPortal();
     }

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

@@ -33,6 +33,7 @@ contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
     {
         setUpInlined();
 
+        // ASSUME: conservative upper bound on the `_message` length
         bytes memory _message = freshBigBytes(600);
 
         // Pause System

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 { KontrolUtils } from "./utils/KontrolUtils.sol";
+import { Types } from "src/libraries/Types.sol";
+import {
+    IL1ERC721Bridge as L1ERC721Bridge,
+    ISuperchainConfig as SuperchainConfig
+} from "./interfaces/KontrolInterfaces.sol";
+
+contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
+    L1ERC721Bridge l1ERC721Bridge;
+    SuperchainConfig superchainConfig;
+
+    function setUpInlined() public {
+        l1ERC721Bridge = L1ERC721Bridge(l1ERC721BridgeProxyAddress);
+        superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
+    }
+
+    /// TODO: Replace symbolic workarounds with the appropriate
+    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
+    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
+    function prove_finalizeBridgeERC21_paused(
+        address _localToken,
+        address _remoteToken,
+        address _from,
+        address _to,
+        uint256 _amount
+    )
+        public
+    {
+        setUpInlined();
+
+        // Current workaround to be replaced with `vm.mockCall`, once the cheatcode is implemented in Kontrol
+        // This overrides the storage slot read by `CrossDomainMessenger::xDomainMessageSender`
+        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/285
+        vm.store(
+            l1CrossDomainMessengerProxyAddress,
+            hex"00000000000000000000000000000000000000000000000000000000000000cc",
+            bytes32(uint256(uint160(address(l1ERC721Bridge.otherBridge()))))
+        );
+
+        // ASSUME: conservative upper bound on the `_extraData` length
+        bytes memory _extraData = freshBigBytes(320);
+
+        // Pause Standard Bridge
+        vm.prank(superchainConfig.guardian());
+        superchainConfig.pause("identifier");
+
+        // Pranking with `vm.prank` instead will result in failure from Kontrol
+        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/316
+        vm.startPrank(address(l1ERC721Bridge.messenger()));
+        vm.expectRevert("L1ERC721Bridge: paused");
+        l1ERC721Bridge.finalizeBridgeERC721(_localToken, _remoteToken, _from, _to, _amount, _extraData);
+        vm.stopPrank();
+    }
+}

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 { KontrolUtils } from "./utils/KontrolUtils.sol";
+import { Types } from "src/libraries/Types.sol";
+import {
+    IL1StandardBridge as L1StandardBridge,
+    ISuperchainConfig as SuperchainConfig
+} from "./interfaces/KontrolInterfaces.sol";
+
+contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
+    L1StandardBridge l1standardBridge;
+    SuperchainConfig superchainConfig;
+
+    function setUpInlined() public {
+        l1standardBridge = L1StandardBridge(payable(l1StandardBridgeProxyAddress));
+        superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
+    }
+
+    /// TODO: Replace symbolic workarounds with the appropriate
+    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
+    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
+    function prove_finalizeBridgeERC20_paused(
+        address _localToken,
+        address _remoteToken,
+        address _from,
+        address _to,
+        uint256 _amount
+    )
+        public
+    {
+        setUpInlined();
+
+        // Current workaround to be replaced with `vm.mockCall`, once the cheatcode is implemented in Kontrol
+        // This overrides the storage slot read by `CrossDomainMessenger::xDomainMessageSender`
+        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/285
+        vm.store(
+            l1CrossDomainMessengerProxyAddress,
+            hex"00000000000000000000000000000000000000000000000000000000000000cc",
+            bytes32(uint256(uint160(address(l1standardBridge.otherBridge()))))
+        );
+
+        // ASSUME: conservative upper bound on the `_extraData` length
+        bytes memory _extraData = freshBigBytes(320);
+
+        // Pause Standard Bridge
+        vm.prank(superchainConfig.guardian());
+        superchainConfig.pause("identifier");
+
+        // Pranking with `vm.prank` instead will result in failure from Kontrol
+        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/316
+        vm.startPrank(address(l1standardBridge.messenger()));
+        vm.expectRevert("StandardBridge: paused");
+        l1standardBridge.finalizeBridgeERC20(_localToken, _remoteToken, _from, _to, _amount, _extraData);
+        vm.stopPrank();
+    }
+
+    /// TODO: Replace symbolic workarounds with the appropriate
+    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
+    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
+    function prove_finalizeBridgeETH_paused(address _from, address _to, uint256 _amount) public {
+        setUpInlined();
+
+        // Current workaround to be replaced with `vm.mockCall`, once the cheatcode is implemented in Kontrol
+        // This overrides the storage slot read by `CrossDomainMessenger::xDomainMessageSender`
+        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/285
+        vm.store(
+            l1CrossDomainMessengerProxyAddress,
+            hex"00000000000000000000000000000000000000000000000000000000000000cc",
+            bytes32(uint256(uint160(address(l1standardBridge.otherBridge()))))
+        );
+
+        // ASSUME: conservative upper bound on the `_extraData` length
+        bytes memory _extraData = freshBigBytes(320);
+
+        // Pause Standard Bridge
+        vm.prank(superchainConfig.guardian());
+        superchainConfig.pause("identifier");
+
+        // Pranking with `vm.prank` instead will result in failure from Kontrol
+        // Tracking issue: https://github.com/runtimeverification/kontrol/issues/316
+        vm.startPrank(address(l1standardBridge.messenger()));
+        vm.expectRevert("StandardBridge: paused");
+        l1standardBridge.finalizeBridgeETH(_from, _to, _amount, _extraData);
+        vm.stopPrank();
+    }
+}

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

@@ -41,8 +41,9 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
         external
     {
         setUpInlined();
-        bytes memory _data = freshBigBytes(320);
 
+        // ASSUME: conservative upper bound on the `_data` length
+        bytes memory _data = freshBigBytes(320);
         bytes[] memory _withdrawalProof = freshWithdrawalProof();
 
         Types.WithdrawalTransaction memory _tx =
@@ -51,7 +52,7 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
             Types.OutputRootProof(_outputRootProof0, _outputRootProof1, _outputRootProof2, _outputRootProof3);
 
         // Pause Optimism Portal
-        vm.prank(optimismPortal.GUARDIAN());
+        vm.prank(optimismPortal.guardian());
         superchainConfig.pause("identifier");
 
         // No one can call proveWithdrawalTransaction
@@ -72,16 +73,17 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
         external
     {
         setUpInlined();
-        bytes memory _data = freshBigBytes(320);
 
-        Types.WithdrawalTransaction memory _tx =
-            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data);
+        // ASSUME: conservative upper bound on the `_data` length
+        bytes memory _data = freshBigBytes(320);
 
         // Pause Optimism Portal
-        vm.prank(optimismPortal.GUARDIAN());
+        vm.prank(optimismPortal.guardian());
         superchainConfig.pause("identifier");
 
         vm.expectRevert("OptimismPortal: paused");
-        optimismPortal.finalizeWithdrawalTransaction(_tx);
+        optimismPortal.finalizeWithdrawalTransaction(
+            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data)
+        );
     }
 }

packages/contracts-bedrock/test/kontrol/proofs/interfaces/KontrolInterfaces.sol

@@ -4,8 +4,6 @@ pragma solidity 0.8.15;
 import { Types } from "src/libraries/Types.sol";
 
 interface IOptimismPortal {
-    function GUARDIAN() external view returns (address);
-
     function guardian() external view returns (address);
 
     function paused() external view returns (bool paused_);
@@ -31,9 +29,45 @@ interface ISuperchainConfig {
     function unpause() external;
 }
 
-interface IL1CrossDomainMessenger {
+interface IL1StandardBridge {
     function paused() external view returns (bool);
 
+    function messenger() external view returns (IL1CrossDomainMessenger);
+
+    function otherBridge() external view returns (IL1StandardBridge);
+
+    function finalizeBridgeERC20(
+        address _localToken,
+        address _remoteToken,
+        address _from,
+        address _to,
+        uint256 _amount,
+        bytes calldata _extraData
+    )
+        external;
+
+    function finalizeBridgeETH(address _from, address _to, uint256 _amount, bytes calldata _extraData) external;
+}
+
+interface IL1ERC721Bridge {
+    function paused() external view returns (bool);
+
+    function messenger() external view returns (IL1CrossDomainMessenger);
+
+    function otherBridge() external view returns (IL1StandardBridge);
+
+    function finalizeBridgeERC721(
+        address _localToken,
+        address _remoteToken,
+        address _from,
+        address _to,
+        uint256 _amount,
+        bytes calldata _extraData
+    )
+        external;
+}
+
+interface IL1CrossDomainMessenger {
     function relayMessage(
         uint256 _nonce,
         address _sender,
@@ -44,4 +78,6 @@ interface IL1CrossDomainMessenger {
     )
         external
         payable;
+
+    function xDomainMessageSender() external view returns (address);
 }

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

@@ -14,7 +14,11 @@ contract DeploymentSummary is DeploymentSummaryCode {
 
     address internal constant addressManagerAddress = 0xBb2180ebd78ce97360503434eD37fcf4a1Df61c3;
     address internal constant l1CrossDomainMessengerAddress = 0x71fA82Ea96672797954C28032b337aA40AAFC99f;
-    address internal constant l1CrossDomainMessengerProxyAddress = 0x0c8b5822b6e02CDa722174F19A1439A7495a3fA6;
+    address internal constant l1CrossDomainMessengerProxyAddress = 0x20A42a5a785622c6Ba2576B2D6e924aA82BFA11D;
+    address internal constant l1ERC721BridgeAddress = 0x44637A4292E0CD2B17A55d5F6B2F05AFcAcD0586;
+    address internal constant l1ERC721BridgeProxyAddress = 0xDeF3bca8c80064589E6787477FFa7Dd616B5574F;
+    address internal constant l1StandardBridgeAddress = 0x0Da314776B267D898dEE57F6Ede357ae28b3b83c;
+    address internal constant l1StandardBridgeProxyAddress = 0x0c8b5822b6e02CDa722174F19A1439A7495a3fA6;
     address internal constant l2OutputOracleAddress = 0x19652082F846171168Daf378C4fD3ee85a0D4A60;
     address internal constant l2OutputOracleProxyAddress = 0x8B71b41D4dBEb2b6821d44692d3fACAAf77480Bb;
     address internal constant optimismPortalAddress = 0x8887E7568E81405c4E0D4cAaabdda949e3B9d4E4;
@@ -156,13 +160,21 @@ contract DeploymentSummary is DeploymentSummaryCode {
         slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
         value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
         vm.store(systemConfigProxyAddress, slot, value);
+        vm.etch(l1StandardBridgeProxyAddress, l1StandardBridgeProxyCode);
+        slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
         vm.etch(l1CrossDomainMessengerProxyAddress, l1CrossDomainMessengerProxyCode);
-        slot = hex"a8f0d50211ac8ff1a40793a899dff3ced4762e0466f69b0078ab7b00d037835c";
+        slot = hex"540cf4e2f45b866b44f44bde51e109474016dc46a0670fbe1684ad8eaf90fdc3";
         value = hex"000000000000000000000000bb2180ebd78ce97360503434ed37fcf4a1df61c3";
         vm.store(l1CrossDomainMessengerProxyAddress, slot, value);
-        slot = hex"eae32376463217751b8fa4dea8c38ab253664fa3605de6d85d2e790aa970f2b8";
+        slot = hex"4505be7acf20898edfef2b5289635349881ad9bf4b57316a74e81e2abec2be52";
         value = hex"4f564d5f4c3143726f7373446f6d61696e4d657373656e676572000000000034";
         vm.store(l1CrossDomainMessengerProxyAddress, slot, value);
+        vm.etch(l1ERC721BridgeProxyAddress, l1ERC721BridgeProxyCode);
+        slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
         vm.store(addressManagerAddress, slot, value);
@@ -239,6 +251,32 @@ contract DeploymentSummary is DeploymentSummaryCode {
         slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
         value = hex"0000000000000000000000000000000000000000000000000000000000000001";
         vm.store(systemConfigAddress, slot, value);
+        vm.etch(l1StandardBridgeAddress, l1StandardBridgeCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1StandardBridgeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(l1StandardBridgeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000004";
+        value = hex"0000000000000000000000004200000000000000000000000000000000000010";
+        vm.store(l1StandardBridgeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1StandardBridgeAddress, slot, value);
+        vm.etch(l1ERC721BridgeAddress, l1ERC721BridgeCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1ERC721BridgeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(l1ERC721BridgeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000002";
+        value = hex"0000000000000000000000004200000000000000000000000000000000000014";
+        vm.store(l1ERC721BridgeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1ERC721BridgeAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
         value = hex"0000000000000000000000000000000000000000000000000000000000000003";
         vm.store(systemOwnerSafeAddress, slot, value);
@@ -276,6 +314,12 @@ contract DeploymentSummary is DeploymentSummaryCode {
         value = hex"000000000000000000000000ff00000000000000000000000000000000000000";
         vm.store(systemConfigProxyAddress, slot, value);
         slot = hex"383f291819e6d54073bc9a648251d97421076bdd101933c0c022219ce9580636";
+        value = hex"00000000000000000000000020a42a5a785622c6ba2576b2d6e924aa82bfa11d";
+        vm.store(systemConfigProxyAddress, slot, value);
+        slot = hex"46adcbebc6be8ce551740c29c47c8798210f23f7f4086c41752944352568d5a7";
+        value = hex"000000000000000000000000def3bca8c80064589e6787477ffa7dd616b5574f";
+        vm.store(systemConfigProxyAddress, slot, value);
+        slot = hex"9904ba90dde5696cda05c9e0dab5cbaa0fea005ace4d11218a02ac668dad6376";
         value = hex"0000000000000000000000000c8b5822b6e02cda722174f19a1439a7495a3fa6";
         vm.store(systemConfigProxyAddress, slot, value);
         slot = hex"e52a667f71ec761b9b381c7b76ca9b852adf7e8905da0e0ad49986a0a6871815";
@@ -297,16 +341,70 @@ contract DeploymentSummary is DeploymentSummaryCode {
         value = hex"0000000000000000000000000000000000000000000000000000000000000004";
         vm.store(systemOwnerSafeAddress, slot, value);
         slot = hex"a8f0d50211ac8ff1a40793a899dff3ced4762e0466f69b0078ab7b00d037835c";
-        value = hex"0000000000000000000000000000000000000000000000000000000000000002";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
         vm.store(proxyAdminAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
         value = hex"0000000000000000000000000000000000000000000000000000000000000005";
         vm.store(systemOwnerSafeAddress, slot, value);
-        slot = hex"7cda2d9a7dd1a58982b7fac9315bdc1ed8c92aeb9c22cd8555aaa54972f01ccb";
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"0000000000000000000000000da314776b267d898dee57f6ede357ae28b3b83c";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000032";
+        value = hex"000000000000000000000000deb1e9a6be7baf84208bb6e10ac9f9bbe1d70809";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000003";
+        value = hex"00000000000000000000000020a42a5a785622c6ba2576b2d6e924aa82bfa11d";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000004";
+        value = hex"0000000000000000000000004200000000000000000000000000000000000010";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1StandardBridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000006";
+        vm.store(systemOwnerSafeAddress, slot, value);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"00000000000000000000000044637a4292e0cd2b17a55d5f6b2f05afcacd0586";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000032";
+        value = hex"000000000000000000000000deb1e9a6be7baf84208bb6e10ac9f9bbe1d70809";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        value = hex"00000000000000000000000020a42a5a785622c6ba2576b2d6e924aa82bfa11d";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000002";
+        value = hex"0000000000000000000000004200000000000000000000000000000000000014";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(l1ERC721BridgeProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000007";
+        vm.store(systemOwnerSafeAddress, slot, value);
+        slot = hex"540cf4e2f45b866b44f44bde51e109474016dc46a0670fbe1684ad8eaf90fdc3";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000002";
+        vm.store(proxyAdminAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000008";
+        vm.store(systemOwnerSafeAddress, slot, value);
+        slot = hex"17eb2365d570ef4d1cc4abe9e522ed8632b11233db9c15f3c2c8aa32407b981b";
         value = hex"4f564d5f4c3143726f7373446f6d61696e4d657373656e676572000000000034";
         vm.store(proxyAdminAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
-        value = hex"0000000000000000000000000000000000000000000000000000000000000006";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000009";
         vm.store(systemOwnerSafeAddress, slot, value);
         slot = hex"515216935740e67dfdda5cf8e248ea32b3277787818ab59153061ac875c9385e";
         value = hex"00000000000000000000000071fa82ea96672797954c28032b337aa40aafc99f";
@@ -333,7 +431,7 @@ contract DeploymentSummary is DeploymentSummaryCode {
         value = hex"0000000000000000000000010000000000000000000000000000000000000000";
         vm.store(l1CrossDomainMessengerProxyAddress, slot, value);
         slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
-        value = hex"0000000000000000000000000000000000000000000000000000000000000007";
+        value = hex"000000000000000000000000000000000000000000000000000000000000000a";
         vm.store(systemOwnerSafeAddress, slot, value);
         slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
         value = hex"0000000000000000000000008887e7568e81405c4e0d4caaabdda949e3b9d4e4";

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

@@ -208,13 +208,30 @@ regen=--regen
 # shellcheck disable=SC2034
 regen=
 
+#################################
+# Tests to symbolically execute #
+#################################
+# Missing: OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused
+test_list=( "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
+            "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
+            "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
+            "L1ERC721BridgeKontrol.prove_finalizeBridgeERC21_paused" \
+            "L1CrossDomainMessengerKontrol.prove_relayMessage_paused"
+          )
+tests=""
+for test_name in "${test_list[@]}"; do
+  tests+="--match-test $test_name "
+done
+
 #########################
 # kontrol prove options #
 #########################
 max_depth=1000000
 max_iterations=1000000
 smt_timeout=100000
-workers=2
+max_workers=7 # Set to 7 since the CI machine has 8 CPUs
+# workers is the minimum between max_workers and the length of test_list
+workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]}))
 reinit=--reinit
 reinit=
 break_on_calls=--no-break-on-calls
@@ -227,14 +244,6 @@ use_booster=--use-booster
 # use_booster=
 state_diff="./snapshots/state-diff/Kontrol-Deploy.json"
 
-#########################################
-# List of tests to symbolically execute #
-#########################################
-tests=""
-#tests+="--match-test OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused "
-tests+="--match-test OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused "
-tests+="--match-test L1CrossDomainMessengerKontrol.prove_relayMessage_paused "
-
 #############
 # RUN TESTS #
 #############