Strategy Properties

Liquity

Property
Echidna
Formally Verified

invest: reverts if msg.sender is not manager

invest: reverts if underlying balance is zero

invest: deposits underlying to the stabilityPool

withdrawToVault: reverts if msg.sender is not manager

withdrawToVault: reverts if amount is zero

withdrawToVault: reverts if amount is greater than invested assets

withdrawToVault: works if amount is less than invested assets

withdrawToVault: works if amount is equal than invested assets

allowSwapTarget: reverts if msg.sender is not settings role

allowSwapTarget: add _swapTarget to allowedSwapTargets.

denySwapTarget: reverts if msg.sender is not settings role

denySwapTarget: remove _swapTarget from allowedSwapTargets.

setMinPrincipalProtectionPct: reverts if msg.sender is not settings role

reinvest: reverts if msg.sender is not keeper role

initialize: can be called only once

harvest: claim ETH and LQTY rewards from stability pool

investedAssets() > 0 <=> hasAssets()

isSync() == true

transferAdminRights: reverts if msg.sender is not admin.

transferAdminRights: transfer admin rights to the new admin

Rysk

Property
Echidna
Formally Verified

invest: reverts if msg.sender is not manager

invest: reverts if underlying balance is zero

invest: deposits underlying to the ryskLqPool.

withdrawToVault: reverts if msg.sender is not manager

withdrawToVault: reverts if amount is zero

withdrawToVault: initiate withdraw from the ryskLqPool if amount > 0

completeWithdrawal: reverts if msg.sender is not keeper

completeWithdrawal: withdraw underlying from the ryskLqPool to vault

investedAssets() > 0 <=> hasAssets()

isSync() == false

transferAdminRights: reverts if msg.sender is not admin.

transferAdminRights: transfer admin rights to the new admin

Last updated