[Bug]: Shortfall value might not be enough for vault to become healthy

[shoham-certora]

Summary

When using VaultHub.rebalanceShortfall value for rebalancing an unhealthy vault (e.g. in VaultHub.forceRebalance), the vault may still remain unhealthy due to rounding issues. Particularly in cases where the vault's reserveRatioBP is equal to its forcedRebalanceThresholdBP.

Expected Behavior

After calling VaultHub.forceRebalance(vault) or VaultHub.rebalance(vault, rebalanceShortfall(vault) for an unhealthy vault, it is expected that the vault will be healthy (i.e. isVaultHealthy(vault) to return true).

Potential Impact

The vault will remain unhealthy, and will require additional rebalancing calls.

Steps to Reproduce

The example below was created by the Certora Prover, see this link for the full details.

1. The vault's initial state:

   totalValue = 1000
   liabilityShares = 689
   sharesValue = 801 (internalEth = 100001, internalShares = 86021. ratio=1.162518454795922)
   reserveRatioBP = forcedRebalanceThresholdBP = 2000
   

2. Shortfall calculation: yield 5:

   shortfall = 5
   sharesByTotalValue = 860
   liabilityShares - shortfall = 684
   sharesByTotalValue - shortfall = 855
   (liabilityShares - shortfall) / (sharesByTotalValue - shortfall) = 0.8 (80%)
   

3. Call rebalance(vault, 5):

   liabilityShares = 684
   valueToRebalance = 6
   totalValue = 994
   (internalEth = 100007, internalShares = 86026. ratio = 1.1625206332969102)
   

4. Is vault healthy returns false:

   liability = 796
   totalValue * (TOTAL_BASIS_POINTS - reserveRatioBP) / TOTAL_BASIS_POINTS = 795 (795.2)
   liability > 795
   

Note that even if we rebalanced by shortfall + 1 the vault remains unhealthy.

• Call rebalance(vault, 6):

  liabilityShares = 683
  valueToRebalance = 7
  totalValue = 993
  (internalEth = 100008, internalShares = 86027. ratio = 1.1625187441152196)
  

• Is vault healthy returns false:

  liability = 795 (by both the current and previous ratio)
  totalValue * (TOTAL_BASIS_POINTS - reserveRatioBP) / TOTAL_BASIS_POINTS = 794 (794.4)
  liability > 794
  

Possible Solutions

No response

Guidelines

• I agree to follow Code of Conduct.
• I have read Lido Contribution Guide.

[shoham-certora]

In addition, another issue with the shortfall calculation is that an unhealthy vault can have zero shortfall. Here is an example by the Certora Prover (the full report is here).

totalValue = 1000
liabilityShares = 235
liability = _getPooledEthBySharesRoundUp(liabilityShares) = 705
reserveRatioBP = 2951

The shortfall calculation:

sharesByTotalValue = _getSharesByPooledEth(totalValue) = 333
maxMintableRatio = 10000 - reserveRatioBP = 7049
shortfall = (liabilityShares * TOTAL_BASIS_POINTS - sharesByTotalValue * maxMintableRatio) / reserveRatioBP
                = (235 * 10000 - 333 * 7049) / 2951
                = 2683 / 2951 = 0

But if we check the health condition (assuming reserveRatioBP == forceRebalanceThresholdBP) we see that the vault can probably be made healthy by rebalancing:

liability = 705 > totalValue * (10000 - reserveRatioBP) / 10000 = 704.9

[shoham-certora]

One last note, the shortfall value might also be too large for making a vault healthy (according to reserveRatioBP). Here is an example from the Certora Prover, the full example is here.

1. Initial state:

   totalValue = 1000
   liabilityShares = 269
   liability = getPooledEthBySharesRoundUp(liabilityShares) = 774
   reserveRatioBP = 2308
   

2. Shortfall calculation returns 9 shares.
3. After calling rebalance(vault, shares=7) (only 7 shares):

   totalValue = 979
   liabilityShares = 262
   liability = getPooledEthBySharesRoundUp(liabilityShares) = 753
   

Calculating if the reserve ratio holds shows the vault has sufficient reserve:

liability = 753 <= totalValue * (TOTAL_BASIS_POINTS - reserveRatioBP) / TOTAL_BASIS_POINTS
                = 979 * (10000 - 2308) / 10000
                = 753