Add Kontrol proof `prove_relayMessage_paused` (#9156)

* `KontrolDeployment`: deploy `L1CrossDomainMessenger`

* KontrolInterfaces: add `IL1CrossDomainMessenger`

* Add deployment summary tests for `L1CrossDomainMessenger`

* Add `prove_relayMessage_paused`

* `run-kontrol.sh`: add `prove_relayMessage_paused`

* `run-kontrol.sh`: correct help message to install right kontrol version

* Bump Kontrol version from `0.1.121` to `0.1.127`

* `forge fmt`

* Update `Kontrol-Deploy.json`

* `README.md`: Add `L1CrossDomainMessenger.k.sol` documentation

* Fix typos

* Make autogenerated address names start with lowercase

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

@@ -25,7 +25,9 @@ contract L1CrossDomainMessenger_Test is Bridge_Initializer {
     uint256 constant senderSlotIndex = 50;
 
     /// @dev Tests that the implementation is initialized correctly.
-    function test_constructor_succeeds() external {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_constructor_succeeds() external virtual {
         L1CrossDomainMessenger impl = L1CrossDomainMessenger(deploy.mustGetAddress("L1CrossDomainMessenger"));
         assertEq(address(impl.superchainConfig()), address(0));
         assertEq(address(impl.PORTAL()), address(0));
@@ -110,7 +112,9 @@ contract L1CrossDomainMessenger_Test is Bridge_Initializer {
 
     /// @dev Tests that the relayMessage function reverts when
     ///      the message version is not 0 or 1.
-    function test_relayMessage_v2_reverts() external {
+    /// @notice Marked virtual to be overridden in
+    ///         test/kontrol/deployment/DeploymentSummary.t.sol
+    function test_relayMessage_v2_reverts() external virtual {
         address target = address(0xabcd);
         address sender = Predeploys.L2_CROSS_DOMAIN_MESSENGER;
 

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

@@ -15,6 +15,7 @@ test/kontrol
 ├── proofs
 │   ├── interfaces
 │   │   └── KontrolInterfaces.sol
+│   ├── L1CrossDomainMessenger.k.sol
 │   ├── OptimismPortal.k.sol
 │   └── utils
 │       ├── DeploymentSummaryCode.sol
@@ -43,9 +44,10 @@ test/kontrol
 
 ### [`proofs`](./proofs) folder
 
-- [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol): Symbolic property tests
+- [`L1CrossDomainMessenger.k.sol`](./proofs/L1CrossDomainMessenger.k.sol): Symbolic property tests for [`L1CrossDomainMessenger`](../../src/L1/L1CrossDomainMessenger.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): Dependencies for `OptimismPortal.k.sol`, including the summary contracts
+- [`utils`](./proofs/utils): Proof dependencies, including the summary contracts
 
 ### [`scripts`](./scripts) folder
 

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

@@ -3,17 +3,20 @@ pragma solidity 0.8.15;
 
 // Libraries
 import { Constants } from "src/libraries/Constants.sol";
+import { Predeploys } from "src/libraries/Predeploys.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 { L1CrossDomainMessenger } from "src/L1/L1CrossDomainMessenger.sol";
 import { DeploymentSummary } from "../proofs/utils/DeploymentSummary.sol";
 import { OptimismPortal_Test } from "test/L1/OptimismPortal.t.sol";
+import { L1CrossDomainMessenger_Test } from "test/L1/L1CrossDomainMessenger.t.sol";
 
 /// @dev Contract testing the deployment summary correctness
-contract DeploymentSummary_Test is DeploymentSummary, OptimismPortal_Test {
+contract DeploymentSummary_TestOptimismPortal is DeploymentSummary, OptimismPortal_Test {
     /// @notice super.setUp is not called on purpose
     function setUp() public override {
         // Recreate Deployment Summary state changes
@@ -21,10 +24,10 @@ contract DeploymentSummary_Test is DeploymentSummary, OptimismPortal_Test {
         deploymentSummary.recreateDeployment();
 
         // Set summary addresses
-        optimismPortal = OptimismPortal(payable(OptimismPortalProxyAddress));
-        superchainConfig = SuperchainConfig(SuperchainConfigProxyAddress);
-        l2OutputOracle = L2OutputOracle(L2OutputOracleProxyAddress);
-        systemConfig = SystemConfig(SystemConfigProxyAddress);
+        optimismPortal = OptimismPortal(payable(optimismPortalProxyAddress));
+        superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
+        l2OutputOracle = L2OutputOracle(l2OutputOracleProxyAddress);
+        systemConfig = SystemConfig(systemConfigProxyAddress);
 
         // Set up utilized addresses
         depositor = makeAddr("depositor");
@@ -39,7 +42,7 @@ contract DeploymentSummary_Test is DeploymentSummary, OptimismPortal_Test {
     ///      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));
+        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));
@@ -73,3 +76,42 @@ contract DeploymentSummary_Test is DeploymentSummary, OptimismPortal_Test {
     ///         the L2OutputOracle, which is needed in this test
     function test_isOutputFinalized_succeeds() external override { }
 }
+
+contract DeploymentSummary_TestL1CrossDomainMessenger is DeploymentSummary, L1CrossDomainMessenger_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);
+
+        // Set up utilized addresses
+        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 {
+        // L1CrossDomainMessenger impl = L1CrossDomainMessenger(deploy.mustGetAddress("L1CrossDomainMessenger"));
+        L1CrossDomainMessenger impl = L1CrossDomainMessenger(l1CrossDomainMessengerAddress);
+        assertEq(address(impl.superchainConfig()), address(0));
+        assertEq(address(impl.PORTAL()), address(0));
+        assertEq(address(impl.portal()), address(0));
+        assertEq(address(impl.OTHER_MESSENGER()), Predeploys.L2_CROSS_DOMAIN_MESSENGER);
+        assertEq(address(impl.otherMessenger()), Predeploys.L2_CROSS_DOMAIN_MESSENGER);
+    }
+
+    /// @notice This test is overridden because `KontrolDeployment` doesn't deploy
+    ///         L2CrossDomainMessenger, which is needed in this test
+    function test_relayMessage_v2_reverts() external override { }
+}

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

@@ -12,15 +12,18 @@ contract KontrolDeployment is Deploy {
         deployERC1967Proxy("OptimismPortalProxy");
         deployERC1967Proxy("L2OutputOracleProxy");
         deployERC1967Proxy("SystemConfigProxy");
+        deployL1CrossDomainMessengerProxy();
         transferAddressManagerOwnership(); // to the ProxyAdmin
 
         // deployImplementations();
         deployOptimismPortal();
+        deployL1CrossDomainMessenger();
         deployL2OutputOracle();
         deploySystemConfig();
 
         // initializeImplementations();
         initializeSystemConfig();
+        initializeL1CrossDomainMessenger();
         initializeOptimismPortal();
     }
 }

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 { KontrolUtils } from "./utils/KontrolUtils.sol";
+import {
+    IL1CrossDomainMessenger as L1CrossDomainMessenger,
+    ISuperchainConfig as SuperchainConfig
+} from "./interfaces/KontrolInterfaces.sol";
+
+contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
+    L1CrossDomainMessenger l1CrossDomainMessenger;
+    SuperchainConfig superchainConfig;
+
+    /// @dev Inlined setUp function for faster Kontrol performance
+    ///      Tracking issue: https://github.com/runtimeverification/kontrol/issues/282
+    function setUpInlined() public {
+        l1CrossDomainMessenger = L1CrossDomainMessenger(l1CrossDomainMessengerProxyAddress);
+        superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
+    }
+
+    /// TODO: Replace struct parameters and workarounds with the appropriate
+    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
+    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
+    function prove_relayMessage_paused(
+        uint256 _nonce,
+        address _sender,
+        address _target,
+        uint256 _value,
+        uint256 _gas
+    )
+        external
+    {
+        setUpInlined();
+
+        bytes memory _message = freshBigBytes(600);
+
+        // Pause System
+        vm.prank(superchainConfig.guardian());
+        superchainConfig.pause("identifier");
+
+        vm.expectRevert("CrossDomainMessenger: paused");
+        l1CrossDomainMessenger.relayMessage(_nonce, _sender, _target, _value, _gas, _message);
+    }
+}

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

@@ -16,8 +16,8 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
     /// @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);
+        optimismPortal = OptimismPortal(payable(optimismPortalProxyAddress));
+        superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
     }
 
     /// TODO: Replace struct parameters and workarounds with the appropriate
@@ -59,7 +59,7 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
         optimismPortal.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
     }
 
-    /// TODO: Replace struct parameters and workarounds with the appropiate
+    /// TODO: Replace struct parameters and workarounds with the appropriate
     /// types once Kontrol supports symbolic `bytes` and `bytes[]`
     /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
     function prove_finalizeWithdrawalTransaction_paused(

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

@@ -30,3 +30,18 @@ interface ISuperchainConfig {
 
     function unpause() external;
 }
+
+interface IL1CrossDomainMessenger {
+    function paused() external view returns (bool);
+
+    function relayMessage(
+        uint256 _nonce,
+        address _sender,
+        address _target,
+        uint256 _value,
+        uint256 _minGasLimit,
+        bytes calldata _message
+    )
+        external
+        payable;
+}

packages/contracts-bedrock/test/kontrol/scripts/json/reverse_key_values.py

@@ -19,7 +19,7 @@ def reverse_json(input_file, output_file):
         with open(input_file, 'r') as file:
             json_data = json.load(file)
 
-        reversed_json = {str(value): key for key, value in json_data.items()}
+        reversed_json = {str(value): key[0].lower() + key[1:] for key, value in json_data.items()}
 
         with open(output_file, 'w') as file:
             json.dump(reversed_json, file, indent=2)

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

@@ -58,7 +58,7 @@ else
       pushd "${WORKSPACE_DIR}" > /dev/null
     else
       notif "Kontrol version does NOT match ${KONTROLRC}"
-      notif "Please run 'kup install kontrol --version ${KONTROLRC}'"
+      notif "Please run 'kup install kontrol --version v${KONTROLRC}'"
       blank_line
       exit 1
     fi
@@ -214,7 +214,7 @@ regen=
 max_depth=1000000
 max_iterations=1000000
 smt_timeout=100000
-workers=1
+workers=2
 reinit=--reinit
 reinit=
 break_on_calls=--no-break-on-calls
@@ -233,6 +233,7 @@ state_diff="./snapshots/state-diff/Kontrol-Deploy.json"
 tests=""
 #tests+="--match-test OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused "
 tests+="--match-test OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused "
+tests+="--match-test L1CrossDomainMessengerKontrol.prove_relayMessage_paused "
 
 #############
 # RUN TESTS #

versions.json

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