[Certora] Formal verification wish list

[QGarchery]

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 message Not 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 marketParamsList in adapter market v1, and marketParamsList doesn'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 mint and redeem #615)
• allocation/deallocation reverts (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))

[adhusson]

• Shares price increase only happens under some conditions, and at a maximum rate.

[MathisGD]

skimming underlying is ok cc this

[adhusson]

Cannot have relativeCap of 0

It clarifies that a cap of 0 must go through absolute caps. Otherwise you have 2 ways of accomplishing the same thing.

source

[MathisGD]

tried some stuff in #241, if it can help

[adhusson]

• Timelocks at time(uint).max cannot change

[colin-morpho]

• any user can force deallocate if allocator or sentinel can deallocate, liveness (see [Certora] deallocate liveness #514)

[MathisGD]

prove that balances are below totalSupply, with partial sums

[colin-morpho]

prove that balances are below totalSupply, with partial sums

Done in #513, may not be relevant anymore.