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,11 +117,23 @@ 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)
 
 here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants
 
 - [ ]  changing the decimals of tokens after deployment
 - [ ]  `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols
+
+# Internal structure
+
+## Medusa campaign
+
+Fuzzing campaigns have both the need to push the contract into different states (state transitions) and assert properties are actually held. This defines a spectrum of function types:
+
+- `handler_`: they only transition the protocol state, and don't perform any assertions.
+- `fuzz_`: they both transition the protocol state and perform assertions on properties. They are further divided in:
+    - unguided: they exist to let the fuzzer try novel or unexpected interactions, and potentially transition to unexpectedly invalid states
+    - guided: they have the goal of quickly covering code and moving the protocol to known valid states (eg: by moving funds between valid users)
+- `property_`: they only assert the protocol is in a valid state, without causing a state transition. Note that they still use assertion-mode testing for simplicity, but could be migrated to run in property-mode.

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/HalmosBase.sol

@@ -5,7 +5,7 @@ import { Test } from "forge-std/Test.sol";
 
 contract HalmosBase is Test {
     uint256 internal constant CURRENT_CHAIN_ID = 1;
-    uint256 internal constant ZERO_AMOUNT = 0;
+    uint256 internal constant ZERO_AMOUNT;
 
     address internal remoteToken = address(bytes20(keccak256("remoteToken")));
     string internal name = "SuperchainERC20";

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,10 @@
+// SPDX-License-Identifier: AGPL-3
+pragma solidity ^0.8.25;
+
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+
+contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 {
+    /// @notice This is used by CryticERC20ExternalBasicProperties to know
+    // which properties to test
+    bool public constant isMintableOrBurnable = true;
+}

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

@@ -0,0 +1,130 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.25;
+
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { ProtocolHandler } from "../handlers/Protocol.t.sol";
+
+contract ProtocolGuided is ProtocolHandler {
+    /// @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
+    function fuzz_deployNewSupertoken(
+        TokenDeployParams memory params,
+        uint256 chainId
+    )
+        external
+        validateTokenDeployParams(params)
+    {
+        chainId = bound(chainId, 0, MAX_CHAINS - 1);
+        OptimismSuperchainERC20 supertoken = _deploySupertoken(
+            remoteTokens[params.remoteTokenIndex],
+            WORDS[params.nameIndex],
+            WORDS[params.symbolIndex],
+            DECIMALS[params.decimalsIndex],
+            chainId
+        );
+        // 14
+        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 fuzz_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(currentActor());
+        uint256 sourceSupplyBefore = sourceToken.totalSupply();
+        uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient);
+        uint256 destinationSupplyBefore = destinationToken.totalSupply();
+
+        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
+            assert(sourceBalanceBefore - amount == sourceBalanceAfter);
+            assert(destinationBalanceBefore + amount == destinationBalanceAfter);
+            uint256 sourceSupplyAfter = sourceToken.totalSupply();
+            uint256 destinationSupplyAfter = destinationToken.totalSupply();
+            // 23
+            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 fuzz_bridgeSupertoken, so we'll just call it
+    // instead of re-implementing it. Keeping the function for visibility of the property.
+    function fuzz_sendZeroDoesNotModifyAccounting(
+        uint256 fromIndex,
+        uint256 recipientIndex,
+        uint256 destinationChainId
+    )
+        external
+    {
+        fuzz_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 fuzz_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 balanceSenderBefore = token.balanceOf(currentActor());
+        uint256 balanceRecipientBefore = token.balanceOf(recipient);
+        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 balanceSenderAfter = token.balanceOf(currentActor());
+        uint256 balanceRecipeintAfter = token.balanceOf(recipient);
+        uint256 supplyAfter = token.totalSupply();
+        assert(balanceSenderBefore == balanceSenderAfter);
+        assert(balanceRecipientBefore == balanceRecipeintAfter);
+        assert(supplyBefore == supplyAfter);
+    }
+}