-
Notifications
You must be signed in to change notification settings - Fork 21
Open
Labels
Description
List of specifications to ongoing/done:
- token transfers (done in [Certora] Token transfers #573 and [Certora] Tokens no adapter #684 )
- liveness: can remove adapter, can remove IRM, can IKR (done in [Certora] Verif liveness #372)
- timelocks of uint256.max cannot change (done in [Certora] Abdicated functions #367)
- gating doesn't allow unwhitelisted users to get shares (done in [Certora] Gate spec #620)
- preview functions return the same value as their non-preview counterparts (done in [Certora] Preview functions #468)
- immutability/reentrancy safety (done in [Certora] Basic safety properties #537)
- owner can recover his vault (done in [Certora] Basic safety properties #537)
- sentinel can derisk vault (done in [Certora] Sentinel liveness properties #541)
-
allocators or sentinel can deallocate if user can force deallocate, liveness (see [Certora] deallocate liveness #514) -
donation resistance (see [Certora] Donation resistance #700)abandoned, see reason in the PR -
ensure adapters are donation resistant, see related messageNot planned because adapters don't have internal accounting of shares anymore -
rate doesn't change without a call Fix: accrue interest in zeroInterestPerSecond #566 (review)this was only true with the manual vic - share price variations, happen only for some functions/conditions, and bound with the max rate; assuming no interest accrual (i.e.
elapsed == 0) share price can’t increase (done in [Certora] Exchange rate #542) - view reentrancy safety (done in [Certora] View reentrancy #769)
- the list of adapters doesn't contain duplicates (done in [Certora] Relative caps #704)
- assuming no withdraw or loss realization allocation < relativeCap (done in [Certora] Relative caps #704)
- market with allocation 0 are not in the
marketParamsListin adapter market v1, andmarketParamsListdoesn't contain duplicates (done in [Certora] Properties about marketParamsList #777) - check each timelocked function, and what abdicating them do (done in [Certora] Abdication per function #762)
- import chainsec spec: ids, change, and vault allocation (done in [Certora] Import Chainsecurity specs #621)
- adapters id list properties (done in [Certora] Import Chainsecurity specs #621)
- prove that the allocation of the market v1 adapter corresponds to the allocation of the vault (see similar ideas in [Certora] new market adapter #799). Not needed after refactor in feat: remove allocation from storage #827
- generalize sentinel liveness spec (see [Certora] Sentinel liveness properties #541 (comment) and [Certora] Sentinel liveness properties #541 (comment)) (done in [Certora] Revamp sentinel liveness #773)
- timelock formula (see docs: timelocks #297 and [Certora] verif timelocks #763, done in [Certora] Earliest time to execute (WIP) #835)
- revert reasons for functions (see [Certora] Reverts (WIP) #368, done in [Certora] Reverts #834)
- it's always possible to remove a market from the list of markets in market v1 adapter (done in [Certora] Remove market liveness #781)
- skimming underlying (ie vault funds cannot be stolen by skimming)
- prove that the other ids allocation are a sum of the allocation of the market id (see
require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change >= 0, "safe because of changeForDeallocateIsBoundedByAllocation and other ids returned have greater allocation than this/marketParams id";in [Certora] Revamp sentinel liveness #773)
Paused for now:
- sentinel can prevent all bad actions from the curator (see [Certora] Sentinel liveness properties #541 (comment))
- similarity spec for mint and redeem (see [Certora] token specs for
mintandredeem#615) -
allocation/deallocationreverts (related to market manipulation prevention, Prevent arbitrary market interaction (in vault) #484) (see draft [Certora] Market manipulation prevention spec #522, see [Certora] Verif allocations #617)
To tackle by Certora:
- total assets is never read before being updated (see Fix: no accrueInterest in deallocate #567 (review))