Skip to content

Commit

Permalink
feat: superc20 kontrol tests (#36)
Browse files Browse the repository at this point in the history
  • Loading branch information
0xDiscotech authored Sep 18, 2024
1 parent 91e306b commit da66366
Show file tree
Hide file tree
Showing 16 changed files with 1,792 additions and 0 deletions.
4 changes: 4 additions & 0 deletions packages/contracts-bedrock/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ broadcast
kout-deployment
kout-proofs
test/kontrol/logs
out/

# Metrics
coverage.out
Expand Down Expand Up @@ -40,3 +41,6 @@ deploy-config/devnetL1.json

# Getting Started guide deploy config
deploy-config/getting-started.json

# Supererc20 kontrol
out-kontrol-properties/
12 changes: 12 additions & 0 deletions packages/contracts-bedrock/foundry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -97,3 +97,15 @@ src = 'test/kontrol/proofs'
out = 'kout-proofs'
test = 'test/kontrol/proofs'
script = 'test/kontrol/proofs'

[profile.kontrol-properties]
src = "test/properties/kontrol"
test = "test/properties/kontrol"
script = "test/properties/kontrol"
out = 'out-kontrol-properties'
# Make sure to export the variables $STATE_DIFF_DIR and $STATE_DIFF_NAME in your shell
fs_permissions = [
{ access = 'read', path = './supererc20-state-diff' },
{ access = 'read-write', path = './supererc20-state-diff/StateDiff.json' },
{ access = 'read-write', path = './supererc20-state-diff/AddressNames.json' }
]
44 changes: 44 additions & 0 deletions packages/contracts-bedrock/kontrol.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
[build.default]
foundry-project-root = './'
regen = false
rekompile = false
verbose = false
debug = false
auxiliary-lemmas = true

# require = 'lemmas.k'
# module-import = 'TestBase:KONTROL-LEMMAS'

[prove.default]
foundry-project-root = './'
verbose = false
debug = false
max-depth = 25000
reinit = false
cse = false
workers = 1
failure-information = true
counterexample-information = true
minimize-proofs = false
fail-fast = true
smt-timeout = 1000
break-every-step = false
break-on-jumpi = false
break-on-calls = false
break-on-storage = false
break-on-basic-blocks = false
break-on-cheatcodes = false
run-constructor = true
symbolic-immutables = false
schedule = 'CANCUN'
init-node-from-diff = 'supererc20-state-diff/StateDiff.json'

[show.default]
foundry-project-root = '.'
verbose = false
debug = false
use-hex-encoding = false

[view-kcfg.default]
foundry-project-root = '.'
use-hex-encoding = false
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{
"0x2e234DAe75C793f67A35089C9d99245E1C58470b": "sourceToken",
"0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f": "superchainERC20Impl",
"0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9": "mockL2ToL2Messenger",
"0xF62849F9A0B5Bf2913b396098F7c7019b51A820a": "destToken"
}
585 changes: 585 additions & 0 deletions packages/contracts-bedrock/supererc20-state-diff/StateDiff.json

Large diffs are not rendered by default.

123 changes: 123 additions & 0 deletions packages/contracts-bedrock/test/properties/FoundryDebugSymbolic.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
import { Predeploys } from "src/libraries/Predeploys.sol";
import { MockL2ToL2Messenger } from "test/properties/kontrol/helpers/MockL2ToL2Messenger.sol";
import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol";
import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol";
import "forge-std/Test.sol";

// TODO: File to debug faster with foundry replicating scenarios where the proof failed, needs removal afterwards.
contract FoundryDebugTests is KontrolBase {
event CrossDomainMessageSender(address _sender);

function setUp() public {
// Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used
superchainERC20Impl = new OptimismSuperchainERC20();
sourceToken = OptimismSuperchainERC20(
address(
// TODO: Update to beacon proxy
new ERC1967Proxy(
address(superchainERC20Impl),
abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
)
)
);

destToken = OptimismSuperchainERC20(
address(
// TODO: Update to beacon proxy
new ERC1967Proxy(
address(superchainERC20Impl),
abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
)
)
);

mockL2ToL2Messenger =
new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, SOURCE);
vm.etch(address(MESSENGER), address(mockL2ToL2Messenger).code);
}

/// Check setup works as expected
function test_proveSetup() public {
// Source token
assert(remoteToken != address(0));
assert(sourceToken.remoteToken() == remoteToken);
assert(eqStrings(sourceToken.name(), name));
assert(eqStrings(sourceToken.symbol(), symbol));
assert(sourceToken.decimals() == decimals);
vm.prank(address(sourceToken));
assert(MESSENGER.crossDomainMessageSender() == address(sourceToken));

// Destination token
assert(destToken.remoteToken() == remoteToken);
assert(eqStrings(destToken.name(), name));
assert(eqStrings(destToken.symbol(), symbol));
assert(destToken.decimals() == decimals);
assert(MESSENGER.DESTINATION_CHAIN_ID() == DESTINATION_CHAIN_ID);
vm.prank(address(destToken));
assert(MESSENGER.crossDomainMessageSender() == address(destToken));

// Custom cross domain sender
MESSENGER.forTest_setCustomCrossDomainSender(address(420));
assert(MESSENGER.crossDomainMessageSender() == address(420));
}

// debug property-id 8
// `sendERC20` with a value of zero does not modify accounting
function test_proveSendERC20ZeroCall() public {
/* Preconditions */
address _from = address(511347974759188522659820409854212399244223280810);
address _to = address(376793390874373408599387495934666716005045108769); // 0x7Fa9385Be102aC3eac297483DD6233d62B3e1497
uint256 _chainId = 0;

uint256 _totalSupplyBefore = sourceToken.totalSupply();
uint256 _fromBalanceBefore = sourceToken.balanceOf(_from);
uint256 _toBalanceBefore = sourceToken.balanceOf(_to);

vm.startPrank(_from);
/* Action */
sourceToken.sendERC20(_to, ZERO_AMOUNT, _chainId);

/* Postcondition */
assert(sourceToken.totalSupply() == _totalSupplyBefore);
assert(sourceToken.balanceOf(_from) == _fromBalanceBefore);
assert(sourceToken.balanceOf(_to) == _toBalanceBefore);
}
// ORIGIN_ID = 645326474426547203313410069153905908525362434350
// CALLER_ID = 645326474426547203313410069153905908525362434350
// NUMBER_CELL = 16777217
// VV2__chainId_114b9705 = 0
// VV0__from_114b9705 = 511347974759188522659820409854212399244223280810
// TIMESTAMP_CELL = 1073741825
// VV1__to_114b9705 = 376793390874373408599387495934666716005045108769

// debug 9
// `relayERC20` with a value of zero does not modify accounting
function test_proveRelayERC20ZeroCall() public {
/* Preconditions */
address _from = address(645326474426547203313410069153905908525362434350);
address _to = address(728815563385977040452943777879061427756277306519);

uint256 _totalSupplyBefore = sourceToken.totalSupply();
uint256 _fromBalanceBefore = sourceToken.balanceOf(_from);
uint256 _toBalanceBefore = sourceToken.balanceOf(_to);

vm.prank(address(MESSENGER));
/* Action */
sourceToken.relayERC20(_from, _to, ZERO_AMOUNT);

/* Postconditions */
assert(sourceToken.totalSupply() == _totalSupplyBefore);
assert(sourceToken.balanceOf(_from) == _fromBalanceBefore);
assert(sourceToken.balanceOf(_to) == _toBalanceBefore);
}
// VV0__from_114b9705 = 645326474426547203313410069153905908525362434350
// ORIGIN_ID = 645326474426547203313410069153905908525362434350
// CALLER_ID = 645326474426547203313410069153905908525362434350
// NUMBER_CELL = 16777217
// VV1__to_114b9705 = 728815563385977040452943777879061427756277306519
// TIMESTAMP_CELL = 1073741825
}
126 changes: 126 additions & 0 deletions packages/contracts-bedrock/test/properties/PROPERTIES.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,126 @@
# 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 [Kontrol](https://docs.runtimeverification.com/kontrol) 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 | kontrol | 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 | kontrol | medusa |
| --- | --------- | ------------------------------------------------------------------------------------------ | ------- | ------ |
| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] |
| 7 | SupERC20 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[x]** | [ ] |

## Variable transition

| id | milestone | description | kontrol | 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 | [x] | [ ] |
| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] |
| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] |
| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] |
| 14 | SupERC20 | supertoken total supply starts at zero | [x] | [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 | kontrol | 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 | kontrol | 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
Loading

0 comments on commit da66366

Please sign in to comment.