wip

defi-wonderland · Aug 29, 2024 · b362a01 · b362a01
1 parent ef58dec
commit b362a01
Show file tree

Hide file tree

Showing 4 changed files with 89 additions and 2 deletions.
diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml
@@ -64,6 +64,12 @@ multiline_func_header='all'
 bracket_spacing=true
 wrap_comments=true
 
+[invariant]
+runs=1000
+depth=500
+fail_on_revert=false
+shrink_run_limit=5000
+
 ################################################################
 #                         PROFILE: CI                          #
 ################################################################

diff --git a/packages/contracts-bedrock/invariant-docs/README.md b/packages/contracts-bedrock/invariant-docs/README.md
@@ -19,6 +19,7 @@ This directory contains documentation for all defined invariant tests within `co
 - [OptimismPortal](./OptimismPortal.md)
 - [OptimismPortal2](./OptimismPortal2.md)
 - [OptimismSuperchainERC20](./OptimismSuperchainERC20.md)
+- [PROPERTIES.md](./PROPERTIES.md.md)
 - [ResourceMetering](./ResourceMetering.md)
 - [SafeCall](./SafeCall.md)
 - [SuperchainWETH](./SuperchainWETH.md)

diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
@@ -1,14 +1,81 @@
 // SPDX-License-Identifier: MIT
 pragma solidity 0.8.25;
+import "forge-std/console.sol";
 
 // Testing utilities
 import { Test, StdUtils, Vm } from "forge-std/Test.sol";
+import { StdInvariant } from "forge-std/StdInvariant.sol";
 import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol";
 
 // Libraries
 import { Predeploys } from "src/libraries/Predeploys.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol";
+import { ProtocolProperties } from "../properties/medusa/Protocol.properties.t.sol";
+import { MockL2ToL2CrossDomainMessenger } from "../properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+
+contract MedusaAdaptooor is Test {
+    ProtocolProperties internal properties;
+    MockL2ToL2CrossDomainMessenger internal constant MESSENGER =
+        MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+
+    function setUp() public {
+        properties = new ProtocolProperties();
+        targetContract(address(properties));
+    }
+
+    // TODO: will need rework after
+    //   - `convert`
+    /// @custom:property-id 19
+    /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
+    /// convert(super, legacy)
+    function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external  {
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < properties.deploySaltsLength(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = properties.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
+            uint256 fundsInTransit = properties.tokensInTransitForDeploySalt(currentSalt);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < properties.MAX_CHAINS(); validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            console.log('trackedSupply   :', trackedSupply);
+            console.log('totalSupply   :', totalSupply);
+            console.log('fundsInTransit   :', fundsInTransit);
+            assert(trackedSupply == totalSupply + fundsInTransit);
+        }
+    }
+
+    // TODO: will need rework after
+    //   - `convert`
+    /// @custom:property-id 21
+    /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
+    /// convert(super, legacy) when all when all cross-chain messages are processed
+    function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external  {
+        if (MESSENGER.messageQueueLength() != 0) {
+            return;
+        }
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < properties.deploySaltsLength(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = properties.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < properties.MAX_CHAINS(); validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            console.log('----');
+            console.log('trackedSupply   :', trackedSupply);
+            console.log('totalSupply   :', totalSupply);
+            assertEq(trackedSupply,  totalSupply);
+        }
+    }
+}
 
 /// @title OptimismSuperchainERC20_User
 /// @notice Actor contract that interacts with the OptimismSuperchainERC20 contract.

diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
@@ -15,12 +15,12 @@ import { Actors } from "../../helpers/Actors.t.sol";
 contract ProtocolHandler is TestBase, StdUtils, Actors {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
-    uint8 internal constant MAX_CHAINS = 4;
+    uint8 public constant MAX_CHAINS = 4;
     uint8 internal constant INITIAL_TOKENS = 1;
     uint8 internal constant INITIAL_SUPERTOKENS = 1;
     uint8 internal constant SUPERTOKEN_INITIAL_MINT = 100;
     address internal constant BRIDGE = Predeploys.L2_STANDARD_BRIDGE;
-    MockL2ToL2CrossDomainMessenger internal constant MESSENGER =
+    MockL2ToL2CrossDomainMessenger public constant MESSENGER =
         MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
     OptimismSuperchainERC20 internal superchainERC20Impl;
     // NOTE: having more options for this enables the fuzzer to configure
@@ -68,6 +68,19 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
         _;
     }
 
+    function deploySaltsLength() external view returns(uint length){
+        return ghost_totalSupplyAcrossChains.length();
+    }
+
+    function totalSupplyAcrossChainsAtIndex(uint index) external view returns(bytes32 salt, uint supply){
+        return ghost_totalSupplyAcrossChains.at(index);
+    }
+
+    function tokensInTransitForDeploySalt(bytes32 salt) external view returns(uint amount){
+        (,amount) = ghost_tokensInTransit.tryGet(salt);
+        return amount;
+    }
+
     function handler_MockNewRemoteToken() external {
         _deployRemoteToken();
     }