test: superc20 tob properties (#27)

* chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady
defi-wonderland · Aug 26, 2024 · 3adeba5 · 3adeba5
1 parent 96ecaad
commit 3adeba5
Show file tree

Hide file tree

Showing 9 changed files with 96 additions and 8 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -32,3 +32,6 @@
 [submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"]
 	path = packages/contracts-bedrock/lib/halmos-cheatcodes
 	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "packages/contracts-bedrock/lib/properties"]
+	path = packages/contracts-bedrock/lib/properties
+	url = https://github.com/crytic/properties
diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml
@@ -17,6 +17,7 @@ remappings = [
   '@rari-capital/solmate/=lib/solmate',
   '@lib-keccak/=lib/lib-keccak/contracts/lib',
   '@solady/=lib/solady/src',
+  '@crytic/properties/=lib/properties/',
   'forge-std/=lib/forge-std/src',
   'ds-test/=lib/forge-std/lib/ds-test/src',
   'safe-contracts/=lib/safe-contracts/contracts',

diff --git a/packages/contracts-bedrock/lib/properties b/packages/contracts-bedrock/lib/properties
diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json
@@ -55,7 +55,11 @@
 				]
 			},
 			"targetFunctionSignatures": [],
-			"excludeFunctionSignatures": []
+			"excludeFunctionSignatures": [
+        "ProtocolProperties.test_ERC20external_zeroAddressBalance()",
+        "ProtocolProperties.test_ERC20external_transferToZeroAddress()",
+        "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)"
+      ]
 		},
 		"chainConfig": {
 			"codeSizeCheckDisabled": true,

diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md
@@ -117,7 +117,7 @@ It’s worth noting that these properties will not hold for a live system
 
 # 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)
+- [x] 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)
 

diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol
@@ -13,16 +13,20 @@ contract Actors is StdUtils {
     /// usually called with msg.sender as a parameter, to track the actors
     /// already provided by the fuzzer
     modifier withActor(address who) {
+        addActor(who);
+        _currentActor = who;
+        _;
+    }
+
+    function addActor(address who) internal {
         if (!_isActor[who]) {
             _isActor[who] = true;
             _actors.push(who);
         }
-        _currentActor = who;
-        _;
     }
 
     /// @notice get the currently configured actor, should equal msg.sender
-    function currentActor() internal view returns(address){
+    function currentActor() internal view returns (address) {
         return _currentActor;
     }
 

diff --git a/...s/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/...s/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: AGPL-3
+pragma solidity ^0.8.25;
+
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+
+contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 {
+    bool public constant isMintableOrBurnable = true;
+    uint256 public initialSupply = 0;
+}
diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
@@ -3,13 +3,30 @@ pragma solidity ^0.8.25;
 
 import { TestBase } from "forge-std/Base.sol";
 
+import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
+import { CryticERC20ExternalBasicProperties } from
+    "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol";
 import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 
-contract ProtocolProperties is ProtocolHandler {
+contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperties {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
+    /// @dev `token` is the token under test for the ToB properties. This is coupled
+    /// to the ProtocolHandler constructor initializing at least one supertoken
+    constructor() {
+        token = ITokenMock(allSuperTokens[0]);
+    }
+
+    /// @dev not that much of a handler, since this only changes which
+    /// supertoken the ToB assertions are performed against. Thankfully, they are
+    /// implemented in a way that don't require tracking ghost variables or can
+    /// break properties defined by us
+    function handler_ToBTestOtherToken(uint256 index) external {
+        token = ITokenMock(allSuperTokens[bound(index, 0, allSuperTokens.length - 1)]);
+    }
+
     // TODO: will need rework after
     //   - non-atomic bridge
     //   - `convert`

diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol
@@ -7,6 +7,7 @@ import { StdUtils } from "forge-std/StdUtils.sol";
 import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { OptimismSuperchainERC20ForToBProperties } from "../../helpers/OptimismSuperchainERC20ForToBProperties.t.sol";
 import { Predeploys } from "src/libraries/Predeploys.sol";
 import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
 import { Actors } from "../../helpers/Actors.t.sol";
@@ -37,18 +38,20 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
     address[] internal remoteTokens;
     address[] internal allSuperTokens;
 
-    //@notice  'real' deploy salt => total supply sum across chains
+    /// @notice  'real' deploy salt => total supply sum across chains
     EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains;
 
     constructor() {
         vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code);
-        superchainERC20Impl = new OptimismSuperchainERC20();
+        superchainERC20Impl = new OptimismSuperchainERC20ForToBProperties();
         for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) {
             _deployRemoteToken();
             for (uint256 supertokenChainId = 0; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) {
                 _deploySupertoken(remoteTokens[remoteTokenIndex], WORDS[0], WORDS[0], DECIMALS[0], supertokenChainId);
             }
         }
+        // integrate with all ToB properties using address(this) as the sender
+        addActor(address(this));
     }
 
     /// @notice the deploy params are _indexes_ to pick from a pre-defined array of options and limit
@@ -81,6 +84,52 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
         ghost_totalSupplyAcrossChains.set(MESSENGER.superTokenInitDeploySalts(addr), currentValue + amount);
     }
 
+    /// @notice The ToB properties don't preclude the need for this since they
+    /// always use address(this) as the caller, which won't get any balance
+    /// until it's transferred to it somehow
+    function handler_SupERC20Transfer(
+        uint256 tokenIndex,
+        uint256 toIndex,
+        uint256 amount
+    )
+        external
+        withActor(msg.sender)
+    {
+        vm.prank(currentActor());
+        OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer(
+            getActorByRawIndex(toIndex), amount
+        );
+    }
+
+    function handler_SupERC20TransferFrom(
+        uint256 tokenIndex,
+        uint256 fromIndex,
+        uint256 toIndex,
+        uint256 amount
+    )
+        external
+        withActor(msg.sender)
+    {
+        vm.prank(currentActor());
+        OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transferFrom(
+            getActorByRawIndex(fromIndex), getActorByRawIndex(toIndex), amount
+        );
+    }
+
+    function handler_SupERC20Approve(
+        uint256 tokenIndex,
+        uint256 spenderIndex,
+        uint256 amount
+    )
+        external
+        withActor(msg.sender)
+    {
+        vm.prank(currentActor());
+        OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).approve(
+            getActorByRawIndex(spenderIndex), amount
+        );
+    }
+
     /// @notice deploy a remote token, that supertokens will be a representation of. They are  never called, so there
     /// is no need to actually deploy a contract for them
     function _deployRemoteToken() internal {