refactor: separate state transitions from pure properties

defi-wonderland · Aug 19, 2024 · 07ca17e · 07ca17e
1 parent 745dcbc
commit 07ca17e
Show file tree

Hide file tree

Showing 3 changed files with 41 additions and 29 deletions.
diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json
@@ -7,7 +7,7 @@
 		"callSequenceLength": 100,
 		"corpusDirectory": "test/properties/medusa/corpus/",
 		"coverageEnabled": true,
-		"targetContracts": ["ProtocolAtomicFuzz"],
+		"targetContracts": ["ProtocolProperties"],
 		"targetContractsBalances": [],
 		"constructorArgs": {},
 		"deployerAddress": "0x30000",
@@ -43,7 +43,7 @@
 				}
 			},
 			"propertyTesting": {
-				"enabled": false,
+				"enabled": true,
 				"testPrefixes": [
 					"property_"
 				]

diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.25;
+
+import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol";
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
+
+contract ProtocolProperties is ProtocolHandler {
+    using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
+    // TODO: will need rework after
+    //   - 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)
+
+    function property_totalSupplyAcrossChainsEqualsMints() external view returns (bool success) {
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < MAX_CHAINS; validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            if (trackedSupply != totalSupply) {
+                return false;
+            }
+        }
+        return true;
+    }
+}
diff --git a/...st/properties/medusa/ProtocolAtomic.t.sol → ...es/medusa/handlers/Protocol.handler.t.sol b/...st/properties/medusa/ProtocolAtomic.t.sol → ...es/medusa/handlers/Protocol.handler.t.sol
@@ -7,9 +7,9 @@ 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 { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
 
-contract ProtocolAtomicFuzz is Test {
+contract ProtocolHandler is Test {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
     uint8 internal constant MAX_CHAINS = 4;
@@ -132,33 +132,10 @@ contract ProtocolAtomicFuzz is Test {
         // medusa calls with different senders by default
         OptimismSuperchainERC20(addr).mint(msg.sender, amount);
         // currentValue will be zero if key is not present
-        (,uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr));
+        (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr));
         ghost_totalSupplyAcrossChains.set(MESSENGER.superTokenInitDeploySalts(addr), currentValue + amount);
     }
 
-    // TODO: will need rework after
-    //   - 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)
-    /// @notice deliberately not a view method so medusa runs it but not the view methods defined by Test
-    function property_totalSupplyAcrossChainsEqualsMints() external {
-        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
-        for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
-            uint256 totalSupply = 0;
-            (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex);
-            // and then over all the (mocked) chain ids where that supertoken could be deployed
-            for (uint256 validChainId = 0; validChainId < MAX_CHAINS; validChainId++) {
-                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
-                if (supertoken != address(0)) {
-                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
-                }
-            }
-            assert(trackedSupply == totalSupply);
-        }
-    }
-
     function fuzz_MockNewRemoteToken() external {
         _deployRemoteToken();
     }
@@ -183,7 +160,7 @@ contract ProtocolAtomicFuzz is Test {
         uint256 chainId
     )
         internal
-        returns(OptimismSuperchainERC20 supertoken)
+        returns (OptimismSuperchainERC20 supertoken)
     {
         // this salt would be used in production. Tokens sharing it will be bridgable with each other
         bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals));