challenger_loses.gate

use Call, Calls, Events, HistoricalEvents, Contains, Len, Range, FilterAddressesInTrace from hexagate;

// Parameters to be passed
param honestChallenger: address;
param disputeGame: address;

// Filter to only run this invariant if the disputeGame address is in the trace
source addressesInTrace: list<address> = FilterAddressesInTrace {
    addresses: list(disputeGame)
};

source zeroAddr: address = 0x0000000000000000000000000000000000000000;

// Source to retrieve `Resolved` events from the specified dispute game contract
source resolveEvents: list<tuple<integer>> = Events {
    contract: disputeGame,
    signature: "event Resolved(uint8 indexed status)"
};

// Track the Resolved event outcome
source resolveStatus: integer = resolveEvents[0][0];

// Source to retrieve historical `Move` events from the specified dispute game contract
source historicalMoveEvents: list<tuple<integer, bytes, address>> = HistoricalEvents {
    contract: disputeGame,
    signature: "event Move(uint256 indexed parentIndex, bytes32 indexed claim, address indexed claimant)"
};

// Retrieve the number of claims
source claimCount: integer = Call {
    contract: disputeGame,
    signature: "function claimDataLen() view returns (uint256)"
};

// Create a list of even parent indices (indicating challenge moves)
source evenParentIndices: list<integer> = Range {
    start: 0,
    stop: claimCount,
    step: 2
};

// Create a list of odd parent indices (indicating defense moves)
source oddParentIndices: list<integer> = Range {
    start: 1,
    stop: claimCount,
    step: 2
};

// Filter the historical events where the claimant is honestChallenger and the parentIndex is even (challenge move)
source challengeMoves: list<tuple<integer, bytes, address>> = [
    event
    for event in historicalMoveEvents
    if (event[2] == honestChallenger) and Contains { sequence: evenParentIndices, item: event[0] }
];

// Filter the historical events where the claimant is honestChallenger and the parentIndex is odd (defense move)
source defenseMoves: list<tuple<integer, bytes, address>> = [
    event
    for event in historicalMoveEvents
    if (event[2] == honestChallenger) and Contains { sequence: oddParentIndices, item: event[0] }
];

// Check if the challenger lost as a challenger
source challengerLost: boolean = (resolveStatus == 2) and (Len { sequence: challengeMoves } > 0);

// Check if the challenger lost as a defender
source defenderLost: boolean = (resolveStatus == 1) and (Len { sequence: defenseMoves } > 0);

// Check if the challenger lost any subgames as well
source claimResults: list<tuple<integer,address,address,integer,bytes,integer,integer>> = [
    Call {
        contract: disputeGame,
        signature: "function claimData(uint256) returns (uint32 parentIndex, address counteredBy, address claimant, uint128 bond, bytes32 claim, uint128 position, uint128 clock)",
        params: tuple(claimIdx)
    }
    for claimIdx in Range {start: 0, stop: claimCount, step: 1}
];

source lostSubgames: list<boolean> = [
    subgame[1] != zeroAddr ? true : false
    for subgame in claimResults
    if (subgame[2] == honestChallenger)
];

// Invariant to trigger an alert if the challenger lost as a challenger
invariant {
    description: "Challenger lost the dispute game while challenging a state root",
    condition: (Len { sequence: addressesInTrace } > 0) ? (Len { sequence: resolveEvents } == 0 ? true : !challengerLost) : true
};

// Invariant to trigger an alert if the challenger lost as a defender
invariant {
    description: "Challenger lost the dispute game while defending a state root",
    condition: (Len { sequence: addressesInTrace } > 0) ? (Len { sequence: resolveEvents } == 0 ? true : !defenderLost) : true
};

// Invariant to trigger an alert if Challenger lost any subgames
invariant {
    description: "Challenger lost one or more subgames",
    condition: (Len { sequence: addressesInTrace } > 0) ? (!Contains { sequence: lostSubgames, item: true }) : true
};