diff --git a/.gitmodules b/.gitmodules index dca839eef08e..21ecaedbb77a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -29,6 +29,3 @@ [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/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 87b5c15318ed..c56d345db708 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -98,8 +98,3 @@ out = 'kout-proofs' test = 'test/kontrol/proofs' script = 'test/kontrol/proofs' -[profile.medusa] -src = 'test/properties/medusa/' -test = 'test/properties/medusa/' -script = 'test/properties/medusa/' -via-ir=true diff --git a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md index 0e3150624da5..7dd70286a4e9 100644 --- a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md +++ b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md @@ -1,10 +1,16 @@ # `OptimismSuperchainERC20` Invariants -## Calls to sendERC20 should always succeed as long as the actor has enough balance. Actor's balance should also not increase out of nowhere but instead should decrease by the amount sent. -**Test:** [`OptimismSuperchainERC20.t.sol#L194`](../test/invariants/OptimismSuperchainERC20.t.sol#L194) +## sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) +**Test:** [`OptimismSuperchainERC20#L36`](../test/invariants/OptimismSuperchainERC20#L36) -## Calls to relayERC20 should always succeeds when a message is received from another chain. Actor's balance should only increase by the amount relayed. -**Test:** [`OptimismSuperchainERC20.t.sol#L212`](../test/invariants/OptimismSuperchainERC20.t.sol#L212) +## sum of supertoken total supply across all chains is equal to convert(legacy, super)- convert(super, legacy) when all when all cross-chain messages are processed +**Test:** [`OptimismSuperchainERC20#L57`](../test/invariants/OptimismSuperchainERC20#L57) + + +## many other assertion mode invariants are also defined under `test/invariants/OptimismSuperchainERC20/fuzz/` . +**Test:** [`OptimismSuperchainERC20#L79`](../test/invariants/OptimismSuperchainERC20#L79) + +since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the handler for assertion test failures \ No newline at end of file diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile index 290f01574ead..45cdd14cfae0 100644 --- a/packages/contracts-bedrock/justfile +++ b/packages/contracts-bedrock/justfile @@ -22,9 +22,6 @@ test: build-go-ffi test-kontrol: ./test/kontrol/scripts/run-kontrol.sh script -test-medusa timeout='100': - FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}} - test-rerun: build-go-ffi forge test --rerun -vvv diff --git a/packages/contracts-bedrock/lib/properties b/packages/contracts-bedrock/lib/properties deleted file mode 160000 index bb1b78542b3f..000000000000 --- a/packages/contracts-bedrock/lib/properties +++ /dev/null @@ -1 +0,0 @@ -Subproject commit bb1b78542b3f38e4ae56cf87389cd3ea94387f48 diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json deleted file mode 100644 index 5df25c2cd63b..000000000000 --- a/packages/contracts-bedrock/medusa.json +++ /dev/null @@ -1,86 +0,0 @@ -{ - "fuzzing": { - "workers": 10, - "workerResetLimit": 50, - "timeout": 0, - "testLimit": 0, - "callSequenceLength": 100, - "corpusDirectory": "test/properties/medusa/corpus/", - "coverageEnabled": true, - "targetContracts": ["ProtocolProperties"], - "targetContractsBalances": [], - "constructorArgs": {}, - "deployerAddress": "0x30000", - "senderAddresses": [ - "0x10000", - "0x20000", - "0x30000" - ], - "blockNumberDelayMax": 60480, - "blockTimestampDelayMax": 604800, - "blockGasLimit": 30000000, - "transactionGasLimit": 12500000, - "testing": { - "stopOnFailedTest": true, - "stopOnFailedContractMatching": false, - "stopOnNoTests": true, - "testAllContracts": false, - "traceAll": true, - "assertionTesting": { - "enabled": true, - "testViewMethods": true, - "panicCodeConfig": { - "failOnCompilerInsertedPanic": false, - "failOnAssertion": true, - "failOnArithmeticUnderflow": false, - "failOnDivideByZero": false, - "failOnEnumTypeConversionOutOfBounds": false, - "failOnIncorrectStorageAccess": false, - "failOnPopEmptyArray": false, - "failOnOutOfBoundsArrayAccess": false, - "failOnAllocateTooMuchMemory": false, - "failOnCallUninitializedVariable": false - } - }, - "propertyTesting": { - "enabled": false, - "testPrefixes": [ - "property_" - ] - }, - "optimizationTesting": { - "enabled": false, - "testPrefixes": [ - "optimize_" - ] - }, - "targetFunctionSignatures": [], - "excludeFunctionSignatures": [ - "ProtocolProperties.test_ERC20external_zeroAddressBalance()", - "ProtocolProperties.test_ERC20external_transferToZeroAddress()", - "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)" - ] - }, - "chainConfig": { - "codeSizeCheckDisabled": true, - "cheatCodes": { - "cheatCodesEnabled": true, - "enableFFI": false - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": ["--foundry-out-directory", "artifacts","--foundry-compile-all"] - } - }, - "logging": { - "level": "info", - "logDirectory": "", - "noColor": false - } -} diff --git a/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go b/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go index f408095483b3..38a0b2e3d166 100644 --- a/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go +++ b/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go @@ -76,6 +76,12 @@ func docGen(invariantsDir, docsDir string) error { // Read the contents of the invariant test file. fileName := file.Name() filePath := filepath.Join(invariantsDir, fileName) + // where invariants for a module have their own directory, interpret + // the test file with the same name as the directory as a 'main' of + // sorts, from where documentation is pulled + if file.IsDir() { + filePath = filepath.Join(filePath, strings.Join([]string{fileName, ".t.sol"}, "")) + } fileContents, err := os.ReadFile(filePath) if err != nil { return fmt.Errorf("error reading file %q: %w", filePath, err) diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol deleted file mode 100644 index 028a0124e6ca..000000000000 --- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol +++ /dev/null @@ -1,225 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity 0.8.25; - -// Testing utilities -import { Test, StdUtils, Vm } from "forge-std/Test.sol"; -import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol"; - -// Libraries -import { Predeploys } from "src/libraries/Predeploys.sol"; -import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol"; - -/// @title OptimismSuperchainERC20_User -/// @notice Actor contract that interacts with the OptimismSuperchainERC20 contract. -contract OptimismSuperchainERC20_User is StdUtils { - address public immutable receiver; - - /// @notice Cross domain message data. - struct MessageData { - bytes32 id; - uint256 amount; - } - - uint256 public totalAmountSent; - uint256 public totalAmountRelayed; - - /// @notice Flag to indicate if the test has failed. - bool public failed = false; - - /// @notice The Vm contract. - Vm internal vm; - - /// @notice The OptimismSuperchainERC20 contract. - OptimismSuperchainERC20 internal superchainERC20; - - /// @notice Mapping of sent messages. - mapping(bytes32 => bool) internal sent; - - /// @notice Array of unrelayed messages. - MessageData[] internal unrelayed; - - /// @param _vm The Vm contract. - /// @param _superchainERC20 The OptimismSuperchainERC20 contract. - /// @param _balance The initial balance of the contract. - constructor(Vm _vm, OptimismSuperchainERC20 _superchainERC20, uint256 _balance, address _receiver) { - vm = _vm; - superchainERC20 = _superchainERC20; - - // Mint balance to this actor. - vm.prank(Predeploys.L2_STANDARD_BRIDGE); - superchainERC20.mint(address(this), _balance); - receiver = _receiver; - } - - /// @notice Send ERC20 tokens to another chain. - /// @param _amount The amount of ERC20 tokens to send. - /// @param _chainId The chain ID to send the tokens to. - /// @param _messageId The message ID. - function sendERC20(uint256 _amount, uint256 _chainId, bytes32 _messageId) public { - // Make sure we aren't reusing a message ID. - if (sent[_messageId]) { - return; - } - - // Bound send amount to our ERC20 balance. - _amount = bound(_amount, 0, superchainERC20.balanceOf(address(this))); - - // Send the amount. - try superchainERC20.sendERC20(receiver, _amount, _chainId) { - // Success. - totalAmountSent += _amount; - } catch { - failed = true; - } - - // Mark message as sent. - sent[_messageId] = true; - unrelayed.push(MessageData({ id: _messageId, amount: _amount })); - } - - /// @notice Relay a message from another chain. - function relayMessage(uint256 _source) public { - // Make sure there are unrelayed messages. - if (unrelayed.length == 0) { - return; - } - - // Grab the latest unrelayed message. - MessageData memory message = unrelayed[unrelayed.length - 1]; - - // Simulate the cross-domain message. - // Make sure the cross-domain message sender is set to this contract. - vm.mockCall( - Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, - abi.encodeCall(IL2ToL2CrossDomainMessenger.crossDomainMessageSender, ()), - abi.encode(address(superchainERC20)) - ); - - // Simulate the cross-domain message source to any chain. - vm.mockCall( - Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, - abi.encodeCall(IL2ToL2CrossDomainMessenger.crossDomainMessageSource, ()), - abi.encode(_source) - ); - - // Prank the relayERC20 function. - // Balance will just go back to our own account. - vm.prank(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - try superchainERC20.relayERC20(address(this), receiver, message.amount) { - // Success. - totalAmountRelayed += message.amount; - } catch { - failed = true; - } - - // Remove the message from the unrelayed list. - unrelayed.pop(); - } -} - -/// @title OptimismSuperchainERC20_Invariant -/// @notice Invariant test that checks that sending OptimismSuperchainERC20 always succeeds if the actor has a -/// sufficient balance to do so and that the actor's balance does not increase out of nowhere. -contract OptimismSuperchainERC20_Invariant is Test { - /// @notice Starting balance of the contract. - uint256 public constant STARTING_BALANCE = type(uint128).max; - - /// @notice The OptimismSuperchainERC20 contract implementation. - address internal optimismSuperchainERC20Impl; - - /// @notice The OptimismSuperchainERC20_User actor. - OptimismSuperchainERC20_User internal actor; - - /// @notice The OptimismSuperchainERC20 contract. - OptimismSuperchainERC20 internal optimismSuperchainERC20; - - /// @notice The address that will receive the tokens when relaying messages - address internal receiver = makeAddr("receiver"); - - /// @notice Test setup. - function setUp() public { - // Deploy the L2ToL2CrossDomainMessenger contract. - address _impl = _setImplementationCode(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - _setProxyCode(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, _impl); - - // Create a new OptimismSuperchainERC20 implementation. - optimismSuperchainERC20Impl = address(new OptimismSuperchainERC20()); - - // Deploy the OptimismSuperchainERC20 contract. - address _proxy = address(0x123456); - _setProxyCode(_proxy, optimismSuperchainERC20Impl); - optimismSuperchainERC20 = OptimismSuperchainERC20(_proxy); - - // Create a new OptimismSuperchainERC20_User actor. - actor = new OptimismSuperchainERC20_User(vm, optimismSuperchainERC20, STARTING_BALANCE, receiver); - - // Set the target contract. - targetContract(address(actor)); - - // Set the target selectors. - bytes4[] memory selectors = new bytes4[](2); - selectors[0] = actor.sendERC20.selector; - selectors[1] = actor.relayMessage.selector; - FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors }); - targetSelector(selector); - - // Setup assertions - assert(optimismSuperchainERC20.balanceOf(address(actor)) == STARTING_BALANCE); - assert(optimismSuperchainERC20.balanceOf(address(receiver)) == 0); - assert(optimismSuperchainERC20.totalSupply() == STARTING_BALANCE); - } - - /// @notice Sets the bytecode in the implementation address. - function _setImplementationCode(address _addr) internal returns (address) { - string memory cname = Predeploys.getName(_addr); - address impl = Predeploys.predeployToCodeNamespace(_addr); - vm.etch(impl, vm.getDeployedCode(string.concat(cname, ".sol:", cname))); - return impl; - } - - /// @notice Sets the bytecode in the proxy address. - function _setProxyCode(address _addr, address _impl) internal { - bytes memory code = vm.getDeployedCode("universal/Proxy.sol:Proxy"); - vm.etch(_addr, code); - EIP1967Helper.setAdmin(_addr, Predeploys.PROXY_ADMIN); - EIP1967Helper.setImplementation(_addr, _impl); - } - - /// @notice Invariant that checks that sending OptimismSuperchainERC20 always succeeds. - /// @custom:invariant Calls to sendERC20 should always succeed as long as the actor has enough balance. - /// Actor's balance should also not increase out of nowhere but instead should decrease by the - /// amount sent. - function invariant_sendERC20_succeeds() public view { - // Assert that the actor has not failed to send OptimismSuperchainERC20. - assertTrue(!actor.failed()); - - // Assert that the actor has sent more than or equal to the amount relayed. - assertTrue(actor.totalAmountSent() >= actor.totalAmountRelayed()); - - // Assert that the actor's balance has decreased by the amount sent. - assertEq(optimismSuperchainERC20.balanceOf(address(actor)), STARTING_BALANCE - actor.totalAmountSent()); - - // Assert that the total supply of the OptimismSuperchainERC20 contract has decreased by the amount unrelayed. - uint256 _unrelayedAmount = actor.totalAmountSent() - actor.totalAmountRelayed(); - assertEq(optimismSuperchainERC20.totalSupply(), STARTING_BALANCE - _unrelayedAmount); - } - - /// @notice Invariant that checks that relaying OptimismSuperchainERC20 always succeeds. - /// @custom:invariant Calls to relayERC20 should always succeeds when a message is received from another chain. - /// Actor's balance should only increase by the amount relayed. - function invariant_relayERC20_succeeds() public view { - // Assert that the actor has not failed to relay OptimismSuperchainERC20. - assertTrue(!actor.failed()); - - // Assert that the actor has sent more than or equal to the amount relayed. - assertTrue(actor.totalAmountSent() >= actor.totalAmountRelayed()); - - // Assert that the actor's balance has increased by the amount relayed. - assertEq(optimismSuperchainERC20.balanceOf(address(receiver)), actor.totalAmountRelayed()); - - // Assert that the total supply of the OptimismSuperchainERC20 contract has decreased by the amount unrelayed. - uint256 _unrelayedAmount = actor.totalAmountSent() - actor.totalAmountRelayed(); - assertEq(optimismSuperchainERC20.totalSupply(), STARTING_BALANCE - _unrelayedAmount); - } -} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol new file mode 100644 index 000000000000..d4662277fbd2 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +// Testing utilities +import { Test, StdUtils, Vm } from "forge-std/Test.sol"; +import { StdInvariant } from "forge-std/StdInvariant.sol"; +import { StdAssertions } from "forge-std/StdAssertions.sol"; +import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol"; + +// Libraries +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol"; +import { ProtocolGuided } from "./fuzz/Protocol.guided.t.sol"; +import { ProtocolUnguided } from "./fuzz/Protocol.unguided.t.sol"; +import { HandlerGetters } from "./helpers/HandlerGetters.t.sol"; +import { MockL2ToL2CrossDomainMessenger } from "./helpers/MockL2ToL2CrossDomainMessenger.t.sol"; + +contract OptimismSuperchainERC20Handler is HandlerGetters, ProtocolGuided, ProtocolUnguided { } + +contract OptimismSuperchainERC20Properties is Test { + OptimismSuperchainERC20Handler internal handler; + MockL2ToL2CrossDomainMessenger internal constant MESSENGER = + MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); + + function setUp() public { + handler = new OptimismSuperchainERC20Handler(); + targetContract(address(handler)); + } + + // TODO: will need rework after + // - `convert` + /// @custom:invariant sum of supertoken total supply across all chains is always <= to convert(legacy, super)- + /// convert(super, legacy) + function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view { + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex); + uint256 fundsInTransit = handler.tokensInTransitForDeploySalt(currentSalt); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assertEq(trackedSupply, totalSupply + fundsInTransit); + } + } + + // TODO: will need rework after + // - `convert` + /// @custom:invariant sum of supertoken total supply across all chains is equal to convert(legacy, super)- + /// convert(super, legacy) when all when all cross-chain messages are processed + function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view { + if (MESSENGER.messageQueueLength() != 0) { + return; + } + // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other + for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) { + uint256 totalSupply = 0; + (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex); + // and then over all the (mocked) chain ids where that supertoken could be deployed + for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) { + address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); + if (supertoken != address(0)) { + totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); + } + } + assertEq(trackedSupply, totalSupply); + } + } + + /// @custom:invariant many other assertion mode invariants are also defined under `test/invariants/OptimismSuperchainERC20/fuzz/` . + /// + /// since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the + /// handler for assertion test failures + function invariant_handlerAssertions() external view { + assertFalse(handler.failed()); + } +} diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol similarity index 84% rename from packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol index d5b5d8b5edc5..2d9c8d52fab3 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol @@ -1,12 +1,13 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.25; -import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; +import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { ProtocolHandler } from "../handlers/Protocol.t.sol"; import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; +import { CompatibleAssert } from '../helpers/CompatibleAssert.t.sol'; -contract ProtocolGuided is ProtocolHandler { +contract ProtocolGuided is ProtocolHandler, CompatibleAssert { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId /// @custom:property-id 14 @@ -27,7 +28,7 @@ contract ProtocolGuided is ProtocolHandler { chainId ); // 14 - assert(supertoken.totalSupply() == 0); + compatibleAssert(supertoken.totalSupply() == 0); } /// @custom:property-id 6 @@ -65,19 +66,19 @@ contract ProtocolGuided is ProtocolHandler { uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); // no free mint - assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); + compatibleAssert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); // 22 - assert(sourceBalanceBefore - amount == sourceBalanceAfter); - assert(destinationBalanceBefore + amount == destinationBalanceAfter); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(destinationBalanceBefore + amount == destinationBalanceAfter); uint256 sourceSupplyAfter = sourceToken.totalSupply(); uint256 destinationSupplyAfter = destinationToken.totalSupply(); // 23 - assert(sourceSupplyBefore - amount == sourceSupplyAfter); - assert(destinationSupplyBefore + amount == destinationSupplyAfter); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(destinationSupplyBefore + amount == destinationSupplyAfter); } catch { MESSENGER.setAtomic(false); // 6 - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } @@ -112,13 +113,13 @@ contract ProtocolGuided is ProtocolHandler { ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); // 26 uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); - assert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); // 10 uint256 sourceSupplyAfter = sourceToken.totalSupply(); - assert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); } catch { // 6 - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } @@ -138,17 +139,17 @@ contract ProtocolGuided is ProtocolHandler { bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken)); (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt); // if sendERC20 didnt intialize this, then test suite is broken - assert(success); + compatibleAssert(success); ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount); // 11 - assert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); + compatibleAssert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply()); // 27 - assert( + compatibleAssert( destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient) ); } catch { // 7 - assert(false); + compatibleAssert(false); } } @@ -194,13 +195,13 @@ contract ProtocolGuided is ProtocolHandler { // should not revert because of 7, and if it *does* revert, I want the test suite // to discard the sequence instead of potentially getting another // error due to the crossDomainMessageSender being manually set - assert(false); + compatibleAssert(false); } uint256 balanceSenderAfter = token.balanceOf(currentActor()); uint256 balanceRecipeintAfter = token.balanceOf(recipient); uint256 supplyAfter = token.totalSupply(); - assert(balanceSenderBefore == balanceSenderAfter); - assert(balanceRecipientBefore == balanceRecipeintAfter); - assert(supplyBefore == supplyAfter); + compatibleAssert(balanceSenderBefore == balanceSenderAfter); + compatibleAssert(balanceRecipientBefore == balanceRecipeintAfter); + compatibleAssert(supplyBefore == supplyAfter); } } diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol similarity index 86% rename from packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol index 71ba64118088..bf6d1386d409 100644 --- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol @@ -4,9 +4,10 @@ pragma solidity ^0.8.25; import { ProtocolHandler } from "../handlers/Protocol.t.sol"; import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { CompatibleAssert } from '../helpers/CompatibleAssert.t.sol'; // TODO: add fuzz_sendERC20 when we implement non-atomic bridging -contract ProtocolUnguided is ProtocolHandler { +contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{ using EnumerableMap for EnumerableMap.Bytes32ToUintMap; /// @custom:property-id 7 @@ -28,8 +29,8 @@ contract ProtocolUnguided is ProtocolHandler { vm.prank(sender); try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) { MESSENGER.setCrossDomainMessageSender(address(0)); - assert(sender == address(MESSENGER)); - assert(crossDomainMessageSender == token); + compatibleAssert(sender == address(MESSENGER)); + compatibleAssert(crossDomainMessageSender == token); // this increases the supply across chains without a call to // `mint` by the MESSENGER, so it kind of breaks an invariant, but // let's walk around that: @@ -37,7 +38,7 @@ contract ProtocolUnguided is ProtocolHandler { (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); } catch { - assert(sender != address(MESSENGER) || crossDomainMessageSender != token); + compatibleAssert(sender != address(MESSENGER) || crossDomainMessageSender != token); MESSENGER.setCrossDomainMessageSender(address(0)); } } @@ -71,13 +72,13 @@ contract ProtocolUnguided is ProtocolHandler { ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount); // 26 uint256 sourceBalanceAfter = sourceToken.balanceOf(sender); - assert(sourceBalanceBefore - amount == sourceBalanceAfter); + compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter); // 10 uint256 sourceSupplyAfter = sourceToken.totalSupply(); - assert(sourceSupplyBefore - amount == sourceSupplyAfter); + compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter); } catch { // 6 - assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); + compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); } } @@ -90,11 +91,11 @@ contract ProtocolUnguided is ProtocolHandler { amount = bound(amount, 0, type(uint256).max - OptimismSuperchainERC20(token).totalSupply()); vm.prank(sender); try OptimismSuperchainERC20(token).mint(to, amount) { - assert(sender == BRIDGE); + compatibleAssert(sender == BRIDGE); (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); ghost_totalSupplyAcrossChains.set(salt, currentValue + amount); } catch { - assert(sender != BRIDGE || to == address(0)); + compatibleAssert(sender != BRIDGE || to == address(0)); } } @@ -107,11 +108,11 @@ contract ProtocolUnguided is ProtocolHandler { uint256 senderBalance = OptimismSuperchainERC20(token).balanceOf(sender); vm.prank(sender); try OptimismSuperchainERC20(token).burn(from, amount) { - assert(sender == BRIDGE); + compatibleAssert(sender == BRIDGE); (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt); ghost_totalSupplyAcrossChains.set(salt, currentValue - amount); } catch { - assert(sender != BRIDGE || senderBalance < amount); + compatibleAssert(sender != BRIDGE || senderBalance < amount); } } @@ -132,7 +133,7 @@ contract ProtocolUnguided is ProtocolHandler { try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize( remoteToken, name, symbol, decimals ) { - assert(false); + compatibleAssert(false); } catch { } } } diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol similarity index 92% rename from packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol index 191c5c44a7e6..921495b467ab 100644 --- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol @@ -7,15 +7,15 @@ import { StdUtils } from "forge-std/StdUtils.sol"; import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; -import { OptimismSuperchainERC20ForToBProperties } from "../../helpers/OptimismSuperchainERC20ForToBProperties.t.sol"; +import { OptimismSuperchainERC20ForToBProperties } from "../helpers/OptimismSuperchainERC20ForToBProperties.t.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; -import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; -import { Actors } from "../../helpers/Actors.t.sol"; +import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol"; +import { Actors } from "../helpers/Actors.t.sol"; contract ProtocolHandler is TestBase, StdUtils, Actors { using EnumerableMap for EnumerableMap.Bytes32ToUintMap; - uint8 internal constant MAX_CHAINS = 4; + uint8 public constant MAX_CHAINS = 4; uint8 internal constant INITIAL_TOKENS = 1; uint8 internal constant INITIAL_SUPERTOKENS = 1; uint8 internal constant SUPERTOKEN_INITIAL_MINT = 100; @@ -79,7 +79,6 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { index = bound(index, 0, allSuperTokens.length - 1); address addr = allSuperTokens[index]; vm.prank(BRIDGE); - // medusa calls with different senders by default OptimismSuperchainERC20(addr).mint(currentActor(), amount); // currentValue will be zero if key is not present (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr)); @@ -156,6 +155,10 @@ contract ProtocolHandler is TestBase, StdUtils, Actors { { // 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)); + // Foundry invariant erroneously show other unrelated invariant breaking + // when this deployment fails due to a create2 collision, so we revert eagerly instead + require(MESSENGER.superTokenAddresses(chainId, realSalt) == address(0), "skip duplicate deployment"); + // 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, name, symbol, decimals, chainId)); diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol similarity index 100% rename from packages/contracts-bedrock/test/properties/helpers/Actors.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol new file mode 100644 index 000000000000..9cca12bf8649 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: GPL-3 +pragma solidity ^0.8.24; + +import { console } from "forge-std/console.sol"; + +/// @title CompatibleAssert +/// @notice meant to add compatibility between medusa assertion tests and +/// foundry invariant test's required architecture +contract CompatibleAssert { + bool public failed; + + function compatibleAssert(bool condition) internal { + compatibleAssert(condition, ""); + } + + function compatibleAssert(bool condition, string memory message) internal { + if (!condition) { + if(bytes(message).length != 0) console.log("Assertion failed: ", message); + else console.log("Assertion failed"); + + // for foundry to call & check + failed = true; + + // for medusa + assert(false); + } + } +} diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol new file mode 100644 index 000000000000..6120f5f75684 --- /dev/null +++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: GPL-3 +pragma solidity ^0.8.24; + +import { ProtocolHandler } from "../handlers/Protocol.t.sol"; +import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; + +contract HandlerGetters is ProtocolHandler { + using EnumerableMap for EnumerableMap.Bytes32ToUintMap; + function deploySaltsLength() external view returns (uint256 length) { + return ghost_totalSupplyAcrossChains.length(); + } + + function totalSupplyAcrossChainsAtIndex(uint256 index) external view returns (bytes32 salt, uint256 supply) { + return ghost_totalSupplyAcrossChains.at(index); + } + + function tokensInTransitForDeploySalt(bytes32 salt) external view returns (uint256 amount) { + (, amount) = ghost_tokensInTransit.tryGet(salt); + return amount; + } +} diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol similarity index 100% rename from packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol diff --git a/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol similarity index 100% rename from packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol diff --git a/packages/contracts-bedrock/test/invariants/PROPERTIES.md b/packages/contracts-bedrock/test/invariants/PROPERTIES.md deleted file mode 100644 index 5a5cc71d73b5..000000000000 --- a/packages/contracts-bedrock/test/invariants/PROPERTIES.md +++ /dev/null @@ -1,73 +0,0 @@ -# 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 deleted file mode 100644 index d915d565633e..000000000000 --- a/packages/contracts-bedrock/test/properties/PROPERTIES.md +++ /dev/null @@ -1,141 +0,0 @@ -# Supertoken advanced testing - -## Overview - -This document defines a set of properties global to the supertoken ecosystem, for which we will: - -- run a [Medusa](https://github.com/crytic/medusa) fuzzing campaign, trying to break system invariants -- formally prove with [Halmos](https://github.com/a16z/halmos) whenever possible - -## Milestones - -The supertoken ecosystem consists of not just the supertoken contract, but the required changes to other contracts for liquidity to reach the former. - -Considering only the supertoken contract is merged into the `develop` branch, and work for the other components is still in progress, we define three milestones for the testing campaign: - -- SupERC20: concerned with only the supertoken contract, the first one to be implemented -- Factories: covers the above + the development of `OptimismSuperchainERC20Factory` and required changes to `OptimismMintableERC20Factory` -- Liquidity Migration: includes the `convert` function on the `L2StandardBridgeInterop` to migrate liquidity from legacy tokens into supertokens - -## Where to place the testing campaign - -Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already has invariant testing provided by foundry, it's not a trivial matter where to place this advanced testing campaign. Two alternatives are proposed: - -- including it in the mainline OP monorepo, in a subdirectory of the existing test contracts such as `test/invariants/medusa/superc20/` -- keep the campaign in wonderland's fork of the repository, in its own feature branch, in which case the deliverable would consist primarily of: - - a summary of the results, extending this document - - PRs with extra unit tests replicating found issues to the main repo where applicable - -## Contracts in scope - -- [ ] [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) (modifications to enable `convert` not yet merged) -- [ ] [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/OptimismSuperchainERC20.sol1) -- [ ] [OptimismSuperchainERC20Factory](https://github.com/defi-wonderland/optimism/pull/8/files#diff-09838f5703c353d0f7c5ff395acc04c1768ef58becac67404bc17e1fb0018517) (not yet merged) -- [ ] [L2StandardBridgeInterop](https://github.com/defi-wonderland/optimism/pull/10/files#diff-56cf869412631eac0a04a03f7d026596f64a1e00fcffa713bc770d67c6856c2f) (not yet merged) - -## Behavior assumed correct - -- [ ] inclusion of relay transactions -- [ ] sequencer implementation -- [ ] [OptimismMintableERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20.sol) -- [ ] [L2ToL2CrossDomainMessenger](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/L2CrossDomainMessenger.sol) -- [ ] [CrossL2Inbox](https://github.com/defi-wonderland/src/L2/CrossL2Inbox.sol) - -## 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* 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 - -- *legacy token:* an OptimismMintableERC20 or L2StandardERC20 token on the suprechain that has either been deployed by the factory after the liquidity migration upgrade to the latter, or has been deployed before it **but** added to factory’s `deployments` mapping as part of the upgrade. This testing campaign is not concerned with tokens on L1 or not listed in the factory’s `deployments` mapping. -- *supertoken:* a SuperchainERC20 contract deployed by the `OptimismSuperchainERC20Factory` - -# 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 -- `[~]`: partially tested/proven property -- `:(`: property won't be tested due to some limitation - -## Unit test - -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 0 | Factories | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | -| 1 | Factories | supertoken token address depends on remote token, name, symbol and decimals | [ ] | [ ] | -| 2 | Liquidity Migration | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | [ ] | -| 3 | Liquidity Migration | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | -| 4 | Liquidity Migration | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | -| 5 | Liquidity Migration | convert() burns the same amount of legacy token that it mints of supertoken, and viceversa | [ ] | [ ] | -| 25 | SupERC20 | supertokens can't be reinitialized | [ ] | [x] | - -## Valid state - -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [x] | -| 7 | SupERC20 | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[~]** | [~] | - -## Variable transition - -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [x] | [x] | -| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [x] | [x] | -| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [x] | -| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [ ] | [x] | -| 27 | SupERC20 | relayERC20 increases sender's balance in the destination 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 | [ ] | [ ] | - -## High level - -| id | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 17 | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | -| 18 | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | -| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | -| 20 | SupERC20 | 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 | Liquidity Migration | 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 | milestone | description | halmos | medusa | -| --- | --- | --- | --- | --- | -| 22 | SupERC20 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [x] | -| 23 | SupERC20 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [x] | -| 24 | Liquidity Migration | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | - -# Expected external interactions - -- [x] 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 - -# Internal structure - -## Medusa campaign - -Fuzzing campaigns have both the need to push the contract into different states (state transitions) and assert properties are actually held. This defines a spectrum of function types: - -- `handler_`: they only transition the protocol state, and don't perform any assertions. -- `fuzz_`: they both transition the protocol state and perform assertions on properties. They are further divided in: - - unguided: they exist to let the fuzzer try novel or unexpected interactions, and potentially transition to unexpectedly invalid states - - guided: they have the goal of quickly covering code and moving the protocol to known valid states (eg: by moving funds between valid users) -- `property_`: they only assert the protocol is in a valid state, without causing a state transition. Note that they still use assertion-mode testing for simplicity, but could be migrated to run in property-mode. diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol deleted file mode 100644 index 7b2f73d54058..000000000000 --- a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol +++ /dev/null @@ -1,72 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.25; - -import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol"; -import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol"; -import { ProtocolGuided } from "../fuzz/Protocol.guided.t.sol"; -import { ProtocolUnguided } from "../fuzz/Protocol.unguided.t.sol"; -import { CryticERC20ExternalBasicProperties } from - "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol"; -import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; - -contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20ExternalBasicProperties { - using EnumerableMap for EnumerableMap.Bytes32ToUintMap; - - /// @dev `token` is the token under test for the ToB properties. This is coupled - /// to the ProtocolSetup constructor initializing at least one supertoken - constructor() { - token = ITokenMock(allSuperTokens[0]); - } - - /// @dev not that much of a handler, since this only changes which - /// supertoken the ToB assertions are performed against. Thankfully, they are - /// implemented in a way that don't require tracking ghost variables or can - /// break properties defined by us - function handler_ToBTestOtherToken(uint256 index) external { - token = ITokenMock(allSuperTokens[bound(index, 0, allSuperTokens.length - 1)]); - } - - // TODO: will need rework after - // - `convert` - /// @custom:property-id 19 - /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)- - /// convert(super, legacy) - function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view { - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply ; - (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex); - (, uint256 fundsInTransit) = ghost_tokensInTransit.tryGet(currentSalt); - // and then over all the (mocked) chain ids where that supertoken could be deployed - for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply + fundsInTransit); - } - } - - // TODO: will need rework after - // - `convert` - /// @custom:property-id 21 - /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)- - /// convert(super, legacy) when all when all cross-chain messages are processed - function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view { - require(MESSENGER.messageQueueLength() == 0); - // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other - for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) { - uint256 totalSupply ; - (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 ; validChainId < MAX_CHAINS; validChainId++) { - address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt); - if (supertoken != address(0)) { - totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); - } - } - assert(trackedSupply == totalSupply); - } - } -}