From 9de48fc250fd641337a12f60cd6f979ea56b4e62 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 17 Sep 2024 21:02:19 -0300 Subject: [PATCH] test: invariant tests for OptimismSuperchainERC20 (#11776) * chore: configure medusa with basic supERC20 self-bridging (#19) - used --foundry-compile-all to ensure the test contract under `test/properties` is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation) - set src,test,script to test/properties/medusa to not waste time compiling contracts that are not required for the medusa campaign - used an atomic bridge, which doesnt allow for testing of several of the proposed invariants fix: delete dead code test: give the fuzzer a head start docs: fix properties order test: document & implement assertions 22, 23 and 24 fix: fixes from self-review test: guide the fuzzer a little bit less previously: initial mint, bound on transfer amount: 146625 calls in 200s now: no initial mint, no bound on transfer amount: 176835 calls in 200s it doesn't seem to slow the fuzzer down fix: fixes after lovely feedback by disco docs: merge both documents and categorized properties by their milestone fix: fixes from parti's review fix: feedback from disco fix: feedback from doc refactor: separate state transitions from pure properties docs: update tested properties refactor: move all assertions into properties contract fix: move function without assertions back into handler test: only use assertion mode fix: improve justfile recipie for medusa * feat: halmos symbolic tests (#21) * feat: introduce OptimismSuperchainERC20 * fix: contract fixes * feat: add snapshots and semver * test: add supports interface tests * test: add invariant test * feat: add parameters to the RelayERC20 event * fix: typo * fix: from param description * fix: event signature and interface pragma * feat: add initializer * feat: use unstructured storage and OZ v5 * feat: update superchain erc20 interfaces * fix: adapt storage to ERC7201 * test: add initializable OZ v5 test * fix: invariant docs * fix: ERC165 implementation * test: improve superc20 invariant (#11) * fix: gas snapshot * chore: configure medusa with basic supERC20 self-bridging - used --foundry-compile-all to ensure the test contract under `test/properties` is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation) - set src,test,script to test/properties/medusa to not waste time compiling contracts that are not required for the medusa campaign - used an atomic bridge, which doesnt allow for testing of several of the proposed invariants * fix: delete dead code * test: give the fuzzer a head start * feat: create suite for sybolic tests with halmos * test: setup and 3 properties with symbolic tests * chore: remove todo comment * docs: fix properties order * test: document & implement assertions 22, 23 and 24 * fix: fixes from self-review * test: guide the fuzzer a little bit less previously: initial mint, bound on transfer amount: 146625 calls in 200s now: no initial mint, no bound on transfer amount: 176835 calls in 200s it doesn't seem to slow the fuzzer down * feat: add property for burn * refactor: remove symbolic address on mint property * refactor: order the tests based on the property id * feat: checkpoint * chore: set xdomain sender on failing test * chore: enhance mocks * Revert "Merge branch 'chore/setup-medusa' into feat/halmos-symbolic-tests" This reverts commit 945d6b6ad265ea5e3790d7ac9c5bf4d6586eb533, reversing changes made to 5dcb3a89252e9e8fa9b54ba9012e714f7cc96395. * refactor: remove symbolic addresses to make all of the test work * chore: remove console logs * feat: add properties file * chore: polish * refactor: enhance test on property 7 using direct try catch (now works) * fix: review comments * refactor: add symbolic addresses on test functions * feat: create halmos toml * chore: polish test contract and mock * chore: update property * refactor: move symbolic folder into properties one * feat: create advanced tests helper contract * refactor: enhance tests using symbolic addresses instead of concrete ones * chore: remove 0 property natspec * feat: add halmos profile and just script * chore: rename symbolic folder to halmos * feat: add halmos commands to justfile * chore: reorder assertions on one test * refactor: complete test property seven * chore: mark properties as completed * chore: add halmos-cheatcodes dependency * chore: rename advancedtest->halmosbase * chore: minimize mocked messenger * chore: delete empty halmos file * chore: revert changes to medusa.json * docs: update changes to PROPERTIES.md from base branch * test: sendERC20 destination fix * chore: natspec fixes --------- Co-authored-by: agusduha Co-authored-by: 0xng Co-authored-by: teddy * 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 * test: fuzz non atomic bridging (#31) * test: changed mocked messenger ABI for message sending but kept assertions the same * docs: add new properties 26&27 * test: queue cross-chain messages and test related properties * test: relay random messages from queue and check associated invariants * chore: rename bridge->senderc20 method for consistency with relayerc20 * test: not-yet-deployed supertokens can get funds sent to them * chore: medusa runs forever by default doable since it also handles SIGINTs gracefully * chore: document the reason behind relay zero and send zero inconsistencies * fix: feedback from doc * fix: walk around possible medusa issue I'm getting an 'unknown opcode 0x4e' in ProtocolAtomic constructor when calling the MockL2ToL2CrossDomainMessenger for the first time * test: unguided handler for sendERC20 * fix: feedback from disco * chore: remove halmos testsuite * chore: foundry migration (#40) * chore: track assertion failures this is so foundry's invariant contract can check that an assertion returned false in the handler, while still allowing `fail_on_revert = false` so we can still take full advantage of medusa's fuzzer & coverage reports * fix: explicitly skip duplicate supertoken deployments * chore: remove duplicated PROPERTIES.md file * chore: expose data to foundry's external invariant checker * test: run medusa fuzzing campaign from within foundry * fix: eagerly check for duplicate deployments * fix: feedback from doc * chore: shoehorn medusa campaign into foundry dir structure * chore: remove PROPERTIES.md file * chore: delete medusa config * docs: limited support for subdirectories in test/invariant * chore: rename contracts to be more sneaky about medusa * docs: rewrite invariant docs in a way compliant with autogen scripts * chore: fixes from rebase * fix: cleanup superc20 invariants (#46) * chore: revert modifications from medusa campaign * docs: extra docs on why ForTest contract is required * doc: add list of all supertoken properties * chore: run forge fmt * ci: allow for testfiles to be deleted * fix: run doc autogen script after rebase --------- Co-authored-by: Disco <131301107+0xDiscotech@users.noreply.github.com> Co-authored-by: agusduha Co-authored-by: 0xng --- .../invariant-docs/OptimismSuperchainERC20.md | 14 +- .../autogen/generate-invariant-docs/main.go | 6 + .../testing/test-heavy-fuzz-modified-tests.sh | 4 + .../invariants/OptimismSuperchainERC20.t.sol | 227 ------------------ .../OptimismSuperchainERC20.t.sol | 83 +++++++ .../OptimismSuperchainERC20/PROPERTIES.md | 82 +++++++ .../fuzz/Protocol.guided.t.sol | 211 ++++++++++++++++ .../fuzz/Protocol.unguided.t.sol | 137 +++++++++++ .../handlers/Protocol.t.sol | 177 ++++++++++++++ .../helpers/Actors.t.sol | 38 +++ .../helpers/CompatibleAssert.t.sol | 28 +++ .../helpers/HandlerGetters.t.sol | 22 ++ .../MockL2ToL2CrossDomainMessenger.t.sol | 118 +++++++++ ...imismSuperchainERC20ForToBProperties.t.sol | 12 + 14 files changed, 928 insertions(+), 231 deletions(-) delete mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/PROPERTIES.md create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol diff --git a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md index 13d03f304d45..8b5c65ebf213 100644 --- a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md +++ b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md @@ -1,10 +1,16 @@ # `OptimismSuperchainERC20` Invariants -## Calls to sendERC20 should always succeed as long as the actor has enough balance. Actor's balance should also not increase out of nowhere but instead should decrease by the amount sent. -**Test:** [`OptimismSuperchainERC20.t.sol#L196`](../test/invariants/OptimismSuperchainERC20.t.sol#L196) +## sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) +**Test:** [`OptimismSuperchainERC20#L36`](../test/invariants/OptimismSuperchainERC20#L36) -## Calls to relayERC20 should always succeeds when a message is received from another chain. Actor's balance should only increase by the amount relayed. -**Test:** [`OptimismSuperchainERC20.t.sol#L214`](../test/invariants/OptimismSuperchainERC20.t.sol#L214) +## sum of supertoken total supply across all chains is equal to convert(legacy, super)- convert(super, legacy) when all when all cross-chain messages are processed +**Test:** [`OptimismSuperchainERC20#L57`](../test/invariants/OptimismSuperchainERC20#L57) + + +## many other assertion mode invariants are also defined under `test/invariants/OptimismSuperchainERC20/fuzz/` . +**Test:** [`OptimismSuperchainERC20#L80`](../test/invariants/OptimismSuperchainERC20#L80) + +since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the handler for assertion test failures \ No newline at end of file diff --git a/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go b/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go index 0f0f5c77e63d..457e100edbe3 100644 --- a/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go +++ b/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go @@ -77,6 +77,12 @@ func docGen(invariantsDir, docsDir string) error { // Read the contents of the invariant test file. fileName := file.Name() filePath := filepath.Join(invariantsDir, fileName) + // where invariants for a module have their own directory, interpret + // the test file with the same name as the directory as a 'main' of + // sorts, from where documentation is pulled + if file.IsDir() { + filePath = filepath.Join(filePath, strings.Join([]string{fileName, ".t.sol"}, "")) + } fileContents, err := os.ReadFile(filePath) if err != nil { return fmt.Errorf("error reading file %q: %w", filePath, err) diff --git a/packages/contracts-bedrock/scripts/testing/test-heavy-fuzz-modified-tests.sh b/packages/contracts-bedrock/scripts/testing/test-heavy-fuzz-modified-tests.sh index 2649c85a5016..b7a8db6b5912 100755 --- a/packages/contracts-bedrock/scripts/testing/test-heavy-fuzz-modified-tests.sh +++ b/packages/contracts-bedrock/scripts/testing/test-heavy-fuzz-modified-tests.sh @@ -63,6 +63,10 @@ for FILE in $CHANGED_FILES; do echo "skipping $FILE" continue fi + if [ ! -e "$FILE" ] ; then + echo "skipping $FILE since it was deleted" + continue + fi # Get the diff for the file. DIFF=$(git diff origin/develop...HEAD --unified=0 -- "$FILE") diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol deleted file mode 100644 index 673df66a4c20..000000000000 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol +++ /dev/null @@ -1,227 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity 0.8.25; - -// Testing utilities -import { Test, StdUtils, Vm } from "forge-std/Test.sol"; -import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol"; - -// Libraries -import { Predeploys } from "src/libraries/Predeploys.sol"; -import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -import { IL2ToL2CrossDomainMessenger } from "src/L2/interfaces/IL2ToL2CrossDomainMessenger.sol"; - -/// @title OptimismSuperchainERC20_User -/// @notice Actor contract that interacts with the OptimismSuperchainERC20 contract. -contract OptimismSuperchainERC20_User is StdUtils { - address public immutable receiver; - - /// @notice Cross domain message data. - struct MessageData { - bytes32 id; - uint256 amount; - } - - uint256 public totalAmountSent; - uint256 public totalAmountRelayed; - - /// @notice Flag to indicate if the test has failed. - bool public failed = false; - - /// @notice The Vm contract. - Vm internal vm; - - /// @notice The OptimismSuperchainERC20 contract. - OptimismSuperchainERC20 internal superchainERC20; - - /// @notice Mapping of sent messages. - mapping(bytes32 => bool) internal sent; - - /// @notice Array of unrelayed messages. - MessageData[] internal unrelayed; - - /// @param _vm The Vm contract. - /// @param _superchainERC20 The OptimismSuperchainERC20 contract. - /// @param _balance The initial balance of the contract. - constructor(Vm _vm, OptimismSuperchainERC20 _superchainERC20, uint256 _balance, address _receiver) { - vm = _vm; - superchainERC20 = _superchainERC20; - - // Mint balance to this actor. - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - superchainERC20.mint(address(this), _balance); - receiver = _receiver; - } - - /// @notice Send ERC20 tokens to another chain. - /// @param _amount The amount of ERC20 tokens to send. - /// @param _chainId The chain ID to send the tokens to. - /// @param _messageId The message ID. - function sendERC20(uint256 _amount, uint256 _chainId, bytes32 _messageId) public { - // Make sure we aren't reusing a message ID. - if (sent[_messageId]) { - return; - } - - if (_chainId == block.chainid) return; - - // Bound send amount to our ERC20 balance. - _amount = bound(_amount, 0, superchainERC20.balanceOf(address(this))); - - // Send the amount. - try superchainERC20.sendERC20(receiver, _amount, _chainId) { - // Success. - totalAmountSent += _amount; - } catch { - failed = true; - } - - // Mark message as sent. - sent[_messageId] = true; - unrelayed.push(MessageData({ id: _messageId, amount: _amount })); - } - - /// @notice Relay a message from another chain. - function relayMessage(uint256 _source) public { - // Make sure there are unrelayed messages. - if (unrelayed.length == 0) { - return; - } - - // Grab the latest unrelayed message. - MessageData memory message = unrelayed[unrelayed.length - 1]; - - // Simulate the cross-domain message. - // Make sure the cross-domain message sender is set to this contract. - vm.mockCall( - Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, - abi.encodeCall(IL2ToL2CrossDomainMessenger.crossDomainMessageSender, ()), - abi.encode(address(superchainERC20)) - ); - - // Simulate the cross-domain message source to any chain. - vm.mockCall( - Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, - abi.encodeCall(IL2ToL2CrossDomainMessenger.crossDomainMessageSource, ()), - abi.encode(_source) - ); - - // Prank the relayERC20 function. - // Balance will just go back to our own account. - vm.prank(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - try superchainERC20.relayERC20(address(this), receiver, message.amount) { - // Success. - totalAmountRelayed += message.amount; - } catch { - failed = true; - } - - // Remove the message from the unrelayed list. - unrelayed.pop(); - } -} - -/// @title OptimismSuperchainERC20_Invariant -/// @notice Invariant test that checks that sending OptimismSuperchainERC20 always succeeds if the actor has a -/// sufficient balance to do so and that the actor's balance does not increase out of nowhere. -contract OptimismSuperchainERC20_Invariant is Test { - /// @notice Starting balance of the contract. - uint256 public constant STARTING_BALANCE = type(uint128).max; - - /// @notice The OptimismSuperchainERC20 contract implementation. - address internal optimismSuperchainERC20Impl; - - /// @notice The OptimismSuperchainERC20_User actor. - OptimismSuperchainERC20_User internal actor; - - /// @notice The OptimismSuperchainERC20 contract. - OptimismSuperchainERC20 internal optimismSuperchainERC20; - - /// @notice The address that will receive the tokens when relaying messages - address internal receiver = makeAddr("receiver"); - - /// @notice Test setup. - function setUp() public { - // Deploy the L2ToL2CrossDomainMessenger contract. - address _impl = _setImplementationCode(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - _setProxyCode(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, _impl); - - // Create a new OptimismSuperchainERC20 implementation. - optimismSuperchainERC20Impl = address(new OptimismSuperchainERC20()); - - // Deploy the OptimismSuperchainERC20 contract. - address _proxy = address(0x123456); - _setProxyCode(_proxy, optimismSuperchainERC20Impl); - optimismSuperchainERC20 = OptimismSuperchainERC20(_proxy); - - // Create a new OptimismSuperchainERC20_User actor. - actor = new OptimismSuperchainERC20_User(vm, optimismSuperchainERC20, STARTING_BALANCE, receiver); - - // Set the target contract. - targetContract(address(actor)); - - // Set the target selectors. - bytes4[] memory selectors = new bytes4[](2); - selectors[0] = actor.sendERC20.selector; - selectors[1] = actor.relayMessage.selector; - FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors }); - targetSelector(selector); - - // Setup assertions - assert(optimismSuperchainERC20.balanceOf(address(actor)) == STARTING_BALANCE); - assert(optimismSuperchainERC20.balanceOf(address(receiver)) == 0); - assert(optimismSuperchainERC20.totalSupply() == STARTING_BALANCE); - } - - /// @notice Sets the bytecode in the implementation address. - function _setImplementationCode(address _addr) internal returns (address) { - string memory cname = Predeploys.getName(_addr); - address impl = Predeploys.predeployToCodeNamespace(_addr); - vm.etch(impl, vm.getDeployedCode(string.concat(cname, ".sol:", cname))); - return impl; - } - - /// @notice Sets the bytecode in the proxy address. - function _setProxyCode(address _addr, address _impl) internal { - bytes memory code = vm.getDeployedCode("universal/Proxy.sol:Proxy"); - vm.etch(_addr, code); - EIP1967Helper.setAdmin(_addr, Predeploys.PROXY_ADMIN); - EIP1967Helper.setImplementation(_addr, _impl); - } - - /// @notice Invariant that checks that sending OptimismSuperchainERC20 always succeeds. - /// @custom:invariant Calls to sendERC20 should always succeed as long as the actor has enough balance. - /// Actor's balance should also not increase out of nowhere but instead should decrease by the - /// amount sent. - function invariant_sendERC20_succeeds() public view { - // Assert that the actor has not failed to send OptimismSuperchainERC20. - assertTrue(!actor.failed()); - - // Assert that the actor has sent more than or equal to the amount relayed. - assertTrue(actor.totalAmountSent() >= actor.totalAmountRelayed()); - - // Assert that the actor's balance has decreased by the amount sent. - assertEq(optimismSuperchainERC20.balanceOf(address(actor)), STARTING_BALANCE - actor.totalAmountSent()); - - // Assert that the total supply of the OptimismSuperchainERC20 contract has decreased by the amount unrelayed. - uint256 _unrelayedAmount = actor.totalAmountSent() - actor.totalAmountRelayed(); - assertEq(optimismSuperchainERC20.totalSupply(), STARTING_BALANCE - _unrelayedAmount); - } - - /// @notice Invariant that checks that relaying OptimismSuperchainERC20 always succeeds. - /// @custom:invariant Calls to relayERC20 should always succeeds when a message is received from another chain. - /// Actor's balance should only increase by the amount relayed. - function invariant_relayERC20_succeeds() public view { - // Assert that the actor has not failed to relay OptimismSuperchainERC20. - assertTrue(!actor.failed()); - - // Assert that the actor has sent more than or equal to the amount relayed. - assertTrue(actor.totalAmountSent() >= actor.totalAmountRelayed()); - - // Assert that the actor's balance has increased by the amount relayed. - assertEq(optimismSuperchainERC20.balanceOf(address(receiver)), actor.totalAmountRelayed()); - - // Assert that the total supply of the OptimismSuperchainERC20 contract has decreased by the amount unrelayed. - uint256 _unrelayedAmount = actor.totalAmountSent() - actor.totalAmountRelayed(); - assertEq(optimismSuperchainERC20.totalSupply(), STARTING_BALANCE - _unrelayedAmount); - } -} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol new file mode 100644 index 000000000000..d90e90a2f811 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +// Testing utilities +import { Test, StdUtils, Vm } from "forge-std/Test.sol"; +import { StdInvariant } from "forge-std/StdInvariant.sol"; +import { StdAssertions } from "forge-std/StdAssertions.sol"; +import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol"; + +// Libraries +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { IL2ToL2CrossDomainMessenger } from "src/L2/interfaces/IL2ToL2CrossDomainMessenger.sol"; +import { ProtocolGuided } from "./fuzz/Protocol.guided.t.sol"; +import { ProtocolUnguided } from "./fuzz/Protocol.unguided.t.sol"; +import { HandlerGetters } from "./helpers/HandlerGetters.t.sol"; +import { MockL2ToL2CrossDomainMessenger } from "./helpers/MockL2ToL2CrossDomainMessenger.t.sol"; + +contract OptimismSuperchainERC20Handler is HandlerGetters, ProtocolGuided, ProtocolUnguided { } + +contract OptimismSuperchainERC20Properties is Test { + OptimismSuperchainERC20Handler internal handler; + MockL2ToL2CrossDomainMessenger internal constant MESSENGER = + MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); + + function setUp() public { + handler = new OptimismSuperchainERC20Handler(); + targetContract(address(handler)); + } + + // TODO: will need rework after + // - `convert` + /// @custom:invariant sum of supertoken total supply across all chains is always <= to convert(legacy, super)- + /// convert(super, legacy) + function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view { + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex); + uint256 fundsInTransit = handler.tokensInTransitForDeploySalt(currentSalt); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assertEq(trackedSupply, totalSupply + fundsInTransit); + } + } + + // TODO: will need rework after + // - `convert` + /// @custom:invariant sum of supertoken total supply across all chains is equal to convert(legacy, super)- + /// convert(super, legacy) when all when all cross-chain messages are processed + function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view { + if (MESSENGER.messageQueueLength() != 0) { + return; + } + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assertEq(trackedSupply, totalSupply); + } + } + + /// @custom:invariant many other assertion mode invariants are also defined under + /// `test/invariants/OptimismSuperchainERC20/fuzz/` . + /// + /// since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the + /// handler for assertion test failures + function invariant_handlerAssertions() external view { + assertFalse(handler.failed()); + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/PROPERTIES.md b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/PROPERTIES.md new file mode 100644 index 000000000000..18970855ca46 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/PROPERTIES.md @@ -0,0 +1,82 @@ +# Supertoken advanced testing + +## Milestones + +The supertoken ecosystem consists of not just the supertoken contract, but the required changes to other contracts for liquidity to reach the former. + +Considering only the supertoken contract is merged into the `develop` branch, and work for the other components is still in progress, we define three milestones for the testing campaign: + +- SupERC20: concerned with only the supertoken contract, the first one to be implemented +- Factories: covers the above + the development of `OptimismSuperchainERC20Factory` and required changes to `OptimismMintableERC20Factory` +- Liquidity Migration: includes the `convert` function on the `L2StandardBridgeInterop` to migrate liquidity from legacy tokens into supertokens + +## Definitions + +- *legacy token:* an OptimismMintableERC20 or L2StandardERC20 token on the suprechain that has either been deployed by the factory after the liquidity migration upgrade to the latter, or has been deployed before it **but** added to factory’s `deployments` mapping as part of the upgrade. This testing campaign is not concerned with tokens on L1 or not listed in the factory’s `deployments` mapping. +- *supertoken:* a SuperchainERC20 contract deployed by the `OptimismSuperchainERC20Factory` + +# Ecosystem properties + +legend: + +- `[ ]`: property not yet tested +- `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it +- `[X]`: tested/proven property +- `[~]`: partially tested/proven property +- `:(`: property won't be tested due to some limitation + +## Unit test + +| id | milestone | description | tested | +| --- | --- | --- | --- | +| 0 | Factories | supertoken token address does not depend on the executing chain’s chainID | [ ] | +| 1 | Factories | supertoken token address depends on remote token, name, symbol and decimals | [ ] | +| 2 | Liquidity Migration | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | +| 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 | tested | +| --- | --- | --- | --- | +| 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 cross-domain caller is valid | [~] | + +## Variable transition + +| id | milestone | description | tested | +| --- | --- | --- | --- | +| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | +| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [x] | +| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | +| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [x] | +| 27 | SupERC20 | relayERC20 increases sender's balance in the destination chain exactly by the input amount | [x] | +| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ] | +| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [~] | +| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [ ] | +| 14 | SupERC20 | supertoken total supply starts at zero | [x] | +| 15 | Factories | deploying a supertoken registers its remote token in the factory | [ ] | +| 16 | Factories | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | + +## High level + +| id | milestone | description | tested | +| --- | --- | --- | --- | +| 17 | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | +| 18 | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | +| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [~] | +| 20 | SupERC20 | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ] | +| 21 | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [~] | + +## Atomic bridging pseudo-properties + +As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction) +It’s worth noting that these properties will not hold for a live system + +| id | milestone | description | tested | +| --- | --- | --- | --- | +| 22 | SupERC20 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [x] | +| 23 | SupERC20 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [x] | +| 24 | Liquidity Migration | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [~] | diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol new file mode 100644 index 000000000000..536a4ea7025a --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol @@ -0,0 +1,211 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { CompatibleAssert } from "../helpers/CompatibleAssert.t.sol"; + +contract ProtocolGuided is ProtocolHandler, CompatibleAssert { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId + /// @custom:property-id 14 + /// @custom:property supertoken total supply starts at zero + + 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 + compatibleAssert(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_bridgeSupertokenAtomic( + 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); + uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient); + uint256 destinationSupplyBefore = destinationToken.totalSupply(); + + MESSENGER.setAtomic(true); + vm.prank(currentActor()); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + MESSENGER.setAtomic(false); + uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); + uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); + // no free mint + compatibleAssert( + sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter + ); + // 22 + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(destinationBalanceBefore + amount == destinationBalanceAfter); + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + uint256 destinationSupplyAfter = destinationToken.totalSupply(); + // 23 + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(destinationSupplyBefore + amount == destinationSupplyAfter); + } catch { + MESSENGER.setAtomic(false); + // 6 + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 26 + /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount + /// @custom:property-id 10 + /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount + function fuzz_sendERC20( + uint256 fromIndex, + uint256 recipientIndex, + uint256 destinationChainId, + uint256 amount + ) + public + withActor(msg.sender) + { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); + address recipient = getActorByRawIndex(recipientIndex); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + + vm.prank(currentActor()); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); + // 26 + uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); + // 10 + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); + } catch { + // 6 + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 11 + /// @custom:property relayERC20 increases the token's totalSupply in the destination chain exactly by the input + /// amount + /// @custom:property-id 27 + /// @custom:property relayERC20 increases sender's balance in the destination chain exactly by the input amount + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + function fuzz_relayERC20(uint256 messageIndex) external { + MockL2ToL2CrossDomainMessenger.CrossChainMessage memory messageToRelay = MESSENGER.messageQueue(messageIndex); + OptimismSuperchainERC20 destinationToken = OptimismSuperchainERC20(messageToRelay.crossDomainMessageSender); + uint256 destinationSupplyBefore = destinationToken.totalSupply(); + uint256 destinationBalanceBefore = destinationToken.balanceOf(messageToRelay.recipient); + + try MESSENGER.relayMessageFromQueue(messageIndex) { + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken)); + (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + // if sendERC20 didnt intialize this, then test suite is broken + compatibleAssert(success); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount); + // 11 + compatibleAssert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); + // 27 + compatibleAssert( + destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient) + ); + } catch { + // 7 + compatibleAssert(false); + } + } + + /// @custom:property-id 8 + /// @custom:property calls to sendERC20 with a value of zero dont modify accounting + // @notice is a subset of fuzz_sendERC20, so we'll just call it + // instead of re-implementing it. Keeping the function for visibility of the property. + function fuzz_sendZeroDoesNotModifyAccounting( + uint256 fromIndex, + uint256 recipientIndex, + uint256 destinationChainId + ) + external + { + fuzz_sendERC20(fromIndex, recipientIndex, destinationChainId, 0); + } + + /// @custom:property-id 9 + /// @custom:property calls to relayERC20 with a value of zero dont modify accounting + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + /// @notice cant call fuzz_RelayERC20 internally since that pops a + /// random message, which we cannot guarantee has a value of zero + function fuzz_relayZeroDoesNotModifyAccounting( + uint256 fromIndex, + uint256 recipientIndex + ) + 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 + compatibleAssert(false); + } + uint256 balanceSenderAfter = token.balanceOf(currentActor()); + uint256 balanceRecipeintAfter = token.balanceOf(recipient); + uint256 supplyAfter = token.totalSupply(); + compatibleAssert(balanceSenderBefore == balanceSenderAfter); + compatibleAssert(balanceRecipientBefore == balanceRecipeintAfter); + compatibleAssert(supplyBefore == supplyAfter); + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol new file mode 100644 index 000000000000..90cad38baa99 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol @@ -0,0 +1,137 @@ +// 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"; +import { CompatibleAssert } from "../helpers/CompatibleAssert.t.sol"; + +// TODO: add fuzz_sendERC20 when we implement non-atomic bridging +contract ProtocolUnguided is ProtocolHandler, CompatibleAssert { + 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)); + compatibleAssert(sender == address(MESSENGER)); + compatibleAssert(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 { + compatibleAssert(sender != address(MESSENGER) || crossDomainMessageSender != token); + MESSENGER.setCrossDomainMessageSender(address(0)); + } + } + + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 26 + /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount + /// @custom:property-id 10 + /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount + function fuzz_sendERC20( + address sender, + address recipient, + uint256 fromIndex, + uint256 destinationChainId, + uint256 amount + ) + public + { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(sender); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + + vm.prank(sender); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); + // 26 + uint256 sourceBalanceAfter = sourceToken.balanceOf(sender); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); + // 10 + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); + } catch { + // 6 + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 12 + /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge + function fuzz_mint(uint256 tokenIndex, address to, address sender, uint256 amount) external { + 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) { + compatibleAssert(sender == BRIDGE); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); + } catch { + compatibleAssert(sender != BRIDGE || to == address(0)); + } + } + + /// @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) { + compatibleAssert(sender == BRIDGE); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + } catch { + compatibleAssert(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 + ) { + compatibleAssert(false); + } catch { } + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol new file mode 100644 index 000000000000..921495b467ab --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol @@ -0,0 +1,177 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { TestBase } from "forge-std/Base.sol"; +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, Actors { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + uint8 public constant MAX_CHAINS = 4; + uint8 internal constant INITIAL_TOKENS = 1; + uint8 internal constant INITIAL_SUPERTOKENS = 1; + uint8 internal constant SUPERTOKEN_INITIAL_MINT = 100; + address internal constant BRIDGE = Predeploys.L2_STANDARD_BRIDGE; + MockL2ToL2CrossDomainMessenger internal constant MESSENGER = + MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); + OptimismSuperchainERC20 internal superchainERC20Impl; + // NOTE: having more options for this enables the fuzzer to configure + // different supertokens for the same remote token + string[] internal WORDS = ["TOKENS"]; + uint8[] internal DECIMALS = [6, 18]; + + struct TokenDeployParams { + uint8 remoteTokenIndex; + uint8 nameIndex; + uint8 symbolIndex; + uint8 decimalsIndex; + } + + address[] internal remoteTokens; + address[] internal allSuperTokens; + + /// @notice 'real' deploy salt => total supply sum across chains + EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains; + /// @notice 'real' deploy salt => tokens sendERC20'd but not yet relayERC20'd + EnumerableMap.Bytes32ToUintMap internal ghost_tokensInTransit; + + constructor() { + vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); + superchainERC20Impl = new OptimismSuperchainERC20ForToBProperties(); + for (uint256 remoteTokenIndex; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { + _deployRemoteToken(); + 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 + /// the amount of supertokens for a given remoteAsset that are incompatible between them, as + /// two supertokens have to share decimals, name, symbol and remoteAsset to be considered + /// the same asset, and therefore bridgable. + modifier validateTokenDeployParams(TokenDeployParams memory params) { + params.remoteTokenIndex = uint8(bound(params.remoteTokenIndex, 0, remoteTokens.length - 1)); + params.nameIndex = uint8(bound(params.nameIndex, 0, WORDS.length - 1)); + params.symbolIndex = uint8(bound(params.symbolIndex, 0, WORDS.length - 1)); + params.decimalsIndex = uint8(bound(params.decimalsIndex, 0, DECIMALS.length - 1)); + _; + } + + 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) { + index = bound(index, 0, allSuperTokens.length - 1); + address addr = allSuperTokens[index]; + vm.prank(BRIDGE); + 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 { + // make sure they don't conflict with predeploys/preinstalls/precompiles/other tokens + remoteTokens.push(address(uint160(1000 + remoteTokens.length))); + } + + /// @notice deploy a new supertoken representing remoteToken + /// remoteToken, name, symbol and decimals determine the 'real' deploy salt + /// and supertokens sharing it are interoperable between them + /// we however use the chainId as part of the deploy salt to mock the ability of + /// supertokens to exist on different chains on a single EVM. + function _deploySupertoken( + address remoteToken, + string memory name, + string memory symbol, + uint8 decimals, + uint256 chainId + ) + internal + returns (OptimismSuperchainERC20 supertoken) + { + // this salt would be used in production. Tokens sharing it will be bridgable with each other + bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals)); + // Foundry invariant erroneously show other unrelated invariant breaking + // when this deployment fails due to a create2 collision, so we revert eagerly instead + require(MESSENGER.superTokenAddresses(chainId, realSalt) == address(0), "skip duplicate deployment"); + + // what we use in the tests to walk around two contracts needing two different addresses + // tbf we could be using CREATE1, but this feels more verbose + bytes32 hackySalt = keccak256(abi.encode(remoteToken, name, symbol, decimals, chainId)); + supertoken = OptimismSuperchainERC20( + address( + // TODO: Use the SuperchainERC20 Beacon Proxy + new ERC1967Proxy{ salt: hackySalt }( + address(superchainERC20Impl), + abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) + ) + ) + ); + MESSENGER.registerSupertoken(realSalt, chainId, address(supertoken)); + allSuperTokens.push(address(supertoken)); + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol new file mode 100644 index 000000000000..3a7400667518 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/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/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol new file mode 100644 index 000000000000..4e69c94c8585 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: GPL-3 +pragma solidity ^0.8.24; + +import { console } from "forge-std/console.sol"; + +/// @title CompatibleAssert +/// @notice meant to add compatibility between medusa assertion tests and +/// foundry invariant test's required architecture +contract CompatibleAssert { + bool public failed; + + function compatibleAssert(bool condition) internal { + compatibleAssert(condition, ""); + } + + function compatibleAssert(bool condition, string memory message) internal { + if (!condition) { + if (bytes(message).length != 0) console.log("Assertion failed: ", message); + else console.log("Assertion failed"); + + // for foundry to call & check + failed = true; + + // for medusa + assert(false); + } + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol new file mode 100644 index 000000000000..b081aa48c6bb --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: GPL-3 +pragma solidity ^0.8.24; + +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; + +contract HandlerGetters is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + function deploySaltsLength() external view returns (uint256 length) { + return ghost_totalSupplyAcrossChains.length(); + } + + function totalSupplyAcrossChainsAtIndex(uint256 index) external view returns (bytes32 salt, uint256 supply) { + return ghost_totalSupplyAcrossChains.at(index); + } + + function tokensInTransitForDeploySalt(bytes32 salt) external view returns (uint256 amount) { + (, amount) = ghost_tokensInTransit.tryGet(salt); + return amount; + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol new file mode 100644 index 000000000000..6eb1c30e6799 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { SafeCall } from "src/libraries/SafeCall.sol"; + +contract MockL2ToL2CrossDomainMessenger { + //////////////////////// + // type definitions // + //////////////////////// + struct CrossChainMessage { + address crossDomainMessageSender; + address crossDomainMessageSource; + bytes payload; + address recipient; + uint256 amount; + } + + ///////////////////////////////////////////////////////// + // State vars mocking the L2toL2CrossDomainMessenger // + ///////////////////////////////////////////////////////// + address public crossDomainMessageSender; + address public crossDomainMessageSource; + + /////////////////////////////////////////////////// + // Helpers for cross-chain interaction mocking // + /////////////////////////////////////////////////// + mapping(address supertoken => bytes32 deploySalt) public superTokenInitDeploySalts; + mapping(uint256 chainId => mapping(bytes32 deploySalt => address supertoken)) public superTokenAddresses; + + CrossChainMessage[] private _messageQueue; + bool private _atomic; + + function messageQueue(uint256 rawIndex) external view returns (CrossChainMessage memory) { + return _messageQueue[rawIndex % _messageQueue.length]; + } + + function crossChainMessageReceiver( + address sender, + uint256 destinationChainId + ) + external + view + returns (OptimismSuperchainERC20) + { + 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; + } + + function messageQueueLength() public view returns (uint256) { + return _messageQueue.length; + } + + function setAtomic(bool atomic) public { + _atomic = atomic; + } + + function relayMessageFromQueue(uint256 rawIndex) public { + uint256 index = rawIndex % _messageQueue.length; + CrossChainMessage memory message = _messageQueue[index]; + _messageQueue[index] = _messageQueue[_messageQueue.length - 1]; + _messageQueue.pop(); + _relayMessage(message); + } + + function _relayMessage(CrossChainMessage memory message) internal { + crossDomainMessageSender = message.crossDomainMessageSender; + crossDomainMessageSource = message.crossDomainMessageSource; + SafeCall.call(crossDomainMessageSender, 0, message.payload); + crossDomainMessageSender = address(0); + crossDomainMessageSource = address(0); + } + + //////////////////////////////////////////////////////// + // Functions mocking the L2toL2CrossDomainMessenger // + //////////////////////////////////////////////////////// + + /// @notice recipient will not be used since in normal execution it's the same + /// address on a different chain, but here we have to compute it to mock + /// cross-chain messaging + function sendMessage(uint256 chainId, address, /*recipient*/ bytes calldata data) external { + address crossChainRecipient = superTokenAddresses[chainId][superTokenInitDeploySalts[msg.sender]]; + if (crossChainRecipient == msg.sender) { + require(false, "same chain"); + } + (address recipient, uint256 amount) = _decodePayload(data); + + CrossChainMessage memory message = CrossChainMessage({ + crossDomainMessageSender: crossChainRecipient, + crossDomainMessageSource: msg.sender, + payload: data, + recipient: recipient, + amount: amount + }); + + if (_atomic) { + _relayMessage(message); + } else { + _messageQueue.push(message); + } + } + + //////////////////////// + // Internal helpers // + //////////////////////// + + function _decodePayload(bytes calldata payload) internal pure returns (address recipient, uint256 amount) { + (, recipient, amount) = abi.decode(payload[4:], (address, address, uint256)); + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol new file mode 100644 index 000000000000..9f80cda92fcc --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol @@ -0,0 +1,12 @@ +// 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 (only used + /// in Medusa testing campaign)to know which properties to test, and + /// remains here so Medusa and Foundry test campaigns can use a single + /// setup + bool public constant isMintableOrBurnable = true; +}