Chore: setup medusa + 1 basic fuzz scenario

packages/contracts-bedrock/.gitignore

@@ -6,6 +6,7 @@ broadcast
 kout-deployment
 kout-proofs
 test/kontrol/logs
+test/properties/medusa/corpus/
 
 # Metrics
 coverage.out

packages/contracts-bedrock/foundry.toml

@@ -96,3 +96,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/'

packages/contracts-bedrock/justfile

@@ -22,6 +22,9 @@ test: build-go-ffi
 test-kontrol:
   ./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
 

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
+	}
+}

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

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);
+    }
+}