From 612c1375694fe3286add09a6a7a964fdbc22cdfe Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 20 Aug 2024 20:30:55 -0300 Subject: [PATCH 1/7] chore: add crytic/properties dependency --- .gitmodules | 3 +++ packages/contracts-bedrock/foundry.toml | 1 + packages/contracts-bedrock/lib/properties | 1 + 3 files changed, 5 insertions(+) create mode 160000 packages/contracts-bedrock/lib/properties 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 From 4893fbabd19a928737515ea665b3e33aebc0a525 Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 21 Aug 2024 11:40:54 -0300 Subject: [PATCH 2/7] test: extend protocol properties so it also covers ToB erc20 properties --- .../test/properties/helpers/Actors.t.sol | 2 +- ...imismSuperchainERC20ForToBProperties.t.sol | 9 +++++++++ .../medusa/Protocol.properties.t.sol | 19 ++++++++++++++++++- .../medusa/handlers/Protocol.handler.t.sol | 3 ++- 4 files changed, 30 insertions(+), 3 deletions(-) create mode 100644 packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol index 2f07acb0e5d9..5843bfd243cd 100644 --- a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol @@ -22,7 +22,7 @@ contract Actors is StdUtils { } /// @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..627c279e79e9 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"; @@ -42,7 +43,7 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { 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++) { From 64b59fb142c471a0f2514b310216e967f9130fce Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 21 Aug 2024 11:41:25 -0300 Subject: [PATCH 3/7] chore: small linter fixes --- .../test/properties/medusa/handlers/Protocol.handler.t.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 627c279e79e9..39d843e3d335 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 @@ -38,7 +38,7 @@ 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() { From dfd25cb9f0d32786e53409d286fd73a7582c1e10 Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 21 Aug 2024 12:20:46 -0300 Subject: [PATCH 4/7] docs: update property list --- packages/contracts-bedrock/test/properties/PROPERTIES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) From 50f6e2e66f55ac7df25b4eb359b71ceae596b3fe Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 20 Aug 2024 20:56:58 -0300 Subject: [PATCH 5/7] test: handlers for remaining superc20 state transitions --- .../medusa/handlers/Protocol.handler.t.sol | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) 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 39d843e3d335..f2069dda66d3 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 @@ -82,6 +82,45 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { ghost_totalSupplyAcrossChains.set(MESSENGER.superTokenInitDeploySalts(addr), currentValue + amount); } + function handler_SupERC20Transfer( + uint256 tokenIndex, + address recipient, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer(recipient, amount); + } + + function handler_SupERC20TransferFrom( + uint256 tokenIndex, + address from, + address to, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transferFrom( + from, to, amount + ); + } + + function handler_SupERC20Approve( + uint256 tokenIndex, + address spender, + uint256 amount + ) + external + withActor(msg.sender) + { + vm.prank(currentActor()); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer(spender, 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 { From 1cbdfab55076d5e433ee486917797cde49589fc8 Mon Sep 17 00:00:00 2001 From: teddy Date: Wed, 21 Aug 2024 18:11:23 -0300 Subject: [PATCH 6/7] fix: disable ToB properties we are not using and guide the fuzzer a bit more --- packages/contracts-bedrock/medusa.json | 5 +++- .../test/properties/helpers/Actors.t.sol | 8 +++++-- .../medusa/handlers/Protocol.handler.t.sol | 23 +++++++++++++------ 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index cb4737956fea..1e76338ea28f 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -55,7 +55,10 @@ ] }, "targetFunctionSignatures": [], - "excludeFunctionSignatures": [] + "excludeFunctionSignatures": [ + "ProtocolProperties.test_ERC20external_transferToZeroAddress()", + "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)" + ] }, "chainConfig": { "codeSizeCheckDisabled": true, diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol index 5843bfd243cd..3a7400667518 100644 --- a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol @@ -13,12 +13,16 @@ 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 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 f2069dda66d3..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 @@ -50,6 +50,8 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { _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 @@ -82,22 +84,27 @@ 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, - address recipient, + uint256 toIndex, uint256 amount ) external withActor(msg.sender) { vm.prank(currentActor()); - OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer(recipient, amount); + OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer( + getActorByRawIndex(toIndex), amount + ); } function handler_SupERC20TransferFrom( uint256 tokenIndex, - address from, - address to, + uint256 fromIndex, + uint256 toIndex, uint256 amount ) external @@ -105,20 +112,22 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { { vm.prank(currentActor()); OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transferFrom( - from, to, amount + getActorByRawIndex(fromIndex), getActorByRawIndex(toIndex), amount ); } function handler_SupERC20Approve( uint256 tokenIndex, - address spender, + uint256 spenderIndex, uint256 amount ) external withActor(msg.sender) { vm.prank(currentActor()); - OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).transfer(spender, amount); + 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 From 3b1af6ca0e26ba5b16016ae1f47a95c54dc63acb Mon Sep 17 00:00:00 2001 From: teddy Date: Thu, 22 Aug 2024 12:26:13 -0300 Subject: [PATCH 7/7] fix: disable another ToB property not implemented by solady --- packages/contracts-bedrock/medusa.json | 1 + 1 file changed, 1 insertion(+) diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index 1e76338ea28f..60e10b641de0 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -56,6 +56,7 @@ }, "targetFunctionSignatures": [], "excludeFunctionSignatures": [ + "ProtocolProperties.test_ERC20external_zeroAddressBalance()", "ProtocolProperties.test_ERC20external_transferToZeroAddress()", "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)" ]