Final version for Kontrol pausability proofs

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

@@ -19,25 +19,18 @@ contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
         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
+        uint256 _gas,
+        bytes calldata _message
     )
         external
     {
         setUpInlined();
 
-        // ASSUME: Conservative upper bound on the `_message` length. Most contract calls will have
-        // a message length less than 600 bytes. This assumption can be removed once Kontrol
-        // supports symbolic `bytes`: https://github.com/runtimeverification/kontrol/issues/272
-        bytes memory _message = freshBigBytes(600);
-
         // Pause System
         vm.prank(superchainConfig.guardian());
         superchainConfig.pause("identifier");

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

@@ -6,6 +6,7 @@ import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { Types } from "src/libraries/Types.sol";
 import {
     IL1ERC721Bridge as L1ERC721Bridge,
+    IL1CrossDomainMessenger as CrossDomainMessenger,
     ISuperchainConfig as SuperchainConfig
 } from "./interfaces/KontrolInterfaces.sol";
 
@@ -18,43 +19,30 @@ contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
         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_finalizeBridgeERC721_paused(
         address _localToken,
         address _remoteToken,
         address _from,
         address _to,
-        uint256 _amount
+        uint256 _amount,
+        bytes calldata _extraData
     )
         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, since extra data is optional
-        // for convenience of off-chain tooling. This assumption can be removed once Kontrol
-        // supports symbolic `bytes`: https://github.com/runtimeverification/kontrol/issues/272
-        bytes memory _extraData = freshBigBytes(64);
-
         // 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.mockCall(
+            address(l1ERC721Bridge.messenger()),
+            abi.encodeWithSelector(CrossDomainMessenger.xDomainMessageSender.selector),
+            abi.encode(address(l1ERC721Bridge.otherBridge()))
+        );
+
+        vm.prank(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

@@ -6,6 +6,7 @@ import { KontrolUtils } from "./utils/KontrolUtils.sol";
 import { Types } from "src/libraries/Types.sol";
 import {
     IL1StandardBridge as L1StandardBridge,
+    IL1CrossDomainMessenger as CrossDomainMessenger,
     ISuperchainConfig as SuperchainConfig
 } from "./interfaces/KontrolInterfaces.sol";
 
@@ -18,77 +19,55 @@ contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
         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
+        uint256 _amount,
+        bytes calldata _extraData
     )
         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: Upper bound on the `_extraData` length, since extra data is optional for
-        // for convenience of off-chain tooling, and should not affect execution  This assumption
-        // can be removed once Kontrol supports symbolic `bytes`:
-        // https://github.com/runtimeverification/kontrol/issues/272
-        bytes memory _extraData = freshBigBytes(32);
-
         // 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.mockCall(
+            address(l1standardBridge.messenger()),
+            abi.encodeWithSelector(CrossDomainMessenger.xDomainMessageSender.selector),
+            abi.encode(address(l1standardBridge.otherBridge()))
+        );
+
+        vm.prank(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 {
+    function prove_finalizeBridgeETH_paused(
+        address _from,
+        address _to,
+        uint256 _amount,
+        bytes calldata _extraData
+    )
+        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: Upper bound on the `_extraData` length, since extra data is optional for
-        // for convenience of off-chain tooling, and should not affect execution  This assumption
-        // can be removed once Kontrol supports symbolic `bytes`:
-        // https://github.com/runtimeverification/kontrol/issues/272
-        bytes memory _extraData = freshBigBytes(32);
-
         // 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.mockCall(
+            address(l1standardBridge.messenger()),
+            abi.encodeWithSelector(CrossDomainMessenger.xDomainMessageSender.selector),
+            abi.encode(address(l1standardBridge.otherBridge()))
+        );
+
+        vm.prank(address(l1standardBridge.messenger()));
         vm.expectRevert("StandardBridge: paused");
         l1standardBridge.finalizeBridgeETH(_from, _to, _amount, _extraData);
-        vm.stopPrank();
     }
 }

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

@@ -20,78 +20,35 @@ contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
         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
+    /// @custom:kontrol-length-equals _withdrawalProof: 10,
+    /// @custom:kontrol-length-equals _withdrawalProof[]: 600,
+    /// @custom:kontrol-length-equals data: 1000,
     function prove_proveWithdrawalTransaction_paused(
-        // WithdrawalTransaction args
-        uint256 _nonce,
-        address _sender,
-        address _target,
-        uint256 _value,
-        uint256 _gasLimit,
-        // bytes   memory _data,
+        Types.WithdrawalTransaction memory _tx,
         uint256 _l2OutputIndex,
-        // OutputRootProof args
-        bytes32 _outputRootProof0,
-        bytes32 _outputRootProof1,
-        bytes32 _outputRootProof2,
-        bytes32 _outputRootProof3
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
     )
         external
     {
         setUpInlined();
 
-        // ASSUME: This bound on the `_data` length is too low, and should be at least 1000 bytes.
-        // Kontrol currently hangs and fails with this value because of the resulting configuration
-        // size. For now we leave this as a low value to avoid the hang, but it should be increased
-        // once Kontrol is improved and supports symbolic `bytes`:
-        // https://github.com/runtimeverification/kontrol/issues/272
-        bytes memory _data = freshBigBytes(320);
-        bytes[] memory _withdrawalProof = freshWithdrawalProof();
-
-        Types.WithdrawalTransaction memory _tx =
-            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data);
-        Types.OutputRootProof memory _outputRootProof =
-            Types.OutputRootProof(_outputRootProof0, _outputRootProof1, _outputRootProof2, _outputRootProof3);
-
         // Pause Optimism Portal
         vm.prank(optimismPortal.guardian());
         superchainConfig.pause("identifier");
 
