test: fuzz non atomic bridging (#31)

* test: changed mocked messenger ABI for message sending but kept assertions the same

* docs: add new properties 26&27

* test: queue cross-chain messages and test related properties

* test: relay random messages from queue and check associated invariants

* chore: rename bridge->senderc20 method for consistency with relayerc20

* test: not-yet-deployed supertokens can get funds sent to them

* chore: medusa runs forever by default

doable since it also handles SIGINTs gracefully

* chore: document the reason behind relay zero and send zero inconsistencies

* fix: feedback from doc

* fix: walk around possible medusa issue

I'm getting an 'unknown opcode 0x4e' in ProtocolAtomic constructor when
calling the MockL2ToL2CrossDomainMessenger for the first time

* test: unguided handler for sendERC20

* fix: feedback from disco

packages/contracts-bedrock/foundry.toml

@@ -103,6 +103,7 @@ script = 'test/kontrol/proofs'
 src = 'test/properties/medusa/'
 test = 'test/properties/medusa/'
 script = 'test/properties/medusa/'
+via-ir=true
 
 [profile.halmos]
 src = 'test/properties/halmos/'

packages/contracts-bedrock/medusa.json

@@ -3,7 +3,7 @@
 		"workers": 10,
 		"workerResetLimit": 50,
 		"timeout": 0,
-		"testLimit": 500000,
+		"testLimit": 0,
 		"callSequenceLength": 100,
 		"corpusDirectory": "test/properties/medusa/corpus/",
 		"coverageEnabled": true,

packages/contracts-bedrock/test/properties/PROPERTIES.md

@@ -86,7 +86,9 @@ legend:
 | --- | ---                 | ---                                                                                               | ---    | ---    |
 | 8   | SupERC20            | sendERC20 with a value of zero does not modify accounting                                         | [x]    | [x]    |
 | 9   | SupERC20            | relayERC20 with a value of zero does not modify accounting                                        | [x]    | [x]    |
-| 10  | SupERC20            | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount       | [x]    | [ ]    |
+| 10  | SupERC20            | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount       | [x]    | [x]    |
+| 26  | SupERC20            | sendERC20 decreases the sender's balance in the source chain exactly by the input amount          | [ ]    | [x]    |
+| 27  | SupERC20            | relayERC20 increases sender's balance in the destination chain exactly by the input amount        | [ ]    | [x]    |
 | 11  | SupERC20            | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x]    | [ ]    |
 | 12  | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge             | [x]    | [~]    |
 | 13  | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge             | [x]    | [ ]    |
@@ -100,9 +102,9 @@ legend:
 | --- | ---                 | ---                                                                                                                                                                   | ---    | ---    |
 | 17  | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s  total supply across chains                                                                          | [ ]    | [ ]    |
 | 18  | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s  total supply across chains                                                                          | [ ]    | [ ]    |
-| 19  | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)                                                       | [ ]    | [ ]    |
+| 19  | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)                                                       | [ ]    | [~]    |
 | 20  | SupERC20            | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ]    | [ ]    |
-| 21  | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed                   | [ ]    | [ ]    |
+| 21  | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed                   | [ ]    | [~]    |
 
 ## Atomic bridging pseudo-properties
 

packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol

