eth_deficit.gate

use Call from hexagate;

param disputeGame: address;
param honestChallenger: address;

// Get the delayedWETH address for the particular dispute game
source delayedWETH: address = Call {
    contract: disputeGame,
    signature: "function weth() returns(address)"
};

// Get the credit due to the honest challenger from the dispute game
source claimCredit: integer = Call {
    contract: disputeGame,
    signature: "function credit(address) returns (uint256)",
    params: tuple(honestChallenger)
};

// Get the total credit amount set to be unlocked for the honest challenger from DelayedWETH
source totalCredit: tuple<integer,integer> = Call {
    contract: delayedWETH,
    signature: "function withdrawals(address game, address recipient) returns (uint256 amount, uint256 timestamp)",
    params: tuple(disputeGame, honestChallenger)
};

// Get the balance of ETH for the disputeGame address in DelayedWETH
source ethBalanceDisputeGame: integer = Call {
    contract: delayedWETH,
    signature: "function balanceOf(address) returns (uint256)",
    params: tuple(disputeGame)
};

invariant {
    description: "Deficit of ETH in DelayedWETH contract",
    // Check to make sure that:
    //   1) the credit to be claimed does not exceeded the amount that was unlocked previously
    //   2) the amount that was unlocked previously does not exceed the total ETH balance of the dispute game
    condition: (claimCredit <= totalCredit[0]) and (totalCredit[0] <= ethBalanceDisputeGame)
    // Also check to make sure that totalCredit is NOT non-zero when claimCredit is zero, which indicates a desync
                and !(claimCredit == 0 and totalCredit[0] != 0)
};