diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json index 88b940370834..c91f69be607e 100644 --- a/packages/contracts-bedrock/medusa.json +++ b/packages/contracts-bedrock/medusa.json @@ -7,7 +7,7 @@ "callSequenceLength": 100, "corpusDirectory": "test/properties/medusa/corpus/", "coverageEnabled": true, - "targetContracts": ["ProtocolAtomicFuzz"], + "targetContracts": ["ProtocolProperties"], "targetContractsBalances": [], "constructorArgs": {}, "deployerAddress": "0x30000", @@ -43,7 +43,7 @@ } }, "propertyTesting": { - "enabled": false, + "enabled": true, "testPrefixes": [ "property_" ] diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol new file mode 100644 index 000000000000..a6ed77dc6c6e --- /dev/null +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { ProtocolHandler } from "./handlers/Protocol.handler.t.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; + +contract ProtocolProperties is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + // TODO: will need rework after + // - non-atomic bridge + // - `convert` + /// @custom:property-id 24 + /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- + /// convert(super, legacy) + + function property_totalSupplyAcrossChainsEqualsMints() external view returns (bool success) { + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId = 0; validChainId < MAX_CHAINS; validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + if (trackedSupply != totalSupply) { + return false; + } + } + return true; + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol similarity index 84% rename from packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol rename to packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol index b4f44d2bcf67..6d6209aca11b 100644 --- a/packages/contracts-bedrock/test/properties/medusa/ProtocolAtomic.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol @@ -7,9 +7,9 @@ import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Pr import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; -import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; +import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; -contract ProtocolAtomicFuzz is Test { +contract ProtocolHandler is Test { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; uint8 internal constant MAX_CHAINS = 4; @@ -132,33 +132,10 @@ contract ProtocolAtomicFuzz is Test { // medusa calls with different senders by default OptimismSuperchainERC20(addr).mint(msg.sender, amount); // currentValue will be zero if key is not present - (,uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr)); + (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr)); ghost_totalSupplyAcrossChains.set(MESSENGER.superTokenInitDeploySalts(addr), currentValue + amount); } - // TODO: will need rework after - // - non-atomic bridge - // - `convert` - /// @custom:property-id 24 - /// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- - /// convert(super, legacy) - /// @notice deliberately not a view method so medusa runs it but not the view methods defined by Test - function property_totalSupplyAcrossChainsEqualsMints() external { - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply = 0; - (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); - // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId = 0; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply); - } - } - function fuzz_MockNewRemoteToken() external { _deployRemoteToken(); } @@ -183,7 +160,7 @@ contract ProtocolAtomicFuzz is Test { uint256 chainId ) internal - returns(OptimismSuperchainERC20 supertoken) + 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, name, symbol, decimals));