@@ -5,6 +5,17 @@ import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { SafeCall } from "src/libraries/SafeCall.sol";
 
 contract MockL2ToL2CrossDomainMessenger {
+    ////////////////////////
+    //  type definitions  //
+    ////////////////////////
+    struct CrossChainMessage {
+        address crossDomainMessageSender;
+        address crossDomainMessageSource;
+        bytes payload;
+        address recipient;
+        uint256 amount;
+    }
+
     /////////////////////////////////////////////////////////
     //  State vars mocking the L2toL2CrossDomainMessenger  //
     /////////////////////////////////////////////////////////
@@ -17,6 +28,13 @@ contract MockL2ToL2CrossDomainMessenger {
     mapping(address supertoken => bytes32 deploySalt) public superTokenInitDeploySalts;
     mapping(uint256 chainId => mapping(bytes32 deploySalt => address supertoken)) public superTokenAddresses;
 
+    CrossChainMessage[] private _messageQueue;
+    bool private _atomic;
+
+    function messageQueue(uint256 rawIndex) external view returns (CrossChainMessage memory) {
+        return _messageQueue[rawIndex % _messageQueue.length];
+    }
+
     function crossChainMessageReceiver(
         address sender,
         uint256 destinationChainId
@@ -37,22 +55,64 @@ contract MockL2ToL2CrossDomainMessenger {
         superTokenInitDeploySalts[token] = deploySalt;
     }
 
+    function messageQueueLength() public view returns (uint256) {
+        return _messageQueue.length;
+    }
+
+    function setAtomic(bool atomic) public {
+        _atomic = atomic;
+    }
+
+    function relayMessageFromQueue(uint256 rawIndex) public {
+        uint256 index = rawIndex % _messageQueue.length;
+        CrossChainMessage memory message = _messageQueue[index];
+        _messageQueue[index] = _messageQueue[_messageQueue.length - 1];
+        _messageQueue.pop();
+        _relayMessage(message);
+    }
+
+    function _relayMessage(CrossChainMessage memory message) internal {
+        crossDomainMessageSender = message.crossDomainMessageSender;
+        crossDomainMessageSource = message.crossDomainMessageSource;
+        SafeCall.call(crossDomainMessageSender, 0, message.payload);
+        crossDomainMessageSender = address(0);
+        crossDomainMessageSource = address(0);
+    }
+
     ////////////////////////////////////////////////////////
     //  Functions mocking the L2toL2CrossDomainMessenger  //
     ////////////////////////////////////////////////////////
 
     /// @notice recipient will not be used since in normal execution it's the same
     /// address on a different chain, but here we have to compute it to mock
     /// cross-chain messaging
-    function sendMessage(uint256 chainId, address, /*recipient*/ bytes memory message) external {
+    function sendMessage(uint256 chainId, address, /*recipient*/ bytes calldata data) external {
         address crossChainRecipient = superTokenAddresses[chainId][superTokenInitDeploySalts[msg.sender]];
         if (crossChainRecipient == msg.sender) {
             require(false, "same chain");
         }
-        crossDomainMessageSender = crossChainRecipient;
-        crossDomainMessageSource = msg.sender;
-        SafeCall.call(crossDomainMessageSender, 0, message);
-        crossDomainMessageSender = address(0);
-        crossDomainMessageSource = address(0);
+        (address recipient, uint256 amount) = _decodePayload(data);
+
+        CrossChainMessage memory message = CrossChainMessage({
+            crossDomainMessageSender: crossChainRecipient,
+            crossDomainMessageSource: msg.sender,
+            payload: data,
+            recipient: recipient,
+            amount: amount
+        });
+
+        if (_atomic) {
+            _relayMessage(message);
+        } else {
+            _messageQueue.push(message);
+        }
+    }
+
+    ////////////////////////
+    //  Internal helpers  //
+    ////////////////////////
+
+    function _decodePayload(bytes calldata payload) internal pure returns (address recipient, uint256 amount) {
+        (, recipient, amount) = abi.decode(payload[4:], (address, address, uint256));
     }
 }

packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol

@@ -1,10 +1,13 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.25;
 
+import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { ProtocolHandler } from "../handlers/Protocol.t.sol";
+import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 
 contract ProtocolGuided is ProtocolHandler {
+    using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
     /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId
     /// @custom:property-id 14
     /// @custom:property supertoken total supply starts at zero
@@ -35,7 +38,7 @@ contract ProtocolGuided is ProtocolHandler {
     /// @custom:property-id 23
     /// @custom:property sendERC20 decreases total supply in source chain and increases it in destination chain exactly
     /// by the input amount
-    function fuzz_bridgeSupertoken(
+    function fuzz_bridgeSupertokenAtomic(
         uint256 fromIndex,
         uint256 recipientIndex,
         uint256 destinationChainId,
@@ -50,16 +53,15 @@ contract ProtocolGuided is ProtocolHandler {
         OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]);
         OptimismSuperchainERC20 destinationToken =
             MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId);
-        // TODO: when implementing non-atomic bridging, allow for the token to
-        // not yet be deployed and funds be recovered afterwards.
-        require(address(destinationToken) != address(0));
         uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor());
         uint256 sourceSupplyBefore = sourceToken.totalSupply();
         uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient);
         uint256 destinationSupplyBefore = destinationToken.totalSupply();
 
+        MESSENGER.setAtomic(true);
         vm.prank(currentActor());
         try sourceToken.sendERC20(recipient, amount, destinationChainId) {
+            MESSENGER.setAtomic(false);
             uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
             uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient);
             // no free mint
@@ -73,14 +75,86 @@ contract ProtocolGuided is ProtocolHandler {
             assert(sourceSupplyBefore - amount == sourceSupplyAfter);
             assert(destinationSupplyBefore + amount == destinationSupplyAfter);
         } catch {
+            MESSENGER.setAtomic(false);
             // 6
             assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }
 
+    /// @custom:property-id 6
+    /// @custom:property calls to sendERC20 succeed as long as caller has enough balance
+    /// @custom:property-id 26
+    /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount
+    /// @custom:property-id 10
+    /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount
+    function fuzz_sendERC20(
+        uint256 fromIndex,
+        uint256 recipientIndex,
+        uint256 destinationChainId,
+        uint256 amount
+    )
+        public
+        withActor(msg.sender)
+    {
+        destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1);
+        fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1);
+        address recipient = getActorByRawIndex(recipientIndex);
+        OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]);
+        OptimismSuperchainERC20 destinationToken =
+            MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId);
+        bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken));
+        uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor());
+        uint256 sourceSupplyBefore = sourceToken.totalSupply();
+
+        vm.prank(currentActor());
+        try sourceToken.sendERC20(recipient, amount, destinationChainId) {
+            (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt);
+            ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount);
+            // 26
+            uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
+            assert(sourceBalanceBefore - amount == sourceBalanceAfter);
+            // 10
+            uint256 sourceSupplyAfter = sourceToken.totalSupply();
+            assert(sourceSupplyBefore - amount == sourceSupplyAfter);
+        } catch {
+            // 6
+            assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
+        }
+    }
+
+    /// @custom:property-id 11
+    /// @custom:property relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount
+    /// @custom:property-id 27
+    /// @custom:property relayERC20 increases sender's balance in the destination chain exactly by the input amount
+    /// @custom:property-id 7
+    /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    function fuzz_relayERC20(uint256 messageIndex) external {
+        MockL2ToL2CrossDomainMessenger.CrossChainMessage memory messageToRelay = MESSENGER.messageQueue(messageIndex);
+        OptimismSuperchainERC20 destinationToken = OptimismSuperchainERC20(messageToRelay.crossDomainMessageSender);
+        uint256 destinationSupplyBefore = destinationToken.totalSupply();
+        uint256 destinationBalanceBefore = destinationToken.balanceOf(messageToRelay.recipient);
+
+        try MESSENGER.relayMessageFromQueue(messageIndex) {
+            bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken));
+            (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt);
+            // if sendERC20 didnt intialize this, then test suite is broken
+            assert(success);
+            ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount);
+            // 11
+            assert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply());
+            // 27
+            assert(
+                destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient)
+            );
+        } catch {
+            // 7
+            assert(false);
+        }
+    }
+
     /// @custom:property-id 8
     /// @custom:property calls to sendERC20 with a value of zero dont modify accounting
