Skip to content

Commit

Permalink
test: queue cross-chain messages and test related properties
Browse files Browse the repository at this point in the history
  • Loading branch information
@0xteddybear
0xteddybear committed Aug 22, 2024
1 parent f2a3830 commit 04bcb7d
Show file tree
Hide file tree
Showing 4 changed files with 80 additions and 12 deletions.
8 changes: 4 additions & 4 deletions packages/contracts-bedrock/test/properties/PROPERTIES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ legend:
| --- | --- | --- | --- | --- |
| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [ ] | [x] |
| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [ ] | [x] |
| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [ ] | [ ] |
| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [ ] | [ ] |
| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [ ] | [x] |
| 26 | SupERC20 | sendERC20 decreases the sender's balance in the source chain exactly by the input amount | [ ] | [x] |
| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [ ] | [ ] |
| 27 | SupERC20 | relayERC20 increases sender's balance in the destination chain exactly by the input amount | [ ] | [ ] |
| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [ ] | [~] |
Expand All @@ -101,9 +101,9 @@ legend:
| --- | --- | --- | --- | --- |
| 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) | [ ] | [ ] |
| 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 | [ ] | [ ] |
| 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

Expand Down
9 changes: 7 additions & 2 deletions packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,12 @@ contract MockL2ToL2CrossDomainMessenger {
_atomic = atomic;
}

function relayMessageFromQueue(uint256 index) public { }
function relayMessageFromQueue(uint256 index) public {
CrossChainMessage memory message = _messageQueue[index];
_messageQueue[index] = _messageQueue[_messageQueue.length - 1];
_messageQueue.pop();
_relayMessage(message);
}

function _relayMessage(CrossChainMessage memory message) internal {
crossDomainMessageSender = message.crossDomainMessageSender;
Expand Down Expand Up @@ -88,7 +93,7 @@ contract MockL2ToL2CrossDomainMessenger {
if (_atomic) {
_relayMessage(message);
} else {
// to be implemented
_messageQueue.push(message);
}
}
}
73 changes: 67 additions & 6 deletions packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,12 +28,34 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti
}

// 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)-
/// @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_totalSupplyAcrossChainsEqualsMints() external view {
function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view {
// 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);
(, uint256 fundsInTransit) = ghost_tokensInTransit.tryGet(currentSalt);
// 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 + 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 = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
uint256 totalSupply = 0;
Expand Down Expand Up @@ -94,8 +116,6 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti
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();
Expand Down Expand Up @@ -125,6 +145,47 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti
}
}

/// @custom:property-id 6
/// @custom:property calls to sendERC20 succeed as long as caller has enough balance
/// @custom:property-id 26
/// @custom:property sendERC20 decreases sender balance in source chain exactly by the input amount
/// @custom:property-id 10
/// @custom:property sendERC20 decreases total supply in source chain exactly by the input amount
function property_BridgeSupertoken(
uint256 fromIndex,
uint256 recipientIndex,
uint256 destinationChainId,
uint256 amount
)
external
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);
bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(sourceToken));
uint256 sourceBalanceBefore = sourceToken.balanceOf(currentActor());
uint256 sourceSupplyBefore = sourceToken.totalSupply();

vm.prank(currentActor());
try sourceToken.sendERC20(recipient, amount, destinationChainId) {
(, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt);
ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount);
// 26
uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
assert(sourceBalanceBefore - amount == sourceBalanceAfter);
// 10
uint256 sourceSupplyAfter = sourceToken.totalSupply();
assert(sourceSupplyBefore - amount == sourceSupplyAfter);
} 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
// NOTE: should we keep it? will cause the exact same coverage as property_BridgeSupertoken
Expand Down
2 changes: 2 additions & 0 deletions packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {

/// @notice 'real' deploy salt => total supply sum across chains
EnumerableMap.Bytes32ToUintMap internal ghost_totalSupplyAcrossChains;
/// @notice 'real' deploy salt => tokens sendERC20'd but not yet relayERC20'd
EnumerableMap.Bytes32ToUintMap internal ghost_tokensInTransit;

constructor() {
vm.etch(address(MESSENGER), address(new MockL2ToL2CrossDomainMessenger()).code);
Expand Down

0 comments on commit 04bcb7d

Please sign in to comment.