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 new file mode 100644 index 000000000000..83da3b70c0a1 --- /dev/null +++ b/packages/contracts-bedrock/package.json @@ -0,0 +1,69 @@ +{ + "name": "@eth-optimism/contracts-bedrock", + "version": "0.17.3", + "description": "Contracts for Optimism Specs", + "license": "MIT", + "engines": { + "node": ">=16", + "pnpm": ">=9" + }, + "files": [ + "forge-artifacts/**/*.json", + "!forge-artifacts/**/*.t.sol/*.json", + "deployments/**/*.json", + "src/**/*.sol" + ], + "scripts": { + "prebuild": "./scripts/checks/check-foundry-install.sh", + "build": "forge build", + "build:go-ffi": "(cd scripts/go-ffi && go build)", + "autogen:invariant-docs": "go run ./scripts/autogen/generate-invariant-docs .", + "test": "pnpm build:go-ffi && forge test", + "test:kontrol": "./test/kontrol/scripts/run-kontrol.sh script", + "genesis": "forge script scripts/L2Genesis.s.sol:L2Genesis --sig 'runWithStateDump()'", + "coverage": "pnpm build:go-ffi && (forge coverage || (bash -c \"forge coverage 2>&1 | grep -q 'Stack too deep' && echo -e '\\033[1;33mWARNING\\033[0m: Coverage failed with stack too deep, so overriding and exiting successfully' && exit 0 || exit 1\"))", + "coverage:lcov": "pnpm build:go-ffi && (forge coverage --report lcov || (bash -c \"forge coverage --report lcov 2>&1 | grep -q 'Stack too deep' && echo -e '\\033[1;33mWARNING\\033[0m: Coverage failed with stack too deep, so overriding and exiting successfully' && exit 0 || exit 1\"))", + "deploy": "./scripts/deploy/deploy.sh", + "gas-snapshot:no-build": "forge snapshot --match-contract GasBenchMark", + "statediff": "./scripts/statediff.sh && git diff --exit-code", + "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", + "medusa":"FOUNDRY_PROFILE=medusa medusa fuzz", + "snapshots": "forge build && go run ./scripts/autogen/generate-snapshots . && pnpm kontrol-summary-fp && pnpm kontrol-summary", + "snapshots:check": "./scripts/checks/check-snapshots.sh", + "semver-lock": "forge script scripts/SemverLock.s.sol", + "validate-deploy-configs": "./scripts/checks/check-deploy-configs.sh", + "validate-spacers:no-build": "go run ./scripts/checks/spacers", + "validate-spacers": "pnpm build && pnpm validate-spacers:no-build", + "clean": "rm -rf ./artifacts ./forge-artifacts ./cache ./tsconfig.tsbuildinfo ./tsconfig.build.tsbuildinfo ./scripts/go-ffi/go-ffi ./.testdata ./deployments/hardhat/*", + "pre-pr:no-build": "pnpm gas-snapshot:no-build && pnpm snapshots && pnpm semver-lock && pnpm autogen:invariant-docs && pnpm lint", + "pre-pr": "pnpm clean && pnpm build:go-ffi && pnpm build && pnpm pre-pr:no-build", + "pre-pr:full": "pnpm test && pnpm validate-deploy-configs && pnpm validate-spacers && pnpm pre-pr", + "lint:ts:check": "eslint . --max-warnings=0", + "lint:forge-tests:check": "go run ./scripts/checks/names", + "lint:contracts:check": "pnpm lint:fix && git diff --exit-code", + "lint:check": "pnpm lint:contracts:check && pnpm lint:ts:check", + "lint:ts:fix": "eslint --fix .", + "lint:contracts:fix": "forge fmt", + "lint:fix": "pnpm lint:contracts:fix && pnpm lint:ts:fix", + "lint": "pnpm lint:fix && pnpm lint:check" + }, + "devDependencies": { + "@babel/eslint-parser": "^7.23.10", + "@typescript-eslint/eslint-plugin": "^6.21.0", + "@typescript-eslint/parser": "^6.21.0", + "@types/node": "^20.14.12", + "doctoc": "^2.2.0", + "eslint": "^8.56.0", + "eslint-config-prettier": "^9.1.0", + "eslint-config-standard": "^16.0.3", + "eslint-plugin-import": "^2.29.1", + "eslint-plugin-jsdoc": "^48.8.3", + "eslint-plugin-prefer-arrow": "^1.2.3", + "eslint-plugin-prettier": "^4.0.0", + "prettier": "^2.8.0", + "tsx": "^4.16.2", + "typescript": "^5.5.4" + } +} diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md new file mode 100644 index 000000000000..540d591f77de --- /dev/null +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -0,0 +1,72 @@ +# 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 | [ ] | [ ] | +| 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 | 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/SUMMARY.md b/packages/contracts-bedrock/test/properties/SUMMARY.md new file mode 100644 index 000000000000..cf9c8a93afa5 --- /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/a16z/halmos) 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://github.com/defi-wonderland/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* 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 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 on the Superchain diff --git a/packages/contracts-bedrock/test/properties/helpers/MockCrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockCrossDomainMessenger.t.sol new file mode 100644 index 000000000000..4ad4d474b738 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/MockCrossDomainMessenger.t.sol @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { SafeCall } from "src/libraries/SafeCall.sol"; + +contract MockCrossDomainMessenger { + ///////////////////////////////////////////////////////// + // State vars mocking the L2toL2CrossDomainMessenger // + ///////////////////////////////////////////////////////// + address public crossDomainMessageSender; + address public crossDomainMessageSource; + + /////////////////////////////////////////////////// + // Helpers for cross-chain interaction mocking // + /////////////////////////////////////////////////// + mapping(address => bytes32) public superTokenInitDeploySalts; + mapping(uint256 chainId => mapping(bytes32 reayDeployData => address)) public superTokenAddresses; + + 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; + } + + //////////////////////////////////////////////////////// + // Functions mocking the L2toL2CrossDomainMessenger // + //////////////////////////////////////////////////////// + + /// @dev 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/ProtocolAtomic.t.sol b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol new file mode 100644 index 000000000000..9c3acd1daa21 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol @@ -0,0 +1,180 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { Test } from "forge-std/Test.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 { MockCrossDomainMessenger } from "../helpers/MockCrossDomainMessenger.t.sol"; + +contract ProtocolAtomicFuzz is Test { + 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; + MockCrossDomainMessenger internal constant MESSENGER = + MockCrossDomainMessenger(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; + + //@dev 'real' deploy salt => total supply sum across chains + EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains; + + constructor() { + vm.etch(address(MESSENGER), address(new MockCrossDomainMessenger()).code); + superchainERC20Impl = new OptimismSuperchainERC20(); + for (uint256 i = 0; i < INITIAL_TOKENS; i++) { + _deployRemoteToken(); + for (uint256 j = 0; j < INITIAL_SUPERTOKENS; j++) { + _deploySupertoken(remoteTokens[i], WORDS[0], WORDS[0], DECIMALS[0], j); + } + } + } + + 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 fuzz_DeployNewSupertoken( + TokenDeployParams memory params, + uint256 chainId + ) + external + validateTokenDeployParams(params) + { + chainId = bound(chainId, 0, MAX_CHAINS - 1); + _deploySupertoken( + remoteTokens[params.remoteTokenIndex], + WORDS[params.nameIndex], + WORDS[params.symbolIndex], + DECIMALS[params.decimalsIndex], + chainId + ); + } + + /// @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_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); + } + } + + 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); + // 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); + } + + // 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) + /// @dev deliberately not a view method so medusa runs it but not the view methods defined by Test + function property_totalSupplyAcrossChainsEqualsMints() external { + for (uint256 i = 0; i < ghost_totalSupplyAcrossChains.length(); i++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(i); + for (uint256 j = 0; j < MAX_CHAINS; j++) { + address supertoken = MESSENGER.superTokenAddresses(j, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assert(trackedSupply == totalSupply); + } + } + + function fuzz_MockNewRemoteToken() external { + _deployRemoteToken(); + } + + function _deployRemoteToken() internal { + // 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 nameIndex, + string memory symbolIndex, + uint8 decimals, + uint256 chainId + ) + internal + { + bytes32 realSalt = keccak256(abi.encode(remoteToken, nameIndex, symbolIndex, decimals)); + bytes32 hackySalt = keccak256(abi.encode(remoteToken, nameIndex, symbolIndex, decimals, chainId)); + OptimismSuperchainERC20 token = OptimismSuperchainERC20( + address( + // TODO: Use the SuperchainERC20 Beacon Proxy + new ERC1967Proxy{ salt: hackySalt }( + address(superchainERC20Impl), + abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, nameIndex, symbolIndex, decimals)) + ) + ) + ); + MESSENGER.registerSupertoken(realSalt, chainId, address(token)); + allSuperTokens.push(address(token)); + } +}