From e998667d24c8df0edafe49225fff5329a180695f Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 15 Aug 2024 12:16:35 -0300 Subject: [PATCH 01/16] test: cross-user fuzzed bridges + actor setup --- .../test/properties/PROPERTIES.md | 2 +- .../test/properties/helpers/Actors.t.sol | 34 +++++++++++++++++++ .../medusa/Protocol.properties.t.sol | 30 +++++++++++----- .../medusa/handlers/Protocol.handler.t.sol | 7 ++-- 4 files changed, 61 insertions(+), 12 deletions(-) create mode 100644 packages/contracts-bedrock/test/properties/helpers/Actors.t.sol diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 25dc9b036d3b..085672e2516f 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -76,7 +76,7 @@ legend: | id | milestone | description | halmos | medusa | | --- | --- | --- | --- | --- | -| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | +| 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 sender and cross-domain caller are 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); From 179fba2a15e303a9b9c8e005ce48252b5fdd8175 Mon Sep 17 00:00:00 2001 From: teddy Date: Mon, 19 Aug 2024 20:46:36 -0300 Subject: [PATCH 02/16] test: fuzz properties 8 and 9 --- .../test/properties/PROPERTIES.md | 4 +- .../MockL2ToL2CrossDomainMessenger.t.sol | 5 ++ .../medusa/Protocol.properties.t.sol | 67 +++++++++++++++++++ 3 files changed, 74 insertions(+), 2 deletions(-) diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 085672e2516f..64314a505b06 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -83,8 +83,8 @@ legend: | 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] | [~] | 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/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol index d3bf184ab167..6b26f83f30f5 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); + } } From 6b671941fd68d7c91b73189e93312f4f1306184a Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 20 Aug 2024 21:07:21 -0300 Subject: [PATCH 03/16] test: properties 7 and 25 --- .../test/properties/PROPERTIES.md | 9 ++-- .../medusa/Protocol.properties.t.sol | 44 +++++++++++++++++++ 2 files changed, 49 insertions(+), 4 deletions(-) diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 64314a505b06..b2b992e371ff 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -71,13 +71,14 @@ 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] | [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 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 6b26f83f30f5..7494d772bc47 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -171,4 +171,48 @@ contract ProtocolProperties is ProtocolHandler { assert(balanceBefore == balanceAfter); assert(supplyBefore == supplyAfter); } + + /// @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 property_SupERC20RelayERC20AlwaysRevert( + uint256 tokenIndex, + address sender, + address recipient, + uint256 amount + ) + external + withActor(msg.sender) + { + // if msg.sender is the L2ToL2CrossDomainMessenger then this will break other invariants + vm.prank(currentActor()); + try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).relayERC20( + sender, recipient, amount + ) { + assert(false); + } catch { } + } + + /// @custom:property-id 25 + /// @custom:property supertokens can't be reinitialized + function property_SupERC20CantBeReinitialized( + uint256 tokenIndex, + address remoteToken, + string memory name, + string memory symbol, + uint8 decimals + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + // 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 { } + } } From 96ecaad6b7f4ea1e433c996fe85dd615aa974c62 Mon Sep 17 00:00:00 2001 From: teddy Date: Fri, 23 Aug 2024 14:50:38 -0300 Subject: [PATCH 04/16] fix: implement doc's feedback --- .../medusa/Protocol.properties.t.sol | 66 ++++++++----------- 1 file changed, 26 insertions(+), 40 deletions(-) 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 7494d772bc47..47d1fe1c61a4 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -68,7 +68,7 @@ contract ProtocolProperties is ProtocolHandler { uint256 destinationChainId, uint256 amount ) - external + public withActor(msg.sender) { destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); @@ -107,45 +107,22 @@ contract ProtocolProperties is ProtocolHandler { /// @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 + // @notice is a subset of property_BridgeSupertoken, so we'll just call it + // instead of re-implementing it. Keeping the function for visibility of the property. 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)); - } + property_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 property_RelayZeroDoesNotModifyAccounting( uint256 fromIndex, uint256 recipientIndex @@ -164,7 +141,10 @@ contract ProtocolProperties is ProtocolHandler { try token.relayERC20(currentActor(), recipient, 0) { MESSENGER.setCrossDomainMessageSender(address(0)); } catch { - MESSENGER.setCrossDomainMessageSender(address(0)); + // 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 balanceAfter = token.balanceOf(currentActor()); uint256 supplyAfter = token.totalSupply(); @@ -180,24 +160,31 @@ contract ProtocolProperties is ProtocolHandler { function property_SupERC20RelayERC20AlwaysRevert( uint256 tokenIndex, address sender, + address crossDomainMessageSender, address recipient, uint256 amount ) external - withActor(msg.sender) { - // if msg.sender is the L2ToL2CrossDomainMessenger then this will break other invariants - vm.prank(currentActor()); - try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).relayERC20( - sender, recipient, amount - ) { - assert(false); - } catch { } + MESSENGER.setCrossDomainMessageSender(crossDomainMessageSender); + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + vm.prank(sender); + try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) { + assert(sender == address(MESSENGER)); + assert(crossDomainMessageSender == token); + // this would increase the supply across chains without a call to + // `mint` by the MESSENGER, so I'm reverting the state transition + require(false); + } catch { + assert(sender != address(MESSENGER) || crossDomainMessageSender != token); + MESSENGER.setCrossDomainMessageSender(address(0)); + } } /// @custom:property-id 25 /// @custom:property supertokens can't be reinitialized function property_SupERC20CantBeReinitialized( + address sender, uint256 tokenIndex, address remoteToken, string memory name, @@ -205,9 +192,8 @@ contract ProtocolProperties is ProtocolHandler { uint8 decimals ) external - withActor(msg.sender) { - vm.prank(currentActor()); + 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 From 3adeba5008a74c1da96bdaf94071b834bc3bfcad Mon Sep 17 00:00:00 2001 From: teddy Date: Mon, 26 Aug 2024 09:51:29 -0300 Subject: [PATCH 05/16] 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 --- .gitmodules | 3 ++ packages/contracts-bedrock/foundry.toml | 1 + packages/contracts-bedrock/lib/properties | 1 + packages/contracts-bedrock/medusa.json | 6 ++- .../test/properties/PROPERTIES.md | 2 +- .../test/properties/helpers/Actors.t.sol | 10 ++-- ...imismSuperchainERC20ForToBProperties.t.sol | 9 ++++ .../medusa/Protocol.properties.t.sol | 19 ++++++- .../medusa/handlers/Protocol.handler.t.sol | 53 ++++++++++++++++++- 9 files changed, 96 insertions(+), 8 deletions(-) create mode 160000 packages/contracts-bedrock/lib/properties create mode 100644 packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.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 b2b992e371ff..5b580b8a37ea 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -117,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) diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol index 2f07acb0e5d9..3a7400667518 100644 --- a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol @@ -13,16 +13,20 @@ contract Actors is StdUtils { /// 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); } - _currentActor = who; - _; } /// @notice get the currently configured actor, should equal msg.sender - function currentActor() internal view returns(address){ + function currentActor() internal view returns (address) { return _currentActor; } 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..865534a9efa8 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: AGPL-3 +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 { + bool public constant isMintableOrBurnable = true; + uint256 public initialSupply = 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 47d1fe1c61a4..c5d227540441 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -3,13 +3,30 @@ pragma solidity ^0.8.25; import { TestBase } from "forge-std/Base.sol"; +import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol"; import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { CryticERC20ExternalBasicProperties } from + "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol"; import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -contract ProtocolProperties is ProtocolHandler { +contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperties { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + /// @dev `token` is the token under test for the ToB properties. This is coupled + /// to the ProtocolHandler 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` 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 15197a6786c6..d773d1ef90d3 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 @@ -7,6 +7,7 @@ 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"; @@ -37,18 +38,20 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { 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(); + superchainERC20Impl = new OptimismSuperchainERC20ForToBProperties(); for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { _deployRemoteToken(); for (uint256 supertokenChainId = 0; 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 @@ -81,6 +84,52 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { 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 { From 5e7eb8731ccc68a8cff8c22a1f2f486aff12d0fc Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 27 Aug 2024 11:35:46 -0300 Subject: [PATCH 06/16] chore: remove zero-initializations --- .../test/properties/helpers/HalmosBase.sol | 2 +- .../test/properties/medusa/Protocol.properties.t.sol | 6 +++--- .../test/properties/medusa/handlers/Protocol.handler.t.sol | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol index 75bfe2f7c9e1..28b1d301147c 100644 --- a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol +++ b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol @@ -5,7 +5,7 @@ import { Test } from "forge-std/Test.sol"; contract HalmosBase is Test { uint256 internal constant CURRENT_CHAIN_ID = 1; - uint256 internal constant ZERO_AMOUNT = 0; + uint256 internal constant ZERO_AMOUNT; address internal remoteToken = address(bytes20(keccak256("remoteToken"))); string internal name = "SuperchainERC20"; 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 c5d227540441..2d8b8b77917f 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -35,11 +35,11 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti /// 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; + 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 = 0; 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(); 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 d773d1ef90d3..1e593266ea18 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 @@ -44,9 +44,9 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { constructor() { vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); superchainERC20Impl = new OptimismSuperchainERC20ForToBProperties(); - for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { + 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); } } From 403dc70de62b19c0e2615a24ca5fc3f0ba2e342f Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 27 Aug 2024 11:36:08 -0300 Subject: [PATCH 07/16] fix: feedback from disco --- .../OptimismSuperchainERC20ForToBProperties.t.sol | 3 ++- .../test/properties/medusa/Protocol.properties.t.sol | 9 ++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol index 865534a9efa8..145bf5ff01e5 100644 --- a/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol @@ -4,6 +4,7 @@ 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; - uint256 public initialSupply = 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 2d8b8b77917f..e73d84f26861 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -150,7 +150,8 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); address recipient = getActorByRawIndex(recipientIndex); OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]); - uint256 balanceBefore = token.balanceOf(currentActor()); + uint256 balanceSenderBefore = token.balanceOf(currentActor()); + uint256 balanceRecipeintBefore = token.balanceOf(recipient); uint256 supplyBefore = token.totalSupply(); MESSENGER.setCrossDomainMessageSender(address(token)); @@ -163,9 +164,11 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti // error due to the crossDomainMessageSender being manually set assert(false); } - uint256 balanceAfter = token.balanceOf(currentActor()); + uint256 balanceSenderAfter = token.balanceOf(currentActor()); + uint256 balanceRecipeintAfter = token.balanceOf(recipient); uint256 supplyAfter = token.totalSupply(); - assert(balanceBefore == balanceAfter); + assert(balanceSenderBefore == balanceSenderAfter); + assert(balanceRecipeintBefore == balanceRecipeintAfter); assert(supplyBefore == supplyAfter); } From dea79ceda19f58f4ef97c051b58f04dede6a206d Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 28 Aug 2024 18:59:54 -0300 Subject: [PATCH 08/16] chore: separate fuzz campaign tests in guided vs unguided --- .../test/properties/medusa/Protocol.t.sol | 50 ++++++++++ .../Protocol.guided.t.sol} | 98 +------------------ .../medusa/fuzz/Protocol.unguided.t.sol | 61 ++++++++++++ ...{Protocol.handler.t.sol => Protocol.t.sol} | 0 4 files changed, 113 insertions(+), 96 deletions(-) create mode 100644 packages/contracts-bedrock/test/properties/medusa/Protocol.t.sol rename packages/contracts-bedrock/test/properties/medusa/{Protocol.properties.t.sol => fuzz/Protocol.guided.t.sol} (56%) 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} (100%) diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.t.sol new file mode 100644 index 000000000000..0f97f88607ad --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/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); + } + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol similarity index 56% rename from packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol rename to packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol index e73d84f26861..79f135808774 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol @@ -1,54 +1,10 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.25; -import { TestBase } from "forge-std/Base.sol"; - -import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol"; -import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; -import { CryticERC20ExternalBasicProperties } from - "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol"; -import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; -contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperties { - using EnumerableMap for EnumerableMap.Bytes32ToUintMap; - - /// @dev `token` is the token under test for the ToB properties. This is coupled - /// to the ProtocolHandler 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); - } - } - +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 @@ -171,54 +127,4 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti assert(balanceRecipeintBefore == balanceRecipeintAfter); assert(supplyBefore == supplyAfter); } - - /// @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 property_SupERC20RelayERC20AlwaysRevert( - 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) { - assert(sender == address(MESSENGER)); - assert(crossDomainMessageSender == token); - // this would increase the supply across chains without a call to - // `mint` by the MESSENGER, so I'm reverting the state transition - require(false); - } catch { - assert(sender != address(MESSENGER) || crossDomainMessageSender != token); - MESSENGER.setCrossDomainMessageSender(address(0)); - } - } - - /// @custom:property-id 25 - /// @custom:property supertokens can't be reinitialized - function property_SupERC20CantBeReinitialized( - 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/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol new file mode 100644 index 000000000000..f249a783b8fe --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol @@ -0,0 +1,61 @@ +// 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) { + assert(sender == address(MESSENGER)); + assert(crossDomainMessageSender == token); + // this would increase the supply across chains without a call to + // `mint` by the MESSENGER, so I'm reverting the state transition + require(false); + } catch { + assert(sender != address(MESSENGER) || crossDomainMessageSender != token); + MESSENGER.setCrossDomainMessageSender(address(0)); + } + } + + /// @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 100% 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 From 7bba3f0159fc76d24de05a21f4a43404d9140535 Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 28 Aug 2024 19:18:28 -0300 Subject: [PATCH 09/16] test: dont revert on successful unguided relay --- .../properties/medusa/fuzz/Protocol.unguided.t.sol | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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 f249a783b8fe..8a4c548678a2 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 @@ -27,11 +27,15 @@ contract ProtocolUnguided is ProtocolHandler { 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 would increase the supply across chains without a call to - // `mint` by the MESSENGER, so I'm reverting the state transition - require(false); + // 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)); From cd2b64b588163c15cb8eb6387927c58b3260f2eb Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 28 Aug 2024 19:10:15 -0300 Subject: [PATCH 10/16] test: add fuzzed calls to burn and mint --- .../medusa/fuzz/Protocol.unguided.t.sol | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) 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 8a4c548678a2..17158e0f8732 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,39 @@ contract ProtocolUnguided is ProtocolHandler { } } + /// @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( From 231c6b5adc988e76d0a0a6d79d7ad6ac3003bceb Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 28 Aug 2024 21:31:54 -0300 Subject: [PATCH 11/16] docs: document the separation of fuzz test functions --- .../contracts-bedrock/test/properties/PROPERTIES.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 5b580b8a37ea..9771f6b936a8 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -125,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. From e97fda0712654f4b0d5d4c2557af8def04c1b8d8 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 13:45:59 -0300 Subject: [PATCH 12/16] chore: move the properties file to its own directory --- .../test/properties/medusa/{ => properties}/Protocol.t.sol | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename packages/contracts-bedrock/test/properties/medusa/{ => properties}/Protocol.t.sol (95%) diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol similarity index 95% rename from packages/contracts-bedrock/test/properties/medusa/Protocol.t.sol rename to packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol index 0f97f88607ad..4f79e78665c7 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol @@ -3,8 +3,8 @@ 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 { 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"; From b08176052ec68c0b8ef5a45a7b2f178e93f5f4a2 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 13:50:13 -0300 Subject: [PATCH 13/16] chore: consistently use fuzz_ and property_ + camelcase --- .../properties/medusa/fuzz/Protocol.guided.t.sol | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) 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 79f135808774..570ba93d63d7 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 @@ -8,7 +8,7 @@ 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 property_DeployNewSupertoken( + function fuzz_deployNewSupertoken( TokenDeployParams memory params, uint256 chainId ) @@ -35,7 +35,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 property_BridgeSupertoken( + function fuzz_bridgeSupertoken( uint256 fromIndex, uint256 recipientIndex, uint256 destinationChainId, @@ -80,23 +80,23 @@ contract ProtocolGuided is ProtocolHandler { /// @custom:property-id 8 /// @custom:property calls to sendERC20 with a value of zero dont modify accounting - // @notice is a subset of property_BridgeSupertoken, so we'll just call it + // @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 property_SendZeroDoesNotModifyAccounting( + function fuzz_sendZeroDoesNotModifyAccounting( uint256 fromIndex, uint256 recipientIndex, uint256 destinationChainId ) external { - property_BridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0); + 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 property_RelayZeroDoesNotModifyAccounting( + function fuzz_relayZeroDoesNotModifyAccounting( uint256 fromIndex, uint256 recipientIndex ) From 8a597a9027fa11c345434ab725ddaf835b1cf503 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 13:51:10 -0300 Subject: [PATCH 14/16] chore: fix typo --- .../test/properties/medusa/fuzz/Protocol.guided.t.sol | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 570ba93d63d7..70f19d79361a 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 @@ -107,7 +107,7 @@ contract ProtocolGuided is ProtocolHandler { address recipient = getActorByRawIndex(recipientIndex); OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]); uint256 balanceSenderBefore = token.balanceOf(currentActor()); - uint256 balanceRecipeintBefore = token.balanceOf(recipient); + uint256 balanceRecipientBefore = token.balanceOf(recipient); uint256 supplyBefore = token.totalSupply(); MESSENGER.setCrossDomainMessageSender(address(token)); @@ -124,7 +124,7 @@ contract ProtocolGuided is ProtocolHandler { uint256 balanceRecipeintAfter = token.balanceOf(recipient); uint256 supplyAfter = token.totalSupply(); assert(balanceSenderBefore == balanceSenderAfter); - assert(balanceRecipeintBefore == balanceRecipeintAfter); + assert(balanceRecipientBefore == balanceRecipeintAfter); assert(supplyBefore == supplyAfter); } } From e26b9c359586e85f697a48126e17ad89973de0cc Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 13:56:24 -0300 Subject: [PATCH 15/16] chore: camelcase for handlers as well --- .../test/properties/medusa/handlers/Protocol.t.sol | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 1e593266ea18..1109b682c063 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol @@ -66,14 +66,14 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { _; } - 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 withActor(msg.sender) { + 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); @@ -87,7 +87,7 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { /// @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( + function handler_supERC20Transfer( uint256 tokenIndex, uint256 toIndex, uint256 amount @@ -101,7 +101,7 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { ); } - function handler_SupERC20TransferFrom( + function handler_supERC20TransferFrom( uint256 tokenIndex, uint256 fromIndex, uint256 toIndex, @@ -116,7 +116,7 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { ); } - function handler_SupERC20Approve( + function handler_supERC20Approve( uint256 tokenIndex, uint256 spenderIndex, uint256 amount From c681a7c8754007b99c78234e381c54570d4d4fe2 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 17:54:36 -0300 Subject: [PATCH 16/16] fix: revert change that broke halmos campaign compile :D --- .../contracts-bedrock/test/properties/helpers/HalmosBase.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol index 28b1d301147c..75bfe2f7c9e1 100644 --- a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol +++ b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol @@ -5,7 +5,7 @@ import { Test } from "forge-std/Test.sol"; contract HalmosBase is Test { uint256 internal constant CURRENT_CHAIN_ID = 1; - uint256 internal constant ZERO_AMOUNT; + uint256 internal constant ZERO_AMOUNT = 0; address internal remoteToken = address(bytes20(keccak256("remoteToken"))); string internal name = "SuperchainERC20";