feat: create suite for sybolic tests with halmos

* test: setup and 3 properties with symbolic tests

packages/contracts-bedrock/test/invariants/symbolic/MockL2ToL2Messenger.sol

@@ -0,0 +1,101 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.25;
+
+import "src/L2/L2ToL2CrossDomainMessenger.sol";
+import "forge-std/Console.sol";
+
+// TODO: move to another file or import it
+interface ITestL2ToL2CrossDomainMessenger {
+    /// @notice Retrieves the sender of the current cross domain message.
+    /// @return _sender Address of the sender of the current cross domain message.
+    function crossDomainMessageSender() external view returns (address _sender);
+
+    /// @notice Retrieves the source of the current cross domain message.
+    /// @return _source Chain ID of the source of the current cross domain message.
+    function crossDomainMessageSource() external view returns (uint256 _source);
+
+    /// @notice Sends a message to some target address on a destination chain. Note that if the call
+    ///         always reverts, then the message will be unrelayable, and any ETH sent will be
+    ///         permanently locked. The same will occur if the target on the other chain is
+    ///         considered unsafe (see the _isUnsafeTarget() function).
+    /// @param _destination Chain ID of the destination chain.
+    /// @param _target      Target contract or wallet address.
+    /// @param _message     Message to trigger the target address with.
+    function sendMessage(uint256 _destination, address _target, bytes calldata _message) external payable;
+
+    /// @notice Relays a message that was sent by the other CrossDomainMessenger contract. Can only
+    ///         be executed via cross-chain call from the other messenger OR if the message was
+    ///         already received once and is currently being replayed.
+    /// @param _destination Chain ID of the destination chain.
+    /// @param _nonce       Nonce of the message being relayed.
+    /// @param _sender      Address of the user who sent the message.
+    /// @param _source      Chain ID of the source chain.
+    /// @param _target      Address that the message is targeted at.
+    /// @param _message     Message to send to the target.
+    function relayMessage(
+        uint256 _destination,
+        uint256 _source,
+        uint256 _nonce,
+        address _sender,
+        address _target,
+        bytes calldata _message
+    )
+        external
+        payable;
+}
+
+contract MockL2ToL2Messenger is ITestL2ToL2CrossDomainMessenger {
+    uint256 internal messageNonce;
+    address internal currentXDomSender;
+
+    constructor(address _currentXDomSender) {
+        currentXDomSender = _currentXDomSender;
+    }
+
+    // TODO
+    function sendMessage(uint256 _destination, address _target, bytes calldata _message) external payable {
+        console.log(11);
+        if (_destination == block.chainid) revert MessageDestinationSameChain();
+        console.log(22);
+        if (_target == Predeploys.CROSS_L2_INBOX) revert MessageTargetCrossL2Inbox();
+        console.log(33);
+        if (_target == Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER) revert MessageTargetL2ToL2CrossDomainMessenger();
+
+        // bytes memory data = abi.encodeCall(
+        //     L2ToL2CrossDomainMessenger.relayMessage,
+        //     (_destination, block.chainid, ++messageNonce, msg.sender, _target, _message)
+        // );
+        // assembly {
+        //     log0(add(data, 0x20), mload(data))
+        // }
+    }
+
+    function relayMessage(
+        uint256 _destination,
+        uint256 _source,
+        uint256 _nonce,
+        address _sender,
+        address _target,
+        bytes calldata _message
+    )
+        external
+        payable
+    {
+        // _currentXDomSender = msg.sender;
+        // messageNonce++;
+        // TODO: Add more logic? Like replacing the `TSTORE` updates with `SSTORE` - or add the checks
+
+        (bool succ, bytes memory ret) = _target.call{ value: msg.value }(_message);
+
+        if (!succ) revert(string(ret));
+    }
+
+    // TODO
+    function crossDomainMessageSource() external view returns (uint256 _source) {
+        _source = block.chainid;
+    }
+
+    function crossDomainMessageSender() external view returns (address _sender) {
+        _sender = currentXDomSender;
+    }
+}

packages/contracts-bedrock/test/invariants/symbolic/OptimismSuperchainERC20.t.sol

