Skip to content

Commit

Permalink
chore: configure medusa with basic supERC20 self-bridging
Browse files Browse the repository at this point in the history 
- 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
  • Loading branch information
@0xteddybear
0xteddybear committed Aug 13, 2024
1 parent 5514694 commit f6c3f90
Show file tree
Hide file tree
Showing 8 changed files with 368 additions and 1 deletion.
1 change: 1 addition & 0 deletions packages/contracts-bedrock/.gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ broadcast
kout-deployment
kout-proofs
test/kontrol/logs
test/properties/medusa/corpus/

# Metrics
coverage.out
Expand Down
5 changes: 5 additions & 0 deletions packages/contracts-bedrock/foundry.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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/'
82 changes: 82 additions & 0 deletions packages/contracts-bedrock/medusa.json
View file
Original file line number Diff line number Diff line change
@@ -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
}
}
2 changes: 1 addition & 1 deletion packages/contracts-bedrock/package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
71 changes: 71 additions & 0 deletions packages/contracts-bedrock/test/properties/PROPERTIES.md
View file
Original file line number Diff line number Diff line change
@@ -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
43 changes: 43 additions & 0 deletions packages/contracts-bedrock/test/properties/SUMMARY.md
View file
Original file line number Diff line number Diff line change
@@ -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
14 changes: 14 additions & 0 deletions packages/contracts-bedrock/test/properties/helpers/Utils.sol
View file
Original file line number Diff line number Diff line change
@@ -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);
}
}
151 changes: 151 additions & 0 deletions packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol
View file
Original file line number Diff line number Diff line change
@@ -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));
}
}

0 comments on commit f6c3f90

Please sign in to comment.