From 51a72e3d7276b4ae7818c0afa9df49ae2e05fedc Mon Sep 17 00:00:00 2001 From: teddy Date: Fri, 16 Aug 2024 15:24:08 -0300 Subject: [PATCH 1/2] fix: feedback from disco --- .../properties/medusa/ProtocolAtomic.t.sol | 38 +++++++++++-------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol index 0368abb5f70f..b4f44d2bcf67 100644 --- a/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol @@ -41,10 +41,10 @@ contract ProtocolAtomicFuzz is Test { constructor() { vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code); superchainERC20Impl = new OptimismSuperchainERC20(); - for (uint256 i = 0; i < INITIAL_TOKENS; i++) { + for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) { _deployRemoteToken(); - for (uint256 j = 0; j < INITIAL_SUPERTOKENS; j++) { - _deploySupertoken(remoteTokens[i], WORDS[0], WORDS[0], DECIMALS[0], j); + for (uint256 supertokenChainId = 0; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) { + _deploySupertoken(remoteTokens[remoteTokenIndex], WORDS[0], WORDS[0], DECIMALS[0], supertokenChainId); } } } @@ -62,6 +62,8 @@ contract ProtocolAtomicFuzz is Test { } /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId + /// @custom:property-id 14 + /// @custom:property supertoken total supply starts at zero function fuzz_DeployNewSupertoken( TokenDeployParams memory params, uint256 chainId @@ -70,13 +72,15 @@ contract ProtocolAtomicFuzz is Test { validateTokenDeployParams(params) { chainId = bound(chainId, 0, MAX_CHAINS - 1); - _deploySupertoken( + OptimismSuperchainERC20 supertoken = _deploySupertoken( remoteTokens[params.remoteTokenIndex], WORDS[params.nameIndex], WORDS[params.symbolIndex], DECIMALS[params.decimalsIndex], chainId ); + // 14 + assert(supertoken.totalSupply() == 0); } /// @custom:property-id 22 @@ -166,34 +170,36 @@ contract ProtocolAtomicFuzz is Test { remoteTokens.push(address(uint160(1000 + remoteTokens.length))); } - /// @custom:property-id 14 - /// @custom:property supertoken total supply starts at zero + /// @notice deploy a new supertoken representing remoteToken + /// remoteToken, name, symbol and decimals determine the 'real' deploy salt + /// and supertokens sharing it are interoperable between them + /// we however use the chainId as part of the deploy salt to mock the ability of + /// supertokens to exist on different chains on a single EVM. function _deploySupertoken( address remoteToken, - string memory nameIndex, - string memory symbolIndex, + string memory name, + string memory symbol, uint8 decimals, uint256 chainId ) internal + returns(OptimismSuperchainERC20 supertoken) { // this salt would be used in production. Tokens sharing it will be bridgable with each other - bytes32 realSalt = keccak256(abi.encode(remoteToken, nameIndex, symbolIndex, decimals)); + bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals)); // what we use in the tests to walk around two contracts needing two different addresses // tbf we could be using CREATE1, but this feels more verbose - bytes32 hackySalt = keccak256(abi.encode(remoteToken, nameIndex, symbolIndex, decimals, chainId)); - OptimismSuperchainERC20 token = OptimismSuperchainERC20( + bytes32 hackySalt = keccak256(abi.encode(remoteToken, name, symbol, decimals, chainId)); + supertoken = OptimismSuperchainERC20( address( // TODO: Use the SuperchainERC20 Beacon Proxy new ERC1967Proxy{ salt: hackySalt }( address(superchainERC20Impl), - abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, nameIndex, symbolIndex, decimals)) + abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) ) ) ); - // 14 - assert(token.totalSupply() == 0); - MESSENGER.registerSupertoken(realSalt, chainId, address(token)); - allSuperTokens.push(address(token)); + MESSENGER.registerSupertoken(realSalt, chainId, address(supertoken)); + allSuperTokens.push(address(supertoken)); } } From 745dcbc90b8940b97492b5fba2eb400cba507051 Mon Sep 17 00:00:00 2001 From: teddy Date: Fri, 16 Aug 2024 16:58:58 -0300 Subject: [PATCH 2/2] fix: feedback from doc --- 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 0262ecd23b52..4bf542771307 100644 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -43,7 +43,7 @@ Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already h ## Pain points -- existing fuzzing tools use the same EVM to run the tested contracts as they do for asserting invariants, tracking ghost variables and everything else necessary to provision a fuzzing campaign. While this is usually very convenient, it means that we can’t assert on the behaviour/state of *different* EVMs from within a fuzzing campaign. This means we will have to walk around the requirement of supertokens having the same address across all chains, and implement a way to mock tokens existing in different chains. We will strive to formally prove it in a unitary fashion to mitigate this in properties 0 and 1 +- existing fuzzing tools use the same EVM to run the tested contracts as they do for asserting invariants, tracking ghost variables and everything else necessary to provision a fuzzing campaign. While this is usually very convenient, it means that we can’t assert on the behaviour/state of *different* chains from within a fuzzing campaign. This means we will have to walk around the requirement of supertokens having the same address across all chains, and implement a way to mock tokens existing in different chains. We will strive to formally prove it in a unitary fashion to mitigate this in properties 0 and 1 - a buffer to represent 'in transit' messages should be implemented to assert on invariants relating to the non-atomicity of bridging from one chain to another. It is yet to be determined if it’ll be a FIFO queue (assuming ideal message ordering by sequencers) or it’ll have random-access capability to simulate messages arriving out of order ## Definitions