@@ -0,0 +1,177 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.25;
+
+import { Test } from "forge-std/Test.sol";
+import "forge-std/Test.sol";
+
+import "src/L2/OptimismSuperchainERC20.sol";
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { SymTest } from "halmos-cheatcodes/src/SymTest.sol";
+import { L2ToL2CrossDomainMessenger } from "src/L2/L2ToL2CrossDomainMessenger.sol";
+import { Predeploys } from "src/libraries/Predeploys.sol";
+import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol";
+import { MockL2ToL2Messenger } from "./MockL2ToL2Messenger.sol";
+import "src/L2/L2ToL2CrossDomainMessenger.sol";
+
+interface IHevm {
+    function chaind(uint256) external;
+
+    function etch(address addr, bytes calldata code) external;
+
+    function prank(address addr) external;
+
+    function deal(address, uint256) external;
+
+    function deal(address, address, uint256) external;
+}
+
+contract HalmosTest is SymTest, Test { }
+
+contract OptimismSuperchainERC20_SymTest is HalmosTest {
+    IHevm hevm = IHevm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+
+    address internal remoteToken = address(bytes20(keccak256("remoteToken")));
+    string internal name = "SuperchainERC20";
+    string internal symbol = "SUPER";
+    uint8 internal decimals = 18;
+    address internal user = address(bytes20(keccak256("user")));
+
+    OptimismSuperchainERC20 public superchainERC20Impl;
+    OptimismSuperchainERC20 internal optimismSuperchainERC20;
+
+    constructor() {
+        superchainERC20Impl = new OptimismSuperchainERC20();
+        optimismSuperchainERC20 = OptimismSuperchainERC20(
+            address(
+                new ERC1967Proxy(
+                    address(superchainERC20Impl),
+                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
+                )
+            )
+        );
+
+        // Etch the mocked L2 to L2 Messenger because the `TSTORE` opcode is not supported, and also due to issues with
+        // `encodeVersionedNonce()`
+        address _mockL2ToL2CrossDomainMessenger = address(new MockL2ToL2Messenger(address(optimismSuperchainERC20)));
+        hevm.etch(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, _mockL2ToL2CrossDomainMessenger.code);
+    }
+
+    function check_setup() public view {
+        assert(optimismSuperchainERC20.remoteToken() == remoteToken);
+        assert(keccak256(abi.encode(optimismSuperchainERC20.name())) == keccak256(abi.encode(name)));
+        assert(keccak256(abi.encode(optimismSuperchainERC20.symbol())) == keccak256(abi.encode(symbol)));
+        assert(optimismSuperchainERC20.decimals() == decimals);
+    }
+
+    // TODO: Update/discuss property
+    // Increases the total supply on the amount minted by the bridge
+    function check_mint(address _to, uint256 _amount) public {
+        vm.assume(_to != address(0));
+
+        uint256 _totalSupplyBef = optimismSuperchainERC20.totalSupply();
+        uint256 _balanceBef = optimismSuperchainERC20.balanceOf(_to);
+
+        vm.startPrank(Predeploys.L2_STANDARD_BRIDGE);
+        optimismSuperchainERC20.mint(_to, _amount);
+
+        assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBef + _amount);
+        assert(optimismSuperchainERC20.balanceOf(_to) == _balanceBef + _amount);
+    }
+
+    /// @custom:property-id 8
+    /// @custom:property SendERC20 with a value of zero does not modify accounting
+    function check_sendERC20ZeroCall(address _to, uint256 _chainId) public {
+        /* Precondition */
+        // The current chain id is 1
+        vm.assume(_to != address(0));
+        vm.assume(_chainId != 1);
+        vm.assume(
+            _to != address(Predeploys.CROSS_L2_INBOX) && _to != address(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER)
+        );
+
+        uint256 _totalSupplyBef = optimismSuperchainERC20.totalSupply();
+
+        /* Action */
+        vm.startPrank(user);
+        optimismSuperchainERC20.sendERC20(_to, 0, _chainId);
+
+        /* Action */
+        assert(_totalSupplyBef == optimismSuperchainERC20.totalSupply());
+    }
+
+    /// @custom:property-id 6
+    /// @custom:property-id Calls to sendERC20 succeed as long as caller has enough balance
+    function check_sendERC20SucceedsOnlyIfEnoughBalance(
+        uint256 _balance,
+        uint256 _amount,
+        address _to,
+        uint256 _chainId
+    )
+        public
+    {
+        vm.assume(_chainId != 1);
+        vm.assume(_to != address(0));
+
+        // Can't use symbolic value for user since it fails due to `NotConcreteError`
+        // hevm.deal(address(optimismSuperchainERC20), user, _balance);
+        vm.prank(Predeploys.L2_STANDARD_BRIDGE);
+        optimismSuperchainERC20.mint(user, _balance);
+
+        /* Action */
+        vm.prank(user);
+        try optimismSuperchainERC20.sendERC20(_to, _amount, _chainId) {
+            /* Postcondition */
+            assert(_balance >= _amount);
+        } catch {
+            assert(_balance < _amount);
+        }
+    }
+
+    // TODO: reverts as expected when the caller is not the messenger, but the test fails. With forge it passes
+    /// @custom:property-id 7
+    /// @custom:property-id Calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    function check_relayERC20OnlyFromL2ToL2Messenger(
+        address _sender,
+        address _from,
+        address _to,
+        uint256 _amount
+    )
+        public
+    {
+        vm.assume(_to != address(0));
+
+        vm.prank(_sender);
+        try optimismSuperchainERC20.relayERC20(_from, _to, _amount) {
+            console.log(7);
+            assert(_sender == Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+        } catch {
+            console.log(8);
+            console.log(_sender);
+            // The error is indeed the expected one, but the test fails
+            assert(_sender != Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+        }
+    }
+
+    // TODO: reverts as expected when the caller is not the messenger, but the test fails. With forge it passes
+    /// @custom:property-id 7
+    /// @custom:property-id Calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    function test_relayERC20OnlyFromL2ToL2Messenger(
+        address _sender,
+        address _from,
+        address _to,
+        uint256 _amount
+    )
+        public
+    {
+        vm.assume(_to != address(0));
+
+        vm.startPrank(_sender);
+        try optimismSuperchainERC20.relayERC20(_from, _to, _amount) {
+            console.log(7);
+            assert(_sender == Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+        } catch (bytes memory _err) {
+            // The error is indeed the expected one, but the test fails
+            assert(_sender != Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+        }
+    }
+}