You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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)
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.
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}
(WIP) 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?}
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 )
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)
from balance after slashing properties, see [Certora] balanceAfterSlashing #523, the suggested change is done in updatePositionEffects now with the line assert creditOf(id, user) == updatedUserCredit
from balance after slashing properties, see [Certora] balanceAfterSlashing #523, that updated user credit is always to the credit of the interacting user (after the interaction)
from balance after slashing properties, see [Certora] balanceAfterSlashing #523, that starting from an updated credit position that is equal to the credit, the only way that it differs from a non-authorized user is because of a bad debt
WIP: new bad-debt logic invariant: sum of balanceOfAfterSlashing(id,user) <= totalUnits(id) (jhoenicke).
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.
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)
done #988invariant 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
todo:
prove that collaterals cannot be seized twice in the same liquidationnot relevant now since liquidation only targets one collateraltake)touchObligation, see this. Done in [Certora] new property on ObligationCreated #672 . No sensible way to prove roundtriptoObligation(toId(obligation)) == obligationin certora because of CREATE2 usage, hence dropped.prices are lower than 1, see buyerPrice > 1 is ok? #226buyer price can be greater than 1 (done it in [Certora] TickLib #880){liquidate does its own implementation of isHealthy, so it’s an interesting property, but hard for the solver?}
isHealthy || liquidationLocked#679 )isHealthy || liquidationLocked#679)consumeproperties: non-decreasing, only take and setConsume can modify consumed, updates of consumed, etc. (done in [Certora] Consume #461 )updatePositionEffectsnow with the lineassert creditOf(id, user) == updatedUserCreditfind a way to removehasCredit(see this thread)can't exploit the bundler allowance, see this comment(moved to its own repo)TakeAmountsLib, also show that the repay function of the bundler can target any units (see this)invariant relating pendingFee, credit, continuousFee, and TTM: pendingFee <= credit * continuousFee * TTMnot true because of roundings and because the continuous fee can change. Instead simply show that pending fee is 0 after maturityrequire 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)