Gearbox V2
Risk management
Math proof of fast collateral check

Fast check proof

In this article, we prove the safety of fast checks to ensure protocol overcollateralization.

Assumptions

  1. Health factor HfH_f is more than 1

  2. Credit account has debt (loan plus interest) DD and c1c_1 units of asset 1. It's liquidity threshold is LT1LT_1, price p1p_1.

  3. Liquidation thresholds are calculated for both assets as

LT=1dPfLfp,LT = 1 - dP- f_L-f_p,

where dPdP is max price drop during liquidation time, fLf_L - liquidation fee (goes to liquidator), fpf_p - liquidation premium (goes to DAO treasury).

  1. User swaps Δc1\Delta c_1 units of asset 1 to Δc2\Delta c_2 asset 2 with liquidation threshold LT2LT_2 and price p2p_2.

  2. During swap protocol calculates fast check

1LT2Δc2p2LT1Δc1p1fp1 - \frac{LT_2\Delta c_2 p_2}{LT_1\Delta c_1 p_1} \le f_p

and allows trade if and only if fast check is successful

  1. Gearbox is enough overcollateralized if in case of liquidation protocol can ensure repaying debt DD and paying liquidation fee fLDf_LD.

Problem formalization / Theorem

To ensure Gearbox protocol's overcollateralization after a financial transaction, it is enough to perform fast checks.

Proof

Our theorem can be written as optimization problem:

Let's define

V=minΔc1[0,c1],Δc20,dp[0,dP2]{(c1Δc1)p1+Δc2p2(1dp)}V=\displaystyle\min_{ \Delta c_1\in[0,c_1],\Delta c_2\ge0, dp\in [0,dP_2]} \left\{ (c_1-\Delta c_1)p_1+\Delta c_2p_2(1-dp) \right\}

as Credit Account's Total Value after trade. Here dpdp means possible price drop during swap (or immediately after it).

It is necessary to proof that VD/(1fL)V \ge D/(1-f_L) under conditions of described in Assumptions section. If this equation is true, than gearbox has enough overcollaterization even in case of liquidations happens next.

Let's find minimum for VV equation. We can find minimum using linear programming methods:

V=minΔc1[0,c1]{c1p1Δc1p1+(1fp)(1dP2)Δc1p1LT1LT2}:V = \displaystyle\min_{\Delta c_1\in[0,c_1]} \left\{c_1p_1-\Delta c_1 p_1+ (1-f_p)(1-dP_2)\Delta c_1 p_1 \frac{LT_1}{LT_2} \right\}:
  1. If (1fp)(1dP2)LT1LT2>1(1-f_p)(1-dP_2)\frac{LT_1}{LT_2}>1, then minimum is reached at Δc1=0\Delta c_1 = 0. In this case system stays overcollateralized as there is no any trades/actions.

  2. If (1fp)(1dP2)LT1LT2=1(1-f_p)(1-dP_2)\frac{LT_1}{LT_2}=1, then V=c1p1V=c_1p_1. Taking into account that at start health factor Hf1H_f\ge 1 we get V=c1p1=DHf/LT1D/LT1D/(1dP1fpfL)D/(1fL)V=c_1p_1=DH_f/LT_1\ge D/LT_1 \ge D/(1-dP_1-f_p-f_L) \ge D/(1-f_L), so system is overcollateralized.

  3. If (1fp)(1dP2)LT1LT2<1(1-f_p)(1-dP_2)\frac{LT_1}{LT_2}<1, then Δc1=c1\Delta c_1 = c_1 and

V=(1fp)(1dP2)c1p1LT1LT2=(1fp)(1dP2)DHfLT2V = (1-f_p)(1-dP_2)c_1p_1\frac{LT_1}{LT_2} = (1-f_p)(1-dP_2)\frac{DH_f}{LT_2}

Let's compare this equation with D/(1fL)D/(1-f_L):

(1fp)(1dP2)DHfLT2D1fL(1-f_p)(1-dP_2)\frac{DH_f}{LT_2} \bigwedge \frac{D}{1-f_L}

Which is equal to

(1fp)(1fL)(1dP2)Hf1dP2fpfL(1-f_p)(1-f_L)(1-dP_2)H_f \bigwedge 1-dP_2-f_p-f_L

As Hf1H_f \ge 1 and

(1fpfL+fpfL)dP2(1fpfL+fpfL)1dP2fpfL(1-f_p-f_L+f_pf_L)-dP_2(1-f_p-f_L+f_pf_L) \ge 1 - dP_2-f_p-f_L

(as

fpfL+dP2(fp+fLfpfL)0f_pf_L+dP_2(f_p+f_L-f_pf_L)\ge 0

for any fp,  fL[0,1]f_p,\;f_L\in[0,1]), we get that

=\bigwedge = \ge

So we get that for case 3 inequality VD/(1fL)V\ge D/(1-f_L) is also true.

Then this inequality is true for all cases and system is always overcollateralized.

Last updated on November 13, 2023