OP StateRoot Invariant

This Gate monitor checks that a state root posted on L1 in a new dispute game to the state root on OP mainnet:

use Len, StateRoot, BlockHash, StorageHash, Keccak256, Events, Call from hexagate;

// Define the DisputeGameFactoryProxy contract address
source disputeGameFactoryProxy: address = 0xe5965Ab5962eDc7477C8520243A95517CD252fA9;

// Fetch DisputeGameCreated events from the DisputeGameFactoryProxy
source disputeGameCreatedEvents: list<tuple<address, integer, bytes>> = Events {
    contract: disputeGameFactoryProxy,
    signature: "event DisputeGameCreated(address indexed disputeProxy, uint32 indexed gameType, bytes32 indexed rootClaim)"
};

// Parse out the Latest DisputeGameCreated event
source disputeGameCreated: tuple<address, integer, bytes> = disputeGameCreatedEvents[0];

// Extract relevant information from the event
source disputeProxy: address = disputeGameCreated[0];
source gameType: integer = disputeGameCreated[1];
source l2OutputProposal: bytes = disputeGameCreated[2];

// Get the starting block number from the disputeProxy contract
source optimismBlockNumber: integer = Call {
    contract: disputeProxy,
    signature: "function l2BlockNumber() public pure returns (uint256 l2BlockNumber_)"
};

// Get the optimism block hash
source optimismBlockHash: bytes = BlockHash {
    block: optimismBlockNumber,
    chainId: 10
};

// Get the optimism state root
source optimismStateRoot: bytes = StateRoot {
    block: optimismBlockNumber,
    chainId: 10
};

// Get the message passer storage hash
source optimismMessagePasserStorageHash: bytes = StorageHash {
    address: 0x4200000000000000000000000000000000000016,
    block: optimismBlockNumber,
    chainId: 10
};

// Compute the L2 output proposal hash
source computedL2OutputProposal: bytes = Keccak256 {
    input: bytes(0x0000000000000000000000000000000000000000000000000000000000000000) + optimismStateRoot + optimismMessagePasserStorageHash + optimismBlockHash
};

// Invariant to check that the computed L2 output proposal matches the L2 output proposal from the event
invariant {
    description: "Dispute game created with correct L2 output proposal",
    condition: Len { sequence: disputeGameCreatedEvents } > 0 ? computedL2OutputProposal == l2OutputProposal : true
};

// Invariant to ensure only one DisputeGameCreated event per block
invariant {
    description: "Only one DisputeGameCreated event should appear in the same block",
    condition: Len { sequence: disputeGameCreatedEvents } < 2
};