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 61a01fdaf7bd..74f516e73050 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -95,3 +95,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/medusa.json b/packages/contracts-bedrock/medusa.json new file mode 100644 index 000000000000..76592655ffa1 --- /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": ["ProtocolAtomicFuzz"], + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": [ + "0x10000", + "0x20000", + "0x30000" + ], + "blockNumberDelayMax": 60480, + "blockTimestampDelayMax": 604800, + "blockGasLimit": 125000000, + "transactionGasLimit": 12500000, + "testing": { + "stopOnFailedTest": true, + "stopOnFailedContractMatching": false, + "stopOnNoTests": true, + "testAllContracts": false, + "traceAll": true, + "assertionTesting": { + "enabled": true, + "testViewMethods": false, + "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/package.json b/packages/contracts-bedrock/package.json index 1cf9873abb6a..1d56d15b6cfc 100644 --- a/packages/contracts-bedrock/package.json +++ b/packages/contracts-bedrock/package.json @@ -29,7 +29,7 @@ "gas-snapshot": "pnpm build:go-ffi && pnpm gas-snapshot:no-build", "kontrol-summary": "./test/kontrol/scripts/make-summary-deployment.sh", "kontrol-summary-fp": "KONTROL_FP_DEPLOYMENT=true pnpm kontrol-summary", - "snapshots": "forge build && go run ./scripts/autogen/generate-snapshots . && pnpm kontrol-summary-fp && pnpm kontrol-summary", + "medusa":"FOUNDRY_PROFILE=medusa medusa fuzz", "snapshots:check": "./scripts/checks/check-snapshots.sh", "semver-lock": "forge script scripts/SemverLock.s.sol", "validate-deploy-configs": "./scripts/checks/check-deploy-configs.sh", diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md new file mode 100644 index 000000000000..b3a18514d254 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -0,0 +1,71 @@ +# 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 +- `:(`: 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 | [ ] | [x] | +| 1 | supertoken token address depends on name, remote token, address and decimals | [ ] | [x] | +| 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 | [ ] | [ ] | +| 7 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[ ]** | [ ] | + +## Variable transition + +| id | description | halmos | medusa | +| --- | --- | --- | --- | +| 8 | sendERC20 with a value of zero does not modify accounting | [ ] | [ ] | +| 9 | relayERC20 with a value of zero does not modify accounting | [ ] | [ ] | +| 10 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [ ] | [ ] | +| 11 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ] | [ ] | +| 12 | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [ ] | [ ] | +| 13 | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [ ] | [ ] | +| 14 | supertoken total supply starts at zero | [ ] | [ ] | +| 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 | echidna | +| --- | --- | --- | --- | +| 20 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [ ] | +| 21 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [ ] | +| 22 | 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/SUMMARY.md b/packages/contracts-bedrock/test/properties/SUMMARY.md new file mode 100644 index 000000000000..ed6c286556fd --- /dev/null +++ b/packages/contracts-bedrock/test/properties/SUMMARY.md @@ -0,0 +1,43 @@ +# SupERC20 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/ethereum-optimism/optimism) whenever possible + +## 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/` +- creating a separate (potentially private) repository for this testing campaign, 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 + +- [ ] [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/pull/9/files#diff-810060510a8a9c06dc60cdce6782e5cafd93b638e2557307a68abe694ee86aee) +- [ ] [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) +- [ ] [SuperchsupERC20ainERC20](https://github.com/defi-wonderland/optimism/pull/8/files#diff-603fd7d5a0b2c403c0d1eee21d0ee60fb8eb72430169eaac5ec7081e01de96b8) (not yet merged) +- [ ] [SuperchainERC20Factory](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://www.notion.so/defi-wonderland/src/L2/L2CrossDomainMessenger.sol) +- [ ] [CrossL2Inbox](https://www.notion.so/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* EVMs 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 13 and 14 +- 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 on the Superchain diff --git a/packages/contracts-bedrock/test/properties/helpers/Utils.sol b/packages/contracts-bedrock/test/properties/helpers/Utils.sol new file mode 100644 index 000000000000..eabf7b483f18 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/Utils.sol @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { MockERC20 } from "forge-std/mocks/MockERC20.sol"; + +contract FuzzERC20 is MockERC20 { + function mint(address _to, uint256 _amount) public { + _mint(_to, _amount); + } + + function burn(address _from, uint256 _amount) public { + _burn(_from, _amount); + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol new file mode 100644 index 000000000000..55e63b42963e --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import "forge-std/console.sol"; + +import { Test } from "forge-std/Test.sol"; + +import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { SafeCall } from "src/libraries/SafeCall.sol"; +import { FuzzERC20 } from "../helpers/Utils.sol"; + +contract MockCrossDomainMessenger { + address public crossDomainMessageSender; + address public crossDomainMessageSource; + mapping(uint256 chainId => mapping(bytes32 reayDeployData => address)) internal superTokenAddresses; + mapping(address => bytes32) internal superTokenInitDeploySalts; + // test-specific functions + + function crossChainMessageReceiver(address sender, uint256 destinationChainId) external returns (OptimismSuperchainERC20) { + return OptimismSuperchainERC20(superTokenAddresses[destinationChainId][superTokenInitDeploySalts[sender]]); + } + + function registerSupertoken(bytes32 deploySalt, uint256 chainId, address token) external { + superTokenAddresses[chainId][deploySalt] = token; + superTokenInitDeploySalts[token] = deploySalt; + } + // mocked functions + + function sendMessage(uint256 chainId, address recipient, bytes memory message) external returns (address) { + 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); + } +} + +contract ProtocolAtomicFuzz is Test { + uint8 internal constant MAX_CHAINS = 4; + address internal constant BRIDGE = Predeploys.L2_STANDARD_BRIDGE; + MockCrossDomainMessenger internal constant MESSENGER = + MockCrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); + OptimismSuperchainERC20 internal superchainERC20Impl; + string[] internal WORDS = ["FANCY", "TOKENS"]; + uint8[] internal DECIMALS = [0, 6, 18, 36]; + + struct TokenDeployParams { + uint8 remoteTokenIndex; + uint8 name; + uint8 symbol; + uint8 decimals; + } + + address[] internal remoteTokens; + address[] internal allSuperTokens; + mapping(bytes32 => uint256) internal superTokenTotalSupply; + mapping(bytes32 => uint256) internal superTokensTotalSupply; + + constructor() { + vm.etch(address(MESSENGER), address(new MockCrossDomainMessenger()).code); + superchainERC20Impl = new OptimismSuperchainERC20(); + } + + modifier validateTokenDeployParams(TokenDeployParams memory params) { + params.remoteTokenIndex = uint8(bound(params.remoteTokenIndex, 0, remoteTokens.length - 1)); + params.name = uint8(bound(params.name, 0, WORDS.length - 1)); + params.symbol = uint8(bound(params.symbol, 0, WORDS.length - 1)); + params.decimals = uint8(bound(params.decimals, 0, DECIMALS.length - 1)); + _; + } + + function fuzz_DeployNewSupertoken( + TokenDeployParams memory params, + uint256 chainId + ) + external + validateTokenDeployParams(params) + { + chainId = bound(chainId, 0, MAX_CHAINS - 1); + _deploySupertoken( + remoteTokens[params.remoteTokenIndex], + WORDS[params.name], + WORDS[params.symbol], + DECIMALS[params.decimals], + chainId + ); + } + + function fuzz_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 balanceFromBefore = sourceToken.balanceOf(msg.sender); + uint256 balanceToBefore = destinationToken.balanceOf(msg.sender); + vm.prank(msg.sender); + try sourceToken.sendERC20(msg.sender, amount, destinationChainId) { + uint256 balanceFromAfter = sourceToken.balanceOf(msg.sender); + uint256 balanceToAfter = destinationToken.balanceOf(msg.sender); + assert(balanceFromBefore + balanceToBefore == balanceFromAfter + balanceToAfter); + } catch { + assert(balanceFromBefore < amount || address(destinationToken) == address(sourceToken)); + } + } + + // TODO: track total supply for invariant checking + function fuzz_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); + } + + function fuzz_MockNewRemoteToken() external { + // make sure they don't conflict with predeploys/preinstalls/precompiles/other tokens + remoteTokens.push(address(uint160(1000 + remoteTokens.length))); + } + + function _deploySupertoken( + address remoteToken, + string memory name, + string memory symbol, + uint8 decimals, + uint256 chainId + ) + internal + { + bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals)); + bytes32 hackySalt = keccak256(abi.encode(remoteToken, name, symbol, decimals, chainId)); + OptimismSuperchainERC20 localToken = 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(localToken)); + allSuperTokens.push(address(localToken)); + } +}