diff --git a/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json b/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json index f1dba0541bbf..27e9fa3c0c13 100644 --- a/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json +++ b/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json @@ -503,8 +503,8 @@ "chainId": 31337, "forkId": 0 }, - "data": "0x610100604052348015610010575f80fd5b5060405161070538038061070583398101604081905261002f9161006a565b6001600160a01b0393841660805291831660a05260c0521660e0526100b4565b80516001600160a01b0381168114610065575f80fd5b919050565b5f805f806080858703121561007d575f80fd5b6100868561004f565b93506100946020860161004f565b9250604085015191506100a96060860161004f565b905092959194509250565b60805160a05160c05160e0516106036101025f395f6102ab01525f818160a901526102cf01525f818161025d0152818161028601526102fa01525f81816101fb015261022401526106035ff3fe608060405260043610610058575f3560e01c80632ea02369116100415780632ea023691461009857806338ffde18146100cb5780637056f41f14610104575f80fd5b80631ecd26f21461005c5780632479446214610071575b5f80fd5b61006f61006a366004610484565b610117565b005b34801561007c575f80fd5b506100856101d2565b6040519081526020015b60405180910390f35b3480156100a3575f80fd5b506100857f000000000000000000000000000000000000000000000000000000000000000081565b3480156100d6575f80fd5b506100df6101e3565b60405173ffffffffffffffffffffffffffffffffffffffff909116815260200161008f565b61006f610112366004610500565b6102cd565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610141929190610556565b5f6040518083038185875af1925050503d805f811461017b576040519150601f19603f3d011682016040523d82523d5f602084013e610180565b606091505b5091509150816101c757806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016101be9190610565565b60405180910390fd5b505050505050505050565b5f6101de4660016105b8565b905090565b5f73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000000000000000000000000000000000000000000016330361024657507f000000000000000000000000000000000000000000000000000000000000000090565b73ffffffffffffffffffffffffffffffffffffffff7f00000000000000000000000000000000000000000000000000000000000000001633036102a857507f000000000000000000000000000000000000000000000000000000000000000090565b507f000000000000000000000000000000000000000000000000000000000000000090565b7f000000000000000000000000000000000000000000000000000000000000000084036103e6575f6103557f00000000000000000000000000000000000000000000000000000000000000005f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f920191909152506103ec92505050565b9050806103e4576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016101be565b505b50505050565b5f6103f9845a8585610401565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff8116811461043a575f80fd5b919050565b5f8083601f84011261044f575f80fd5b50813567ffffffffffffffff811115610466575f80fd5b60208301915083602082850101111561047d575f80fd5b9250929050565b5f805f805f805f60c0888a03121561049a575f80fd5b8735965060208801359550604088013594506104b860608901610417565b93506104c660808901610417565b925060a088013567ffffffffffffffff8111156104e1575f80fd5b6104ed8a828b0161043f565b989b979a50959850939692959293505050565b5f805f8060608587031215610513575f80fd5b8435935061052360208601610417565b9250604085013567ffffffffffffffff81111561053e575f80fd5b61054a8782880161043f565b95989497509550505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011684010191505092915050565b808201808211156105f0577f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b9291505056fea164736f6c6343000819000a0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000", - "deployedCode": "0x608060405260043610610058575f3560e01c80632ea02369116100415780632ea023691461009857806338ffde18146100cb5780637056f41f14610104575f80fd5b80631ecd26f21461005c5780632479446214610071575b5f80fd5b61006f61006a366004610484565b610117565b005b34801561007c575f80fd5b506100856101d2565b6040519081526020015b60405180910390f35b3480156100a3575f80fd5b506100857f000000000000000000000000000000000000000000000000000000000000000281565b3480156100d6575f80fd5b506100df6101e3565b60405173ffffffffffffffffffffffffffffffffffffffff909116815260200161008f565b61006f610112366004610500565b6102cd565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610141929190610556565b5f6040518083038185875af1925050503d805f811461017b576040519150601f19603f3d011682016040523d82523d5f602084013e610180565b606091505b5091509150816101c757806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016101be9190610565565b60405180910390fd5b505050505050505050565b5f6101de4660016105b8565b905090565b5f73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b16330361024657507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a1633036102a857507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a90565b507f000000000000000000000000000000000000000000000000000000000000000090565b7f000000000000000000000000000000000000000000000000000000000000000284036103e6575f6103557f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f920191909152506103ec92505050565b9050806103e4576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016101be565b505b50505050565b5f6103f9845a8585610401565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff8116811461043a575f80fd5b919050565b5f8083601f84011261044f575f80fd5b50813567ffffffffffffffff811115610466575f80fd5b60208301915083602082850101111561047d575f80fd5b9250929050565b5f805f805f805f60c0888a03121561049a575f80fd5b8735965060208801359550604088013594506104b860608901610417565b93506104c660808901610417565b925060a088013567ffffffffffffffff8111156104e1575f80fd5b6104ed8a828b0161043f565b989b979a50959850939692959293505050565b5f805f8060608587031215610513575f80fd5b8435935061052360208601610417565b9250604085013567ffffffffffffffff81111561053e575f80fd5b61054a8782880161043f565b95989497509550505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011684010191505092915050565b808201808211156105f0577f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b9291505056fea164736f6c6343000819000a", + "data": "0x610100604052348015610010575f80fd5b5060405161078f38038061078f83398101604081905261002f9161006d565b6001600160a01b039384166080529190921660a05260c09190915260e0526100ad565b80516001600160a01b0381168114610068575f80fd5b919050565b5f805f8060808587031215610080575f80fd5b61008985610052565b935061009760208601610052565b6040860151606090960151949790965092505050565b60805160a05160c05160e05161068e6101015f395f8181609501526101b801525f818160d9015261037801525f818161030f0152818161033801526103a301525f81816102ad01526102d6015261068e5ff3fe60806040526004361061006e575f3560e01c806338ffde181161004c57806338ffde18146100fb5780637056f41f14610134578063722c2a4d14610147578063f230b4c2146101a7575f80fd5b80631ecd26f21461007257806324794462146100875780632ea02369146100c8575b5f80fd5b61008561008036600461052d565b6101da565b005b348015610092575f80fd5b507f00000000000000000000000000000000000000000000000000000000000000005b6040519081526020015b60405180910390f35b3480156100d3575f80fd5b506100b57f000000000000000000000000000000000000000000000000000000000000000081565b348015610106575f80fd5b5061010f610295565b60405173ffffffffffffffffffffffffffffffffffffffff90911681526020016100bf565b6100856101423660046105a9565b610376565b348015610152575f80fd5b506100856101613660046105ff565b5f80547fffffffffffffffffffffffff00000000000000000000000000000000000000001673ffffffffffffffffffffffffffffffffffffffff92909216919091179055565b3480156101b2575f80fd5b506100b57f000000000000000000000000000000000000000000000000000000000000000081565b5f808473ffffffffffffffffffffffffffffffffffffffff1634858560405161020492919061061f565b5f6040518083038185875af1925050503d805f811461023e576040519150601f19603f3d011682016040523d82523d5f602084013e610243565b606091505b50915091508161028a57806040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610281919061062e565b60405180910390fd5b505050505050505050565b5f73ffffffffffffffffffffffffffffffffffffffff7f00000000000000000000000000000000000000000000000000000000000000001633036102f857507f000000000000000000000000000000000000000000000000000000000000000090565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000000000000000000000000000000000000000000016330361035a57507f000000000000000000000000000000000000000000000000000000000000000090565b505f5473ffffffffffffffffffffffffffffffffffffffff1690565b7f0000000000000000000000000000000000000000000000000000000000000000840361048f575f6103fe7f00000000000000000000000000000000000000000000000000000000000000005f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f9201919091525061049592505050565b90508061048d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c6564000000000000000000000000000000000000000000000000006064820152608401610281565b505b50505050565b5f6104a2845a85856104aa565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff811681146104e3575f80fd5b919050565b5f8083601f8401126104f8575f80fd5b50813567ffffffffffffffff81111561050f575f80fd5b602083019150836020828501011115610526575f80fd5b9250929050565b5f805f805f805f60c0888a031215610543575f80fd5b873596506020880135955060408801359450610561606089016104c0565b935061056f608089016104c0565b925060a088013567ffffffffffffffff81111561058a575f80fd5b6105968a828b016104e8565b989b979a50959850939692959293505050565b5f805f80606085870312156105bc575f80fd5b843593506105cc602086016104c0565b9250604085013567ffffffffffffffff8111156105e7575f80fd5b6105f3878288016104e8565b95989497509550505050565b5f6020828403121561060f575f80fd5b610618826104c0565b9392505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f8301168401019150509291505056fea164736f6c6343000819000a0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000003", + "deployedCode": "0x60806040526004361061006e575f3560e01c806338ffde181161004c57806338ffde18146100fb5780637056f41f14610134578063722c2a4d14610147578063f230b4c2146101a7575f80fd5b80631ecd26f21461007257806324794462146100875780632ea02369146100c8575b5f80fd5b61008561008036600461052d565b6101da565b005b348015610092575f80fd5b507f00000000000000000000000000000000000000000000000000000000000000035b6040519081526020015b60405180910390f35b3480156100d3575f80fd5b506100b57f000000000000000000000000000000000000000000000000000000000000000281565b348015610106575f80fd5b5061010f610295565b60405173ffffffffffffffffffffffffffffffffffffffff90911681526020016100bf565b6100856101423660046105a9565b610376565b348015610152575f80fd5b506100856101613660046105ff565b5f80547fffffffffffffffffffffffff00000000000000000000000000000000000000001673ffffffffffffffffffffffffffffffffffffffff92909216919091179055565b3480156101b2575f80fd5b506100b57f000000000000000000000000000000000000000000000000000000000000000381565b5f808473ffffffffffffffffffffffffffffffffffffffff1634858560405161020492919061061f565b5f6040518083038185875af1925050503d805f811461023e576040519150601f19603f3d011682016040523d82523d5f602084013e610243565b606091505b50915091508161028a57806040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610281919061062e565b60405180910390fd5b505050505050505050565b5f73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b1633036102f857507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a16330361035a57507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a90565b505f5473ffffffffffffffffffffffffffffffffffffffff1690565b7f0000000000000000000000000000000000000000000000000000000000000002840361048f575f6103fe7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f9201919091525061049592505050565b90508061048d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c6564000000000000000000000000000000000000000000000000006064820152608401610281565b505b50505050565b5f6104a2845a85856104aa565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff811681146104e3575f80fd5b919050565b5f8083601f8401126104f8575f80fd5b50813567ffffffffffffffff81111561050f575f80fd5b602083019150836020828501011115610526575f80fd5b9250929050565b5f805f805f805f60c0888a031215610543575f80fd5b873596506020880135955060408801359450610561606089016104c0565b935061056f608089016104c0565b925060a088013567ffffffffffffffff81111561058a575f80fd5b6105968a828b016104e8565b989b979a50959850939692959293505050565b5f805f80606085870312156105bc575f80fd5b843593506105cc602086016104c0565b9250604085013567ffffffffffffffff8111156105e7575f80fd5b6105f3878288016104e8565b95989497509550505050565b5f6020828403121561060f575f80fd5b610618826104c0565b9392505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f8301168401019150509291505056fea164736f6c6343000819000a", "initialized": true, "kind": "Create", "newBalance": 0, diff --git a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol index cdbae879d0ff..37c591f24a63 100644 --- a/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol +++ b/packages/contracts-bedrock/test/properties/halmos/OptimismSuperchainERC20.t.sol @@ -50,6 +50,7 @@ contract SymTest_OptimismSuperchainERC20 is SymTest, HalmosBase { /// @notice Check setup works as expected function check_setup() public { // Source token + assert(remoteToken != address(0)); assert(sourceToken.remoteToken() == remoteToken); assert(eqStrings(sourceToken.name(), name)); assert(eqStrings(sourceToken.symbol(), symbol)); @@ -200,8 +201,6 @@ contract SymTest_OptimismSuperchainERC20 is SymTest, HalmosBase { /// @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 = sourceToken.totalSupply(); uint256 _toBalanceBefore = sourceToken.balanceOf(_to); diff --git a/packages/contracts-bedrock/test/properties/kontrol/FoundryDebugSymbolic.t.sol b/packages/contracts-bedrock/test/properties/kontrol/FoundryDebugSymbolic.t.sol index dd82f69dc6af..e6fd0b5ac8d9 100644 --- a/packages/contracts-bedrock/test/properties/kontrol/FoundryDebugSymbolic.t.sol +++ b/packages/contracts-bedrock/test/properties/kontrol/FoundryDebugSymbolic.t.sol @@ -3,7 +3,7 @@ pragma solidity 0.8.25; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; -import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol"; +import { MockL2ToL2Messenger } from "test/properties/kontrol/helpers/MockL2ToL2Messenger.sol"; import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol"; import { InitialState } from "./deployments/InitialState.sol"; import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; @@ -36,13 +36,14 @@ contract FoundryDebugTests is KontrolBase { ); mockL2ToL2Messenger = - new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, address(0)); + new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, SOURCE); vm.etch(address(MESSENGER), address(mockL2ToL2Messenger).code); } /// @notice Check setup works as expected function test_proveSetup() public { // Source token + assert(remoteToken != address(0)); assert(sourceToken.remoteToken() == remoteToken); assert(eqStrings(sourceToken.name(), name)); assert(eqStrings(sourceToken.symbol(), symbol)); @@ -65,40 +66,43 @@ contract FoundryDebugTests is KontrolBase { /// @custom:property-id 7 /// @custom:property Calls to relayERC20 always succeed as long as the sender the cross-domain caller are valid - function test_proveRelayERC20OnlyFromL2ToL2Messenger() public { - address _crossDomainSender = address(0); - address _sender = address(0); - address _from = address(645326474426547203313410069153905908525362434350); - address _to = address(728815563385977040452943777879061427756277306519); - uint256 _amount = 0; - - /* 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. - // Used 0 address on source token so when the `soureToken` calls it if returns the symbolic `_crossDomainSender` - vm.etch( - address(MESSENGER), address(new MockL2ToL2Messenger(address(0), address(0), 0, _crossDomainSender)).code - ); - - vm.prank(_sender); - /* Action */ - try sourceToken.relayERC20(_from, _to, _amount) { - /* Postconditions */ - assert(_sender == address(MESSENGER) && MESSENGER.crossDomainMessageSender() == address(sourceToken)); - } catch { - assert(_sender != address(MESSENGER) || MESSENGER.crossDomainMessageSender() != address(sourceToken)); - } - } + // function test_proveRelayERC20OnlyFromL2ToL2Messenger() public { + // address _crossDomainSender = address(0); + // address _sender = address(0); + // address _from = address(645326474426547203313410069153905908525362434350); + // address _to = address(728815563385977040452943777879061427756277306519); + // uint256 _amount = 0; + + // /* 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. + // // Used 0 address on source token so when the `soureToken` calls it if returns the symbolic + // `_crossDomainSender` + // vm.etch( + // address(MESSENGER), address(new MockL2ToL2Messenger(address(0), address(0), 0, _crossDomainSender)).code + // ); + + // vm.prank(_sender); + // /* Action */ + // try sourceToken.relayERC20(_from, _to, _amount) { + // /* Postconditions */ + // assert(_sender == address(MESSENGER) && MESSENGER.crossDomainMessageSender() == address(sourceToken)); + // } catch { + // assert(_sender != address(MESSENGER) || MESSENGER.crossDomainMessageSender() != address(sourceToken)); + // } + // } /// @custom:property-id 8 /// @custom:property `sendERC20` with a value of zero does not modify accounting function test_proveSendERC20ZeroCall() public { /* Preconditions */ // 0x4200000000000000000000000000000000000024 - address _from = address(376793390874373408599387495934666716005045108772); + // address _from = address(376793390874373408599387495934666716005045108772); // // 0x7Fa9385Be102aC3eac297483DD6233d62B3e1497 - address _to = address(728815563385977040452943777879061427756277306519); + // address _to = address(728815563385977040452943777879061427756277306519); // + address _from = address(263400868551549723330807389252719309078400616204); // 0x2e234dAE75c793F67a35089C9D99245e1C58470c + address _to = address(1); uint256 _chainId = 0; console.log("from : ", _from); diff --git a/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol b/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol index 283c4e639113..467b8c225540 100644 --- a/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol +++ b/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol @@ -4,7 +4,7 @@ pragma solidity ^0.8.25; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; -import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol"; +import { MockL2ToL2Messenger } from "test/properties/kontrol/helpers/MockL2ToL2Messenger.sol"; import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol"; import { RecordStateDiff } from "./helpers/RecordStateDiff.sol"; import { Test } from "forge-std/Test.sol"; @@ -12,6 +12,7 @@ import { Test } from "forge-std/Test.sol"; contract KontrolBase is Test, KontrolCheats, RecordStateDiff { uint256 internal constant CURRENT_CHAIN_ID = 1; uint256 internal constant DESTINATION_CHAIN_ID = 2; + uint256 internal constant SOURCE = 3; uint256 internal constant ZERO_AMOUNT = 0; MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); @@ -51,7 +52,7 @@ contract KontrolBase is Test, KontrolCheats, RecordStateDiff { ); mockL2ToL2Messenger = - new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, address(0)); + new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, SOURCE); save_address(address(superchainERC20Impl), "superchainERC20Impl"); save_address(address(sourceToken), "sourceToken"); diff --git a/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol b/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol index e805b26c0aa3..1a1a83ec3c22 100644 --- a/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol +++ b/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol @@ -3,7 +3,7 @@ pragma solidity 0.8.25; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; -import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol"; +import { MockL2ToL2Messenger } from "test/properties/kontrol/helpers/MockL2ToL2Messenger.sol"; import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol"; import { InitialState } from "./deployments/InitialState.sol"; @@ -36,8 +36,12 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { vm.prank(address(destToken)); assert(MESSENGER.crossDomainMessageSender() == address(destToken)); - // Custom cross domain sender + // Messenger + assert(MESSENGER.SOURCE() == SOURCE); assert(MESSENGER.crossDomainMessageSender() == address(0)); + // Check the setter works properly + MESSENGER.forTest_setCustomCrossDomainSender(address(420)); + assert(MESSENGER.crossDomainMessageSender() == address(420)); } /// @custom:property-id 6 @@ -87,17 +91,13 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { { setUpInlined(); + /* Preconditions */ + vm.assume(_to != address(0)); vm.assume(notBuiltinAddress(_from)); vm.assume(notBuiltinAddress(_to)); + vm.assume(notBuiltinAddress(_sender)); - /* 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. - // Used 0 address on source token so when the `soureToken` calls it if returns the symbolic `_crossDomainSender` - vm.etch( - address(MESSENGER), address(new MockL2ToL2Messenger(address(0), address(0), 0, _crossDomainSender)).code - ); + MESSENGER.forTest_setCustomCrossDomainSender(_crossDomainSender); vm.prank(_sender); /* Action */ @@ -117,6 +117,8 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { /* Preconditions */ vm.assume(_to != address(0)); vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER)); + // TODO + vm.assume(_from != address(0)); vm.assume(notBuiltinAddress(_from)); vm.assume(notBuiltinAddress(_to)); @@ -142,6 +144,10 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { /* Preconditions */ vm.assume(_to != address(0)); + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + // TODO + vm.assume(_to != address(1)); uint256 _totalSupplyBefore = sourceToken.totalSupply(); uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); @@ -274,7 +280,7 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { /// @custom:property-id 23 /// @custom:property `sendERC20` decreases total supply in source chain and increases it in destination chain /// exactly by the input amount - function prove_crossChainMintAndBurn(address _from, address _to, uint256 _amount, uint256 _chainId) public { + function prove_crossChainSendERC20(address _from, address _to, uint256 _amount, uint256 _chainId) public { setUpInlined(); vm.assume(notBuiltinAddress(_from)); diff --git a/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol b/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol index e4c80facdabf..87eb904359d4 100644 --- a/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol +++ b/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol @@ -11,5 +11,5 @@ contract InitialStateCode { bytes internal constant destTokenCode = hex"6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a"; bytes internal constant mockL2ToL2MessengerCode = - hex"608060405260043610610058575f3560e01c80632ea02369116100415780632ea023691461009857806338ffde18146100cb5780637056f41f14610104575f80fd5b80631ecd26f21461005c5780632479446214610071575b5f80fd5b61006f61006a366004610484565b610117565b005b34801561007c575f80fd5b506100856101d2565b6040519081526020015b60405180910390f35b3480156100a3575f80fd5b506100857f000000000000000000000000000000000000000000000000000000000000000281565b3480156100d6575f80fd5b506100df6101e3565b60405173ffffffffffffffffffffffffffffffffffffffff909116815260200161008f565b61006f610112366004610500565b6102cd565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610141929190610556565b5f6040518083038185875af1925050503d805f811461017b576040519150601f19603f3d011682016040523d82523d5f602084013e610180565b606091505b5091509150816101c757806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016101be9190610565565b60405180910390fd5b505050505050505050565b5f6101de4660016105b8565b905090565b5f73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b16330361024657507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a1633036102a857507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a90565b507f000000000000000000000000000000000000000000000000000000000000000090565b7f000000000000000000000000000000000000000000000000000000000000000284036103e6575f6103557f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f920191909152506103ec92505050565b9050806103e4576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016101be565b505b50505050565b5f6103f9845a8585610401565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff8116811461043a575f80fd5b919050565b5f8083601f84011261044f575f80fd5b50813567ffffffffffffffff811115610466575f80fd5b60208301915083602082850101111561047d575f80fd5b9250929050565b5f805f805f805f60c0888a03121561049a575f80fd5b8735965060208801359550604088013594506104b860608901610417565b93506104c660808901610417565b925060a088013567ffffffffffffffff8111156104e1575f80fd5b6104ed8a828b0161043f565b989b979a50959850939692959293505050565b5f805f8060608587031215610513575f80fd5b8435935061052360208601610417565b9250604085013567ffffffffffffffff81111561053e575f80fd5b61054a8782880161043f565b95989497509550505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011684010191505092915050565b808201808211156105f0577f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b9291505056fea164736f6c6343000819000a"; + hex"60806040526004361061006e575f3560e01c806338ffde181161004c57806338ffde18146100fb5780637056f41f14610134578063722c2a4d14610147578063f230b4c2146101a7575f80fd5b80631ecd26f21461007257806324794462146100875780632ea02369146100c8575b5f80fd5b61008561008036600461052d565b6101da565b005b348015610092575f80fd5b507f00000000000000000000000000000000000000000000000000000000000000035b6040519081526020015b60405180910390f35b3480156100d3575f80fd5b506100b57f000000000000000000000000000000000000000000000000000000000000000281565b348015610106575f80fd5b5061010f610295565b60405173ffffffffffffffffffffffffffffffffffffffff90911681526020016100bf565b6100856101423660046105a9565b610376565b348015610152575f80fd5b506100856101613660046105ff565b5f80547fffffffffffffffffffffffff00000000000000000000000000000000000000001673ffffffffffffffffffffffffffffffffffffffff92909216919091179055565b3480156101b2575f80fd5b506100b57f000000000000000000000000000000000000000000000000000000000000000381565b5f808473ffffffffffffffffffffffffffffffffffffffff1634858560405161020492919061061f565b5f6040518083038185875af1925050503d805f811461023e576040519150601f19603f3d011682016040523d82523d5f602084013e610243565b606091505b50915091508161028a57806040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610281919061062e565b60405180910390fd5b505050505050505050565b5f73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b1633036102f857507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a16330361035a57507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a90565b505f5473ffffffffffffffffffffffffffffffffffffffff1690565b7f0000000000000000000000000000000000000000000000000000000000000002840361048f575f6103fe7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f9201919091525061049592505050565b90508061048d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c6564000000000000000000000000000000000000000000000000006064820152608401610281565b505b50505050565b5f6104a2845a85856104aa565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff811681146104e3575f80fd5b919050565b5f8083601f8401126104f8575f80fd5b50813567ffffffffffffffff81111561050f575f80fd5b602083019150836020828501011115610526575f80fd5b9250929050565b5f805f805f805f60c0888a031215610543575f80fd5b873596506020880135955060408801359450610561606089016104c0565b935061056f608089016104c0565b925060a088013567ffffffffffffffff81111561058a575f80fd5b6105968a828b016104e8565b989b979a50959850939692959293505050565b5f805f80606085870312156105bc575f80fd5b843593506105cc602086016104c0565b9250604085013567ffffffffffffffff8111156105e7575f80fd5b6105f3878288016104e8565b95989497509550505050565b5f6020828403121561060f575f80fd5b610618826104c0565b9392505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f8301168401019150509291505056fea164736f6c6343000819000a"; } diff --git a/packages/contracts-bedrock/test/properties/kontrol/helpers/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/properties/kontrol/helpers/MockL2ToL2Messenger.sol new file mode 100644 index 000000000000..78898c42ea31 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/helpers/MockL2ToL2Messenger.sol @@ -0,0 +1,67 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +import "src/L2/L2ToL2CrossDomainMessenger.sol"; +import { SafeCall } from "src/libraries/SafeCall.sol"; + +// TODO: Try to merge to a single mocked contract used by fuzzing and symbolic invariant tests - only if possible +// and is a low priorty +contract MockL2ToL2Messenger is IL2ToL2CrossDomainMessenger { + address internal immutable SOURCE_TOKEN; + address internal immutable DESTINATION_TOKEN; + uint256 public immutable DESTINATION_CHAIN_ID; + uint256 public immutable SOURCE; + + // Custom cross domain sender to be used when neither the source nor destination token are the callers + address internal customCrossDomainSender; + + constructor(address _sourceToken, address _destinationToken, uint256 _destinationChainId, uint256 _source) { + SOURCE_TOKEN = _sourceToken; + DESTINATION_TOKEN = _destinationToken; + DESTINATION_CHAIN_ID = _destinationChainId; + SOURCE = _source; + } + + // Mock the sendMessage function to execute the message call and simulate an atomic environmanet if the destination + // chain id matches the defined one + function sendMessage(uint256 _destination, address, bytes calldata _message) external payable { + // Mocking the environment to allow atomicity by executing the message call + if (_destination == DESTINATION_CHAIN_ID) { + (bool _success) = SafeCall.call(DESTINATION_TOKEN, 0, _message); + if (!_success) revert("MockL2ToL2Messenger: sendMessage failed"); + } + } + + // Mock the relay message function to just call the target address with the input message + function relayMessage( + uint256, + uint256, + uint256, + address, + address _target, + bytes calldata _message + ) + external + payable + { + (bool succ, bytes memory ret) = _target.call{ value: msg.value }(_message); + if (!succ) revert(string(ret)); + } + + function crossDomainMessageSource() external view returns (uint256 _source) { + _source = SOURCE; + } + + // Mock this function so it just always returns the expected if called by the supertoken to pass throgh the + // `address(this)` checks, or otherwise defaults to the custom cross domain sender + function crossDomainMessageSender() external view returns (address _sender) { + if (msg.sender == SOURCE_TOKEN) _sender = SOURCE_TOKEN; + else if (msg.sender == DESTINATION_TOKEN) _sender = DESTINATION_TOKEN; + else _sender = customCrossDomainSender; + } + + /// Setter function for the customCrossDomainSender + function forTest_setCustomCrossDomainSender(address _customCrossDomainSender) external { + customCrossDomainSender = _customCrossDomainSender; + } +}