diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol index 8e1526bca7948..6eb1c30e67994 100644 --- a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol +++ b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -31,8 +31,8 @@ contract MockL2ToL2CrossDomainMessenger { CrossChainMessage[] private _messageQueue; bool private _atomic; - function messageQueue(uint256 index) external view returns (CrossChainMessage memory) { - return _messageQueue[index]; + function messageQueue(uint256 rawIndex) external view returns (CrossChainMessage memory) { + return _messageQueue[rawIndex % _messageQueue.length]; } function crossChainMessageReceiver( @@ -63,7 +63,8 @@ contract MockL2ToL2CrossDomainMessenger { _atomic = atomic; } - function relayMessageFromQueue(uint256 index) public { + function relayMessageFromQueue(uint256 rawIndex) public { + uint256 index = rawIndex % _messageQueue.length; CrossChainMessage memory message = _messageQueue[index]; _messageQueue[index] = _messageQueue[_messageQueue.length - 1]; _messageQueue.pop(); diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol index 849e3af18cab6..089e19ccf3f5b 100644 --- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol +++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol @@ -193,8 +193,6 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti /// @custom:property-id 7 /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid function property_RelayERC20(uint256 messageIndex) external { - uint256 queueLength = MESSENGER.messageQueueLength(); - messageIndex = bound(messageIndex, 0, queueLength - 1); MockL2ToL2CrossDomainMessenger.CrossChainMessage memory messageToRelay = MESSENGER.messageQueue(messageIndex); OptimismSuperchainERC20 destinationToken = OptimismSuperchainERC20(messageToRelay.crossDomainMessageSender); uint256 destinationSupplyBefore = destinationToken.totalSupply();