From 3adeba5008a74c1da96bdaf94071b834bc3bfcad Mon Sep 17 00:00:00 2001 From: teddy Date: Mon, 26 Aug 2024 09:51:29 -0300 Subject: [PATCH] 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 --- .gitmodules | 3 ++ packages/contracts-bedrock/foundry.toml | 1 + packages/contracts-bedrock/lib/properties | 1 + packages/contracts-bedrock/medusa.json | 6 ++- .../test/properties/PROPERTIES.md | 2 +- .../test/properties/helpers/Actors.t.sol | 10 ++-- ...imismSuperchainERC20ForToBProperties.t.sol | 9 ++++ .../medusa/Protocol.properties.t.sol | 19 ++++++- .../medusa/handlers/Protocol.handler.t.sol | 53 ++++++++++++++++++- 9 files changed, 96 insertions(+), 8 deletions(-) create mode 160000 packages/contracts-bedrock/lib/properties create mode 100644 packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol diff --git a/.gitmodules b/.gitmodules index 222d45be7ccc..7aacfd154993 100644 --- 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 index 69b1fde5c5eb..0e4aa4d0e354 100644 --- 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 new file mode 160000 index 000000000000..bb1b78542b3f --- /dev/null +++ b/packages/contracts-bedrock/lib/properties @@ -0,0 +1 @@ +Subproject commit bb1b78542b3f38e4ae56cf87389cd3ea94387f48 diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index cb4737956fea..60e10b641de0 100644 --- 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 index b2b992e371ff..5b580b8a37ea 100644 --- 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 index 2f07acb0e5d9..3a7400667518 100644 --- 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/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol new file mode 100644 index 000000000000..865534a9efa8 --- /dev/null +++ b/packages/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 index 47d1fe1c61a4..c5d227540441 100644 --- 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 index 15197a6786c6..d773d1ef90d3 100644 --- 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 {