Fast check proof
In this article, we prove the safety of fast checks to ensure protocol overcollateralization.
Health factor is more than 1
Credit account has debt (loan plus interest) and units of asset 1. It's liquidity threshold is , price .
Liquidation thresholds are calculated for both assets as
where is max price drop during liquidation time, - liquidation fee (goes to liquidator), - liquidation premium (goes to DAO treasury).
User swaps units of asset 1 to asset 2 with liquidation threshold and price .
During swap protocol calculates fast check
and allows trade if and only if fast check is successful
- Gearbox is enough overcollateralized if in case of liquidation protocol can ensure repaying debt and paying liquidation fee .
To ensure Gearbox protocol's overcollateralization after a financial transaction, it is enough to perform fast checks.
Our theorem can be written as optimization problem:
as Credit Account's Total Value after trade. Here means possible price drop during swap (or immediately after it).
It is necessary to proof that 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 equation. We can find minimum using linear programming methods:
If , then minimum is reached at . In this case system stays overcollateralized as there is no any trades/actions.
If , then . Taking into account that at start health factor we get , so system is overcollateralized.
If , then and
Let's compare this equation with :
Which is equal to
for any ), we get that
So we get that for case 3 inequality is also true.
Then this inequality is true for all cases and system is always overcollateralized.