test: remaining protocol properties

.gitmodules

@@ -32,3 +32,6 @@
 [submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"]
 	path = packages/contracts-bedrock/lib/halmos-cheatcodes
 	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "packages/contracts-bedrock/lib/properties"]
+	path = packages/contracts-bedrock/lib/properties
+	url = https://github.com/crytic/properties

packages/contracts-bedrock/foundry.toml

@@ -17,6 +17,7 @@ remappings = [
   '@rari-capital/solmate/=lib/solmate',
   '@lib-keccak/=lib/lib-keccak/contracts/lib',
   '@solady/=lib/solady/src',
+  '@crytic/properties/=lib/properties/',
   'forge-std/=lib/forge-std/src',
   'ds-test/=lib/forge-std/lib/ds-test/src',
   'safe-contracts/=lib/safe-contracts/contracts',

packages/contracts-bedrock/medusa.json

@@ -55,7 +55,11 @@
 				]
 			},
 			"targetFunctionSignatures": [],
-			"excludeFunctionSignatures": []
+			"excludeFunctionSignatures": [
+        "ProtocolProperties.test_ERC20external_zeroAddressBalance()",
+        "ProtocolProperties.test_ERC20external_transferToZeroAddress()",
+        "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)"
+      ]
 		},
 		"chainConfig": {
 			"codeSizeCheckDisabled": true,

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

@@ -71,20 +71,21 @@ legend:
 | 3   | Liquidity Migration | convert() only allows migrations between tokens representing the same remote asset         | [ ]    | [ ]    |
 | 4   | Liquidity Migration | convert() only allows migrations from tokens with the same decimals                        | [ ]    | [ ]    |
 | 5   | Liquidity Migration | convert() burns the same amount of legacy token that it mints of supertoken, and viceversa | [ ]    | [ ]    |
+| 25  | SupERC20            | supertokens can't be reinitialized                                                         | [ ]    | [x]    |
 
 ## Valid state
 
-| id  | milestone | description                                                                                | halmos  | medusa |
-| --- | ---       | ---                                                                                        | ---     | ---    |
-| 6   | SupERC20  | calls to sendERC20 succeed as long as caller has enough balance                            | [x]     | [ ]    |
-| 7   | SupERC20  | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ]    |
+| id  | milestone | description                                                                    | halmos  | medusa |
+| --- | ---       | ---                                                                            | ---     | ---    |
+| 6   | SupERC20  | calls to sendERC20 succeed as long as caller has enough balance                | [x]     | [x]    |
+| 7   | SupERC20  | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[~]** | [~]    |
 
 ## Variable transition
 
 | id  | milestone           | description                                                                                       | halmos | medusa |
 | --- | ---                 | ---                                                                                               | ---    | ---    |
-| 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]    | [ ]    |
+| 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]    | [ ]    |
 | 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]    | [~]    |
@@ -116,7 +117,7 @@ It’s worth noting that these properties will not hold for a live system
 
 # Expected external interactions
 
-- regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
+- [x] regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
 
 # Invariant-breaking candidates (brain dump)
 

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

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.25;
+
+import { StdUtils } from "forge-std/StdUtils.sol";
+
+/// @notice helper for tracking actors, taking advantage of the fuzzer already using several `msg.sender`s
+contract Actors is StdUtils {
+    mapping(address => bool) private _isActor;
+    address[] private _actors;
+    address private _currentActor;
+
+    /// @notice register an actor if it's not already registered
+    /// usually called with msg.sender as a parameter, to track the actors
+    /// already provided by the fuzzer
+    modifier withActor(address who) {
+        addActor(who);
+        _currentActor = who;
+        _;
+    }
+
+    function addActor(address who) internal {
+        if (!_isActor[who]) {
+            _isActor[who] = true;
+            _actors.push(who);
+        }
+    }
+
+    /// @notice get the currently configured actor, should equal msg.sender
+    function currentActor() internal view returns (address) {
+        return _currentActor;
+    }
+
+    /// @notice get one of the actors by index, useful to get another random
+    /// actor than the one set as currentActor, to perform operations between them
+    function getActorByRawIndex(uint256 rawIndex) internal view returns (address) {
+        return _actors[bound(rawIndex, 0, _actors.length - 1)];
+    }
+}

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/helpers/OptimismSuperchainERC20ForToBProperties.t.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: AGPL-3
+pragma solidity ^0.8.25;
+
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+
+contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 {
+    bool public constant isMintableOrBurnable = true;
+    uint256 public initialSupply = 0;
+}

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

@@ -1,13 +1,32 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.25;
 
+import { TestBase } from "forge-std/Base.sol";
+
+import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol";
+import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
+import { CryticERC20ExternalBasicProperties } from
+    "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol";
 import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
