diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 36b7b330ab0b..dbb711d27f01 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/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 diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol new file mode 100644 index 000000000000..2f07acb0e5d9 --- /dev/null +++ b/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)]; + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol index dd169dc5748d..d3bf184ab167 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/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); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol index 266650486e34..15197a6786c6 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol +++ b/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);