From c8ccdc7b0c03c03228a9edaf48cf6bfc8c3f5281 Mon Sep 17 00:00:00 2001 From: 0xDiscotech <131301107+0xDiscotech@users.noreply.github.com> Date: Wed, 14 Aug 2024 02:46:32 -0300 Subject: [PATCH] feat: create suite for sybolic tests with halmos * test: setup and 3 properties with symbolic tests --- .../symbolic/MockL2ToL2Messenger.sol | 101 ++++++++++ .../symbolic/OptimismSuperchainERC20.t.sol | 177 ++++++++++++++++++ 2 files changed, 278 insertions(+) create mode 100644 packages/contracts-bedrock/test/invariants/symbolic/MockL2ToL2Messenger.sol create mode 100644 packages/contracts-bedrock/test/invariants/symbolic/OptimismSuperchainERC20.t.sol diff --git a/packages/contracts-bedrock/test/invariants/symbolic/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/invariants/symbolic/MockL2ToL2Messenger.sol new file mode 100644 index 000000000000..905f38b464f4 --- /dev/null +++ b/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; + } +} diff --git a/packages/contracts-bedrock/test/invariants/symbolic/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/symbolic/OptimismSuperchainERC20.t.sol new file mode 100644 index 000000000000..c3c5572da2e7 --- /dev/null +++ b/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); + } + } +}