-import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 
-contract ProtocolProperties is ProtocolHandler {
+contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperties {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
+    /// @dev `token` is the token under test for the ToB properties. This is coupled
+    /// to the ProtocolHandler constructor initializing at least one supertoken
+    constructor() {
+        token = ITokenMock(allSuperTokens[0]);
+    }
+
+    /// @dev not that much of a handler, since this only changes which
+    /// supertoken the ToB assertions are performed against. Thankfully, they are
+    /// implemented in a way that don't require tracking ghost variables or can
+    /// break properties defined by us
+    function handler_ToBTestOtherToken(uint256 index) external {
+        token = ITokenMock(allSuperTokens[bound(index, 0, allSuperTokens.length - 1)]);
+    }
+
     // TODO: will need rework after
     //   - non-atomic bridge
     //   - `convert`
@@ -52,30 +71,41 @@ contract ProtocolProperties is ProtocolHandler {
         assert(supertoken.totalSupply() == 0);
     }
 
+    /// @custom:property-id 6
+    /// @custom:property calls to sendERC20 succeed as long as caller has enough balance
     /// @custom:property-id 22
     /// @custom:property sendERC20 decreases sender balance in source chain and increases receiver balance in
     /// destination chain exactly by the input amount
     /// @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 property_SelfBridgeSupertoken(uint256 fromIndex, uint256 destinationChainId, uint256 amount) external {
+    function property_BridgeSupertoken(
+        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);
         // 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(msg.sender);
+        uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor());
         uint256 sourceSupplyBefore = sourceToken.totalSupply();
-        uint256 destinationBalanceBefore = destinationToken.balanceOf(msg.sender);
+        uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient);
         uint256 destinationSupplyBefore = destinationToken.totalSupply();
 
-        vm.prank(msg.sender);
-        try sourceToken.sendERC20(msg.sender, amount, destinationChainId) {
-            uint256 sourceBalanceAfter = sourceToken.balanceOf(msg.sender);
-            uint256 destinationBalanceAfter = destinationToken.balanceOf(msg.sender);
+        vm.prank(currentActor());
+        try sourceToken.sendERC20(recipient, amount, destinationChainId) {
+            uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
+            uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient);
             // no free mint
             assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter);
             // 22
@@ -87,7 +117,105 @@ contract ProtocolProperties is ProtocolHandler {
             assert(sourceSupplyBefore - amount == sourceSupplyAfter);
             assert(destinationSupplyBefore + amount == destinationSupplyAfter);
         } catch {
+            // 6
             assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }
+
+    /// @custom:property-id 8
+    /// @custom:property calls to sendERC20 with a value of zero dont modify accounting
+    // @notice is a subset of property_BridgeSupertoken, so we'll just call it
+    // instead of re-implementing it. Keeping the function for visibility of the property.
+    function property_SendZeroDoesNotModifyAccounting(
+        uint256 fromIndex,
+        uint256 recipientIndex,
+        uint256 destinationChainId
+    )
+        external
+    {
+        property_BridgeSupertoken(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
+    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 {
+            // should not revert because of 7, and if it *does* revert, I want the test suite
+            // to discard the sequence instead of potentially getting another
+            // error due to the crossDomainMessageSender being manually set
+            assert(false);
+        }
+        uint256 balanceAfter = token.balanceOf(currentActor());
+        uint256 supplyAfter = token.totalSupply();
+        assert(balanceBefore == balanceAfter);
+        assert(supplyBefore == supplyAfter);
+    }
+
+    /// @custom:property-id 7
+    /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    /// @notice this ensures actors cant simply call relayERC20 and get tokens, no matter the system state
+    /// but there's still some possible work on how hard we can bork the system state with handlers calling
+    /// the L2ToL2CrossDomainMessenger or bridge directly (pending on non-atomic bridging)
+    function property_SupERC20RelayERC20AlwaysRevert(
+        uint256 tokenIndex,
+        address sender,
+        address crossDomainMessageSender,
+        address recipient,
+        uint256 amount
+    )
+        external
+    {
+        MESSENGER.setCrossDomainMessageSender(crossDomainMessageSender);
+        address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)];
+        vm.prank(sender);
+        try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) {
+            assert(sender == address(MESSENGER));
+            assert(crossDomainMessageSender == token);
+            // this would increase the supply across chains without a call to
+            // `mint` by the MESSENGER, so I'm reverting the state transition
+            require(false);
+        } catch {
+            assert(sender != address(MESSENGER) || crossDomainMessageSender != token);
+            MESSENGER.setCrossDomainMessageSender(address(0));
+        }
+    }
+
+    /// @custom:property-id 25
+    /// @custom:property supertokens can't be reinitialized
+    function property_SupERC20CantBeReinitialized(
+        address sender,
+        uint256 tokenIndex,
+        address remoteToken,
+        string memory name,
+        string memory symbol,
+        uint8 decimals
+    )
+        external
+    {
+        vm.prank(sender);
+        // revert is possible in bound, but is not part of the external call
+        try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize(
+            remoteToken, name, symbol, decimals
+        ) {
+            assert(false);
+        } catch { }
+    }
 }