diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index dbb711d27f014..9023076b9a3d2 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/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 | [ ] | [~] | diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol index 0e3f819a6f064..3bace13bc74ad 100644 --- a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol +++ b/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); } } 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 d3bf184ab1679..6b26f83f30f5e 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/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); + } }