From 8cea35148e12faae1b1919b7d2a19c2b81e48174 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 8 Aug 2024 14:38:56 -0300 Subject: [PATCH 01/11] 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 --- packages/contracts-bedrock/.gitignore | 1 + packages/contracts-bedrock/foundry.toml | 5 + packages/contracts-bedrock/justfile | 3 + packages/contracts-bedrock/medusa.json | 82 ++++++++++++ .../test/properties/PROPERTIES.md | 125 ++++++++++++++++++ .../MockL2ToL2CrossDomainMessenger.t.sol | 53 ++++++++ .../medusa/Protocol.properties.t.sol | 93 +++++++++++++ .../medusa/handlers/Protocol.handler.t.sol | 122 +++++++++++++++++ 8 files changed, 484 insertions(+) create mode 100644 packages/contracts-bedrock/medusa.json create mode 100644 packages/contracts-bedrock/test/properties/PROPERTIES.md create mode 100644 packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol create mode 100644 packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol create mode 100644 packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol diff --git a/packages/contracts-bedrock/.gitignore b/packages/contracts-bedrock/.gitignore index 96e09c8c7190..396c03d4458d 100644 --- a/packages/contracts-bedrock/.gitignore +++ b/packages/contracts-bedrock/.gitignore @@ -6,6 +6,7 @@ broadcast kout-deployment kout-proofs test/kontrol/logs +test/properties/medusa/corpus/ # Metrics coverage.out diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index cef9f85bbaeb..08ae8840dc49 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -97,3 +97,8 @@ src = 'test/kontrol/proofs' out = 'kout-proofs' test = 'test/kontrol/proofs' script = 'test/kontrol/proofs' + +[profile.medusa] +src = 'test/properties/medusa/' +test = 'test/properties/medusa/' +script = 'test/properties/medusa/' diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile index bf96fd17cad1..654ad64cadee 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -26,6 +26,9 @@ test-kontrol: build-go-ffi build kontrol-summary-full test-kontrol-no-build test-kontrol-no-build: ./test/kontrol/scripts/run-kontrol.sh script +test-medusa timeout='100': + FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}} + test-rerun: build-go-ffi forge test --rerun -vvv diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json new file mode 100644 index 000000000000..cb4737956fea --- /dev/null +++ b/packages/contracts-bedrock/medusa.json @@ -0,0 +1,82 @@ +{ + "fuzzing": { + "workers": 10, + "workerResetLimit": 50, + "timeout": 0, + "testLimit": 500000, + "callSequenceLength": 100, + "corpusDirectory": "test/properties/medusa/corpus/", + "coverageEnabled": true, + "targetContracts": ["ProtocolProperties"], + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": [ + "0x10000", + "0x20000", + "0x30000" + ], + "blockNumberDelayMax": 60480, + "blockTimestampDelayMax": 604800, + "blockGasLimit": 30000000, + "transactionGasLimit": 12500000, + "testing": { + "stopOnFailedTest": true, + "stopOnFailedContractMatching": false, + "stopOnNoTests": true, + "testAllContracts": false, + "traceAll": true, + "assertionTesting": { + "enabled": true, + "testViewMethods": true, + "panicCodeConfig": { + "failOnCompilerInsertedPanic": false, + "failOnAssertion": true, + "failOnArithmeticUnderflow": false, + "failOnDivideByZero": false, + "failOnEnumTypeConversionOutOfBounds": false, + "failOnIncorrectStorageAccess": false, + "failOnPopEmptyArray": false, + "failOnOutOfBoundsArrayAccess": false, + "failOnAllocateTooMuchMemory": false, + "failOnCallUninitializedVariable": false + } + }, + "propertyTesting": { + "enabled": false, + "testPrefixes": [ + "property_" + ] + }, + "optimizationTesting": { + "enabled": false, + "testPrefixes": [ + "optimize_" + ] + }, + "targetFunctionSignatures": [], + "excludeFunctionSignatures": [] + }, + "chainConfig": { + "codeSizeCheckDisabled": true, + "cheatCodes": { + "cheatCodesEnabled": true, + "enableFFI": false + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": ["--foundry-out-directory", "artifacts","--foundry-compile-all"] + } + }, + "logging": { + "level": "info", + "logDirectory": "", + "noColor": false + } +} diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md new file mode 100644 index 000000000000..36b7b330ab0b --- /dev/null +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -0,0 +1,125 @@ +# Supertoken advanced testing + +## Overview + +This document defines a set of properties global to the supertoken ecosystem, for which we will: + +- run a [Medusa](https://github.com/crytic/medusa) fuzzing campaign, trying to break system invariants +- formally prove with [Halmos](https://github.com/a16z/halmos) whenever possible + +## 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 + +## Where to place the testing campaign + +Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already has invariant testing provided by foundry, it's not a trivial matter where to place this advanced testing campaign. Two alternatives are proposed: + +- including it in the mainline OP monorepo, in a subdirectory of the existing test contracts such as `test/invariants/medusa/superc20/` +- keep the campaign in wonderland's fork of the repository, in its own feature branch, in which case the deliverable would consist primarily of: + - a summary of the results, extending this document + - PRs with extra unit tests replicating found issues to the main repo where applicable + +## Contracts in scope + +- [ ] [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) (modifications to enable `convert` not yet merged) +- [ ] [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/OptimismSuperchainERC20.sol1) +- [ ] [OptimismSuperchainERC20Factory](https://github.com/defi-wonderland/optimism/pull/8/files#diff-09838f5703c353d0f7c5ff395acc04c1768ef58becac67404bc17e1fb0018517) (not yet merged) +- [ ] [L2StandardBridgeInterop](https://github.com/defi-wonderland/optimism/pull/10/files#diff-56cf869412631eac0a04a03f7d026596f64a1e00fcffa713bc770d67c6856c2f) (not yet merged) + +## Behavior assumed correct + +- [ ] inclusion of relay transactions +- [ ] sequencer implementation +- [ ] [OptimismMintableERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20.sol) +- [ ] [L2ToL2CrossDomainMessenger](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/L2CrossDomainMessenger.sol) +- [ ] [CrossL2Inbox](https://github.com/defi-wonderland/src/L2/CrossL2Inbox.sol) + +## Pain points + +- existing fuzzing tools use the same EVM to run the tested contracts as they do for asserting invariants, tracking ghost variables and everything else necessary to provision a fuzzing campaign. While this is usually very convenient, it means that we can’t assert on the behaviour/state of *different* chains from within a fuzzing campaign. This means we will have to walk around the requirement of supertokens having the same address across all chains, and implement a way to mock tokens existing in different chains. We will strive to formally prove it in a unitary fashion to mitigate this in properties 0 and 1 +- a buffer to represent 'in transit' messages should be implemented to assert on invariants relating to the non-atomicity of bridging from one chain to another. It is yet to be determined if it’ll be a FIFO queue (assuming ideal message ordering by sequencers) or it’ll have random-access capability to simulate messages arriving out of order + +## 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 | halmos | medusa | +| --- | --- | --- | --- | --- | +| 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 | [ ] | [ ] | + +## Valid state + +| id | milestone | description | halmos | medusa | +| --- | --- | --- | --- | --- | +| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [ ] | [ ] | +| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[ ]** | [ ] | + +## Variable transition + +| id | milestone | description | halmos | medusa | +| --- | --- | --- | --- | --- | +| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [ ] | [ ] | +| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [ ] | [ ] | +| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [ ] | [ ] | +| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ] | [ ] | +| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [ ] | [~] | +| 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 | halmos | medusa | +| --- | --- | --- | --- | --- | +| 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 | halmos | medusa | +| --- | --- | --- | --- | --- | +| 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) | [ ] | [~] | + +# 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) + +# Invariant-breaking candidates (brain dump) + +here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants + +- [ ] changing the decimals of tokens after deployment +- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol new file mode 100644 index 000000000000..0e3f819a6f06 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -0,0 +1,53 @@ +// 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 { + ///////////////////////////////////////////////////////// + // 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; + + function crossChainMessageReceiver( + address sender, + uint256 destinationChainId + ) + external + view + returns (OptimismSuperchainERC20) + { + return OptimismSuperchainERC20(superTokenAddresses[destinationChainId][superTokenInitDeploySalts[sender]]); + } + + function registerSupertoken(bytes32 deploySalt, uint256 chainId, address token) external { + superTokenAddresses[chainId][deploySalt] = token; + superTokenInitDeploySalts[token] = deploySalt; + } + + //////////////////////////////////////////////////////// + // 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 memory message) external { + address crossChainRecipient = superTokenAddresses[chainId][superTokenInitDeploySalts[msg.sender]]; + if (crossChainRecipient == msg.sender) { + require(false, "same chain"); + } + crossDomainMessageSender = crossChainRecipient; + crossDomainMessageSource = msg.sender; + SafeCall.call(crossDomainMessageSender, 0, message); + crossDomainMessageSender = address(0); + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol new file mode 100644 index 000000000000..dd169dc5748d --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -0,0 +1,93 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; + +contract ProtocolProperties is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + // TODO: will need rework after + // - non-atomic bridge + // - `convert` + /// @custom:property-id 24 + /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- + /// convert(super, legacy) + function property_totalSupplyAcrossChainsEqualsMints() external view { + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId = 0; validChainId < MAX_CHAINS; validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assert(trackedSupply == totalSupply); + } + } + + /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId + /// @custom:property-id 14 + /// @custom:property supertoken total supply starts at zero + function property_DeployNewSupertoken( + TokenDeployParams memory params, + uint256 chainId + ) + external + validateTokenDeployParams(params) + { + chainId = bound(chainId, 0, MAX_CHAINS - 1); + OptimismSuperchainERC20 supertoken = _deploySupertoken( + remoteTokens[params.remoteTokenIndex], + WORDS[params.nameIndex], + WORDS[params.symbolIndex], + DECIMALS[params.decimalsIndex], + chainId + ); + // 14 + assert(supertoken.totalSupply() == 0); + } + + /// @custom:property-id 22 + /// @custom:property sendERC20 decreases sender balance in source chain and increases receiver balance in + /// destination chain exactly by the input amount + /// @custom:property-id 23 + /// @custom:property sendERC20 decreases total supply in source chain and increases it in destination chain exactly + /// by the input amount + function property_SelfBridgeSupertoken(uint256 fromIndex, uint256 destinationChainId, uint256 amount) external { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + // TODO: when implementing non-atomic bridging, allow for the token to + // not yet be deployed and funds be recovered afterwards. + require(address(destinationToken) != address(0)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(msg.sender); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + uint256 destinationBalanceBefore = destinationToken.balanceOf(msg.sender); + uint256 destinationSupplyBefore = destinationToken.totalSupply(); + + vm.prank(msg.sender); + try sourceToken.sendERC20(msg.sender, amount, destinationChainId) { + uint256 sourceBalanceAfter = sourceToken.balanceOf(msg.sender); + uint256 destinationBalanceAfter = destinationToken.balanceOf(msg.sender); + // no free mint + assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); + // 22 + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + assert(destinationBalanceBefore + amount == destinationBalanceAfter); + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + uint256 destinationSupplyAfter = destinationToken.totalSupply(); + // 23 + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + assert(destinationSupplyBefore + amount == destinationSupplyAfter); + } catch { + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol new file mode 100644 index 000000000000..266650486e34 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol @@ -0,0 +1,122 @@ +// 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 { Predeploys } from "src/libraries/Predeploys.sol"; +import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; + +contract ProtocolHandler is TestBase, StdUtils { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + uint8 internal 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; + + constructor() { + vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); + superchainERC20Impl = new OptimismSuperchainERC20(); + 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); + } + } + } + + /// @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 { + 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); + // 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 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)); + // 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)); + } +} From 84b797e40efbc4a2326faeb5d6e56e8a48c3995a Mon Sep 17 00:00:00 2001 From: Disco <131301107+0xDiscotech@users.noreply.github.com> Date: Fri, 23 Aug 2024 13:22:01 -0300 Subject: [PATCH 02/11] 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 --- .gitmodules | 3 + packages/contracts-bedrock/foundry.toml | 8 +- packages/contracts-bedrock/halmos.toml | 15 ++ packages/contracts-bedrock/justfile | 7 + .../contracts-bedrock/lib/halmos-cheatcodes | 1 + .../test/invariants/PROPERTIES.md | 73 ++++++ .../test/properties/PROPERTIES.md | 23 +- .../properties/halmos/MockL2ToL2Messenger.sol | 25 ++ .../halmos/OptimismSuperchainERC20.t.sol | 237 ++++++++++++++++++ .../test/properties/helpers/HalmosBase.sol | 18 ++ 10 files changed, 398 insertions(+), 12 deletions(-) create mode 100644 packages/contracts-bedrock/halmos.toml create mode 160000 packages/contracts-bedrock/lib/halmos-cheatcodes create mode 100644 packages/contracts-bedrock/test/invariants/PROPERTIES.md create mode 100644 packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol create mode 100644 packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol create mode 100644 packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol diff --git a/.gitmodules b/.gitmodules index 21ecaedbb77a..222d45be7ccc 100644 --- a/.gitmodules +++ b/.gitmodules @@ -29,3 +29,6 @@ [submodule "packages/contracts-bedrock/lib/openzeppelin-contracts-v5"] path = packages/contracts-bedrock/lib/openzeppelin-contracts-v5 url = https://github.com/OpenZeppelin/openzeppelin-contracts +[submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"] + path = packages/contracts-bedrock/lib/halmos-cheatcodes + url = https://github.com/a16z/halmos-cheatcodes diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 08ae8840dc49..bd6910d7c911 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -21,7 +21,8 @@ remappings = [ 'ds-test/=lib/forge-std/lib/ds-test/src', 'safe-contracts/=lib/safe-contracts/contracts', 'kontrol-cheatcodes/=lib/kontrol-cheatcodes/src', - 'gelato/=lib/automate/contracts' + 'gelato/=lib/automate/contracts', + 'halmos-cheatcodes/=lib/halmos-cheatcodes/' ] extra_output = ['devdoc', 'userdoc', 'metadata', 'storageLayout'] bytecode_hash = 'none' @@ -102,3 +103,8 @@ script = 'test/kontrol/proofs' src = 'test/properties/medusa/' test = 'test/properties/medusa/' script = 'test/properties/medusa/' + +[profile.halmos] +src = 'test/properties/halmos/' +test = 'test/properties/halmos/' +script = 'test/properties/halmos/' diff --git a/packages/contracts-bedrock/halmos.toml b/packages/contracts-bedrock/halmos.toml new file mode 100644 index 000000000000..c431c6c3a532 --- /dev/null +++ b/packages/contracts-bedrock/halmos.toml @@ -0,0 +1,15 @@ +# Halmos configuration file + +## The version needed is `halmos 0.1.15.dev2+gc3f45dd` +## Just running `halmos` will run the tests with the default configuration + +[global] +# Contract to test +match-contract = "SymTest_" + +# Path to the Forge artifacts directory +forge_build_out = "./forge-artifacts" + + +# Storage layout +storage_layout = "generic" \ No newline at end of file diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile index 654ad64cadee..043a3650e3c2 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -29,6 +29,13 @@ test-kontrol-no-build: test-medusa timeout='100': FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}} + +test-halmos-all VERBOSE="-v": + FOUNDRY_PROFILE=halmos halmos {{VERBOSE}} + +test-halmos TEST VERBOSE="-v": + FOUNDRY_PROFILE=halmos halmos --function {{TEST}} {{VERBOSE}} + test-rerun: build-go-ffi forge test --rerun -vvv diff --git a/packages/contracts-bedrock/lib/halmos-cheatcodes b/packages/contracts-bedrock/lib/halmos-cheatcodes new file mode 160000 index 000000000000..c0d865508c0f --- /dev/null +++ b/packages/contracts-bedrock/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/packages/contracts-bedrock/test/invariants/PROPERTIES.md b/packages/contracts-bedrock/test/invariants/PROPERTIES.md new file mode 100644 index 000000000000..5a5cc71d73b5 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/PROPERTIES.md @@ -0,0 +1,73 @@ +# supertoken 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 | description | halmos | medusa | +| --- | ---------------------------------------------------------------------------------- | ------ | ------ | +| 0 | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | +| 1 | supertoken token address depends on name, remote token, address and decimals | [ ] | [ ] | +| 2 | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | [ ] | +| 3 | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | +| 4 | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | +| 5 | convert() burns the same amount of one token that it mints of the other | [ ] | [ ] | + +## Valid state + +| id | description | halmos | medusa | +| --- | ------------------------------------------------------------------------------------------ | ------- | ------ | +| 6 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | +| 7 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | + +## Variable transition + +| id | description | halmos | medusa | +| --- | ------------------------------------------------------------------------------------------------- | ------ | ------ | +| 8 | sendERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 9 | relayERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 10 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | +| 11 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | +| 12 | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [ ] | +| 13 | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | +| 14 | supertoken total supply starts at zero | [x] | [ ] | +| 15 | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | +| 16 | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | [ ] | + +## High level + +| id | description | halmos | medusa | +| --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | +| 17 | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | +| 18 | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | +| 19 | sum of total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | +| 20 | 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 | 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 | description | halmos | medusa | +| --- | ---------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | +| 22 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [x] | +| 23 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [x] | +| 24 | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | + +# 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) + +# Invariant-breaking candidates (brain dump) + +here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants + +- [ ] changing the decimals of tokens after deployment +- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 36b7b330ab0b..25dc9b036d3b 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -54,6 +54,7 @@ Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already h # 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 @@ -73,22 +74,22 @@ legend: ## Valid state -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [ ] | [ ] | -| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[ ]** | [ ] | +| id | milestone | description | halmos | medusa | +| --- | --- | --- | --- | --- | +| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | +| 7 | SupERC20 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | ## Variable transition | id | milestone | description | halmos | medusa | | --- | --- | --- | --- | --- | -| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [ ] | [ ] | -| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [ ] | [ ] | -| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [ ] | [ ] | -| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ] | [ ] | -| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [ ] | [~] | -| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [ ] | [ ] | -| 14 | SupERC20 | supertoken total supply starts at zero | [ ] | [x] | +| 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] | [ ] | +| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | +| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] | +| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | +| 14 | SupERC20 | supertoken total supply starts at zero | [x] | [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 | [ ] | [ ] | diff --git a/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol new file mode 100644 index 000000000000..fb8732f384f8 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + + +// TODO: Try to merge to a single mocked contract used by fuzzing and symbolic invariant tests - only if possible +// and low priorty +contract MockL2ToL2Messenger { + // Setting the current cross domain sender for the check of sender address equals the supertoken address + address internal immutable CROSS_DOMAIN_SENDER; + + constructor(address _xDomainSender) { + CROSS_DOMAIN_SENDER = _xDomainSender; + } + + function sendMessage(uint256 , address , bytes calldata) external payable { + } + + function crossDomainMessageSource() external view returns (uint256 _source) { + _source = block.chainid + 1; + } + + function crossDomainMessageSender() external view returns (address _sender) { + _sender = CROSS_DOMAIN_SENDER; + } +} diff --git a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol new file mode 100644 index 000000000000..a6285ac58e08 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol @@ -0,0 +1,237 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { SymTest } from "halmos-cheatcodes/src/SymTest.sol"; +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; +import { MockL2ToL2Messenger } from "./MockL2ToL2Messenger.sol"; +import { HalmosBase } from "../helpers/HalmosBase.sol"; + +contract SymTest_OptimismSuperchainERC20 is SymTest, HalmosBase { + MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); + + OptimismSuperchainERC20 public superchainERC20Impl; + OptimismSuperchainERC20 internal optimismSuperchainERC20; + + function setUp() public { + // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used + superchainERC20Impl = new OptimismSuperchainERC20(); + optimismSuperchainERC20 = OptimismSuperchainERC20( + address( + // TODO: Update to beacon proxy + new ERC1967Proxy( + address(superchainERC20Impl), + abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) + ) + ) + ); + + // Etch the mocked L2 to L2 Messenger since the messenger logic is out of scope for these test suite. Also, we + // avoid issues such as `TSTORE` opcode not being supported, or issues with `encodeVersionedNonce()` + address _mockL2ToL2CrossDomainMessenger = address(new MockL2ToL2Messenger(address(optimismSuperchainERC20))); + vm.etch(address(MESSENGER), _mockL2ToL2CrossDomainMessenger.code); + // NOTE: We need to set the crossDomainMessageSender as an immutable or otherwise storage vars and not taken + // into account when etching on halmos. Setting a constant slot with setters and getters didn't work neither. + } + + /// @notice Check setup works as expected + function check_setup() public view { + assert(optimismSuperchainERC20.remoteToken() == remoteToken); + assert(eqStrings(optimismSuperchainERC20.name(), name)); + assert(eqStrings(optimismSuperchainERC20.symbol(), symbol)); + assert(optimismSuperchainERC20.decimals() == decimals); + assert(MESSENGER.crossDomainMessageSender() == address(optimismSuperchainERC20)); + } + + /// @custom:property-id 6 + /// @custom:property Calls to sendERC20 succeed as long as caller has enough balance + function check_sendERC20SucceedsOnlyIfEnoughBalance( + uint256 _initialBalance, + address _from, + uint256 _amount, + address _to, + uint256 _chainId + ) + public + { + /* Preconditions */ + vm.assume(_chainId != CURRENT_CHAIN_ID); + vm.assume(_to != address(0)); + vm.assume(_from != address(0)); + + // Can't deal to unsupported cheatcode + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + optimismSuperchainERC20.mint(_from, _initialBalance); + + vm.prank(_from); + /* Action */ + try optimismSuperchainERC20.sendERC20(_to, _amount, _chainId) { + /* Postcondition */ + assert(_initialBalance >= _amount); + } catch { + assert(_initialBalance < _amount); + } + } + + /// @custom:property-id 7 + /// @custom:property Calls to relayERC20 always succeed as long as the sender the cross-domain caller are valid + function check_relayERC20OnlyFromL2ToL2Messenger( + address _crossDomainSender, + address _sender, + address _from, + address _to, + uint256 _amount + ) + public + { + /* Precondition */ + vm.assume(_to != address(0)); + // Deploying a new messenger because of an issue of not being able to etch the storage layout of the mock + // contract. So needed to a new one setting the symbolic immutable variable for the crossDomainSender. + vm.etch(address(MESSENGER), address(new MockL2ToL2Messenger(_crossDomainSender)).code); + + vm.prank(_sender); + /* Action */ + try optimismSuperchainERC20.relayERC20(_from, _to, _amount) { + /* Postconditions */ + assert( + _sender == address(MESSENGER) + && MESSENGER.crossDomainMessageSender() == address(optimismSuperchainERC20) + ); + } catch { + assert( + _sender != address(MESSENGER) + || MESSENGER.crossDomainMessageSender() != address(optimismSuperchainERC20) + ); + } + } + + /// @custom:property-id 8 + /// @custom:property `sendERC20` with a value of zero does not modify accounting + function check_sendERC20ZeroCall(address _from, address _to, uint256 _chainId) public { + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(_chainId != CURRENT_CHAIN_ID); + vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER)); + + uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); + uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); + + vm.startPrank(_from); + /* Action */ + optimismSuperchainERC20.sendERC20(_to, ZERO_AMOUNT, _chainId); + + /* Postcondition */ + assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore); + assert(optimismSuperchainERC20.balanceOf(_from) == _fromBalanceBefore); + } + + /// @custom:property-id 9 + /// @custom:property `relayERC20` with a value of zero does not modify accounting + function check_relayERC20ZeroCall(address _from, address _to) public { + uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); + /* Preconditions */ + uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); + uint256 _toBalanceBefore = optimismSuperchainERC20.balanceOf(_to); + vm.prank(address(MESSENGER)); + + /* Action */ + optimismSuperchainERC20.relayERC20(_from, _to, ZERO_AMOUNT); + + /* Postconditions */ + assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore); + assert(optimismSuperchainERC20.balanceOf(_from) == _fromBalanceBefore); + assert(optimismSuperchainERC20.balanceOf(_to) == _toBalanceBefore); + } + + /// @custom:property-id 10 + /// @custom:property `sendERC20` decreases the token's totalSupply in the source chain exactly by the input amount + function check_sendERC20DecreasesTotalSupply( + address _sender, + address _to, + uint256 _amount, + uint256 _chainId + ) + public + { + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(_chainId != CURRENT_CHAIN_ID); + + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + optimismSuperchainERC20.mint(_sender, _amount); + + uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); + uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_sender); + + vm.prank(_sender); + /* Action */ + optimismSuperchainERC20.sendERC20(_to, _amount, _chainId); + + /* Postconditions */ + assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore - _amount); + assert(optimismSuperchainERC20.balanceOf(_sender) == _balanceBefore - _amount); + } + + /// @custom:property-id 11 + /// @custom:property `relayERC20` increases the token's totalSupply in the destination chain exactly by the input + /// amount + function check_relayERC20IncreasesTotalSupply(address _from, address _to, uint256 _amount) public { + vm.assume(_to != address(0)); + + /* Preconditions */ + uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); + uint256 _toBalanceBefore = optimismSuperchainERC20.balanceOf(_to); + + vm.prank(address(MESSENGER)); + /* Action */ + optimismSuperchainERC20.relayERC20(_from, _to, _amount); + + /* Postconditions */ + assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore + _amount); + assert(optimismSuperchainERC20.balanceOf(_to) == _toBalanceBefore + _amount); + } + + /// @custom:property-id 12 + /// @custom:property Increases the total supply on the amount minted by the bridge + function check_mint(address _from, uint256 _amount) public { + /* Preconditions */ + uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); + uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_from); + + vm.startPrank(Predeploys.L2_STANDARD_BRIDGE); + /* Action */ + optimismSuperchainERC20.mint(_from, _amount); + + /* Postconditions */ + assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore + _amount); + assert(optimismSuperchainERC20.balanceOf(_from) == _balanceBefore + _amount); + } + + /// @custom:property-id 13 + /// @custom:property Supertoken total supply only decreases on the amount burned by the bridge + function check_burn(address _from, uint256 _amount) public { + /* Preconditions */ + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + optimismSuperchainERC20.mint(_from, _amount); + + uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); + uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_from); + + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + /* Action */ + optimismSuperchainERC20.burn(_from, _amount); + + /* Postconditions */ + assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore - _amount); + assert(optimismSuperchainERC20.balanceOf(_from) == _balanceBefore - _amount); + } + + /// @custom:property-id 14 + /// @custom:property Supertoken total supply starts at zero + function check_totalSupplyStartsAtZero() public view { + /* Postconditions */ + assert(optimismSuperchainERC20.totalSupply() == 0); + } +} diff --git a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol new file mode 100644 index 000000000000..75bfe2f7c9e1 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { Test } from "forge-std/Test.sol"; + +contract HalmosBase is Test { + uint256 internal constant CURRENT_CHAIN_ID = 1; + uint256 internal constant ZERO_AMOUNT = 0; + + address internal remoteToken = address(bytes20(keccak256("remoteToken"))); + string internal name = "SuperchainERC20"; + string internal symbol = "SUPER"; + uint8 internal decimals = 18; + + function eqStrings(string memory a, string memory b) internal pure returns (bool) { + return keccak256(abi.encode(a)) == keccak256(abi.encode(b)); + } +} From 8ad735a4aadd1c9450f5e4c4cc56e03d819f6e76 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 29 Aug 2024 17:56:12 -0300 Subject: [PATCH 03/11] test: remaining protocol properties (#26) * test: cross-user fuzzed bridges + actor setup * test: fuzz properties 8 and 9 * test: properties 7 and 25 * fix: implement doc's feedback * test: superc20 tob properties (#27) * chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady * chore: remove zero-initializations * fix: feedback from disco * chore: separate fuzz campaign tests in guided vs unguided * test: dont revert on successful unguided relay * test: add fuzzed calls to burn and mint * docs: document the separation of fuzz test functions * chore: move the properties file to its own directory * chore: consistently use fuzz_ and property_ + camelcase * chore: fix typo * chore: camelcase for handlers as well * fix: revert change that broke halmos campaign compile :D --- .gitmodules | 3 + packages/contracts-bedrock/foundry.toml | 1 + packages/contracts-bedrock/lib/properties | 1 + packages/contracts-bedrock/medusa.json | 6 +- .../test/properties/PROPERTIES.md | 27 +++- .../test/properties/helpers/Actors.t.sol | 38 +++++ .../MockL2ToL2CrossDomainMessenger.t.sol | 5 + ...imismSuperchainERC20ForToBProperties.t.sol | 10 ++ .../medusa/Protocol.properties.t.sol | 93 ------------- .../medusa/fuzz/Protocol.guided.t.sol | 130 ++++++++++++++++++ .../medusa/fuzz/Protocol.unguided.t.sol | 98 +++++++++++++ ...{Protocol.handler.t.sol => Protocol.t.sol} | 66 +++++++-- .../medusa/properties/Protocol.t.sol | 50 +++++++ 13 files changed, 419 insertions(+), 109 deletions(-) create mode 160000 packages/contracts-bedrock/lib/properties create mode 100644 packages/contracts-bedrock/test/properties/helpers/Actors.t.sol create mode 100644 packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol delete mode 100644 packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol create mode 100644 packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol create mode 100644 packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol rename packages/contracts-bedrock/test/properties/medusa/handlers/{Protocol.handler.t.sol => Protocol.t.sol} (70%) create mode 100644 packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol diff --git a/.gitmodules b/.gitmodules index 222d45be7ccc..7aacfd154993 100644 --- a/.gitmodules +++ b/.gitmodules @@ -32,3 +32,6 @@ [submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"] path = packages/contracts-bedrock/lib/halmos-cheatcodes url = https://github.com/a16z/halmos-cheatcodes +[submodule "packages/contracts-bedrock/lib/properties"] + path = packages/contracts-bedrock/lib/properties + url = https://github.com/crytic/properties diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index bd6910d7c911..9c12596b86ed 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -17,6 +17,7 @@ remappings = [ '@rari-capital/solmate/=lib/solmate', '@lib-keccak/=lib/lib-keccak/contracts/lib', '@solady/=lib/solady/src', + '@crytic/properties/=lib/properties/', 'forge-std/=lib/forge-std/src', 'ds-test/=lib/forge-std/lib/ds-test/src', 'safe-contracts/=lib/safe-contracts/contracts', diff --git a/packages/contracts-bedrock/lib/properties b/packages/contracts-bedrock/lib/properties new file mode 160000 index 000000000000..bb1b78542b3f --- /dev/null +++ b/packages/contracts-bedrock/lib/properties @@ -0,0 +1 @@ +Subproject commit bb1b78542b3f38e4ae56cf87389cd3ea94387f48 diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index cb4737956fea..60e10b641de0 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -55,7 +55,11 @@ ] }, "targetFunctionSignatures": [], - "excludeFunctionSignatures": [] + "excludeFunctionSignatures": [ + "ProtocolProperties.test_ERC20external_zeroAddressBalance()", + "ProtocolProperties.test_ERC20external_transferToZeroAddress()", + "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)" + ] }, "chainConfig": { "codeSizeCheckDisabled": true, diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 25dc9b036d3b..9771f6b936a8 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -71,20 +71,21 @@ legend: | 3 | Liquidity Migration | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | | 4 | Liquidity Migration | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | | 5 | Liquidity Migration | convert() burns the same amount of legacy token that it mints of supertoken, and viceversa | [ ] | [ ] | +| 25 | SupERC20 | supertokens can't be reinitialized | [ ] | [x] | ## Valid state -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | -| 7 | SupERC20 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | +| id | milestone | description | halmos | medusa | +| --- | --- | --- | --- | --- | +| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [x] | +| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[~]** | [~] | ## Variable transition | id | milestone | description | halmos | medusa | | --- | --- | --- | --- | --- | -| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | [ ] | -| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | [x] | +| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [x] | [x] | | 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | | 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | | 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] | @@ -116,7 +117,7 @@ It’s worth noting that these properties will not hold for a live system # Expected external interactions -- regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) +- [x] regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) # Invariant-breaking candidates (brain dump) @@ -124,3 +125,15 @@ here we’ll list possible interactions that we intend the fuzzing campaign to s - [ ] changing the decimals of tokens after deployment - [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols + +# Internal structure + +## Medusa campaign + +Fuzzing campaigns have both the need to push the contract into different states (state transitions) and assert properties are actually held. This defines a spectrum of function types: + +- `handler_`: they only transition the protocol state, and don't perform any assertions. +- `fuzz_`: they both transition the protocol state and perform assertions on properties. They are further divided in: + - unguided: they exist to let the fuzzer try novel or unexpected interactions, and potentially transition to unexpectedly invalid states + - guided: they have the goal of quickly covering code and moving the protocol to known valid states (eg: by moving funds between valid users) +- `property_`: they only assert the protocol is in a valid state, without causing a state transition. Note that they still use assertion-mode testing for simplicity, but could be migrated to run in property-mode. diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol new file mode 100644 index 000000000000..3a7400667518 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { StdUtils } from "forge-std/StdUtils.sol"; + +/// @notice helper for tracking actors, taking advantage of the fuzzer already using several `msg.sender`s +contract Actors is StdUtils { + mapping(address => bool) private _isActor; + address[] private _actors; + address private _currentActor; + + /// @notice register an actor if it's not already registered + /// usually called with msg.sender as a parameter, to track the actors + /// already provided by the fuzzer + modifier withActor(address who) { + addActor(who); + _currentActor = who; + _; + } + + function addActor(address who) internal { + if (!_isActor[who]) { + _isActor[who] = true; + _actors.push(who); + } + } + + /// @notice get the currently configured actor, should equal msg.sender + function currentActor() internal view returns (address) { + return _currentActor; + } + + /// @notice get one of the actors by index, useful to get another random + /// actor than the one set as currentActor, to perform operations between them + function getActorByRawIndex(uint256 rawIndex) internal view returns (address) { + return _actors[bound(rawIndex, 0, _actors.length - 1)]; + } +} diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol index 0e3f819a6f06..3bace13bc74a 100644 --- a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -28,6 +28,10 @@ contract MockL2ToL2CrossDomainMessenger { return OptimismSuperchainERC20(superTokenAddresses[destinationChainId][superTokenInitDeploySalts[sender]]); } + function setCrossDomainMessageSender(address sender) external { + crossDomainMessageSender = sender; + } + function registerSupertoken(bytes32 deploySalt, uint256 chainId, address token) external { superTokenAddresses[chainId][deploySalt] = token; superTokenInitDeploySalts[token] = deploySalt; @@ -49,5 +53,6 @@ contract MockL2ToL2CrossDomainMessenger { crossDomainMessageSource = msg.sender; SafeCall.call(crossDomainMessageSender, 0, message); crossDomainMessageSender = address(0); + crossDomainMessageSource = address(0); } } diff --git a/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol new file mode 100644 index 000000000000..145bf5ff01e5 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: AGPL-3 +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 { + /// @notice This is used by CryticERC20ExternalBasicProperties to know + // which properties to test + bool public constant isMintableOrBurnable = true; +} diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol deleted file mode 100644 index dd169dc5748d..000000000000 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ /dev/null @@ -1,93 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.25; - -import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol"; -import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; - -contract ProtocolProperties is ProtocolHandler { - using EnumerableMap for EnumerableMap.Bytes32ToUintMap; - - // TODO: will need rework after - // - non-atomic bridge - // - `convert` - /// @custom:property-id 24 - /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- - /// convert(super, legacy) - function property_totalSupplyAcrossChainsEqualsMints() external view { - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply = 0; - (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); - // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId = 0; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply); - } - } - - /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId - /// @custom:property-id 14 - /// @custom:property supertoken total supply starts at zero - function property_DeployNewSupertoken( - TokenDeployParams memory params, - uint256 chainId - ) - external - validateTokenDeployParams(params) - { - chainId = bound(chainId, 0, MAX_CHAINS - 1); - OptimismSuperchainERC20 supertoken = _deploySupertoken( - remoteTokens[params.remoteTokenIndex], - WORDS[params.nameIndex], - WORDS[params.symbolIndex], - DECIMALS[params.decimalsIndex], - chainId - ); - // 14 - assert(supertoken.totalSupply() == 0); - } - - /// @custom:property-id 22 - /// @custom:property sendERC20 decreases sender balance in source chain and increases receiver balance in - /// destination chain exactly by the input amount - /// @custom:property-id 23 - /// @custom:property sendERC20 decreases total supply in source chain and increases it in destination chain exactly - /// by the input amount - function property_SelfBridgeSupertoken(uint256 fromIndex, uint256 destinationChainId, uint256 amount) external { - destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); - fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); - OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); - OptimismSuperchainERC20 destinationToken = - MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); - // TODO: when implementing non-atomic bridging, allow for the token to - // not yet be deployed and funds be recovered afterwards. - require(address(destinationToken) != address(0)); - uint256 sourceBalanceBefore = sourceToken.balanceOf(msg.sender); - uint256 sourceSupplyBefore = sourceToken.totalSupply(); - uint256 destinationBalanceBefore = destinationToken.balanceOf(msg.sender); - uint256 destinationSupplyBefore = destinationToken.totalSupply(); - - vm.prank(msg.sender); - try sourceToken.sendERC20(msg.sender, amount, destinationChainId) { - uint256 sourceBalanceAfter = sourceToken.balanceOf(msg.sender); - uint256 destinationBalanceAfter = destinationToken.balanceOf(msg.sender); - // no free mint - assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); - // 22 - assert(sourceBalanceBefore - amount == sourceBalanceAfter); - assert(destinationBalanceBefore + amount == destinationBalanceAfter); - uint256 sourceSupplyAfter = sourceToken.totalSupply(); - uint256 destinationSupplyAfter = destinationToken.totalSupply(); - // 23 - assert(sourceSupplyBefore - amount == sourceSupplyAfter); - assert(destinationSupplyBefore + amount == destinationSupplyAfter); - } catch { - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); - } - } -} diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol new file mode 100644 index 000000000000..70f19d79361a --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol @@ -0,0 +1,130 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; + +contract ProtocolGuided is ProtocolHandler { + /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId + /// @custom:property-id 14 + /// @custom:property supertoken total supply starts at zero + function fuzz_deployNewSupertoken( + TokenDeployParams memory params, + uint256 chainId + ) + external + validateTokenDeployParams(params) + { + chainId = bound(chainId, 0, MAX_CHAINS - 1); + OptimismSuperchainERC20 supertoken = _deploySupertoken( + remoteTokens[params.remoteTokenIndex], + WORDS[params.nameIndex], + WORDS[params.symbolIndex], + DECIMALS[params.decimalsIndex], + chainId + ); + // 14 + assert(supertoken.totalSupply() == 0); + } + + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 22 + /// @custom:property sendERC20 decreases sender balance in source chain and increases receiver balance in + /// destination chain exactly by the input amount + /// @custom:property-id 23 + /// @custom:property sendERC20 decreases total supply in source chain and increases it in destination chain exactly + /// by the input amount + function fuzz_bridgeSupertoken( + uint256 fromIndex, + uint256 recipientIndex, + uint256 destinationChainId, + uint256 amount + ) + public + withActor(msg.sender) + { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); + address recipient = getActorByRawIndex(recipientIndex); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + // TODO: when implementing non-atomic bridging, allow for the token to + // not yet be deployed and funds be recovered afterwards. + require(address(destinationToken) != address(0)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient); + uint256 destinationSupplyBefore = destinationToken.totalSupply(); + + vm.prank(currentActor()); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); + uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); + // no free mint + assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); + // 22 + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + assert(destinationBalanceBefore + amount == destinationBalanceAfter); + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + uint256 destinationSupplyAfter = destinationToken.totalSupply(); + // 23 + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + assert(destinationSupplyBefore + amount == destinationSupplyAfter); + } catch { + // 6 + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 8 + /// @custom:property calls to sendERC20 with a value of zero dont modify accounting + // @notice is a subset of fuzz_bridgeSupertoken, so we'll just call it + // instead of re-implementing it. Keeping the function for visibility of the property. + function fuzz_sendZeroDoesNotModifyAccounting( + uint256 fromIndex, + uint256 recipientIndex, + uint256 destinationChainId + ) + external + { + fuzz_bridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0); + } + + /// @custom:property-id 9 + /// @custom:property calls to relayERC20 with a value of zero dont modify accounting + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + function fuzz_relayZeroDoesNotModifyAccounting( + uint256 fromIndex, + uint256 recipientIndex + ) + external + withActor(msg.sender) + { + fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); + address recipient = getActorByRawIndex(recipientIndex); + OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + uint256 balanceSenderBefore = token.balanceOf(currentActor()); + uint256 balanceRecipientBefore = token.balanceOf(recipient); + uint256 supplyBefore = token.totalSupply(); + + MESSENGER.setCrossDomainMessageSender(address(token)); + vm.prank(address(MESSENGER)); + try token.relayERC20(currentActor(), recipient, 0) { + MESSENGER.setCrossDomainMessageSender(address(0)); + } catch { + // should not revert because of 7, and if it *does* revert, I want the test suite + // to discard the sequence instead of potentially getting another + // error due to the crossDomainMessageSender being manually set + assert(false); + } + uint256 balanceSenderAfter = token.balanceOf(currentActor()); + uint256 balanceRecipeintAfter = token.balanceOf(recipient); + uint256 supplyAfter = token.totalSupply(); + assert(balanceSenderBefore == balanceSenderAfter); + assert(balanceRecipientBefore == balanceRecipeintAfter); + assert(supplyBefore == supplyAfter); + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol new file mode 100644 index 000000000000..17158e0f8732 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +// TODO: add fuzz_sendERC20 when we implement non-atomic bridging +contract ProtocolUnguided is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + /// @notice this ensures actors cant simply call relayERC20 and get tokens, no matter the system state + /// but there's still some possible work on how hard we can bork the system state with handlers calling + /// the L2ToL2CrossDomainMessenger or bridge directly (pending on non-atomic bridging) + function fuzz_relayERC20( + uint256 tokenIndex, + address sender, + address crossDomainMessageSender, + address recipient, + uint256 amount + ) + external + { + MESSENGER.setCrossDomainMessageSender(crossDomainMessageSender); + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + vm.prank(sender); + try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) { + MESSENGER.setCrossDomainMessageSender(address(0)); + assert(sender == address(MESSENGER)); + assert(crossDomainMessageSender == token); + // this increases the supply across chains without a call to + // `mint` by the MESSENGER, so it kind of breaks an invariant, but + // let's walk around that: + bytes32 salt = MESSENGER.superTokenInitDeploySalts(token); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); + } catch { + assert(sender != address(MESSENGER) || crossDomainMessageSender != token); + MESSENGER.setCrossDomainMessageSender(address(0)); + } + } + + /// @custom:property-id 12 + /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge + function fuzz_mint(uint256 tokenIndex, address to, address sender, uint256 amount) external { + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + bytes32 salt = MESSENGER.superTokenInitDeploySalts(token); + amount = bound(amount, 0, type(uint256).max - OptimismSuperchainERC20(token).totalSupply()); + vm.prank(sender); + try OptimismSuperchainERC20(token).mint(to, amount) { + assert(sender == BRIDGE); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + } catch { + assert(sender != BRIDGE); + } + } + + + /// @custom:property-id 13 + /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge + function fuzz_burn(uint256 tokenIndex, address from, address sender, uint256 amount) external { + address token = allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]; + bytes32 salt = MESSENGER.superTokenInitDeploySalts(token); + uint256 senderBalance = OptimismSuperchainERC20(token).balanceOf(sender); + vm.prank(sender); + try OptimismSuperchainERC20(token).burn(from, amount) { + assert(sender == BRIDGE); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); + ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + } catch { + assert(sender != BRIDGE || senderBalance < amount); + } + } + + /// @custom:property-id 25 + /// @custom:property supertokens can't be reinitialized + function fuzz_initialize( + address sender, + uint256 tokenIndex, + address remoteToken, + string memory name, + string memory symbol, + uint8 decimals + ) + external + { + vm.prank(sender); + // revert is possible in bound, but is not part of the external call + try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize( + remoteToken, name, symbol, decimals + ) { + assert(false); + } catch { } + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol similarity index 70% rename from packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol rename to packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol index 266650486e34..1109b682c063 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol @@ -7,10 +7,12 @@ import { StdUtils } from "forge-std/StdUtils.sol"; import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { OptimismSuperchainERC20ForToBProperties } from "../../helpers/OptimismSuperchainERC20ForToBProperties.t.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; +import { Actors } from "../../helpers/Actors.t.sol"; -contract ProtocolHandler is TestBase, StdUtils { +contract ProtocolHandler is TestBase, StdUtils, Actors { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; uint8 internal constant MAX_CHAINS = 4; @@ -36,18 +38,20 @@ contract ProtocolHandler is TestBase, StdUtils { address[] internal remoteTokens; address[] internal allSuperTokens; - //@notice 'real' deploy salt => total supply sum across chains + /// @notice 'real' deploy salt => total supply sum across chains EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains; constructor() { vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); - superchainERC20Impl = new OptimismSuperchainERC20(); - for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { + superchainERC20Impl = new OptimismSuperchainERC20ForToBProperties(); + for (uint256 remoteTokenIndex; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { _deployRemoteToken(); - for (uint256 supertokenChainId = 0; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) { + for (uint256 supertokenChainId; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) { _deploySupertoken(remoteTokens[remoteTokenIndex], WORDS[0], WORDS[0], DECIMALS[0], supertokenChainId); } } + // integrate with all ToB properties using address(this) as the sender + addActor(address(this)); } /// @notice the deploy params are _indexes_ to pick from a pre-defined array of options and limit @@ -62,24 +66,70 @@ contract ProtocolHandler is TestBase, StdUtils { _; } - function handler_MockNewRemoteToken() external { + function handler_mockNewRemoteToken() external { _deployRemoteToken(); } /// @notice pick one already-deployed supertoken and mint an arbitrary amount of it /// necessary so there is something to be bridged :D /// TODO: will be replaced when testing the factories and `convert()` - function handler_MintSupertoken(uint256 index, uint96 amount) external { + function handler_mintSupertoken(uint256 index, uint96 amount) external withActor(msg.sender) { index = bound(index, 0, allSuperTokens.length - 1); address addr = allSuperTokens[index]; vm.prank(BRIDGE); // medusa calls with different senders by default - OptimismSuperchainERC20(addr).mint(msg.sender, amount); + OptimismSuperchainERC20(addr).mint(currentActor(), amount); // currentValue will be zero if key is not present (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr)); ghost_totalSupplyAcrossChains.set(MESSENGER.superTokenInitDeploySalts(addr), currentValue + amount); } + /// @notice The ToB properties don't preclude the need for this since they + /// always use address(this) as the caller, which won't get any balance + /// until it's transferred to it somehow + function handler_supERC20Transfer( + uint256 tokenIndex, + uint256 toIndex, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer( + getActorByRawIndex(toIndex), amount + ); + } + + function handler_supERC20TransferFrom( + uint256 tokenIndex, + uint256 fromIndex, + uint256 toIndex, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transferFrom( + getActorByRawIndex(fromIndex), getActorByRawIndex(toIndex), amount + ); + } + + function handler_supERC20Approve( + uint256 tokenIndex, + uint256 spenderIndex, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).approve( + getActorByRawIndex(spenderIndex), amount + ); + } + /// @notice deploy a remote token, that supertokens will be a representation of. They are never called, so there /// is no need to actually deploy a contract for them function _deployRemoteToken() internal { diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol new file mode 100644 index 000000000000..4f79e78665c7 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { ProtocolGuided } from "../fuzz/Protocol.guided.t.sol"; +import { ProtocolUnguided } from "../fuzz/Protocol.unguided.t.sol"; +import { CryticERC20ExternalBasicProperties } from + "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; + +contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20ExternalBasicProperties { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + + /// @dev `token` is the token under test for the ToB properties. This is coupled + /// to the ProtocolSetup constructor initializing at least one supertoken + constructor() { + token = ITokenMock(allSuperTokens[0]); + } + + /// @dev not that much of a handler, since this only changes which + /// supertoken the ToB assertions are performed against. Thankfully, they are + /// implemented in a way that don't require tracking ghost variables or can + /// break properties defined by us + function handler_ToBTestOtherToken(uint256 index) external { + token = ITokenMock(allSuperTokens[bound(index, 0, allSuperTokens.length - 1)]); + } + + // TODO: will need rework after + // - non-atomic bridge + // - `convert` + /// @custom:property-id 24 + /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- + /// convert(super, legacy) + function property_totalSupplyAcrossChainsEqualsMints() external view { + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply; + (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId; validChainId < MAX_CHAINS; validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assert(trackedSupply == totalSupply); + } + } +} From 9f1e4f706e3927e3133557d65f03133e89e37820 Mon Sep 17 00:00:00 2001 From: teddy Date: Mon, 2 Sep 2024 15:25:08 -0300 Subject: [PATCH 04/11] 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 --- packages/contracts-bedrock/foundry.toml | 1 + packages/contracts-bedrock/medusa.json | 2 +- .../test/properties/PROPERTIES.md | 8 +- .../MockL2ToL2CrossDomainMessenger.t.sol | 72 +++++++++++++-- .../medusa/fuzz/Protocol.guided.t.sol | 88 +++++++++++++++++-- .../medusa/fuzz/Protocol.unguided.t.sol | 44 +++++++++- .../properties/medusa/handlers/Protocol.t.sol | 2 + .../medusa/properties/Protocol.t.sol | 36 ++++++-- 8 files changed, 228 insertions(+), 25 deletions(-) diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 9c12596b86ed..db03bacb4719 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -104,6 +104,7 @@ script = 'test/kontrol/proofs' src = 'test/properties/medusa/' test = 'test/properties/medusa/' script = 'test/properties/medusa/' +via-ir=true [profile.halmos] src = 'test/properties/halmos/' diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index 60e10b641de0..5df25c2cd63b 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -3,7 +3,7 @@ "workers": 10, "workerResetLimit": 50, "timeout": 0, - "testLimit": 500000, + "testLimit": 0, "callSequenceLength": 100, "corpusDirectory": "test/properties/medusa/corpus/", "coverageEnabled": true, diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 9771f6b936a8..d915d565633e 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -86,7 +86,9 @@ legend: | --- | --- | --- | --- | --- | | 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | [x] | | 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [x] | [x] | -| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | +| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [x] | +| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [ ] | [x] | +| 27 | SupERC20 | relayERC20 increases sender's balance in the destination chain exactly by the input amount | [ ] | [x] | | 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | | 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] | | 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | @@ -100,9 +102,9 @@ legend: | --- | --- | --- | --- | --- | | 17 | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | | 18 | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | -| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | +| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | | 20 | SupERC20 | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ] | [ ] | -| 21 | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [ ] | +| 21 | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [~] | ## Atomic bridging pseudo-properties diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol index 3bace13bc74a..6eb1c30e6799 100644 --- a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -5,6 +5,17 @@ import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { SafeCall } from "src/libraries/SafeCall.sol"; contract MockL2ToL2CrossDomainMessenger { + //////////////////////// + // type definitions // + //////////////////////// + struct CrossChainMessage { + address crossDomainMessageSender; + address crossDomainMessageSource; + bytes payload; + address recipient; + uint256 amount; + } + ///////////////////////////////////////////////////////// // State vars mocking the L2toL2CrossDomainMessenger // ///////////////////////////////////////////////////////// @@ -17,6 +28,13 @@ contract MockL2ToL2CrossDomainMessenger { mapping(address supertoken => bytes32 deploySalt) public superTokenInitDeploySalts; mapping(uint256 chainId => mapping(bytes32 deploySalt => address supertoken)) public superTokenAddresses; + CrossChainMessage[] private _messageQueue; + bool private _atomic; + + function messageQueue(uint256 rawIndex) external view returns (CrossChainMessage memory) { + return _messageQueue[rawIndex % _messageQueue.length]; + } + function crossChainMessageReceiver( address sender, uint256 destinationChainId @@ -37,6 +55,30 @@ contract MockL2ToL2CrossDomainMessenger { superTokenInitDeploySalts[token] = deploySalt; } + function messageQueueLength() public view returns (uint256) { + return _messageQueue.length; + } + + function setAtomic(bool atomic) public { + _atomic = atomic; + } + + function relayMessageFromQueue(uint256 rawIndex) public { + uint256 index = rawIndex % _messageQueue.length; + CrossChainMessage memory message = _messageQueue[index]; + _messageQueue[index] = _messageQueue[_messageQueue.length - 1]; + _messageQueue.pop(); + _relayMessage(message); + } + + function _relayMessage(CrossChainMessage memory message) internal { + crossDomainMessageSender = message.crossDomainMessageSender; + crossDomainMessageSource = message.crossDomainMessageSource; + SafeCall.call(crossDomainMessageSender, 0, message.payload); + crossDomainMessageSender = address(0); + crossDomainMessageSource = address(0); + } + //////////////////////////////////////////////////////// // Functions mocking the L2toL2CrossDomainMessenger // //////////////////////////////////////////////////////// @@ -44,15 +86,33 @@ contract MockL2ToL2CrossDomainMessenger { /// @notice recipient will not be used since in normal execution it's the same /// address on a different chain, but here we have to compute it to mock /// cross-chain messaging - function sendMessage(uint256 chainId, address, /*recipient*/ bytes memory message) external { + function sendMessage(uint256 chainId, address, /*recipient*/ bytes calldata data) external { address crossChainRecipient = superTokenAddresses[chainId][superTokenInitDeploySalts[msg.sender]]; if (crossChainRecipient == msg.sender) { require(false, "same chain"); } - crossDomainMessageSender = crossChainRecipient; - crossDomainMessageSource = msg.sender; - SafeCall.call(crossDomainMessageSender, 0, message); - crossDomainMessageSender = address(0); - crossDomainMessageSource = address(0); + (address recipient, uint256 amount) = _decodePayload(data); + + CrossChainMessage memory message = CrossChainMessage({ + crossDomainMessageSender: crossChainRecipient, + crossDomainMessageSource: msg.sender, + payload: data, + recipient: recipient, + amount: amount + }); + + if (_atomic) { + _relayMessage(message); + } else { + _messageQueue.push(message); + } + } + + //////////////////////// + // Internal helpers // + //////////////////////// + + function _decodePayload(bytes calldata payload) internal pure returns (address recipient, uint256 amount) { + (, recipient, amount) = abi.decode(payload[4:], (address, address, uint256)); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol index 70f19d79361a..d5b5d8b5edc5 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol @@ -1,10 +1,13 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.25; +import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; contract ProtocolGuided is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId /// @custom:property-id 14 /// @custom:property supertoken total supply starts at zero @@ -35,7 +38,7 @@ contract ProtocolGuided is ProtocolHandler { /// @custom:property-id 23 /// @custom:property sendERC20 decreases total supply in source chain and increases it in destination chain exactly /// by the input amount - function fuzz_bridgeSupertoken( + function fuzz_bridgeSupertokenAtomic( uint256 fromIndex, uint256 recipientIndex, uint256 destinationChainId, @@ -50,16 +53,15 @@ contract ProtocolGuided is ProtocolHandler { OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); OptimismSuperchainERC20 destinationToken = MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); - // TODO: when implementing non-atomic bridging, allow for the token to - // not yet be deployed and funds be recovered afterwards. - require(address(destinationToken) != address(0)); uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); uint256 sourceSupplyBefore = sourceToken.totalSupply(); uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient); uint256 destinationSupplyBefore = destinationToken.totalSupply(); + MESSENGER.setAtomic(true); vm.prank(currentActor()); try sourceToken.sendERC20(recipient, amount, destinationChainId) { + MESSENGER.setAtomic(false); uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); // no free mint @@ -73,14 +75,86 @@ contract ProtocolGuided is ProtocolHandler { assert(sourceSupplyBefore - amount == sourceSupplyAfter); assert(destinationSupplyBefore + amount == destinationSupplyAfter); } catch { + MESSENGER.setAtomic(false); // 6 assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 26 + /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount + /// @custom:property-id 10 + /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount + function fuzz_sendERC20( + uint256 fromIndex, + uint256 recipientIndex, + uint256 destinationChainId, + uint256 amount + ) + public + withActor(msg.sender) + { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); + address recipient = getActorByRawIndex(recipientIndex); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + + vm.prank(currentActor()); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); + // 26 + uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + // 10 + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + } catch { + // 6 + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 11 + /// @custom:property relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount + /// @custom:property-id 27 + /// @custom:property relayERC20 increases sender's balance in the destination chain exactly by the input amount + /// @custom:property-id 7 + /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + function fuzz_relayERC20(uint256 messageIndex) external { + MockL2ToL2CrossDomainMessenger.CrossChainMessage memory messageToRelay = MESSENGER.messageQueue(messageIndex); + OptimismSuperchainERC20 destinationToken = OptimismSuperchainERC20(messageToRelay.crossDomainMessageSender); + uint256 destinationSupplyBefore = destinationToken.totalSupply(); + uint256 destinationBalanceBefore = destinationToken.balanceOf(messageToRelay.recipient); + + try MESSENGER.relayMessageFromQueue(messageIndex) { + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken)); + (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + // if sendERC20 didnt intialize this, then test suite is broken + assert(success); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount); + // 11 + assert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); + // 27 + assert( + destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient) + ); + } catch { + // 7 + assert(false); + } + } + /// @custom:property-id 8 /// @custom:property calls to sendERC20 with a value of zero dont modify accounting - // @notice is a subset of fuzz_bridgeSupertoken, so we'll just call it + // @notice is a subset of fuzz_sendERC20, so we'll just call it // instead of re-implementing it. Keeping the function for visibility of the property. function fuzz_sendZeroDoesNotModifyAccounting( uint256 fromIndex, @@ -89,13 +163,15 @@ contract ProtocolGuided is ProtocolHandler { ) external { - fuzz_bridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0); + fuzz_sendERC20(fromIndex, recipientIndex, destinationChainId, 0); } /// @custom:property-id 9 /// @custom:property calls to relayERC20 with a value of zero dont modify accounting /// @custom:property-id 7 /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid + /// @notice cant call fuzz_RelayERC20 internally since that pops a + /// random message, which we cannot guarantee has a value of zero function fuzz_relayZeroDoesNotModifyAccounting( uint256 fromIndex, uint256 recipientIndex diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol index 17158e0f8732..71ba64118088 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol @@ -42,6 +42,46 @@ contract ProtocolUnguided is ProtocolHandler { } } + /// @custom:property-id 6 + /// @custom:property calls to sendERC20 succeed as long as caller has enough balance + /// @custom:property-id 26 + /// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount + /// @custom:property-id 10 + /// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount + function fuzz_sendERC20( + address sender, + address recipient, + uint256 fromIndex, + uint256 destinationChainId, + uint256 amount + ) + public + { + destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); + OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); + OptimismSuperchainERC20 destinationToken = + MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); + bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken)); + uint256 sourceBalanceBefore = sourceToken.balanceOf(sender); + uint256 sourceSupplyBefore = sourceToken.totalSupply(); + + vm.prank(sender); + try sourceToken.sendERC20(recipient, amount, destinationChainId) { + (, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); + ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); + // 26 + uint256 sourceBalanceAfter = sourceToken.balanceOf(sender); + assert(sourceBalanceBefore - amount == sourceBalanceAfter); + // 10 + uint256 sourceSupplyAfter = sourceToken.totalSupply(); + assert(sourceSupplyBefore - amount == sourceSupplyAfter); + } catch { + // 6 + assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + } + } + + /// @custom:property-id 12 /// @custom:property supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge function fuzz_mint(uint256 tokenIndex, address to, address sender, uint256 amount) external { @@ -52,9 +92,9 @@ contract ProtocolUnguided is ProtocolHandler { try OptimismSuperchainERC20(token).mint(to, amount) { assert(sender == BRIDGE); (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); - ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); + ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); } catch { - assert(sender != BRIDGE); + assert(sender != BRIDGE || to == address(0)); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol index 1109b682c063..191c5c44a7e6 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol @@ -40,6 +40,8 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { /// @notice 'real' deploy salt => total supply sum across chains EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains; + /// @notice 'real' deploy salt => tokens sendERC20'd but not yet relayERC20'd + EnumerableMap.Bytes32ToUintMap internal ghost_tokensInTransit; constructor() { vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol index 4f79e78665c7..7b2f73d54058 100644 --- a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol @@ -27,18 +27,40 @@ contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20Exte } // TODO: will need rework after - // - non-atomic bridge // - `convert` - /// @custom:property-id 24 - /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- + /// @custom:property-id 19 + /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)- /// convert(super, legacy) - function property_totalSupplyAcrossChainsEqualsMints() external view { + function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view { // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply; + for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply ; (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + (, uint256 fundsInTransit) = ghost_tokensInTransit.tryGet(currentSalt); // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId; validChainId < MAX_CHAINS; validChainId++) { + for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assert(trackedSupply == totalSupply + fundsInTransit); + } + } + + // TODO: will need rework after + // - `convert` + /// @custom:property-id 21 + /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)- + /// convert(super, legacy) when all when all cross-chain messages are processed + function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view { + require(MESSENGER.messageQueueLength() == 0); + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply ; + (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); if (supertoken != address(0)) { totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); From 2359022f1a049bae7c6f31961d25469389555b47 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 3 Sep 2024 18:45:28 -0300 Subject: [PATCH 05/11] chore: remove halmos testsuite --- .gitmodules | 3 - packages/contracts-bedrock/foundry.toml | 6 - packages/contracts-bedrock/halmos.toml | 15 -- packages/contracts-bedrock/justfile | 7 - .../contracts-bedrock/lib/halmos-cheatcodes | 1 - .../properties/halmos/MockL2ToL2Messenger.sol | 25 -- .../halmos/OptimismSuperchainERC20.t.sol | 237 ------------------ .../test/properties/helpers/HalmosBase.sol | 18 -- 8 files changed, 312 deletions(-) delete mode 100644 packages/contracts-bedrock/halmos.toml delete mode 160000 packages/contracts-bedrock/lib/halmos-cheatcodes delete mode 100644 packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol delete mode 100644 packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol delete mode 100644 packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol diff --git a/.gitmodules b/.gitmodules index 7aacfd154993..dca839eef08e 100644 --- a/.gitmodules +++ b/.gitmodules @@ -29,9 +29,6 @@ [submodule "packages/contracts-bedrock/lib/openzeppelin-contracts-v5"] path = packages/contracts-bedrock/lib/openzeppelin-contracts-v5 url = https://github.com/OpenZeppelin/openzeppelin-contracts -[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 db03bacb4719..6dde1ebbceb5 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -23,7 +23,6 @@ remappings = [ 'safe-contracts/=lib/safe-contracts/contracts', 'kontrol-cheatcodes/=lib/kontrol-cheatcodes/src', 'gelato/=lib/automate/contracts', - 'halmos-cheatcodes/=lib/halmos-cheatcodes/' ] extra_output = ['devdoc', 'userdoc', 'metadata', 'storageLayout'] bytecode_hash = 'none' @@ -105,8 +104,3 @@ src = 'test/properties/medusa/' test = 'test/properties/medusa/' script = 'test/properties/medusa/' via-ir=true - -[profile.halmos] -src = 'test/properties/halmos/' -test = 'test/properties/halmos/' -script = 'test/properties/halmos/' diff --git a/packages/contracts-bedrock/halmos.toml b/packages/contracts-bedrock/halmos.toml deleted file mode 100644 index c431c6c3a532..000000000000 --- a/packages/contracts-bedrock/halmos.toml +++ /dev/null @@ -1,15 +0,0 @@ -# Halmos configuration file - -## The version needed is `halmos 0.1.15.dev2+gc3f45dd` -## Just running `halmos` will run the tests with the default configuration - -[global] -# Contract to test -match-contract = "SymTest_" - -# Path to the Forge artifacts directory -forge_build_out = "./forge-artifacts" - - -# Storage layout -storage_layout = "generic" \ No newline at end of file diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile index 043a3650e3c2..654ad64cadee 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -29,13 +29,6 @@ test-kontrol-no-build: test-medusa timeout='100': FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}} - -test-halmos-all VERBOSE="-v": - FOUNDRY_PROFILE=halmos halmos {{VERBOSE}} - -test-halmos TEST VERBOSE="-v": - FOUNDRY_PROFILE=halmos halmos --function {{TEST}} {{VERBOSE}} - test-rerun: build-go-ffi forge test --rerun -vvv diff --git a/packages/contracts-bedrock/lib/halmos-cheatcodes b/packages/contracts-bedrock/lib/halmos-cheatcodes deleted file mode 160000 index c0d865508c0f..000000000000 --- a/packages/contracts-bedrock/lib/halmos-cheatcodes +++ /dev/null @@ -1 +0,0 @@ -Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol deleted file mode 100644 index fb8732f384f8..000000000000 --- a/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol +++ /dev/null @@ -1,25 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity 0.8.25; - - -// TODO: Try to merge to a single mocked contract used by fuzzing and symbolic invariant tests - only if possible -// and low priorty -contract MockL2ToL2Messenger { - // Setting the current cross domain sender for the check of sender address equals the supertoken address - address internal immutable CROSS_DOMAIN_SENDER; - - constructor(address _xDomainSender) { - CROSS_DOMAIN_SENDER = _xDomainSender; - } - - function sendMessage(uint256 , address , bytes calldata) external payable { - } - - function crossDomainMessageSource() external view returns (uint256 _source) { - _source = block.chainid + 1; - } - - function crossDomainMessageSender() external view returns (address _sender) { - _sender = CROSS_DOMAIN_SENDER; - } -} diff --git a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol deleted file mode 100644 index a6285ac58e08..000000000000 --- a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol +++ /dev/null @@ -1,237 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity 0.8.25; - -import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -import { SymTest } from "halmos-cheatcodes/src/SymTest.sol"; -import { Predeploys } from "src/libraries/Predeploys.sol"; -import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; -import { MockL2ToL2Messenger } from "./MockL2ToL2Messenger.sol"; -import { HalmosBase } from "../helpers/HalmosBase.sol"; - -contract SymTest_OptimismSuperchainERC20 is SymTest, HalmosBase { - MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - - OptimismSuperchainERC20 public superchainERC20Impl; - OptimismSuperchainERC20 internal optimismSuperchainERC20; - - function setUp() public { - // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used - superchainERC20Impl = new OptimismSuperchainERC20(); - optimismSuperchainERC20 = OptimismSuperchainERC20( - address( - // TODO: Update to beacon proxy - new ERC1967Proxy( - address(superchainERC20Impl), - abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) - ) - ) - ); - - // Etch the mocked L2 to L2 Messenger since the messenger logic is out of scope for these test suite. Also, we - // avoid issues such as `TSTORE` opcode not being supported, or issues with `encodeVersionedNonce()` - address _mockL2ToL2CrossDomainMessenger = address(new MockL2ToL2Messenger(address(optimismSuperchainERC20))); - vm.etch(address(MESSENGER), _mockL2ToL2CrossDomainMessenger.code); - // NOTE: We need to set the crossDomainMessageSender as an immutable or otherwise storage vars and not taken - // into account when etching on halmos. Setting a constant slot with setters and getters didn't work neither. - } - - /// @notice Check setup works as expected - function check_setup() public view { - assert(optimismSuperchainERC20.remoteToken() == remoteToken); - assert(eqStrings(optimismSuperchainERC20.name(), name)); - assert(eqStrings(optimismSuperchainERC20.symbol(), symbol)); - assert(optimismSuperchainERC20.decimals() == decimals); - assert(MESSENGER.crossDomainMessageSender() == address(optimismSuperchainERC20)); - } - - /// @custom:property-id 6 - /// @custom:property Calls to sendERC20 succeed as long as caller has enough balance - function check_sendERC20SucceedsOnlyIfEnoughBalance( - uint256 _initialBalance, - address _from, - uint256 _amount, - address _to, - uint256 _chainId - ) - public - { - /* Preconditions */ - vm.assume(_chainId != CURRENT_CHAIN_ID); - vm.assume(_to != address(0)); - vm.assume(_from != address(0)); - - // Can't deal to unsupported cheatcode - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - optimismSuperchainERC20.mint(_from, _initialBalance); - - vm.prank(_from); - /* Action */ - try optimismSuperchainERC20.sendERC20(_to, _amount, _chainId) { - /* Postcondition */ - assert(_initialBalance >= _amount); - } catch { - assert(_initialBalance < _amount); - } - } - - /// @custom:property-id 7 - /// @custom:property Calls to relayERC20 always succeed as long as the sender the cross-domain caller are valid - function check_relayERC20OnlyFromL2ToL2Messenger( - address _crossDomainSender, - address _sender, - address _from, - address _to, - uint256 _amount - ) - public - { - /* Precondition */ - vm.assume(_to != address(0)); - // Deploying a new messenger because of an issue of not being able to etch the storage layout of the mock - // contract. So needed to a new one setting the symbolic immutable variable for the crossDomainSender. - vm.etch(address(MESSENGER), address(new MockL2ToL2Messenger(_crossDomainSender)).code); - - vm.prank(_sender); - /* Action */ - try optimismSuperchainERC20.relayERC20(_from, _to, _amount) { - /* Postconditions */ - assert( - _sender == address(MESSENGER) - && MESSENGER.crossDomainMessageSender() == address(optimismSuperchainERC20) - ); - } catch { - assert( - _sender != address(MESSENGER) - || MESSENGER.crossDomainMessageSender() != address(optimismSuperchainERC20) - ); - } - } - - /// @custom:property-id 8 - /// @custom:property `sendERC20` with a value of zero does not modify accounting - function check_sendERC20ZeroCall(address _from, address _to, uint256 _chainId) public { - /* Preconditions */ - vm.assume(_to != address(0)); - vm.assume(_chainId != CURRENT_CHAIN_ID); - vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER)); - - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); - - vm.startPrank(_from); - /* Action */ - optimismSuperchainERC20.sendERC20(_to, ZERO_AMOUNT, _chainId); - - /* Postcondition */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore); - assert(optimismSuperchainERC20.balanceOf(_from) == _fromBalanceBefore); - } - - /// @custom:property-id 9 - /// @custom:property `relayERC20` with a value of zero does not modify accounting - function check_relayERC20ZeroCall(address _from, address _to) public { - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - /* Preconditions */ - uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); - uint256 _toBalanceBefore = optimismSuperchainERC20.balanceOf(_to); - vm.prank(address(MESSENGER)); - - /* Action */ - optimismSuperchainERC20.relayERC20(_from, _to, ZERO_AMOUNT); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore); - assert(optimismSuperchainERC20.balanceOf(_from) == _fromBalanceBefore); - assert(optimismSuperchainERC20.balanceOf(_to) == _toBalanceBefore); - } - - /// @custom:property-id 10 - /// @custom:property `sendERC20` decreases the token's totalSupply in the source chain exactly by the input amount - function check_sendERC20DecreasesTotalSupply( - address _sender, - address _to, - uint256 _amount, - uint256 _chainId - ) - public - { - /* Preconditions */ - vm.assume(_to != address(0)); - vm.assume(_chainId != CURRENT_CHAIN_ID); - - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - optimismSuperchainERC20.mint(_sender, _amount); - - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_sender); - - vm.prank(_sender); - /* Action */ - optimismSuperchainERC20.sendERC20(_to, _amount, _chainId); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore - _amount); - assert(optimismSuperchainERC20.balanceOf(_sender) == _balanceBefore - _amount); - } - - /// @custom:property-id 11 - /// @custom:property `relayERC20` increases the token's totalSupply in the destination chain exactly by the input - /// amount - function check_relayERC20IncreasesTotalSupply(address _from, address _to, uint256 _amount) public { - vm.assume(_to != address(0)); - - /* Preconditions */ - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _toBalanceBefore = optimismSuperchainERC20.balanceOf(_to); - - vm.prank(address(MESSENGER)); - /* Action */ - optimismSuperchainERC20.relayERC20(_from, _to, _amount); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore + _amount); - assert(optimismSuperchainERC20.balanceOf(_to) == _toBalanceBefore + _amount); - } - - /// @custom:property-id 12 - /// @custom:property Increases the total supply on the amount minted by the bridge - function check_mint(address _from, uint256 _amount) public { - /* Preconditions */ - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_from); - - vm.startPrank(Predeploys.L2_STANDARD_BRIDGE); - /* Action */ - optimismSuperchainERC20.mint(_from, _amount); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore + _amount); - assert(optimismSuperchainERC20.balanceOf(_from) == _balanceBefore + _amount); - } - - /// @custom:property-id 13 - /// @custom:property Supertoken total supply only decreases on the amount burned by the bridge - function check_burn(address _from, uint256 _amount) public { - /* Preconditions */ - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - optimismSuperchainERC20.mint(_from, _amount); - - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_from); - - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - /* Action */ - optimismSuperchainERC20.burn(_from, _amount); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore - _amount); - assert(optimismSuperchainERC20.balanceOf(_from) == _balanceBefore - _amount); - } - - /// @custom:property-id 14 - /// @custom:property Supertoken total supply starts at zero - function check_totalSupplyStartsAtZero() public view { - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == 0); - } -} diff --git a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol deleted file mode 100644 index 75bfe2f7c9e1..000000000000 --- a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol +++ /dev/null @@ -1,18 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.25; - -import { Test } from "forge-std/Test.sol"; - -contract HalmosBase is Test { - uint256 internal constant CURRENT_CHAIN_ID = 1; - uint256 internal constant ZERO_AMOUNT = 0; - - address internal remoteToken = address(bytes20(keccak256("remoteToken"))); - string internal name = "SuperchainERC20"; - string internal symbol = "SUPER"; - uint8 internal decimals = 18; - - function eqStrings(string memory a, string memory b) internal pure returns (bool) { - return keccak256(abi.encode(a)) == keccak256(abi.encode(b)); - } -} From 5969d60d12bba23f59beb1c49117432835c0a6e5 Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 5 Sep 2024 19:37:04 -0300 Subject: [PATCH 06/11] 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 --- .gitmodules | 3 - packages/contracts-bedrock/foundry.toml | 5 - .../invariant-docs/OptimismSuperchainERC20.md | 15 ++ packages/contracts-bedrock/justfile | 3 - packages/contracts-bedrock/lib/properties | 1 - packages/contracts-bedrock/medusa.json | 86 ------- .../autogen/generate-invariant-docs/main.go | 6 + .../invariants/OptimismSuperchainERC20.t.sol | 227 ------------------ .../OptimismSuperchainERC20.t.sol | 82 +++++++ .../fuzz/Protocol.guided.t.sol | 41 ++-- .../fuzz/Protocol.unguided.t.sol | 25 +- .../handlers/Protocol.t.sol | 13 +- .../helpers/Actors.t.sol | 0 .../helpers/CompatibleAssert.t.sol | 28 +++ .../helpers/HandlerGetters.t.sol | 21 ++ .../MockL2ToL2CrossDomainMessenger.t.sol | 0 ...imismSuperchainERC20ForToBProperties.t.sol | 0 .../test/invariants/PROPERTIES.md | 73 ------ .../test/properties/PROPERTIES.md | 141 ----------- .../medusa/properties/Protocol.t.sol | 72 ------ 20 files changed, 194 insertions(+), 648 deletions(-) delete mode 160000 packages/contracts-bedrock/lib/properties delete mode 100644 packages/contracts-bedrock/medusa.json delete mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol rename packages/contracts-bedrock/test/{properties/medusa => invariants/OptimismSuperchainERC20}/fuzz/Protocol.guided.t.sol (84%) rename packages/contracts-bedrock/test/{properties/medusa => invariants/OptimismSuperchainERC20}/fuzz/Protocol.unguided.t.sol (86%) rename packages/contracts-bedrock/test/{properties/medusa => invariants/OptimismSuperchainERC20}/handlers/Protocol.t.sol (92%) rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/Actors.t.sol (100%) 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 rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/MockL2ToL2CrossDomainMessenger.t.sol (100%) rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/OptimismSuperchainERC20ForToBProperties.t.sol (100%) delete mode 100644 packages/contracts-bedrock/test/invariants/PROPERTIES.md delete mode 100644 packages/contracts-bedrock/test/properties/PROPERTIES.md delete mode 100644 packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol diff --git a/.gitmodules b/.gitmodules index dca839eef08e..21ecaedbb77a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -29,6 +29,3 @@ [submodule "packages/contracts-bedrock/lib/openzeppelin-contracts-v5"] path = packages/contracts-bedrock/lib/openzeppelin-contracts-v5 url = https://github.com/OpenZeppelin/openzeppelin-contracts -[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 6dde1ebbceb5..cec47412a4fe 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -99,8 +99,3 @@ out = 'kout-proofs' test = 'test/kontrol/proofs' script = 'test/kontrol/proofs' -[profile.medusa] -src = 'test/properties/medusa/' -test = 'test/properties/medusa/' -script = 'test/properties/medusa/' -via-ir=true diff --git a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md index 13d03f304d45..bdd95df27af6 100644 --- a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md +++ b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md @@ -1,5 +1,20 @@ # `OptimismSuperchainERC20` Invariants +## sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) +**Test:** [`OptimismSuperchainERC20#L36`](../test/invariants/OptimismSuperchainERC20#L36) + + + +## 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#L79`](../test/invariants/OptimismSuperchainERC20#L79) + +since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the handler for assertion test failures + ## 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) diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile index 654ad64cadee..bf96fd17cad1 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -26,9 +26,6 @@ test-kontrol: build-go-ffi build kontrol-summary-full test-kontrol-no-build test-kontrol-no-build: ./test/kontrol/scripts/run-kontrol.sh script -test-medusa timeout='100': - FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}} - test-rerun: build-go-ffi forge test --rerun -vvv diff --git a/packages/contracts-bedrock/lib/properties b/packages/contracts-bedrock/lib/properties deleted file mode 160000 index bb1b78542b3f..000000000000 --- a/packages/contracts-bedrock/lib/properties +++ /dev/null @@ -1 +0,0 @@ -Subproject commit bb1b78542b3f38e4ae56cf87389cd3ea94387f48 diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json deleted file mode 100644 index 5df25c2cd63b..000000000000 --- a/packages/contracts-bedrock/medusa.json +++ /dev/null @@ -1,86 +0,0 @@ -{ - "fuzzing": { - "workers": 10, - "workerResetLimit": 50, - "timeout": 0, - "testLimit": 0, - "callSequenceLength": 100, - "corpusDirectory": "test/properties/medusa/corpus/", - "coverageEnabled": true, - "targetContracts": ["ProtocolProperties"], - "targetContractsBalances": [], - "constructorArgs": {}, - "deployerAddress": "0x30000", - "senderAddresses": [ - "0x10000", - "0x20000", - "0x30000" - ], - "blockNumberDelayMax": 60480, - "blockTimestampDelayMax": 604800, - "blockGasLimit": 30000000, - "transactionGasLimit": 12500000, - "testing": { - "stopOnFailedTest": true, - "stopOnFailedContractMatching": false, - "stopOnNoTests": true, - "testAllContracts": false, - "traceAll": true, - "assertionTesting": { - "enabled": true, - "testViewMethods": true, - "panicCodeConfig": { - "failOnCompilerInsertedPanic": false, - "failOnAssertion": true, - "failOnArithmeticUnderflow": false, - "failOnDivideByZero": false, - "failOnEnumTypeConversionOutOfBounds": false, - "failOnIncorrectStorageAccess": false, - "failOnPopEmptyArray": false, - "failOnOutOfBoundsArrayAccess": false, - "failOnAllocateTooMuchMemory": false, - "failOnCallUninitializedVariable": false - } - }, - "propertyTesting": { - "enabled": false, - "testPrefixes": [ - "property_" - ] - }, - "optimizationTesting": { - "enabled": false, - "testPrefixes": [ - "optimize_" - ] - }, - "targetFunctionSignatures": [], - "excludeFunctionSignatures": [ - "ProtocolProperties.test_ERC20external_zeroAddressBalance()", - "ProtocolProperties.test_ERC20external_transferToZeroAddress()", - "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)" - ] - }, - "chainConfig": { - "codeSizeCheckDisabled": true, - "cheatCodes": { - "cheatCodesEnabled": true, - "enableFFI": false - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": ["--foundry-out-directory", "artifacts","--foundry-compile-all"] - } - }, - "logging": { - "level": "info", - "logDirectory": "", - "noColor": false - } -} 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/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..d4662277fbd2 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol @@ -0,0 +1,82 @@ +// 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/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/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol similarity index 84% rename from packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol index d5b5d8b5edc5..2d9c8d52fab3 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol @@ -1,12 +1,13 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.25; -import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; +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 { +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 @@ -27,7 +28,7 @@ contract ProtocolGuided is ProtocolHandler { chainId ); // 14 - assert(supertoken.totalSupply() == 0); + compatibleAssert(supertoken.totalSupply() == 0); } /// @custom:property-id 6 @@ -65,19 +66,19 @@ contract ProtocolGuided is ProtocolHandler { uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); // no free mint - assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); + compatibleAssert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); // 22 - assert(sourceBalanceBefore - amount == sourceBalanceAfter); - assert(destinationBalanceBefore + amount == destinationBalanceAfter); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(destinationBalanceBefore + amount == destinationBalanceAfter); uint256 sourceSupplyAfter = sourceToken.totalSupply(); uint256 destinationSupplyAfter = destinationToken.totalSupply(); // 23 - assert(sourceSupplyBefore - amount == sourceSupplyAfter); - assert(destinationSupplyBefore + amount == destinationSupplyAfter); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(destinationSupplyBefore + amount == destinationSupplyAfter); } catch { MESSENGER.setAtomic(false); // 6 - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } @@ -112,13 +113,13 @@ contract ProtocolGuided is ProtocolHandler { ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); // 26 uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); - assert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); // 10 uint256 sourceSupplyAfter = sourceToken.totalSupply(); - assert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); } catch { // 6 - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } @@ -138,17 +139,17 @@ contract ProtocolGuided is ProtocolHandler { bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken)); (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); // if sendERC20 didnt intialize this, then test suite is broken - assert(success); + compatibleAssert(success); ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount); // 11 - assert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); + compatibleAssert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); // 27 - assert( + compatibleAssert( destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient) ); } catch { // 7 - assert(false); + compatibleAssert(false); } } @@ -194,13 +195,13 @@ contract ProtocolGuided is ProtocolHandler { // 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); + compatibleAssert(false); } uint256 balanceSenderAfter = token.balanceOf(currentActor()); uint256 balanceRecipeintAfter = token.balanceOf(recipient); uint256 supplyAfter = token.totalSupply(); - assert(balanceSenderBefore == balanceSenderAfter); - assert(balanceRecipientBefore == balanceRecipeintAfter); - assert(supplyBefore == supplyAfter); + compatibleAssert(balanceSenderBefore == balanceSenderAfter); + compatibleAssert(balanceRecipientBefore == balanceRecipeintAfter); + compatibleAssert(supplyBefore == supplyAfter); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol similarity index 86% rename from packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol index 71ba64118088..bf6d1386d409 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol @@ -4,9 +4,10 @@ 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 { +contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{ using EnumerableMap for EnumerableMap.Bytes32ToUintMap; /// @custom:property-id 7 @@ -28,8 +29,8 @@ contract ProtocolUnguided is ProtocolHandler { vm.prank(sender); try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) { MESSENGER.setCrossDomainMessageSender(address(0)); - assert(sender == address(MESSENGER)); - assert(crossDomainMessageSender == token); + 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: @@ -37,7 +38,7 @@ contract ProtocolUnguided is ProtocolHandler { (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); } catch { - assert(sender != address(MESSENGER) || crossDomainMessageSender != token); + compatibleAssert(sender != address(MESSENGER) || crossDomainMessageSender != token); MESSENGER.setCrossDomainMessageSender(address(0)); } } @@ -71,13 +72,13 @@ contract ProtocolUnguided is ProtocolHandler { ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); // 26 uint256 sourceBalanceAfter = sourceToken.balanceOf(sender); - assert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); // 10 uint256 sourceSupplyAfter = sourceToken.totalSupply(); - assert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); } catch { // 6 - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } @@ -90,11 +91,11 @@ contract ProtocolUnguided is ProtocolHandler { amount = bound(amount, 0, type(uint256).max - OptimismSuperchainERC20(token).totalSupply()); vm.prank(sender); try OptimismSuperchainERC20(token).mint(to, amount) { - assert(sender == BRIDGE); + compatibleAssert(sender == BRIDGE); (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); } catch { - assert(sender != BRIDGE || to == address(0)); + compatibleAssert(sender != BRIDGE || to == address(0)); } } @@ -107,11 +108,11 @@ contract ProtocolUnguided is ProtocolHandler { uint256 senderBalance = OptimismSuperchainERC20(token).balanceOf(sender); vm.prank(sender); try OptimismSuperchainERC20(token).burn(from, amount) { - assert(sender == BRIDGE); + compatibleAssert(sender == BRIDGE); (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); } catch { - assert(sender != BRIDGE || senderBalance < amount); + compatibleAssert(sender != BRIDGE || senderBalance < amount); } } @@ -132,7 +133,7 @@ contract ProtocolUnguided is ProtocolHandler { try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize( remoteToken, name, symbol, decimals ) { - assert(false); + compatibleAssert(false); } catch { } } } diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol similarity index 92% rename from packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol index 191c5c44a7e6..921495b467ab 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol @@ -7,15 +7,15 @@ 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 { 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"; +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 internal constant MAX_CHAINS = 4; + 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; @@ -79,7 +79,6 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { index = bound(index, 0, allSuperTokens.length - 1); address addr = allSuperTokens[index]; vm.prank(BRIDGE); - // medusa calls with different senders by default OptimismSuperchainERC20(addr).mint(currentActor(), amount); // currentValue will be zero if key is not present (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr)); @@ -156,6 +155,10 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { { // 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)); diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol similarity index 100% rename from packages/contracts-bedrock/test/properties/helpers/Actors.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol 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..9cca12bf8649 --- /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..6120f5f75684 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol @@ -0,0 +1,21 @@ +// 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/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol similarity index 100% rename from packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol diff --git a/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol similarity index 100% rename from packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol diff --git a/packages/contracts-bedrock/test/invariants/PROPERTIES.md b/packages/contracts-bedrock/test/invariants/PROPERTIES.md deleted file mode 100644 index 5a5cc71d73b5..000000000000 --- a/packages/contracts-bedrock/test/invariants/PROPERTIES.md +++ /dev/null @@ -1,73 +0,0 @@ -# supertoken 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 | description | halmos | medusa | -| --- | ---------------------------------------------------------------------------------- | ------ | ------ | -| 0 | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | -| 1 | supertoken token address depends on name, remote token, address and decimals | [ ] | [ ] | -| 2 | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | [ ] | -| 3 | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | -| 4 | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | -| 5 | convert() burns the same amount of one token that it mints of the other | [ ] | [ ] | - -## Valid state - -| id | description | halmos | medusa | -| --- | ------------------------------------------------------------------------------------------ | ------- | ------ | -| 6 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | -| 7 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | - -## Variable transition - -| id | description | halmos | medusa | -| --- | ------------------------------------------------------------------------------------------------- | ------ | ------ | -| 8 | sendERC20 with a value of zero does not modify accounting | [x] | [ ] | -| 9 | relayERC20 with a value of zero does not modify accounting | [x] | [ ] | -| 10 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | -| 11 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | -| 12 | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [ ] | -| 13 | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | -| 14 | supertoken total supply starts at zero | [x] | [ ] | -| 15 | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | -| 16 | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | [ ] | - -## High level - -| id | description | halmos | medusa | -| --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | -| 17 | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | -| 18 | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | -| 19 | sum of total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | -| 20 | 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 | 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 | description | halmos | medusa | -| --- | ---------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | -| 22 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [x] | -| 23 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [x] | -| 24 | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | - -# 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) - -# Invariant-breaking candidates (brain dump) - -here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants - -- [ ] changing the decimals of tokens after deployment -- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md deleted file mode 100644 index d915d565633e..000000000000 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ /dev/null @@ -1,141 +0,0 @@ -# Supertoken advanced testing - -## Overview - -This document defines a set of properties global to the supertoken ecosystem, for which we will: - -- run a [Medusa](https://github.com/crytic/medusa) fuzzing campaign, trying to break system invariants -- formally prove with [Halmos](https://github.com/a16z/halmos) whenever possible - -## 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 - -## Where to place the testing campaign - -Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already has invariant testing provided by foundry, it's not a trivial matter where to place this advanced testing campaign. Two alternatives are proposed: - -- including it in the mainline OP monorepo, in a subdirectory of the existing test contracts such as `test/invariants/medusa/superc20/` -- keep the campaign in wonderland's fork of the repository, in its own feature branch, in which case the deliverable would consist primarily of: - - a summary of the results, extending this document - - PRs with extra unit tests replicating found issues to the main repo where applicable - -## Contracts in scope - -- [ ] [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) (modifications to enable `convert` not yet merged) -- [ ] [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/OptimismSuperchainERC20.sol1) -- [ ] [OptimismSuperchainERC20Factory](https://github.com/defi-wonderland/optimism/pull/8/files#diff-09838f5703c353d0f7c5ff395acc04c1768ef58becac67404bc17e1fb0018517) (not yet merged) -- [ ] [L2StandardBridgeInterop](https://github.com/defi-wonderland/optimism/pull/10/files#diff-56cf869412631eac0a04a03f7d026596f64a1e00fcffa713bc770d67c6856c2f) (not yet merged) - -## Behavior assumed correct - -- [ ] inclusion of relay transactions -- [ ] sequencer implementation -- [ ] [OptimismMintableERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20.sol) -- [ ] [L2ToL2CrossDomainMessenger](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/L2CrossDomainMessenger.sol) -- [ ] [CrossL2Inbox](https://github.com/defi-wonderland/src/L2/CrossL2Inbox.sol) - -## Pain points - -- existing fuzzing tools use the same EVM to run the tested contracts as they do for asserting invariants, tracking ghost variables and everything else necessary to provision a fuzzing campaign. While this is usually very convenient, it means that we can’t assert on the behaviour/state of *different* chains from within a fuzzing campaign. This means we will have to walk around the requirement of supertokens having the same address across all chains, and implement a way to mock tokens existing in different chains. We will strive to formally prove it in a unitary fashion to mitigate this in properties 0 and 1 -- a buffer to represent 'in transit' messages should be implemented to assert on invariants relating to the non-atomicity of bridging from one chain to another. It is yet to be determined if it’ll be a FIFO queue (assuming ideal message ordering by sequencers) or it’ll have random-access capability to simulate messages arriving out of order - -## 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 | halmos | medusa | -| --- | --- | --- | --- | --- | -| 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 | halmos | medusa | -| --- | --- | --- | --- | --- | -| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [x] | -| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[~]** | [~] | - -## Variable transition - -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | [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] | [x] | -| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [ ] | [x] | -| 27 | SupERC20 | relayERC20 increases sender's balance in the destination chain exactly by the input amount | [ ] | [x] | -| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | -| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] | -| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | -| 14 | SupERC20 | supertoken total supply starts at zero | [x] | [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 | halmos | medusa | -| --- | --- | --- | --- | --- | -| 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 | halmos | medusa | -| --- | --- | --- | --- | --- | -| 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) | [ ] | [~] | - -# Expected external interactions - -- [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) - -here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants - -- [ ] changing the decimals of tokens after deployment -- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols - -# Internal structure - -## Medusa campaign - -Fuzzing campaigns have both the need to push the contract into different states (state transitions) and assert properties are actually held. This defines a spectrum of function types: - -- `handler_`: they only transition the protocol state, and don't perform any assertions. -- `fuzz_`: they both transition the protocol state and perform assertions on properties. They are further divided in: - - unguided: they exist to let the fuzzer try novel or unexpected interactions, and potentially transition to unexpectedly invalid states - - guided: they have the goal of quickly covering code and moving the protocol to known valid states (eg: by moving funds between valid users) -- `property_`: they only assert the protocol is in a valid state, without causing a state transition. Note that they still use assertion-mode testing for simplicity, but could be migrated to run in property-mode. diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol deleted file mode 100644 index 7b2f73d54058..000000000000 --- a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol +++ /dev/null @@ -1,72 +0,0 @@ -// 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 - // - `convert` - /// @custom:property-id 19 - /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)- - /// convert(super, legacy) - function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view { - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply ; - (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); - (, uint256 fundsInTransit) = ghost_tokensInTransit.tryGet(currentSalt); - // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply + fundsInTransit); - } - } - - // TODO: will need rework after - // - `convert` - /// @custom:property-id 21 - /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)- - /// convert(super, legacy) when all when all cross-chain messages are processed - function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view { - require(MESSENGER.messageQueueLength() == 0); - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply ; - (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); - // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply); - } - } -} From 2e315625d863d6e716d9f14171f6319b4ed7b99a Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 10 Sep 2024 17:08:59 -0300 Subject: [PATCH 07/11] chore: fixes from rebase --- .../invariant-docs/OptimismSuperchainERC20.md | 11 +---------- .../OptimismSuperchainERC20.t.sol | 2 +- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md index bdd95df27af6..7dd70286a4e9 100644 --- a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md +++ b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md @@ -13,13 +13,4 @@ ## many other assertion mode invariants are also defined under `test/invariants/OptimismSuperchainERC20/fuzz/` . **Test:** [`OptimismSuperchainERC20#L79`](../test/invariants/OptimismSuperchainERC20#L79) -since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the handler for assertion test failures - -## 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) - - - -## 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) - +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/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol index d4662277fbd2..189e569e992e 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol @@ -10,7 +10,7 @@ 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/IL2ToL2CrossDomainMessenger.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"; From 1da37b17dea1592d1546feb2b61708744a220e23 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 10 Sep 2024 17:17:15 -0300 Subject: [PATCH 08/11] 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 --- packages/contracts-bedrock/.gitignore | 1 - packages/contracts-bedrock/foundry.toml | 4 +- .../OptimismSuperchainERC20/PROPERTIES.md | 82 +++++++++++++++++++ ...imismSuperchainERC20ForToBProperties.t.sol | 6 +- 4 files changed, 87 insertions(+), 6 deletions(-) create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/PROPERTIES.md diff --git a/packages/contracts-bedrock/.gitignore b/packages/contracts-bedrock/.gitignore index 396c03d4458d..96e09c8c7190 100644 --- a/packages/contracts-bedrock/.gitignore +++ b/packages/contracts-bedrock/.gitignore @@ -6,7 +6,6 @@ broadcast kout-deployment kout-proofs test/kontrol/logs -test/properties/medusa/corpus/ # Metrics coverage.out diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index cec47412a4fe..cef9f85bbaeb 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -17,12 +17,11 @@ 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', 'kontrol-cheatcodes/=lib/kontrol-cheatcodes/src', - 'gelato/=lib/automate/contracts', + 'gelato/=lib/automate/contracts' ] extra_output = ['devdoc', 'userdoc', 'metadata', 'storageLayout'] bytecode_hash = 'none' @@ -98,4 +97,3 @@ src = 'test/kontrol/proofs' out = 'kout-proofs' test = 'test/kontrol/proofs' script = 'test/kontrol/proofs' - 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/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol index 145bf5ff01e5..9f80cda92fcc 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol @@ -4,7 +4,9 @@ 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 + /// @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; } From 6fd64c5406df022f053154ce8a8ef81f685ca27c Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 11 Sep 2024 12:49:12 -0300 Subject: [PATCH 09/11] chore: run forge fmt --- .../OptimismSuperchainERC20.t.sol | 3 ++- .../OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol | 10 +++++++--- .../fuzz/Protocol.unguided.t.sol | 6 ++---- .../helpers/CompatibleAssert.t.sol | 2 +- .../helpers/HandlerGetters.t.sol | 1 + 5 files changed, 13 insertions(+), 9 deletions(-) diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol index 189e569e992e..d90e90a2f811 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol @@ -72,7 +72,8 @@ contract OptimismSuperchainERC20Properties is Test { } } - /// @custom:invariant many other assertion mode invariants are also defined under `test/invariants/OptimismSuperchainERC20/fuzz/` . + /// @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 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 index 2d9c8d52fab3..536a4ea7025a 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol @@ -5,13 +5,14 @@ import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomain 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'; +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 @@ -66,7 +67,9 @@ contract ProtocolGuided is ProtocolHandler, CompatibleAssert { uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); // no free mint - compatibleAssert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); + compatibleAssert( + sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter + ); // 22 compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); compatibleAssert(destinationBalanceBefore + amount == destinationBalanceAfter); @@ -124,7 +127,8 @@ contract ProtocolGuided is ProtocolHandler, CompatibleAssert { } /// @custom:property-id 11 - /// @custom:property relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount + /// @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 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 index bf6d1386d409..90cad38baa99 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol @@ -4,10 +4,10 @@ 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'; +import { CompatibleAssert } from "../helpers/CompatibleAssert.t.sol"; // TODO: add fuzz_sendERC20 when we implement non-atomic bridging -contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{ +contract ProtocolUnguided is ProtocolHandler, CompatibleAssert { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; /// @custom:property-id 7 @@ -82,7 +82,6 @@ contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{ } } - /// @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 { @@ -99,7 +98,6 @@ contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{ } } - /// @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 { diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol index 9cca12bf8649..4e69c94c8585 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol @@ -15,7 +15,7 @@ contract CompatibleAssert { function compatibleAssert(bool condition, string memory message) internal { if (!condition) { - if(bytes(message).length != 0) console.log("Assertion failed: ", message); + if (bytes(message).length != 0) console.log("Assertion failed: ", message); else console.log("Assertion failed"); // for foundry to call & check diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol index 6120f5f75684..b081aa48c6bb 100644 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol @@ -6,6 +6,7 @@ import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableM contract HandlerGetters is ProtocolHandler { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + function deploySaltsLength() external view returns (uint256 length) { return ghost_totalSupplyAcrossChains.length(); } From 9b66f39d3866c1d4234b714ecfb1161c51f158fb Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 17 Sep 2024 12:30:04 -0300 Subject: [PATCH 10/11] ci: allow for testfiles to be deleted --- .../scripts/testing/test-heavy-fuzz-modified-tests.sh | 4 ++++ 1 file changed, 4 insertions(+) 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") From 0ede77531794f40232ade31e89bdf60814a29f9a Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 17 Sep 2024 13:48:59 -0300 Subject: [PATCH 11/11] fix: run doc autogen script after rebase --- .../contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md index 7dd70286a4e9..8b5c65ebf213 100644 --- a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md +++ b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md @@ -11,6 +11,6 @@ ## many other assertion mode invariants are also defined under `test/invariants/OptimismSuperchainERC20/fuzz/` . -**Test:** [`OptimismSuperchainERC20#L79`](../test/invariants/OptimismSuperchainERC20#L79) +**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