Cross Chain Bridge gate

This example explains how to combine data from multiple chains (L1 and L2) and verify a specific mechanism, which in this case is the bridge. On that invariant monitor, we verify two basic things on the bridge:

1. We check that the minted tokens on L2 are always less than the number of locked tokens on L1 (otherwise, someone has found a way to print money on L2).

2. We verify that the delay is not too significant, meaning there should not be too much difference between the locked and minted tokens.

Bridge Gate

use Call, Max, Min, Abs from hexagate;

source arbcbETH: address = 0x1debd73e752beaf79865fd6446b0c970eae7732f;
source cbETH: address = 0xbe9895146f7af43049ca1c1ae358b0541ea49704;

source arbBridge: address = 0xa3A7B6F88361F48403514059F1F16C8E78d60EeC;

/* Get the cbETH total supply */
source L2cbETHtotalSupply: integer = Call {
  contract: arbcbETH,
  signature: "function totalSupply() returns (uint256)",
  chainId: 42161
};

/* Get the bridge cbETH balance */
source L1BridgecbETHBalance: integer = Call {
  contract: cbETH,
  signature: "function balanceOf(address account) returns (uint256)",
  params: tuple(arbBridge),
  chainId: 1
};


/* Multiplying by 10000 to keep precision of 2 numbers after the decimal point since we work with integers */
source deviation: integer = 10000 - (L2cbETHtotalSupply * 10000) / L1BridgecbETHBalance;

invariant {
  description: "The total supply of the token on L1 allways has to be greater than on L2",
  condition: L1BridgecbETHBalance >= L2cbETHtotalSupply
};

rule {
  description: "L1 Bridge cbETH balance vs L2 cbETH total supply deviated by more than 1%",
  condition: deviation <= 100
};