Sandclock
  • Introduction
    • Glossary
    • Disclaimer
  • Strategies
    • v1 (Deprecated)
      • Amethyst
      • Jade
    • v2
      • scETH
      • scUSDC
      • scLUSD
      • scDAI
      • scSDAI
      • scUSDS
      • scUSDT
  • QUARTZ & The DAO
    • QUARTZ
    • Staking
    • Governance
    • Allocation
  • Partnerships
  • Technical Documentation
    • Specification
      • Vault
        • Vault Properties
      • Strategies
        • Strategy Properties
    • Security
      • External
      • Internal
      • Emergency Procedure
    • Resources
    • Integration
    • Deployments
Powered by GitBook
On this page
  • Sandclock System Properties
  • Arithmetic
  • Access Control
  1. Technical Documentation
  2. Specification
  3. Vault

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 depositstotalPrincipal==∑deposits

Property
Echidna
Formally Verified

✓

✓

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

✓

PreviousVaultNextStrategies

Last updated 1 year ago

deposits preserve

withdrawals preserve

totalPrincipal==∑depositstotalPrincipal == \sum depositstotalPrincipal==∑deposits
totalPrincipal==∑depositstotalPrincipal == \sum depositstotalPrincipal==∑deposits