diff --git a/.gitmodules b/.gitmodules index 21ecaedbb77a..222d45be7ccc 100644 --- a/.gitmodules +++ b/.gitmodules @@ -29,3 +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 diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 3b69c67412f6..69b1fde5c5eb 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -21,7 +21,8 @@ remappings = [ 'ds-test/=lib/forge-std/lib/ds-test/src', 'safe-contracts/=lib/safe-contracts/contracts', 'kontrol-cheatcodes/=lib/kontrol-cheatcodes/src', - 'gelato/=lib/automate/contracts' + 'gelato/=lib/automate/contracts', + 'halmos-cheatcodes/=lib/halmos-cheatcodes/' ] extra_output = ['devdoc', 'userdoc', 'metadata', 'storageLayout'] bytecode_hash = 'none' @@ -101,3 +102,8 @@ script = 'test/kontrol/proofs' src = 'test/properties/medusa/' test = 'test/properties/medusa/' script = 'test/properties/medusa/' + +[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 new file mode 100644 index 000000000000..c431c6c3a532 --- /dev/null +++ b/packages/contracts-bedrock/halmos.toml @@ -0,0 +1,15 @@ +# 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 290f01574ead..a003558bb91e 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -25,6 +25,13 @@ 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 new file mode 160000 index 000000000000..c0d865508c0f --- /dev/null +++ b/packages/contracts-bedrock/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/packages/contracts-bedrock/test/invariants/PROPERTIES.md b/packages/contracts-bedrock/test/invariants/PROPERTIES.md new file mode 100644 index 000000000000..5a5cc71d73b5 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/PROPERTIES.md @@ -0,0 +1,73 @@ +# supertoken properties + +legend: + +- `[ ]`: property not yet tested +- `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it +- `[X]`: tested/proven property +- `[~]`: partially tested/proven property +- `:(`: property won't be tested due to some limitation + +## Unit test + +| id | description | halmos | medusa | +| --- | ---------------------------------------------------------------------------------- | ------ | ------ | +| 0 | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | +| 1 | supertoken token address depends on name, remote token, address and decimals | [ ] | [ ] | +| 2 | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | [ ] | +| 3 | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | +| 4 | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | +| 5 | convert() burns the same amount of one token that it mints of the other | [ ] | [ ] | + +## Valid state + +| id | description | halmos | medusa | +| --- | ------------------------------------------------------------------------------------------ | ------- | ------ | +| 6 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | +| 7 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | + +## Variable transition + +| id | description | halmos | medusa | +| --- | ------------------------------------------------------------------------------------------------- | ------ | ------ | +| 8 | sendERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 9 | relayERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 10 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | +| 11 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | +| 12 | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [ ] | +| 13 | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | +| 14 | supertoken total supply starts at zero | [x] | [ ] | +| 15 | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | +| 16 | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | [ ] | + +## High level + +| id | description | halmos | medusa | +| --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | +| 17 | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | +| 18 | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | +| 19 | sum of total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | +| 20 | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ] | [ ] | +| 21 | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [ ] | + +## Atomic bridging pseudo-properties + +As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction) +It’s worth noting that these properties will not hold for a live system + +| id | description | halmos | medusa | +| --- | ---------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | +| 22 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [x] | +| 23 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [x] | +| 24 | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | + +# 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) + +# Invariant-breaking candidates (brain dump) + +here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants + +- [ ] changing the decimals of tokens after deployment +- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 36b7b330ab0b..25dc9b036d3b 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -54,6 +54,7 @@ Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already h # Ecosystem properties legend: + - `[ ]`: property not yet tested - `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it - `[X]`: tested/proven property @@ -73,22 +74,22 @@ legend: ## Valid state -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [ ] | [ ] | -| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[ ]** | [ ] | +| id | milestone | description | halmos | medusa | +| --- | --- | --- | --- | --- | +| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | +| 7 | SupERC20 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | ## Variable transition | id | milestone | description | halmos | medusa | | --- | --- | --- | --- | --- | -| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [ ] | [ ] | -| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [ ] | [ ] | -| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [ ] | [ ] | -| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ] | [ ] | -| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [ ] | [~] | -| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [ ] | [ ] | -| 14 | SupERC20 | supertoken total supply starts at zero | [ ] | [x] | +| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [x] | [ ] | +| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | +| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | +| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] | +| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | +| 14 | SupERC20 | supertoken total supply starts at zero | [x] | [x] | | 15 | Factories | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | | 16 | Factories | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | [ ] | diff --git a/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol new file mode 100644 index 000000000000..fb8732f384f8 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol @@ -0,0 +1,25 @@ +// 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 new file mode 100644 index 000000000000..a6285ac58e08 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol @@ -0,0 +1,237 @@ +// 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 new file mode 100644 index 000000000000..75bfe2f7c9e1 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/HalmosBase.sol @@ -0,0 +1,18 @@ +// 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)); + } +}