From fea2dc557aace39f7d8d6eee97d3eeecf4d15313 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 3 Sep 2024 18:45:28 -0300 Subject: [PATCH] chore: remove halmos testsuite --- .gitmodules | 3 - packages/contracts-bedrock/foundry.toml | 6 - packages/contracts-bedrock/halmos.toml | 15 -- packages/contracts-bedrock/justfile | 7 - .../contracts-bedrock/lib/halmos-cheatcodes | 1 - .../properties/halmos/MockL2ToL2Messenger.sol | 25 -- .../halmos/OptimismSuperchainERC20.t.sol | 237 ------------------ .../test/properties/helpers/HalmosBase.sol | 18 -- 8 files changed, 312 deletions(-) delete mode 100644 packages/contracts-bedrock/halmos.toml delete mode 160000 packages/contracts-bedrock/lib/halmos-cheatcodes delete mode 100644 packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol delete mode 100644 packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol delete mode 100644 packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol diff --git a/.gitmodules b/.gitmodules index 7aacfd154993..dca839eef08e 100644 --- a/.gitmodules +++ b/.gitmodules @@ -29,9 +29,6 @@ [submodule "packages/contracts-bedrock/lib/openzeppelin-contracts-v5"] path = packages/contracts-bedrock/lib/openzeppelin-contracts-v5 url = https://github.com/OpenZeppelin/openzeppelin-contracts -[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 0e0d6959c5b6..87b5c15318ed 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -23,7 +23,6 @@ remappings = [ 'safe-contracts/=lib/safe-contracts/contracts', 'kontrol-cheatcodes/=lib/kontrol-cheatcodes/src', 'gelato/=lib/automate/contracts', - 'halmos-cheatcodes/=lib/halmos-cheatcodes/' ] extra_output = ['devdoc', 'userdoc', 'metadata', 'storageLayout'] bytecode_hash = 'none' @@ -104,8 +103,3 @@ src = 'test/properties/medusa/' test = 'test/properties/medusa/' script = 'test/properties/medusa/' via-ir=true - -[profile.halmos] -src = 'test/properties/halmos/' -test = 'test/properties/halmos/' -script = 'test/properties/halmos/' diff --git a/packages/contracts-bedrock/halmos.toml b/packages/contracts-bedrock/halmos.toml deleted file mode 100644 index c431c6c3a532..000000000000 --- a/packages/contracts-bedrock/halmos.toml +++ /dev/null @@ -1,15 +0,0 @@ -# Halmos configuration file - -## The version needed is `halmos 0.1.15.dev2+gc3f45dd` -## Just running `halmos` will run the tests with the default configuration - -[global] -# Contract to test -match-contract = "SymTest_" - -# Path to the Forge artifacts directory -forge_build_out = "./forge-artifacts" - - -# Storage layout -storage_layout = "generic" \ No newline at end of file diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile index a003558bb91e..290f01574ead 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -25,13 +25,6 @@ test-kontrol: test-medusa timeout='100': FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}} - -test-halmos-all VERBOSE="-v": - FOUNDRY_PROFILE=halmos halmos {{VERBOSE}} - -test-halmos TEST VERBOSE="-v": - FOUNDRY_PROFILE=halmos halmos --function {{TEST}} {{VERBOSE}} - test-rerun: build-go-ffi forge test --rerun -vvv diff --git a/packages/contracts-bedrock/lib/halmos-cheatcodes b/packages/contracts-bedrock/lib/halmos-cheatcodes deleted file mode 160000 index c0d865508c0f..000000000000 --- a/packages/contracts-bedrock/lib/halmos-cheatcodes +++ /dev/null @@ -1 +0,0 @@ -Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol deleted file mode 100644 index fb8732f384f8..000000000000 --- a/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol +++ /dev/null @@ -1,25 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity 0.8.25; - - -// TODO: Try to merge to a single mocked contract used by fuzzing and symbolic invariant tests - only if possible -// and low priorty -contract MockL2ToL2Messenger { - // Setting the current cross domain sender for the check of sender address equals the supertoken address - address internal immutable CROSS_DOMAIN_SENDER; - - constructor(address _xDomainSender) { - CROSS_DOMAIN_SENDER = _xDomainSender; - } - - function sendMessage(uint256 , address , bytes calldata) external payable { - } - - function crossDomainMessageSource() external view returns (uint256 _source) { - _source = block.chainid + 1; - } - - function crossDomainMessageSender() external view returns (address _sender) { - _sender = CROSS_DOMAIN_SENDER; - } -} diff --git a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol deleted file mode 100644 index a6285ac58e08..000000000000 --- a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol +++ /dev/null @@ -1,237 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity 0.8.25; - -import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -import { SymTest } from "halmos-cheatcodes/src/SymTest.sol"; -import { Predeploys } from "src/libraries/Predeploys.sol"; -import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; -import { MockL2ToL2Messenger } from "./MockL2ToL2Messenger.sol"; -import { HalmosBase } from "../helpers/HalmosBase.sol"; - -contract SymTest_OptimismSuperchainERC20 is SymTest, HalmosBase { - MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - - OptimismSuperchainERC20 public superchainERC20Impl; - OptimismSuperchainERC20 internal optimismSuperchainERC20; - - function setUp() public { - // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used - superchainERC20Impl = new OptimismSuperchainERC20(); - optimismSuperchainERC20 = OptimismSuperchainERC20( - address( - // TODO: Update to beacon proxy - new ERC1967Proxy( - address(superchainERC20Impl), - abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) - ) - ) - ); - - // Etch the mocked L2 to L2 Messenger since the messenger logic is out of scope for these test suite. Also, we - // avoid issues such as `TSTORE` opcode not being supported, or issues with `encodeVersionedNonce()` - address _mockL2ToL2CrossDomainMessenger = address(new MockL2ToL2Messenger(address(optimismSuperchainERC20))); - vm.etch(address(MESSENGER), _mockL2ToL2CrossDomainMessenger.code); - // NOTE: We need to set the crossDomainMessageSender as an immutable or otherwise storage vars and not taken - // into account when etching on halmos. Setting a constant slot with setters and getters didn't work neither. - } - - /// @notice Check setup works as expected - function check_setup() public view { - assert(optimismSuperchainERC20.remoteToken() == remoteToken); - assert(eqStrings(optimismSuperchainERC20.name(), name)); - assert(eqStrings(optimismSuperchainERC20.symbol(), symbol)); - assert(optimismSuperchainERC20.decimals() == decimals); - assert(MESSENGER.crossDomainMessageSender() == address(optimismSuperchainERC20)); - } - - /// @custom:property-id 6 - /// @custom:property Calls to sendERC20 succeed as long as caller has enough balance - function check_sendERC20SucceedsOnlyIfEnoughBalance( - uint256 _initialBalance, - address _from, - uint256 _amount, - address _to, - uint256 _chainId - ) - public - { - /* Preconditions */ - vm.assume(_chainId != CURRENT_CHAIN_ID); - vm.assume(_to != address(0)); - vm.assume(_from != address(0)); - - // Can't deal to unsupported cheatcode - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - optimismSuperchainERC20.mint(_from, _initialBalance); - - vm.prank(_from); - /* Action */ - try optimismSuperchainERC20.sendERC20(_to, _amount, _chainId) { - /* Postcondition */ - assert(_initialBalance >= _amount); - } catch { - assert(_initialBalance < _amount); - } - } - - /// @custom:property-id 7 - /// @custom:property Calls to relayERC20 always succeed as long as the sender the cross-domain caller are valid - function check_relayERC20OnlyFromL2ToL2Messenger( - address _crossDomainSender, - address _sender, - address _from, - address _to, - uint256 _amount - ) - public - { - /* Precondition */ - vm.assume(_to != address(0)); - // Deploying a new messenger because of an issue of not being able to etch the storage layout of the mock - // contract. So needed to a new one setting the symbolic immutable variable for the crossDomainSender. - vm.etch(address(MESSENGER), address(new MockL2ToL2Messenger(_crossDomainSender)).code); - - vm.prank(_sender); - /* Action */ - try optimismSuperchainERC20.relayERC20(_from, _to, _amount) { - /* Postconditions */ - assert( - _sender == address(MESSENGER) - && MESSENGER.crossDomainMessageSender() == address(optimismSuperchainERC20) - ); - } catch { - assert( - _sender != address(MESSENGER) - || MESSENGER.crossDomainMessageSender() != address(optimismSuperchainERC20) - ); - } - } - - /// @custom:property-id 8 - /// @custom:property `sendERC20` with a value of zero does not modify accounting - function check_sendERC20ZeroCall(address _from, address _to, uint256 _chainId) public { - /* Preconditions */ - vm.assume(_to != address(0)); - vm.assume(_chainId != CURRENT_CHAIN_ID); - vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER)); - - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); - - vm.startPrank(_from); - /* Action */ - optimismSuperchainERC20.sendERC20(_to, ZERO_AMOUNT, _chainId); - - /* Postcondition */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore); - assert(optimismSuperchainERC20.balanceOf(_from) == _fromBalanceBefore); - } - - /// @custom:property-id 9 - /// @custom:property `relayERC20` with a value of zero does not modify accounting - function check_relayERC20ZeroCall(address _from, address _to) public { - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - /* Preconditions */ - uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); - uint256 _toBalanceBefore = optimismSuperchainERC20.balanceOf(_to); - vm.prank(address(MESSENGER)); - - /* Action */ - optimismSuperchainERC20.relayERC20(_from, _to, ZERO_AMOUNT); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore); - assert(optimismSuperchainERC20.balanceOf(_from) == _fromBalanceBefore); - assert(optimismSuperchainERC20.balanceOf(_to) == _toBalanceBefore); - } - - /// @custom:property-id 10 - /// @custom:property `sendERC20` decreases the token's totalSupply in the source chain exactly by the input amount - function check_sendERC20DecreasesTotalSupply( - address _sender, - address _to, - uint256 _amount, - uint256 _chainId - ) - public - { - /* Preconditions */ - vm.assume(_to != address(0)); - vm.assume(_chainId != CURRENT_CHAIN_ID); - - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - optimismSuperchainERC20.mint(_sender, _amount); - - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_sender); - - vm.prank(_sender); - /* Action */ - optimismSuperchainERC20.sendERC20(_to, _amount, _chainId); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore - _amount); - assert(optimismSuperchainERC20.balanceOf(_sender) == _balanceBefore - _amount); - } - - /// @custom:property-id 11 - /// @custom:property `relayERC20` increases the token's totalSupply in the destination chain exactly by the input - /// amount - function check_relayERC20IncreasesTotalSupply(address _from, address _to, uint256 _amount) public { - vm.assume(_to != address(0)); - - /* Preconditions */ - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _toBalanceBefore = optimismSuperchainERC20.balanceOf(_to); - - vm.prank(address(MESSENGER)); - /* Action */ - optimismSuperchainERC20.relayERC20(_from, _to, _amount); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore + _amount); - assert(optimismSuperchainERC20.balanceOf(_to) == _toBalanceBefore + _amount); - } - - /// @custom:property-id 12 - /// @custom:property Increases the total supply on the amount minted by the bridge - function check_mint(address _from, uint256 _amount) public { - /* Preconditions */ - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_from); - - vm.startPrank(Predeploys.L2_STANDARD_BRIDGE); - /* Action */ - optimismSuperchainERC20.mint(_from, _amount); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore + _amount); - assert(optimismSuperchainERC20.balanceOf(_from) == _balanceBefore + _amount); - } - - /// @custom:property-id 13 - /// @custom:property Supertoken total supply only decreases on the amount burned by the bridge - function check_burn(address _from, uint256 _amount) public { - /* Preconditions */ - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - optimismSuperchainERC20.mint(_from, _amount); - - uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); - uint256 _balanceBefore = optimismSuperchainERC20.balanceOf(_from); - - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - /* Action */ - optimismSuperchainERC20.burn(_from, _amount); - - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == _totalSupplyBefore - _amount); - assert(optimismSuperchainERC20.balanceOf(_from) == _balanceBefore - _amount); - } - - /// @custom:property-id 14 - /// @custom:property Supertoken total supply starts at zero - function check_totalSupplyStartsAtZero() public view { - /* Postconditions */ - assert(optimismSuperchainERC20.totalSupply() == 0); - } -} diff --git a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol deleted file mode 100644 index 75bfe2f7c9e1..000000000000 --- a/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol +++ /dev/null @@ -1,18 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.25; - -import { Test } from "forge-std/Test.sol"; - -contract HalmosBase is Test { - uint256 internal constant CURRENT_CHAIN_ID = 1; - uint256 internal constant ZERO_AMOUNT = 0; - - address internal remoteToken = address(bytes20(keccak256("remoteToken"))); - string internal name = "SuperchainERC20"; - string internal symbol = "SUPER"; - uint8 internal decimals = 18; - - function eqStrings(string memory a, string memory b) internal pure returns (bool) { - return keccak256(abi.encode(a)) == keccak256(abi.encode(b)); - } -}