fix: fixes from self-review

Layr-Labs · Aug 14, 2024 · 466c605 · 466c605
1 parent 8331006
commit 466c605
Show file tree

Hide file tree

Showing 5 changed files with 89 additions and 63 deletions.
diff --git a/packages/contracts-bedrock/package.json b/packages/contracts-bedrock/package.json
@@ -30,6 +30,7 @@
     "kontrol-summary": "./test/kontrol/scripts/make-summary-deployment.sh",
     "kontrol-summary-fp": "KONTROL_FP_DEPLOYMENT=true pnpm kontrol-summary",
     "medusa":"FOUNDRY_PROFILE=medusa medusa fuzz",
+    "snapshots": "forge build && go run ./scripts/autogen/generate-snapshots . && pnpm kontrol-summary-fp && pnpm kontrol-summary",
     "snapshots:check": "./scripts/checks/check-snapshots.sh",
     "semver-lock": "forge script scripts/SemverLock.s.sol",
     "validate-deploy-configs": "./scripts/checks/check-deploy-configs.sh",

diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md
@@ -4,14 +4,15 @@ 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  | 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]    |
+| 0   | supertoken token address does not depend on the executing chain’s chainID          | [ ]    | [ ]    |
+| 1   | supertoken token address depends on name, remote token, address and decimals       | [ ]    | [ ]    |
 | 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                | [ ]    | [ ]    |
@@ -53,11 +54,11 @@ legend:
 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 |
+| id  | description                                                                                                                        | halmos | medusa  |
 | --- | ---                                                                                                                                | ---    | ---     |
-| 22  | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ]    | [ ]     |
-| 23  | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount                 | [ ]    | [ ]     |
-| 24  | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy)                 | [ ]    | [ ]     |
+| 22  | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ]    | [x]     |
+| 23  | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount                 | [ ]    | [x]     |
+| 24  | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy)                 | [ ]    | [~]     |
 
 # Expected external interactions
 

diff --git a/packages/contracts-bedrock/test/properties/SUMMARY.md b/packages/contracts-bedrock/test/properties/SUMMARY.md
@@ -5,7 +5,7 @@
 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
+- formally prove with [Halmos](https://github.com/a16z/halmos) whenever possible
 
 ## Where to place the testing campaign
 
@@ -29,12 +29,12 @@ Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already h
 - [ ]  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)
+- [ ]  [L2ToL2CrossDomainMessenger](https://github.com/defi-wonderland/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* 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
+- 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 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

diff --git a/packages/contracts-bedrock/test/properties/helpers/MockCrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockCrossDomainMessenger.t.sol
@@ -0,0 +1,52 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.25;
+
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { SafeCall } from "src/libraries/SafeCall.sol";
+
+contract MockCrossDomainMessenger {
+    /////////////////////////////////////////////////////////
+    //  State vars mocking the L2toL2CrossDomainMessenger  //
+    /////////////////////////////////////////////////////////
+    address public crossDomainMessageSender;
+    address public crossDomainMessageSource;
+
+    ///////////////////////////////////////////////////
+    //  Helpers for cross-chain interaction mocking  //
+    ///////////////////////////////////////////////////
+    mapping(address => bytes32) public superTokenInitDeploySalts;
+    mapping(uint256 chainId => mapping(bytes32 reayDeployData => address)) public superTokenAddresses;
+
+    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;
+    }
+
+    ////////////////////////////////////////////////////////
+    //  Functions mocking the L2toL2CrossDomainMessenger  //
+    ////////////////////////////////////////////////////////
+
+    /// @dev 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);
+    }
+}
diff --git a/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol
@@ -7,42 +7,7 @@ import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Pr
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { Predeploys } from "src/libraries/Predeploys.sol";
-import { SafeCall } from "src/libraries/SafeCall.sol";
-
-contract MockCrossDomainMessenger {
-    address public crossDomainMessageSender;
-    address public crossDomainMessageSource;
-    mapping(address => bytes32) public superTokenInitDeploySalts;
-    mapping(uint256 chainId => mapping(bytes32 reayDeployData => address)) public superTokenAddresses;
-    // 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 {
-        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);
-    }
-}
+import { MockCrossDomainMessenger } from "../helpers/MockCrossDomainMessenger.t.sol";
 
 contract ProtocolAtomicFuzz is Test {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
@@ -62,15 +27,15 @@ contract ProtocolAtomicFuzz is Test {
 
     struct TokenDeployParams {
         uint8 remoteTokenIndex;
-        uint8 name;
-        uint8 symbol;
-        uint8 decimals;
+        uint8 nameIndex;
+        uint8 symbolIndex;
+        uint8 decimalsIndex;
     }
 
     address[] internal remoteTokens;
     address[] internal allSuperTokens;
 
-    // deploy salt => total supply sum across chains
+    //@dev  'real' deploy salt => total supply sum across chains
     EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains;
 
     constructor() {
@@ -86,9 +51,9 @@ contract ProtocolAtomicFuzz is Test {
 
     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));
+        params.nameIndex = uint8(bound(params.nameIndex, 0, WORDS.length - 1));
+        params.symbolIndex = uint8(bound(params.symbolIndex, 0, WORDS.length - 1));
+        params.decimalsIndex = uint8(bound(params.decimalsIndex, 0, DECIMALS.length - 1));
         _;
     }
 
@@ -102,15 +67,19 @@ contract ProtocolAtomicFuzz is Test {
         chainId = bound(chainId, 0, MAX_CHAINS - 1);
         _deploySupertoken(
             remoteTokens[params.remoteTokenIndex],
-            WORDS[params.name],
-            WORDS[params.symbol],
-            DECIMALS[params.decimals],
+            WORDS[params.nameIndex],
+            WORDS[params.symbolIndex],
+            DECIMALS[params.decimalsIndex],
             chainId
         );
     }
 
     /// @custom:property-id 22
+    /// @custom:property sendERC20 decreases sender balance in source chain and increases receiver balance in
+    /// destination chain exactly by the input amount
     /// @custom:property-id 23
+    /// @custom:property sendERC20 decreases total supply in source chain and increases it in destination chain exactly
+    /// by the input amount
     function fuzz_SelfBridgeSupertoken(uint256 fromIndex, uint256 destinationChainId, uint256 amount) external {
         destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1);
         fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1);
