From f138b96501da0b537c13a069bed77bd34f5fb8f2 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 17:56:12 -0300 Subject: [PATCH] test: remaining protocol properties (#26) * test: cross-user fuzzed bridges + actor setup * test: fuzz properties 8 and 9 * test: properties 7 and 25 * fix: implement doc's feedback * test: superc20 tob properties (#27) * chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady * chore: remove zero-initializations * fix: feedback from disco * chore: separate fuzz campaign tests in guided vs unguided * test: dont revert on successful unguided relay * test: add fuzzed calls to burn and mint * docs: document the separation of fuzz test functions * chore: move the properties file to its own directory * chore: consistently use fuzz_ and property_ + camelcase * chore: fix typo * chore: camelcase for handlers as well * fix: revert change that broke halmos campaign compile :D --- .gitmodules | 3 + packages/contracts-bedrock/foundry.toml | 1 + packages/contracts-bedrock/lib/properties | 1 + packages/contracts-bedrock/medusa.json | 6 +- .../test/properties/PROPERTIES.md | 27 +++- .../test/properties/helpers/Actors.t.sol | 38 +++++ .../MockL2ToL2CrossDomainMessenger.t.sol | 5 + ...imismSuperchainERC20ForToBProperties.t.sol | 10 ++ .../medusa/Protocol.properties.t.sol | 93 ------------- .../medusa/fuzz/Protocol.guided.t.sol | 130 ++++++++++++++++++ .../medusa/fuzz/Protocol.unguided.t.sol | 98 +++++++++++++ ...{Protocol.handler.t.sol => Protocol.t.sol} | 66 +++++++-- .../medusa/properties/Protocol.t.sol | 50 +++++++ 13 files changed, 419 insertions(+), 109 deletions(-) create mode 160000 packages/contracts-bedrock/lib/properties create mode 100644 packages/contracts-bedrock/test/properties/helpers/Actors.t.sol create mode 100644 packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol delete mode 100644 packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol create mode 100644 packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol create mode 100644 packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol rename packages/contracts-bedrock/test/properties/medusa/handlers/{Protocol.handler.t.sol => Protocol.t.sol} (70%) create mode 100644 packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol diff --git a/.gitmodules b/.gitmodules index 222d45be7ccc..7aacfd154993 100644 --- a/.gitmodules +++ b/.gitmodules @@ -32,3 +32,6 @@ [submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"] path = packages/contracts-bedrock/lib/halmos-cheatcodes url = https://github.com/a16z/halmos-cheatcodes +[submodule "packages/contracts-bedrock/lib/properties"] + path = packages/contracts-bedrock/lib/properties + url = https://github.com/crytic/properties diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 69b1fde5c5eb..0e4aa4d0e354 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -17,6 +17,7 @@ remappings = [ '@rari-capital/solmate/=lib/solmate', '@lib-keccak/=lib/lib-keccak/contracts/lib', '@solady/=lib/solady/src', + '@crytic/properties/=lib/properties/', 'forge-std/=lib/forge-std/src', 'ds-test/=lib/forge-std/lib/ds-test/src', 'safe-contracts/=lib/safe-contracts/contracts', diff --git a/packages/contracts-bedrock/lib/properties b/packages/contracts-bedrock/lib/properties new file mode 160000 index 000000000000..bb1b78542b3f --- /dev/null +++ b/packages/contracts-bedrock/lib/properties @@ -0,0 +1 @@ +Subproject commit bb1b78542b3f38e4ae56cf87389cd3ea94387f48 diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index cb4737956fea..60e10b641de0 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -55,7 +55,11 @@ ] }, "targetFunctionSignatures": [], - "excludeFunctionSignatures": [] + "excludeFunctionSignatures": [ + "ProtocolProperties.test_ERC20external_zeroAddressBalance()", + "ProtocolProperties.test_ERC20external_transferToZeroAddress()", + "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)" + ] }, "chainConfig": { "codeSizeCheckDisabled": true, diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 25dc9b036d3b..9771f6b936a8 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -71,20 +71,21 @@ legend: | 3 | Liquidity Migration | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | | 4 | Liquidity Migration | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | | 5 | Liquidity Migration | convert() burns the same amount of legacy token that it mints of supertoken, and viceversa | [ ] | [ ] | +| 25 | SupERC20 | supertokens can't be reinitialized | [ ] | [x] | ## Valid state -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 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 sender and cross-domain caller are valid | **[~]** | [ ] | +| id | milestone | description | halmos | medusa | +| --- | --- | --- | --- | --- | +| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [x] | +| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[~]** | [~] | ## Variable transition | id | milestone | description | halmos | medusa | | --- | --- | --- | --- | --- | -| 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] | [ ] | +| 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] | [ ] | | 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] | [~] | @@ -116,7 +117,7 @@ It’s worth noting that these properties will not hold for a live system # Expected external interactions -- regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) +- [x] regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) # Invariant-breaking candidates (brain dump) @@ -124,3 +125,15 @@ here we’ll list possible interactions that we intend the fuzzing campaign to s - [ ] changing the decimals of tokens after deployment - [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols + +# Internal structure + +## Medusa campaign + +Fuzzing campaigns have both the need to push the contract into different states (state transitions) and assert properties are actually held. This defines a spectrum of function types: + +- `handler_`: they only transition the protocol state, and don't perform any assertions. +- `fuzz_`: they both transition the protocol state and perform assertions on properties. They are further divided in: + - unguided: they exist to let the fuzzer try novel or unexpected interactions, and potentially transition to unexpectedly invalid states + - guided: they have the goal of quickly covering code and moving the protocol to known valid states (eg: by moving funds between valid users) +- `property_`: they only assert the protocol is in a valid state, without causing a state transition. Note that they still use assertion-mode testing for simplicity, but could be migrated to run in property-mode. 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..3a7400667518 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol @@ -0,0 +1,38 @@ +// 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) { + addActor(who); + _currentActor = who; + _; + } + + function addActor(address who) internal { + if (!_isActor[who]) { + _isActor[who] = true; + _actors.push(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/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol index 0e3f819a6f06..3bace13bc74a 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/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol new file mode 100644 index 000000000000..145bf5ff01e5 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: AGPL-3 +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 { + /// @notice This is used by CryticERC20ExternalBasicProperties to know + // which properties to test + bool public constant isMintableOrBurnable = true; +} diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol deleted file mode 100644 index dd169dc5748d..000000000000 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ /dev/null @@ -1,93 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.25; - -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; - - // 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)- - /// convert(super, legacy) - function property_totalSupplyAcrossChainsEqualsMints() external view { - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply = 0; - (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 = 0; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply); - } - } - - /// @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 - function property_DeployNewSupertoken( - TokenDeployParams memory params, - uint256 chainId - ) - external - validateTokenDeployParams(params) - { - chainId = bound(chainId, 0, MAX_CHAINS - 1); - OptimismSuperchainERC20 supertoken = _deploySupertoken( - remoteTokens[params.remoteTokenIndex], - WORDS[params.nameIndex], - WORDS[params.symbolIndex], - DECIMALS[params.decimalsIndex], - chainId - ); - // 14 - assert(supertoken.totalSupply() == 0); - } - - /// @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 { - destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); - fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); - 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 sourceSupplyBefore = sourceToken.totalSupply(); - uint256 destinationBalanceBefore = destinationToken.balanceOf(msg.sender); - 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); - // no free mint - assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); - // 22 - assert(sourceBalanceBefore - amount == sourceBalanceAfter); - assert(destinationBalanceBefore + amount == destinationBalanceAfter); - uint256 sourceSupplyAfter = sourceToken.totalSupply(); - uint256 destinationSupplyAfter = destinationToken.totalSupply(); - // 23 - assert(sourceSupplyBefore - amount == sourceSupplyAfter); - assert(destinationSupplyBefore + amount == destinationSupplyAfter); - } catch { - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); - } - } -} 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 new file mode 100644 index 000000000000..70f19d79361a --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol @@ -0,0 +1,130 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; + +contract ProtocolGuided is ProtocolHandler { + /// @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 + function fuzz_deployNewSupertoken( + TokenDeployParams memory params, + uint256 chainId + ) + external + validateTokenDeployParams(params) + { + chainId = bound(chainId, 0, MAX_CHAINS - 1); + OptimismSuperchainERC20 supertoken = _deploySupertoken( + remoteTokens[params.remoteTokenIndex], + WORDS[params.nameIndex], + WORDS[params.symbolIndex], + DECIMALS[params.decimalsIndex], + chainId + ); + // 14 + 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 fuzz_bridgeSupertoken( + 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); + // 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(); + + 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 + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + assert(destinationBalanceBefore + amount == destinationBalanceAfter); + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + uint256 destinationSupplyAfter = destinationToken.totalSupply(); + // 23 + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + assert(destinationSupplyBefore + amount == destinationSupplyAfter); + } catch { + // 6 + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @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 + // instead of re-implementing it. Keeping the function for visibility of the property. + function fuzz_sendZeroDoesNotModifyAccounting( + uint256 fromIndex, + uint256 recipientIndex, + uint256 destinationChainId + ) + external + { + fuzz_bridgeSupertoken(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 + 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 balanceSenderBefore = token.balanceOf(currentActor()); + uint256 balanceRecipientBefore = token.balanceOf(recipient); + uint256 supplyBefore = token.totalSupply(); + + MESSENGER.setCrossDomainMessageSender(address(token)); + vm.prank(address(MESSENGER)); + try token.relayERC20(currentActor(), recipient, 0) { + MESSENGER.setCrossDomainMessageSender(address(0)); + } catch { + // should not revert because of 7, and if it *does* revert, I want the test suite + // to discard the sequence instead of potentially getting another + // error due to the crossDomainMessageSender being manually set + assert(false); + } + uint256 balanceSenderAfter = token.balanceOf(currentActor()); + uint256 balanceRecipeintAfter = token.balanceOf(recipient); + uint256 supplyAfter = token.totalSupply(); + assert(balanceSenderBefore == balanceSenderAfter); + assert(balanceRecipientBefore == balanceRecipeintAfter); + assert(supplyBefore == supplyAfter); + } +} 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 new file mode 100644 index 000000000000..17158e0f8732 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +// TODO: add fuzz_sendERC20 when we implement non-atomic bridging +contract ProtocolUnguided is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + /// @notice this ensures actors cant simply call relayERC20 and get tokens, no matter the system state + /// but there's still some possible work on how hard we can bork the system state with handlers calling + /// the L2ToL2CrossDomainMessenger or bridge directly (pending on non-atomic bridging) + function fuzz_relayERC20( + uint256 tokenIndex, + address sender, + address crossDomainMessageSender, + address recipient, + uint256 amount + ) + external + { + MESSENGER.setCrossDomainMessageSender(crossDomainMessageSender); + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + vm.prank(sender); + try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) { + MESSENGER.setCrossDomainMessageSender(address(0)); + assert(sender == address(MESSENGER)); + assert(crossDomainMessageSender == token); + // this increases the supply across chains without a call to + // `mint` by the MESSENGER, so it kind of breaks an invariant, but + // let's walk around that: + bytes32 salt = MESSENGER.superTokenInitDeploySalts(token); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); + } catch { + assert(sender != address(MESSENGER) || crossDomainMessageSender != token); + MESSENGER.setCrossDomainMessageSender(address(0)); + } + } + + /// @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 { + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + bytes32 salt = MESSENGER.superTokenInitDeploySalts(token); + amount = bound(amount, 0, type(uint256).max - OptimismSuperchainERC20(token).totalSupply()); + vm.prank(sender); + try OptimismSuperchainERC20(token).mint(to, amount) { + assert(sender == BRIDGE); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + } catch { + assert(sender != BRIDGE); + } + } + + + /// @custom:property-id 13 + /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge + function fuzz_burn(uint256 tokenIndex, address from, address sender, uint256 amount) external { + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + bytes32 salt = MESSENGER.superTokenInitDeploySalts(token); + uint256 senderBalance = OptimismSuperchainERC20(token).balanceOf(sender); + vm.prank(sender); + try OptimismSuperchainERC20(token).burn(from, amount) { + assert(sender == BRIDGE); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + } catch { + assert(sender != BRIDGE || senderBalance < amount); + } + } + + /// @custom:property-id 25 + /// @custom:property supertokens can't be reinitialized + function fuzz_initialize( + address sender, + uint256 tokenIndex, + address remoteToken, + string memory name, + string memory symbol, + uint8 decimals + ) + external + { + vm.prank(sender); + // revert is possible in bound, but is not part of the external call + try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize( + remoteToken, name, symbol, decimals + ) { + assert(false); + } catch { } + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol similarity index 70% rename from packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol rename to packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol index 266650486e34..1109b682c063 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol @@ -7,10 +7,12 @@ import { StdUtils } from "forge-std/StdUtils.sol"; import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { OptimismSuperchainERC20ForToBProperties } from "../../helpers/OptimismSuperchainERC20ForToBProperties.t.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; @@ -36,18 +38,20 @@ contract ProtocolHandler is TestBase, StdUtils { address[] internal remoteTokens; address[] internal allSuperTokens; - //@notice 'real' deploy salt => total supply sum across chains + /// @notice 'real' deploy salt => total supply sum across chains EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains; constructor() { vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); - superchainERC20Impl = new OptimismSuperchainERC20(); - for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { + superchainERC20Impl = new OptimismSuperchainERC20ForToBProperties(); + for (uint256 remoteTokenIndex; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { _deployRemoteToken(); - for (uint256 supertokenChainId = 0; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) { + for (uint256 supertokenChainId; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) { _deploySupertoken(remoteTokens[remoteTokenIndex], WORDS[0], WORDS[0], DECIMALS[0], supertokenChainId); } } + // integrate with all ToB properties using address(this) as the sender + addActor(address(this)); } /// @notice the deploy params are _indexes_ to pick from a pre-defined array of options and limit @@ -62,24 +66,70 @@ contract ProtocolHandler is TestBase, StdUtils { _; } - function handler_MockNewRemoteToken() external { + function handler_mockNewRemoteToken() external { _deployRemoteToken(); } /// @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); } + /// @notice The ToB properties don't preclude the need for this since they + /// always use address(this) as the caller, which won't get any balance + /// until it's transferred to it somehow + function handler_supERC20Transfer( + uint256 tokenIndex, + uint256 toIndex, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer( + getActorByRawIndex(toIndex), amount + ); + } + + function handler_supERC20TransferFrom( + uint256 tokenIndex, + uint256 fromIndex, + uint256 toIndex, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transferFrom( + getActorByRawIndex(fromIndex), getActorByRawIndex(toIndex), amount + ); + } + + function handler_supERC20Approve( + uint256 tokenIndex, + uint256 spenderIndex, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).approve( + getActorByRawIndex(spenderIndex), amount + ); + } + /// @notice deploy a remote token, that supertokens will be a representation of. They are never called, so there /// is no need to actually deploy a contract for them function _deployRemoteToken() internal { diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol new file mode 100644 index 000000000000..4f79e78665c7 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { ProtocolGuided } from "../fuzz/Protocol.guided.t.sol"; +import { ProtocolUnguided } from "../fuzz/Protocol.unguided.t.sol"; +import { CryticERC20ExternalBasicProperties } from + "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20ExternalBasicProperties { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + /// @dev `token` is the token under test for the ToB properties. This is coupled + /// to the ProtocolSetup constructor initializing at least one supertoken + constructor() { + token = ITokenMock(allSuperTokens[0]); + } + + /// @dev not that much of a handler, since this only changes which + /// supertoken the ToB assertions are performed against. Thankfully, they are + /// implemented in a way that don't require tracking ghost variables or can + /// break properties defined by us + function handler_ToBTestOtherToken(uint256 index) external { + token = ITokenMock(allSuperTokens[bound(index, 0, allSuperTokens.length - 1)]); + } + + // 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)- + /// convert(super, legacy) + function property_totalSupplyAcrossChainsEqualsMints() 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; + (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(); + } + } + assert(trackedSupply == totalSupply); + } + } +}