diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 0e4aa4d0e354..0e0d6959c5b6 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -103,6 +103,7 @@ script = 'test/kontrol/proofs' src = 'test/properties/medusa/' test = 'test/properties/medusa/' script = 'test/properties/medusa/' +via-ir=true [profile.halmos] src = 'test/properties/halmos/' diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index 60e10b641de0..5df25c2cd63b 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -3,7 +3,7 @@ "workers": 10, "workerResetLimit": 50, "timeout": 0, - "testLimit": 500000, + "testLimit": 0, "callSequenceLength": 100, "corpusDirectory": "test/properties/medusa/corpus/", "coverageEnabled": true, diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 9771f6b936a8..d915d565633e 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -86,7 +86,9 @@ legend: | --- | --- | --- | --- | --- | | 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] | [ ] | +| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [x] | +| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [ ] | [x] | +| 27 | SupERC20 | relayERC20 increases sender's balance in the destination 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] | [~] | | 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | @@ -100,9 +102,9 @@ legend: | --- | --- | --- | --- | --- | | 17 | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | | 18 | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | -| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | +| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | | 20 | SupERC20 | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ] | [ ] | -| 21 | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [ ] | +| 21 | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [~] | ## Atomic bridging pseudo-properties diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol index 3bace13bc74a..6eb1c30e6799 100644 --- a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -5,6 +5,17 @@ import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { SafeCall } from "src/libraries/SafeCall.sol"; contract MockL2ToL2CrossDomainMessenger { + //////////////////////// + // type definitions // + //////////////////////// + struct CrossChainMessage { + address crossDomainMessageSender; + address crossDomainMessageSource; + bytes payload; + address recipient; + uint256 amount; + } + ///////////////////////////////////////////////////////// // State vars mocking the L2toL2CrossDomainMessenger // ///////////////////////////////////////////////////////// @@ -17,6 +28,13 @@ contract MockL2ToL2CrossDomainMessenger { mapping(address supertoken => bytes32 deploySalt) public superTokenInitDeploySalts; mapping(uint256 chainId => mapping(bytes32 deploySalt => address supertoken)) public superTokenAddresses; + CrossChainMessage[] private _messageQueue; + bool private _atomic; + + function messageQueue(uint256 rawIndex) external view returns (CrossChainMessage memory) { + return _messageQueue[rawIndex % _messageQueue.length]; + } + function crossChainMessageReceiver( address sender, uint256 destinationChainId @@ -37,6 +55,30 @@ contract MockL2ToL2CrossDomainMessenger { superTokenInitDeploySalts[token] = deploySalt; } + function messageQueueLength() public view returns (uint256) { + return _messageQueue.length; + } + + function setAtomic(bool atomic) public { + _atomic = atomic; + } + + function relayMessageFromQueue(uint256 rawIndex) public { + uint256 index = rawIndex % _messageQueue.length; + CrossChainMessage memory message = _messageQueue[index]; + _messageQueue[index] = _messageQueue[_messageQueue.length - 1]; + _messageQueue.pop(); + _relayMessage(message); + } + + function _relayMessage(CrossChainMessage memory message) internal { + crossDomainMessageSender = message.crossDomainMessageSender; + crossDomainMessageSource = message.crossDomainMessageSource; + SafeCall.call(crossDomainMessageSender, 0, message.payload); + crossDomainMessageSender = address(0); + crossDomainMessageSource = address(0); + } + //////////////////////////////////////////////////////// // Functions mocking the L2toL2CrossDomainMessenger // //////////////////////////////////////////////////////// @@ -44,15 +86,33 @@ contract MockL2ToL2CrossDomainMessenger { /// @notice recipient will not be used since in normal execution it's the same /// address on a different chain, but here we have to compute it to mock /// cross-chain messaging - function sendMessage(uint256 chainId, address, /*recipient*/ bytes memory message) external { + function sendMessage(uint256 chainId, address, /*recipient*/ bytes calldata data) external { address crossChainRecipient = superTokenAddresses[chainId][superTokenInitDeploySalts[msg.sender]]; if (crossChainRecipient == msg.sender) { require(false, "same chain"); } - crossDomainMessageSender = crossChainRecipient; - crossDomainMessageSource = msg.sender; - SafeCall.call(crossDomainMessageSender, 0, message); - crossDomainMessageSender = address(0); - crossDomainMessageSource = address(0); + (address recipient, uint256 amount) = _decodePayload(data); + + CrossChainMessage memory message = CrossChainMessage({ + crossDomainMessageSender: crossChainRecipient, + crossDomainMessageSource: msg.sender, + payload: data, + recipient: recipient, + amount: amount + }); + + if (_atomic) { + _relayMessage(message); + } else { + _messageQueue.push(message); + } + } + + //////////////////////// + // Internal helpers // + //////////////////////// + + function _decodePayload(bytes calldata payload) internal pure returns (address recipient, uint256 amount) { + (, recipient, amount) = abi.decode(payload[4:], (address, address, uint256)); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol index 70f19d79361a..d5b5d8b5edc5 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol @@ -1,10 +1,13 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.25; +import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; contract ProtocolGuided is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; /// @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 @@ -35,7 +38,7 @@ contract ProtocolGuided is ProtocolHandler { /// @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( + function fuzz_bridgeSupertokenAtomic( uint256 fromIndex, uint256 recipientIndex, uint256 destinationChainId, @@ -50,16 +53,15 @@ contract ProtocolGuided is ProtocolHandler { 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(); + MESSENGER.setAtomic(true); vm.prank(currentActor()); try sourceToken.sendERC20(recipient, amount, destinationChainId) { + MESSENGER.setAtomic(false); uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); // no free mint @@ -73,14 +75,86 @@ contract ProtocolGuided is ProtocolHandler { assert(sourceSupplyBefore - amount == sourceSupplyAfter); assert(destinationSupplyBefore + amount == destinationSupplyAfter); } catch { + MESSENGER.setAtomic(false); // 6 assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 26 + /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount + /// @custom:property-id 10 + /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount + function fuzz_sendERC20( + 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); + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + + vm.prank(currentActor()); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); + // 26 + uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + // 10 + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + } catch { + // 6 + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 11 + /// @custom:property relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount + /// @custom:property-id 27 + /// @custom:property relayERC20 increases sender's balance in the destination chain exactly by the input amount + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + function fuzz_relayERC20(uint256 messageIndex) external { + MockL2ToL2CrossDomainMessenger.CrossChainMessage memory messageToRelay = MESSENGER.messageQueue(messageIndex); + OptimismSuperchainERC20 destinationToken = OptimismSuperchainERC20(messageToRelay.crossDomainMessageSender); + uint256 destinationSupplyBefore = destinationToken.totalSupply(); + uint256 destinationBalanceBefore = destinationToken.balanceOf(messageToRelay.recipient); + + try MESSENGER.relayMessageFromQueue(messageIndex) { + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken)); + (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + // if sendERC20 didnt intialize this, then test suite is broken + assert(success); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount); + // 11 + assert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); + // 27 + assert( + destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient) + ); + } catch { + // 7 + assert(false); + } + } + /// @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 + // @notice is a subset of fuzz_sendERC20, so we'll just call it // instead of re-implementing it. Keeping the function for visibility of the property. function fuzz_sendZeroDoesNotModifyAccounting( uint256 fromIndex, @@ -89,13 +163,15 @@ contract ProtocolGuided is ProtocolHandler { ) external { - fuzz_bridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0); + fuzz_sendERC20(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 + /// @notice cant call fuzz_RelayERC20 internally since that pops a + /// random message, which we cannot guarantee has a value of zero function fuzz_relayZeroDoesNotModifyAccounting( uint256 fromIndex, uint256 recipientIndex diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol index 17158e0f8732..71ba64118088 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol @@ -42,6 +42,46 @@ contract ProtocolUnguided is ProtocolHandler { } } + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 26 + /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount + /// @custom:property-id 10 + /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount + function fuzz_sendERC20( + address sender, + address recipient, + uint256 fromIndex, + uint256 destinationChainId, + uint256 amount + ) + public + { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(sender); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + + vm.prank(sender); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); + // 26 + uint256 sourceBalanceAfter = sourceToken.balanceOf(sender); + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + // 10 + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + } catch { + // 6 + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 12 /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge function fuzz_mint(uint256 tokenIndex, address to, address sender, uint256 amount) external { @@ -52,9 +92,9 @@ contract ProtocolUnguided is ProtocolHandler { try OptimismSuperchainERC20(token).mint(to, amount) { assert(sender == BRIDGE); (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); - ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); } catch { - assert(sender != BRIDGE); + assert(sender != BRIDGE || to == address(0)); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol index 1109b682c063..191c5c44a7e6 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol @@ -40,6 +40,8 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { /// @notice 'real' deploy salt => total supply sum across chains EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains; + /// @notice 'real' deploy salt => tokens sendERC20'd but not yet relayERC20'd + EnumerableMap.Bytes32ToUintMap internal ghost_tokensInTransit; constructor() { vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol index 4f79e78665c7..7b2f73d54058 100644 --- a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol @@ -27,18 +27,40 @@ contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20Exte } // TODO: will need rework after - // - non-atomic bridge // - `convert` - /// @custom:property-id 24 - /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- + /// @custom:property-id 19 + /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)- /// convert(super, legacy) - function property_totalSupplyAcrossChainsEqualsMints() external view { + function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view { // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply; + for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply ; (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + (, uint256 fundsInTransit) = ghost_tokensInTransit.tryGet(currentSalt); // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId; validChainId < MAX_CHAINS; validChainId++) { + for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assert(trackedSupply == totalSupply + fundsInTransit); + } + } + + // TODO: will need rework after + // - `convert` + /// @custom:property-id 21 + /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)- + /// convert(super, legacy) when all when all cross-chain messages are processed + function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view { + require(MESSENGER.messageQueueLength() == 0); + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply ; + (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); if (supertoken != address(0)) { totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();