Compound V2 - New Market with Zero Liquidity

This invariant monitors for new markets listed with zero liquidity. This detects this scenario: https://www.comp.xyz/t/hundred-finance-exploit-and-compound-v2/4266

If this occurs, it indicates that a blackhat hacker could instantly exploit the market due to a vulnerability in creating new markets in Compound without initial liquidity. To prevent this, protocols should atomically mint some tokens as soon as the market opens, all within the same transaction. Otherwise, there's a gap that this monitoring invariant would detect in real-time, flagging the risk immediately.

use Call, Events, Len from hexagate;

source unitroller: address = <provide the unitroller address>;
source newMarket: list<tuple<address>> = Events {
  contract: unitroller,
  signature: "event MarketListed(address rToken)"
};

source rToken: address = newMarket[0][0];

source supply: integer = Call {
  contract: rToken,
  signature: "function totalSupply() returns (uint256)"
};

rule {
  description: "New market listed but supply is zero - CRITICAL: add supply",
  condition: Len { sequence: newMarket } > 0 ? supply > 0 : true
};