Merge branch 'chore/setup-medusa' into feat/halmos-symbolic-tests

defi-wonderland · Aug 14, 2024 · 945d6b6 · 945d6b6
2 parents 5dcb3a8 + d8ad2b1
commit 945d6b6
Show file tree

Hide file tree

Showing 8 changed files with 504 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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);
+    }
+}