@@ -122,10 +91,10 @@ contract ProtocolAtomicFuzz is Test {
         require(address(destinationToken) != address(0));
         uint256 sourceBalanceBefore = sourceToken.balanceOf(msg.sender);
         uint256 sourceSupplyBefore = sourceToken.totalSupply();
-        // NOTE: lift this requirement to allow one more failure mode
         uint256 destinationBalanceBefore = destinationToken.balanceOf(msg.sender);
         uint256 destinationSupplyBefore = destinationToken.totalSupply();
 
+        // NOTE: lift this requirement to allow one more failure mode
         amount = bound(amount, 0, sourceBalanceBefore);
         vm.prank(msg.sender);
         try sourceToken.sendERC20(msg.sender, amount, destinationChainId) {
@@ -160,6 +129,9 @@ contract ProtocolAtomicFuzz is Test {
     //   - non-atomic bridge
     //   - `convert`
     /// @custom:property-id 24
+    /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)-
+    /// convert(super, legacy)
+    /// @dev deliberately not a view method so medusa runs it but not the view methods defined by Test
     function property_totalSupplyAcrossChainsEqualsMints() external {
         for (uint256 i = 0; i < ghost_totalSupplyAcrossChains.length(); i++) {
             uint256 totalSupply = 0;
@@ -185,21 +157,21 @@ contract ProtocolAtomicFuzz is Test {
 
     function _deploySupertoken(
         address remoteToken,
-        string memory name,
-        string memory symbol,
+        string memory nameIndex,
+        string memory symbolIndex,
         uint8 decimals,
         uint256 chainId
     )
         internal
     {
-        bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals));
-        bytes32 hackySalt = keccak256(abi.encode(remoteToken, name, symbol, decimals, chainId));
+        bytes32 realSalt = keccak256(abi.encode(remoteToken, nameIndex, symbolIndex, decimals));
+        bytes32 hackySalt = keccak256(abi.encode(remoteToken, nameIndex, symbolIndex, decimals, chainId));
         OptimismSuperchainERC20 token = OptimismSuperchainERC20(
             address(
                 // TODO: Use the SuperchainERC20 Beacon Proxy
                 new ERC1967Proxy{ salt: hackySalt }(
                     address(superchainERC20Impl),
-                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
+                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, nameIndex, symbolIndex, decimals))
                 )
             )
         );
@@ -208,7 +180,7 @@ contract ProtocolAtomicFuzz is Test {
         uint256 mintAmount = INITIAL_TOKENS * 10 ** decimals;
         vm.prank(BRIDGE);
         token.mint(msg.sender, mintAmount);
-        (,uint256 curr) = ghost_totalSupplyAcrossChains.tryGet(realSalt);
+        (, uint256 curr) = ghost_totalSupplyAcrossChains.tryGet(realSalt);
         ghost_totalSupplyAcrossChains.set(realSalt, curr + mintAmount);
     }
 }