feat: kontrol symoblic tests

packages/contracts-bedrock/.gitignore

@@ -6,6 +6,7 @@ broadcast
 kout-deployment
 kout-proofs
 test/kontrol/logs
+out/
 
 # Metrics
 coverage.out
@@ -40,3 +41,6 @@ deploy-config/devnetL1.json
 
 # Getting Started guide deploy config
 deploy-config/getting-started.json
+
+# Supererc20 kontrol
+out-kontrol-properties/

packages/contracts-bedrock/foundry.toml

@@ -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' }
+]

packages/contracts-bedrock/kontrol.toml

@@ -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

packages/contracts-bedrock/supererc20-state-diff/AddressNames.json

@@ -0,0 +1,6 @@
+{
+  "0x2e234DAe75C793f67A35089C9d99245E1C58470b": "sourceToken",
+  "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f": "superchainERC20Impl",
+  "0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9": "mockL2ToL2Messenger",
+  "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a": "destToken"
+}

packages/contracts-bedrock/test/properties/FoundryDebugSymbolic.t.sol

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

packages/contracts-bedrock/test/properties/PROPERTIES.md

@@ -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