Sandclock
Search
K

Vault Properties

Sandclock System Properties

This file outlines the properties tested using Echidna, as well as properties that have been formally verified. Because proof by contradiction is usually sufficient, negative properties will not be formally verified. On the other hand, Echidna was used on every property.

Arithmetic

Invoking Vault.deposit() with valid parameters always succeeds when
Property
Echidna
Formally Verified
vault total underlying balance increases by the amount deposited
user balance decreases by the amount deposited
total shares of the vault increase by the amount deposited multiplied by shares multiplier
total principal of the vault increases by the amount deposited
Invoking Vault.deposit() with invalid parameters always reverts when
Property
Echidna
Formally Verified
deposit amount equals zero
claim percentage is zero
lock duration is less than the minimum timelock
lock duration is greater than the maximum timelock
claim percentages do not add up to 100 percent
claim percentages are greater than 100 percent
input token is not supported
Invoking Vault.sponsor() with valid parameters always succeeds when
Property
Echidna
Formally Verified
vault total underlying balance increases by the amount deposited
vault balance increases by the amount deposited
user balance decreases by the amount deposited
total shares of the vault remains unchanged
total principal of the vault remains unchanged
Invoking Vault.sponsor() with invalid parameters always reverts when
Property
Echidna
Formally Verified
deposit amount equals zero
lock duration is less than the minimum timelock
lock duration is greater than the maximum timelock
input token is not supported
Invoking Vault.withdraw() with valid parameters always succeeds when
Property
Echidna
Formally Verified
vault total underlying balance decreases by amount withdrawn
user balance increases by the amount withdrawn
total shares of the vault decrease by the withdrawn amount multiplied by the shares multiplier
total principal of vault decreases by the amount deposited
Invoking Vault.withdraw() with invalid parameters always reverts when
Property
Echidna
Formally Verified
lock duration has not passed yet
user has not made a deposit and tries to withdraw more than zero
Invoking Vault.deposit() or Vault.withdraw() does not change price per share
Property
Echidna
Formally Verified
deposits preserve price per share
withdrawals preserve price per share
Invoking Vault.deposit() or Vault.withdraw() does not change the relation
totalPrincipal==depositstotalPrincipal == \sum deposits
Property
Echidna
Formally Verified
deposits preserve
totalPrincipal==depositstotalPrincipal == \sum deposits
withdrawals preserve
totalPrincipal==depositstotalPrincipal == \sum deposits

Access Control

Property
Echidna
Formally Verified
invoking strategy function invest, finishDepositstable or initRedeemstable always reverts if caller is not manager
invoking sponsor always reverts if caller does not have the SPONSOR_ROLE
invoking deposit or sponsor always reverts if vault is Paused
invoking withdraw, partialWithdraw, forceWithdraw or claimYield always reverts if vault is ExitPaused
invoking unsponsor or partial Unsponsor always reverts if vault is ExitPaused
invoking deposit always reverts if vault is in Loss Mode
invoking deposit or sponsor always succeeds when all preconditions are met
invoking withdraw always reverts if vault is in Loss Mode
Last modified 4mo ago