forked from ethereum-optimism/optimism
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
test: remaining protocol properties (#26)
* test: cross-user fuzzed bridges + actor setup * test: fuzz properties 8 and 9 * test: properties 7 and 25 * fix: implement doc's feedback * test: superc20 tob properties (#27) * chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady * chore: remove zero-initializations * fix: feedback from disco * chore: separate fuzz campaign tests in guided vs unguided * test: dont revert on successful unguided relay * test: add fuzzed calls to burn and mint * docs: document the separation of fuzz test functions * chore: move the properties file to its own directory * chore: consistently use fuzz_ and property_ + camelcase * chore: fix typo * chore: camelcase for handlers as well * fix: revert change that broke halmos campaign compile :D
- Loading branch information
1 parent
c9b0792
commit 800cb80
Showing
13 changed files
with
419 additions
and
109 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Submodule properties
added at
bb1b78
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
38 changes: 38 additions & 0 deletions
38
packages/contracts-bedrock/test/properties/helpers/Actors.t.sol
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,38 @@ | ||
| // SPDX-License-Identifier: MIT | ||
| pragma solidity ^0.8.25; | ||
|
|
||
| import { StdUtils } from "forge-std/StdUtils.sol"; | ||
|
|
||
| /// @notice helper for tracking actors, taking advantage of the fuzzer already using several `msg.sender`s | ||
| contract Actors is StdUtils { | ||
| mapping(address => bool) private _isActor; | ||
| address[] private _actors; | ||
| address private _currentActor; | ||
|
|
||
| /// @notice register an actor if it's not already registered | ||
| /// usually called with msg.sender as a parameter, to track the actors | ||
| /// already provided by the fuzzer | ||
| modifier withActor(address who) { | ||
| addActor(who); | ||
| _currentActor = who; | ||
| _; | ||
| } | ||
|
|
||
| function addActor(address who) internal { | ||
| if (!_isActor[who]) { | ||
| _isActor[who] = true; | ||
| _actors.push(who); | ||
| } | ||
| } | ||
|
|
||
| /// @notice get the currently configured actor, should equal msg.sender | ||
| function currentActor() internal view returns (address) { | ||
| return _currentActor; | ||
| } | ||
|
|
||
| /// @notice get one of the actors by index, useful to get another random | ||
| /// actor than the one set as currentActor, to perform operations between them | ||
| function getActorByRawIndex(uint256 rawIndex) internal view returns (address) { | ||
| return _actors[bound(rawIndex, 0, _actors.length - 1)]; | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
10 changes: 10 additions & 0 deletions
10
...s/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| // SPDX-License-Identifier: AGPL-3 | ||
| pragma solidity ^0.8.25; | ||
|
|
||
| import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; | ||
|
|
||
| contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 { | ||
| /// @notice This is used by CryticERC20ExternalBasicProperties to know | ||
| // which properties to test | ||
| bool public constant isMintableOrBurnable = true; | ||
| } |
93 changes: 0 additions & 93 deletions
93
packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
This file was deleted.
Oops, something went wrong.
130 changes: 130 additions & 0 deletions
130
packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,130 @@ | ||
| // SPDX-License-Identifier: MIT | ||
| pragma solidity ^0.8.25; | ||
|
|
||
| import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; | ||
| import { ProtocolHandler } from "../handlers/Protocol.t.sol"; | ||
|
|
||
| contract ProtocolGuided is ProtocolHandler { | ||
| /// @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 | ||
| ) | ||
| external | ||
| validateTokenDeployParams(params) | ||
| { | ||
| chainId = bound(chainId, 0, MAX_CHAINS - 1); | ||
| OptimismSuperchainERC20 supertoken = _deploySupertoken( | ||
| remoteTokens[params.remoteTokenIndex], | ||
| WORDS[params.nameIndex], | ||
| WORDS[params.symbolIndex], | ||
| DECIMALS[params.decimalsIndex], | ||
| chainId | ||
| ); | ||
| // 14 | ||
| assert(supertoken.totalSupply() == 0); | ||
| } | ||
|
|
||
| /// @custom:property-id 6 | ||
| /// @custom:property calls to sendERC20 succeed as long as caller has enough balance | ||
| /// @custom:property-id 22 | ||
| /// @custom:property sendERC20 decreases sender balance in source chain and increases receiver balance in | ||
| /// destination chain exactly by the input amount | ||
| /// @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 fuzz_bridgeSupertoken( | ||
| uint256 fromIndex, | ||
| uint256 recipientIndex, | ||
| uint256 destinationChainId, | ||
| uint256 amount | ||
| ) | ||
| public | ||
| withActor(msg.sender) | ||
| { | ||
| destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); | ||
| fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); | ||
| address recipient = getActorByRawIndex(recipientIndex); | ||
| OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); | ||
| OptimismSuperchainERC20 destinationToken = | ||
| MESSENGER.crossChainMessageReceiver(address(sourceToken), destinationChainId); | ||
| // TODO: when implementing non-atomic bridging, allow for the token to | ||
| // not yet be deployed and funds be recovered afterwards. | ||
| require(address(destinationToken) != address(0)); | ||
| uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor()); | ||
| uint256 sourceSupplyBefore = sourceToken.totalSupply(); | ||
| uint256 destinationBalanceBefore = destinationToken.balanceOf(recipient); | ||
| uint256 destinationSupplyBefore = destinationToken.totalSupply(); | ||
|
|
||
| vm.prank(currentActor()); | ||
| try sourceToken.sendERC20(recipient, amount, destinationChainId) { | ||
| uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor()); | ||
| uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient); | ||
| // no free mint | ||
| assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter); | ||
| // 22 | ||
| assert(sourceBalanceBefore - amount == sourceBalanceAfter); | ||
| assert(destinationBalanceBefore + amount == destinationBalanceAfter); | ||
| uint256 sourceSupplyAfter = sourceToken.totalSupply(); | ||
| uint256 destinationSupplyAfter = destinationToken.totalSupply(); | ||
| // 23 | ||
| assert(sourceSupplyBefore - amount == sourceSupplyAfter); | ||
| assert(destinationSupplyBefore + amount == destinationSupplyAfter); | ||
| } catch { | ||
| // 6 | ||
| assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount); | ||
| } | ||
| } | ||
|
|
||
| /// @custom:property-id 8 | ||
| /// @custom:property calls to sendERC20 with a value of zero dont modify accounting | ||
| // @notice is a subset of fuzz_bridgeSupertoken, so we'll just call it | ||
| // instead of re-implementing it. Keeping the function for visibility of the property. | ||
| function fuzz_sendZeroDoesNotModifyAccounting( | ||
| uint256 fromIndex, | ||
| uint256 recipientIndex, | ||
| uint256 destinationChainId | ||
| ) | ||
| external | ||
| { | ||
| fuzz_bridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0); | ||
| } | ||
|
|
||
| /// @custom:property-id 9 | ||
| /// @custom:property calls to relayERC20 with a value of zero dont modify accounting | ||
| /// @custom:property-id 7 | ||
| /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid | ||
| function fuzz_relayZeroDoesNotModifyAccounting( | ||
| uint256 fromIndex, | ||
| uint256 recipientIndex | ||
| ) | ||
| external | ||
| withActor(msg.sender) | ||
| { | ||
| fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); | ||
| address recipient = getActorByRawIndex(recipientIndex); | ||
| OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]); | ||
| uint256 balanceSenderBefore = token.balanceOf(currentActor()); | ||
| uint256 balanceRecipientBefore = token.balanceOf(recipient); | ||
| uint256 supplyBefore = token.totalSupply(); | ||
|
|
||
| MESSENGER.setCrossDomainMessageSender(address(token)); | ||
| vm.prank(address(MESSENGER)); | ||
| try token.relayERC20(currentActor(), recipient, 0) { | ||
| MESSENGER.setCrossDomainMessageSender(address(0)); | ||
| } catch { | ||
| // 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); | ||
| } | ||
| uint256 balanceSenderAfter = token.balanceOf(currentActor()); | ||
| uint256 balanceRecipeintAfter = token.balanceOf(recipient); | ||
| uint256 supplyAfter = token.totalSupply(); | ||
| assert(balanceSenderBefore == balanceSenderAfter); | ||
| assert(balanceRecipientBefore == balanceRecipeintAfter); | ||
| assert(supplyBefore == supplyAfter); | ||
| } | ||
| } |
Oops, something went wrong.