diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index dbb711d27f01..9023076b9a3d 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/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol index d3bf184ab167..74810fe39b46 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 fuzz_BridgeSupertoken + function fuzz_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 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 balanceBefore = token.balanceOf(currentActor()); + uint256 supplyBefore = token.totalSupply(); + + vm.prank(address(MESSENGER)); + vm.mockCall( + address(MESSENGER), + abi.encodeWithSignature("crossDomainMessageSource()"), + abi.encode(address(token)) + ); + token.relayERC20(currentActor(), recipient, 0); + uint256 balanceAfter = token.balanceOf(currentActor()); + uint256 supplyAfter = token.totalSupply(); + assert(balanceBefore == balanceAfter); + assert(supplyBefore == supplyAfter); + } }