-    // @notice is a subset of fuzz_bridgeSupertoken, so we'll just call it
+    // @notice is a subset of fuzz_sendERC20, so we'll just call it
     // instead of re-implementing it. Keeping the function for visibility of the property.
     function fuzz_sendZeroDoesNotModifyAccounting(
         uint256 fromIndex,
@@ -89,13 +163,15 @@ contract ProtocolGuided is ProtocolHandler {
     )
         external
     {
-        fuzz_bridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0);
+        fuzz_sendERC20(fromIndex, recipientIndex, destinationChainId, 0);
     }
 
     /// @custom:property-id 9
     /// @custom:property calls to relayERC20 with a value of zero dont modify accounting
     /// @custom:property-id 7
     /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    /// @notice cant call fuzz_RelayERC20 internally since that pops a
+    /// random message, which we cannot guarantee has a value of zero
     function fuzz_relayZeroDoesNotModifyAccounting(
         uint256 fromIndex,
         uint256 recipientIndex

packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol

@@ -42,6 +42,46 @@ contract ProtocolUnguided is ProtocolHandler {
         }
     }
 
+    /// @custom:property-id 6
+    /// @custom:property calls to sendERC20 succeed as long as caller has enough balance
+    /// @custom:property-id 26
+    /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount
+    /// @custom:property-id 10
+    /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount
+    function fuzz_sendERC20(
+        address sender,
+        address recipient,
+        uint256 fromIndex,
+        uint256 destinationChainId,
+        uint256 amount
+    )
+        public
+    {
+        destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1);
+        OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]);
+        OptimismSuperchainERC20 destinationToken =
+            MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId);
+        bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken));
+        uint256 sourceBalanceBefore = sourceToken.balanceOf(sender);
+        uint256 sourceSupplyBefore = sourceToken.totalSupply();
+
+        vm.prank(sender);
+        try sourceToken.sendERC20(recipient, amount, destinationChainId) {
+            (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt);
+            ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount);
+            // 26
+            uint256 sourceBalanceAfter = sourceToken.balanceOf(sender);
+            assert(sourceBalanceBefore - amount == sourceBalanceAfter);
+            // 10
+            uint256 sourceSupplyAfter = sourceToken.totalSupply();
+            assert(sourceSupplyBefore - amount == sourceSupplyAfter);
+        } catch {
+            // 6
+            assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
+        }
+    }
+
+
     /// @custom:property-id 12
     /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge
     function fuzz_mint(uint256 tokenIndex, address to, address sender, uint256 amount) external {
@@ -52,9 +92,9 @@ contract ProtocolUnguided is ProtocolHandler {
         try OptimismSuperchainERC20(token).mint(to, amount) {
             assert(sender == BRIDGE);
             (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt);
-            ghost_totalSupplyAcrossChains.set(salt, currentValue - amount);
+            ghost_totalSupplyAcrossChains.set(salt, currentValue + amount);
         } catch {
-            assert(sender != BRIDGE);
+            assert(sender != BRIDGE || to == address(0));
         }
     }
 

packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol

@@ -40,6 +40,8 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
 
     /// @notice  'real' deploy salt => total supply sum across chains
     EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains;
+    /// @notice  'real' deploy salt => tokens sendERC20'd but not yet relayERC20'd
+    EnumerableMap.Bytes32ToUintMap internal ghost_tokensInTransit;
 
     constructor() {
         vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code);