[Certora] verif wish list

[MathisGD]

• use HAVOC_ALL by default, see this comment
• only withdraw decrease withdrawable liquidity + total units cannot increase after maturity (wip see [Certora] Added spec PostMaturityWithdrawable #1206)
• liveness of withdraw after maturity: after maturity withdrawing less than the withdrawable amount (and the credit) doesn't revert (wip, see [Certora] Withdraw does not revert rule. #1209)
• after updatePosition, the updated user credit is always equal to the credit (see [Certora] balanceAfterSlashing #523), wip Antti (see [Certora] Update position credit and loss #1210)
• after updatePosition, the loss factor is up-to-date, and lastAccrual is up-to-date, wip Antti1 (see [Certora] Update position credit and loss #1210)
• starting from a position such that the updated user credit is equal to the credit, the only way that it differs is because of a bad debt (see [Certora] balanceAfterSlashing #523), wip Antti in [Certora] Only bad debt can desync credit from view #1212
• maxRepaid overestimation bounds. [Certora] liquidate maxRepaid restores health #1083 proves that it is an overestimation of the quantity needed to make the position healthy. The question is "by how much?", wip Jochen
• prove some bounds on the taker assets (see this message)
• set loop iter back to 2 in BalanceEffects and SplitDoesNotPunishMakerOrFavorTaker, see [Certora] cleaning #1211 (comment)

DONE

• integrate [Certora] some invariants #30

• prove that collaterals cannot be seized twice in the same liquidation not relevant now since liquidation only targets one collateral

• prove the properties of trading fee #106

  • trading fee = units * fee (done in [Certora] Maker Price Guarantees #612)
  • makerAssets = units * offerPrice (done in [Certora] Maker Price Guarantees #612)
  • fee = 0 => feeAmount = 0 (already done very early in takeInputOutputConsistency)
  • buyerPrice >= sellerPrice (abandoned, because it's subsumed by the one below and because the buyerPrice&sellerPrice only live as local variables in take)
  • buyerAssets >= sellerAssets (done in [Certora] Maker Price Guarantees #612, is a result of the rule feeIsNotBypassed)

• properties of fix: require collats to be sorted #169 (done in [Certora] Created obligations #374)

• additional properties of touchObligation, see this. Done in [Certora] new property on ObligationCreated #672 . No sensible way to prove roundtrip toObligation(toId(obligation)) == obligation in certora because of CREATE2 usage, hence dropped.

• show that maker price is lower than or equal to 1 prices are lower than 1, see buyerPrice > 1 is ok? #226 buyer price can be greater than 1 (done it in [Certora] TickLib #880)

• (stuck) properties related to recovery close factor + min collat #303 (see [Certora] liquidate maxRepaid restores health #1083)

  • health can be restored by a max liquidation [Certora] liquidate maxRepaid restores health #1083
  • prove the rounding bound of maxRepaid

• token balance should cover all collateral, and all withdrawable funds. (done in [Certora] Solvency #348)
  $\mathit{token}.\mathtt{balanceOf}(\mathtt{this}) ≥ \sum_{\mathit{obligation} | \mathit{obligation}.\mathtt{loantoken} = \mathit{token}} \mathtt{withdrawable}(\mathtt{toId}(obligation)) + \sum_{\mathit{owner}, \mathit{obligation}} \mathtt{collateralOf}(\mathit{owner}, \mathit{obligation}, \mathit{token})$

• $\mathtt{totalUnits}(\mathit{id}) = (\sum_{\mathit{owner}} \mathtt{debtOf}(\mathit{owner},\mathit{id})) + \mathtt{withdrawable}(\mathit{id})$

• sum of value of collateral * lltv ≥ value of debt (for each healthy owner, obligation pair) {This is kind of hard for formal: muldiv with rounding, oracle prices, loop over collaterals.}

  • Hence, value of all tokens ≥ sum of all totalUnits(id) for all id. {this is a corollary of the above}

• (abandoned as too complex) Debts can always be liquidated if unhealthy or expired.
  {liquidate does its own implementation of isHealthy, so it’s an interesting property, but hard for the solver?}

• Debts can only be liquidated if unhealthy or expired. (pr in [Certora] Added rule liquidateRequireUnhealthy #373)

• Vault logic: share/asset ratio can only decrease on bad debt. share/asset ratio only increases due to rounding errors

• Share/asset ratio is never above 1 (done in [Certora] Share price less than one #157, disabled for now)

• Healthy position cannot be made unhealthy without moving prices or waiting for maturity. (pr in [Certora] Check that isHealthy is preserved if price does not change #388) (pr in [Certora] Check strong invariant isHealthy || liquidationLocked #679 )

• ishealthy or liquidation locked verif: callback issue #496 (will be fixed in [Certora] Check strong invariant isHealthy || liquidationLocked #679)

• Liquidation is profitable: the value of paid out collateral is larger than the value of paid loan tokens. ([Certora] liquidation is profitable and bounded by LIF #497)

• The profit of liquidation is bounded by LIF, which is bounded by 15 %. ([Certora] liquidation is profitable and bounded by LIF #497)

• Splitting an offer will not punish the maker. ([Certora] Split Properties  #542)

• Offers can be split. ([Certora] Split Properties  #542)

• Maker Price Guarantees (in [Certora] Maker Price Guarantees #612 )

• Continuous Fee Protections (in [Certora] ContinuousFee Protections #633 )

• Offers cannot be replayed; a fully taken offer can never be taken again (partially done in rules offerInputsConsumed/offerInputsLimit) (done in [Certora] more robust consume spec #498 )

• Offers can be canceled (only) by maker.

• Only authorized users can decrease the share of a lender (done in [Certora] Only authorized users can decrease the share of a lender #410)

  • also show that making an offer can lead to your shares decreasing

• Only authorized users can increase the debt of a borrower (done in [Certora] only authorized user can increase debt of a borrower  #411)

  • also show that making an offer can lead to your debt increasing

• Only authorized users and liquidation can decrease the collateral of a borrower. #519

• (done in [Certora] takeBuyerEffects and takeSellerEffects #728) In take, only the seller side can newly become a borrower; the buyer can only reduce existing debt.

• For each (maker, group), consumed[maker][group] never exceeds the offer’s configured maximum in its chosen dimension (the latter is only true for take)

• consume properties: non-decreasing, only take and setConsume can modify consumed, updates of consumed, etc. (done in [Certora] Consume #461 )

• repay and liquidate can only increase withdrawable[id]; only withdraw decreases it, exactly by the withdrawn amount. All other functions keep it unchanged (done in [Certora] Withdrawable Monotonicity #450)

• Trading fees bounds (done in [Certora] Fee Boundaries #449)

  • improvement of the rule (see [Certora] Fee Boundaries #449 (comment))

• Reentrancy, see Callback execution fix without Reentrancy Guard #395 (caught by [Certora] Check that isHealthy is preserved if price does not change #388)

• WIP: new bad-debt logic invariant: sum of balanceOfAfterSlashing(id,user) <= totalUnits(id) (jhoenicke).

• properties about the collateral bitmap

  • borrowers can only have non-zero collateral if the corresponding bit is set (done in [Certora] Check that isHealthy is preserved if price does not change #388)
  • removing the bitmap is equivalent to the naive approach (done for isHealthy in [Certora] Check that isHealthy is preserved if price does not change #388)
  • check that the number of bits set is less than or equal to 10, equivalently we could check that a given borrower never has more than 10 non-zero collaterals

• properties about the loss index: it's monotonic, can't cause reverts, and is only changed when bad debt happens ([Certora] Loss index properties #570 )

• the creditOf properties (nobody can change other users' credit, should also hold for updatePositionView()) (except for bad debt on liquidations). Proven in the rule onlyAuthorizedCanChangeCreditAndDebtExceptLiquidateAndUpdatePosition, first introduced in [Certora] improve onlyXXXCanChange specs #490

• (done) similarly use updatePositionView(affectedUser) instead of creditOf(affectedUser) for the credit after the op or prove that both functions return the same.

• check slot saving PR is safe on take with another method (maybe observationally), see here ([Certora] Check that non-zero credit is not accessed before update even in take #608 )

• find a way to remove hasCredit (see this thread)

• can't exploit the bundler allowance, see this comment (moved to its own repo)

• done no position can have collateral = 0 everywhere and some debt, see this comment

• (done) update position does not change relevant position after an interaction. Also update position does not modify credit if the loss index is up to date. see handle max loss index (spearbit-9) #743

• (done) show that all the assets are reachable in TakeAmountsLib, also show that the repay function of the bundler can target any units (see this)

• post maturity the debt cannot increase (see this) (done in [certora] Post Maturity Debt check #967)

• Continuous fee (from 470)

  • (done) updatePosition and updatePositionView give the same result
  • done #988 debt at maturity prediction is accurate (face value is credit - pending)
  • roundings are in the user's favor (the ratio pending/debt decreases) (done in [Certora] ContinuousFee Protections #633)
  • equivalence reverts (continuous fee activation never make you revert in new ways) (done in [Certora] Prove that take has no new reverts due to continuous fees #998)
  • pendingFee is updated by deltaDebt * fee * ttm
  • [continuous fee] per borrower, remaining #470 (comment) (no longer relevant after lender side continuous fee #547)
  • [continuous fee] per borrower, remaining #470 (comment) (no longer relevant after lender side continuous fee #547)
  • done #988 invariant relating pendingFee, credit, continuousFee, and TTM: pendingFee <= credit * continuousFee * TTM not true because of roundings and because the continuous fee can change. Instead simply show that pending fee is 0 after maturity

• show that a market is not read before it is created (certora: prove a market is not read before it is created #1076)

• require to_mathint(offer.obligation.maturity) <= to_mathint(e.block.timestamp) + MAX_TTM(); // TODO verify this cleanly (done in Prove maturity ≤ timestamp + MAX_TTM bound #1078)

• realizableBadDebt cannot increase (without price update). Liquidation is a special case: it's not enough for it to not increase realizableBadDebt, as it also realizes it ([Certora] realizable bad debt cannot increase without price update #1079)

• variation: [Certora] post-price-drop realizable bad debt cannot increase (liquidate) #1084

• the previewed credit is equal to the credit after updating the position. Done in updatePositionEffects now with the line assert credit(id, user) == updatedUserCredit (see [Certora] balanceAfterSlashing #523)

[MathisGD]

prove that prices can't be above 1

[MathisGD]

properties related to #303

[MathisGD]

resolve the unsound require added here: #742

[MathisGD]

prove that debt > 0 => !(all collats at zero)

(or all collats at zero => debt == 0)