test: fuzz properties 8 and 9

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

@@ -82,8 +82,8 @@ legend:
 
 | id  | milestone           | description                                                                                       | halmos | medusa |
 | --- | ---                 | ---                                                                                               | ---    | ---    |
-| 8   | SupERC20            | sendERC20 with a value of zero does not modify accounting                                         | [ ]    | [ ]    |
-| 9   | SupERC20            | relayERC20 with a value of zero does not modify accounting                                        | [ ]    | [ ]    |
+| 8   | SupERC20            | sendERC20 with a value of zero does not modify accounting                                         | [ ]    | [x]    |
+| 9   | SupERC20            | relayERC20 with a value of zero does not modify accounting                                        | [ ]    | [x]    |
 | 10  | SupERC20            | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount       | [ ]    | [ ]    |
 | 11  | SupERC20            | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ]    | [ ]    |
 | 12  | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge             | [ ]    | [~]    |

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

@@ -28,6 +28,10 @@ contract MockL2ToL2CrossDomainMessenger {
         return OptimismSuperchainERC20(superTokenAddresses[destinationChainId][superTokenInitDeploySalts[sender]]);
     }
 
+    function setCrossDomainMessageSender(address sender) external {
+        crossDomainMessageSender = sender;
+    }
+
     function registerSupertoken(bytes32 deploySalt, uint256 chainId, address token) external {
         superTokenAddresses[chainId][deploySalt] = token;
         superTokenInitDeploySalts[token] = deploySalt;
@@ -49,5 +53,6 @@ contract MockL2ToL2CrossDomainMessenger {
         crossDomainMessageSource = msg.sender;
         SafeCall.call(crossDomainMessageSender, 0, message);
         crossDomainMessageSender = address(0);
+        crossDomainMessageSource = address(0);
     }
 }

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

@@ -104,4 +104,71 @@ contract ProtocolProperties is ProtocolHandler {
             assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }
+
+    /// @custom:property-id 8
+    /// @custom:property calls to sendERC20 with a value of zero dont modify accounting
+    // NOTE: should we keep it? will cause the exact same coverage as property_BridgeSupertoken
+    function property_SendZeroDoesNotModifyAccounting(
+        uint256 fromIndex,
+        uint256 recipientIndex,
+        uint256 destinationChainId
+    )
+        external
+        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);
+        // TODO: perhaps the mock should already start ignoring this?
+        require(address(destinationToken) != address(0));
+        uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor());
+        uint256 sourceSupplyBefore = sourceToken.totalSupply();
+        uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient);
+        uint256 destinationSupplyBefore = destinationToken.totalSupply();
+
+        vm.prank(currentActor());
+        try sourceToken.sendERC20(recipient, 0, destinationChainId) {
+            uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
+            uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient);
+            assert(sourceBalanceBefore == sourceBalanceAfter);
+            assert(destinationBalanceBefore == destinationBalanceAfter);
+            uint256 sourceSupplyAfter = sourceToken.totalSupply();
+            uint256 destinationSupplyAfter = destinationToken.totalSupply();
+            assert(sourceSupplyBefore == sourceSupplyAfter);
+            assert(destinationSupplyBefore == destinationSupplyAfter);
+        } catch {
+            assert(address(destinationToken) == address(sourceToken));
+        }
+    }
+
+    /// @custom:property-id 9
+    /// @custom:property calls to relayERC20 with a value of zero dont modify accounting
+    function property_RelayZeroDoesNotModifyAccounting(
+        uint256 fromIndex,
+        uint256 recipientIndex
+    )
+        external
+        withActor(msg.sender)
+    {
+        fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1);
+        address recipient = getActorByRawIndex(recipientIndex);
+        OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]);
+        uint256 balanceBefore = token.balanceOf(currentActor());
+        uint256 supplyBefore = token.totalSupply();
+
+        MESSENGER.setCrossDomainMessageSender(address(token));
+        vm.prank(address(MESSENGER));
+        try token.relayERC20(currentActor(), recipient, 0) {
+            MESSENGER.setCrossDomainMessageSender(address(0));
+        } catch {
+            MESSENGER.setCrossDomainMessageSender(address(0));
+        }
+        uint256 balanceAfter = token.balanceOf(currentActor());
+        uint256 supplyAfter = token.totalSupply();
+        assert(balanceBefore == balanceAfter);
+        assert(supplyBefore == supplyAfter);
+    }
 }