test: cross-user fuzzed bridges + actor setup

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

@@ -75,7 +75,7 @@ legend:
 
 | id  | milestone | description                                                                    | halmos  | medusa |
 | --- | ---       | ---                                                                            | ---     | ---    |
-| 6   | SupERC20  | calls to sendERC20 succeed as long as caller has enough balance                | [ ]     | [ ]    |
+| 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 cross-domain caller is valid | **[ ]** | [ ]    |
 
 ## Variable transition

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

@@ -0,0 +1,34 @@
+// 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) {
+        if (!_isActor[who]) {
+            _isActor[who] = true;
+            _actors.push(who);
+        }
+        _currentActor = 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/medusa/Protocol.properties.t.sol

@@ -1,9 +1,11 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.25;
 
+import { TestBase } from "forge-std/Base.sol";
+
+import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.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 {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
@@ -52,30 +54,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
+    )
+        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: 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,6 +100,7 @@ contract ProtocolProperties is ProtocolHandler {
             assert(sourceSupplyBefore - amount == sourceSupplyAfter);
             assert(destinationSupplyBefore + amount == destinationSupplyAfter);
         } catch {
+            // 6
             assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }

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

@@ -9,8 +9,9 @@ import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableM
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { Predeploys } from "src/libraries/Predeploys.sol";
 import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+import { Actors } from "../../helpers/Actors.t.sol";
 
-contract ProtocolHandler is TestBase, StdUtils {
+contract ProtocolHandler is TestBase, StdUtils, Actors {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
     uint8 internal constant MAX_CHAINS = 4;
@@ -69,12 +70,12 @@ contract ProtocolHandler is TestBase, StdUtils {
     /// @notice pick one already-deployed supertoken and mint an arbitrary amount of it
     /// necessary so there is something to be bridged :D
     /// TODO: will be replaced when testing the factories and `convert()`
-    function handler_MintSupertoken(uint256 index, uint96 amount) external {
+    function handler_MintSupertoken(uint256 index, uint96 amount) external withActor(msg.sender) {
         index = bound(index, 0, allSuperTokens.length - 1);
         address addr = allSuperTokens[index];
         vm.prank(BRIDGE);
         // medusa calls with different senders by default
-        OptimismSuperchainERC20(addr).mint(msg.sender, amount);
+        OptimismSuperchainERC20(addr).mint(currentActor(), amount);
         // currentValue will be zero if key is not present
         (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr));
         ghost_totalSupplyAcrossChains.set(MESSENGER.superTokenInitDeploySalts(addr), currentValue + amount);