-        // No one can call proveWithdrawalTransaction
         vm.expectRevert("OptimismPortal: paused");
         optimismPortal.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
     }
 
-    /// 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(
-        uint256 _nonce,
-        address _sender,
-        address _target,
-        uint256 _value,
-        uint256 _gasLimit
-    )
-        external
-    {
+    function prove_finalizeWithdrawalTransaction_paused(Types.WithdrawalTransaction calldata _tx) external {
         setUpInlined();
 
-        // ASSUME: This bound on the `_data` length is too low, and should be at least 1000 bytes.
-        // Kontrol currently hangs and fails with this value because of the resulting configuration
-        // size. For now we leave this as a low value to avoid the hang, but it should be increased
-        // once Kontrol is improved and supports symbolic `bytes`:
-        // https://github.com/runtimeverification/kontrol/issues/272
-        bytes memory _data = freshBigBytes(320);
-
         // Pause Optimism Portal
         vm.prank(optimismPortal.guardian());
         superchainConfig.pause("identifier");
 
         vm.expectRevert("OptimismPortal: paused");
-        optimismPortal.finalizeWithdrawalTransaction(
-            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data)
-        );
+        optimismPortal.finalizeWithdrawalTransaction(_tx);
     }
 }

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

@@ -4,78 +4,7 @@ pragma solidity 0.8.15;
 import { Vm } from "forge-std/Vm.sol";
 import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol";
 
-// The GhostBytes contracts are a workaround to create a symbolic bytes array. This is slow, but
-// required until symbolic bytes are supported in Kontrol: https://github.com/runtimeverification/kontrol/issues/272
-contract GhostBytes {
-    bytes public ghostBytes;
-}
-
-contract GhostBytes10 {
-    bytes public ghostBytes0;
-    bytes public ghostBytes1;
-    bytes public ghostBytes2;
-    bytes public ghostBytes3;
-    bytes public ghostBytes4;
-    bytes public ghostBytes5;
-    bytes public ghostBytes6;
-    bytes public ghostBytes7;
-    bytes public ghostBytes8;
-    bytes public ghostBytes9;
-
-    function getGhostBytesArray() public view returns (bytes[] memory _arr) {
-        _arr = new bytes[](10);
-        _arr[0] = ghostBytes0;
-        _arr[1] = ghostBytes1;
-        _arr[2] = ghostBytes2;
-        _arr[3] = ghostBytes3;
-        _arr[4] = ghostBytes4;
-        _arr[5] = ghostBytes5;
-        _arr[6] = ghostBytes6;
-        _arr[7] = ghostBytes7;
-        _arr[8] = ghostBytes8;
-        _arr[9] = ghostBytes9;
-    }
-}
-
 /// @notice Tests inheriting this contract cannot be run with forge
 abstract contract KontrolUtils is KontrolCheats {
     Vm internal constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code")))));
-
-    /// @dev Creates a fresh bytes with length greater than 31
-    /// @param bytesLength: Length of the fresh bytes. Should be concrete
-    function freshBigBytes(uint256 bytesLength) internal returns (bytes memory sBytes) {
-        require(bytesLength >= 32, "Small bytes");
-
-        uint256 bytesSlotValue;
-        unchecked {
-            bytesSlotValue = bytesLength * 2 + 1;
-        }
-
-        // Deploy ghost contract
-        GhostBytes ghostBytes = new GhostBytes();
-
-        // Make the storage of the ghost contract symbolic
-        kevm.symbolicStorage(address(ghostBytes));
-
-        // Load the size encoding into the first slot of ghostBytes
-        vm.store(address(ghostBytes), bytes32(uint256(0)), bytes32(bytesSlotValue));
-
-        sBytes = ghostBytes.ghostBytes();
-    }
-
-    /// @dev Creates a bounded symbolic bytes[] memory representing a withdrawal proof.
-    function freshWithdrawalProof() public returns (bytes[] memory withdrawalProof) {
-        // ASSUME: Withdrawal proofs do not currently exceed 6 elements in length. This can be
-        // shrank to 2 for faster proof speeds during testing and development.
-        // TODO: Allow the array length range between 0 and 10 elements. This can be done once
-        // symbolic bytes are supported in Kontrol: https://github.com/runtimeverification/kontrol/issues/272
-        uint256 arrayLength = 6;
-        withdrawalProof = new bytes[](arrayLength);
-
-        for (uint256 i = 0; i < withdrawalProof.length; ++i) {
-            // ASSUME: Each element is 600 bytes. Proof elements are 17 * 32 = 544 bytes long, plus
-            // ~10% margin for RLP encoding:, giving us the 600 byte assumption.
-            withdrawalProof[i] = freshBigBytes(600);
-        }
-    }
 }

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

@@ -105,8 +105,8 @@ regen=
 #################################
 # Tests to symbolically execute #
 #################################
-# Missing: OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused
-test_list=( "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
+test_list=( "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused" \
+            "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
             "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
             "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
             "L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused" \
@@ -120,8 +120,8 @@ done
 #########################
 # kontrol prove options #
 #########################
-max_depth=1000000
-max_iterations=1000000
+max_depth=10000
+max_iterations=10000
 smt_timeout=100000
 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
@@ -131,7 +131,7 @@ reinit=
 break_on_calls=--no-break-on-calls
 # break_on_calls=
 auto_abstract=--auto-abstract-gas
-# auto_abstract=
+auto_abstract=
 bug_report=--bug-report
 bug_report=
 use_booster=--use-booster