diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..3518b61 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,67 @@ +name: Certora Prover + +on: + push: + branches: [cvlm] + +jobs: + certora_run: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write + id-token: write + steps: + - name: Checkout repository + uses: actions/checkout@v4 + with: + submodules: recursive + - name: Install sui + run: | + curl -sSfL https://raw.githubusercontent.com/Mystenlabs/suiup/main/install.sh | sh + export PATH="$HOME/.local/bin:$PATH" + suiup install -y sui@1.65.2 + - name: Sui version + run: | + sui -V + sui move -V + - name: Apply patch + run: ./certora/munges/munge.sh + - name: Submit Jobs to Certora Prover (Part I) + uses: Certora/certora-run-action@v2 + with: + cli-version: "8.10.1" + cli-release: beta + ecosystem: sui + working-directory: certora/spec/ + configurations: |- + confs/supply_control_decreases.conf + confs/supply_control_increases_p1.conf + confs/supply_control_increases_p2.conf + confs/accounting_no_lst_no_sui.conf + confs/accounting_total_sui_supply.conf + confs/accounting_value_conservation.conf + confs/fees.conf + job-name: "Verification Part I" + certora-key: ${{ secrets.CERTORAKEY }} + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + - name: Submit Jobs to Certora Prover (Part II) + uses: Certora/certora-run-action@v2 + with: + cli-version: "8.10.1" + cli-release: beta + ecosystem: sui + working-directory: certora/spec/ + configurations: |- + confs/no_arbitrage.conf + confs/solvency.conf + confs/solvency_monotonicity.conf + confs/validators_consistency_p1.conf + confs/validators_consistency_p2.conf + confs/validators_integrity.conf + job-name: "Verification Part II" + certora-key: ${{ secrets.CERTORAKEY }} + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} \ No newline at end of file diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 0000000..187518f --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1,7 @@ +# certora +.certora_internal +.venv/ +emv-*/ +build/ +Move.lock +package_summaries \ No newline at end of file diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..c01f070 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,87 @@ +# Certora Formal Verification: Suilend Liquid Staking + +This directory contains Certora's formal verification of the Suilend liquid staking protocol, written in Move on Sui. + +## Directory Structure + +### `spec/` + +The primary verification package. Contains all specification files (written in Move using the `cvlm` framework), per-rule configuration files, and package metadata. + +- `spec/sources/`:Specification modules. Each `.move` file encodes one or more verifiable properties as rules. +- `spec/confs/`:Per-rule Certora Prover configuration files (`.conf`), one per property group. +- `spec/Move.toml`:Package manifest for spec sources. References the `liquid_staking` contract, the `cvlm` (Certora Verification Language for Move) library, Certora Sui framework summaries, and overrides for Sui system packages. + +### `munges/` + +Code modification scripts and patch files. These make internal functions accessible to the Prover by widening their visibility, and reduce `MAX_VALIDATORS` to make verification tractable. + +- `munge.sh`:Applies all patches before running verification. +- `unmunge.sh`:Reverts all patches. +- `record_patches.sh`:Regenerates patch files from current working-directory diffs against HEAD. +- `fees.patch`:Makes `validate_fees()` public. +- `storage.patch`:Widens visibility of view functions and internal helpers; reduces `MAX_VALIDATORS` from 50 to 5. + +> [!NOTE] +> The patches are applied as git patches and must be kept in sync with the source code. If the patched files change, `munge.sh` will fail to apply and verification will not run. Use `record_patches.sh` to regenerate the patches after updating the source. + +### `assumptions/` + +A separate package that verifies assumptions made by summaries in the main spec. Currently contains one rule proving that `liquid_staking::storage::get_sui_amount` is equivalent to `sui_system::staking_pool::get_sui_amount`. + +- `assumptions/sources/assumptions.move`:Assumption validation rules. +- `assumptions/Move.toml`:Package manifest. +- `Assumptions.conf`:Prover configuration for running assumption checks. + +## Certora Prover + +The Certora Prover is a formal verification tool for smart contracts. It statically proves or disproves properties expressed as rules in the Certora Verification Language for Move. + +## Running Instructions + +0. Install the latest certora prover by following the [installation guide](https://docs.certora.com/en/latest/docs/user-guide/install.html). + +1. From the repository root, apply the munges: + + ```sh + sh certora/munges/munge.sh + ``` + + This only needs to be done once per working copy. **Do not commit the munged files.** + +2. Change into the `certora/spec/` directory and run the desired verification job (see table below for all scripts). Example: + + ```sh + certoraRun confs/solvency.conf + ``` + + Note that `certora/spec/` must be the working directory for `certoraRun`, otherwise it will fail to compile. + +3. To revert munges: + + ```sh + sh certora/munges/unmunge.sh + ``` + +## High-Level Properties + +See the doc-comments in each spec file for detailed descriptions of individual rules. + +- **Solvency and Exchange Rate Monotonicity** (`solvency.move`, `solvency.conf`, `solvency_monotonicity.conf`): `total_sui_supply >= total_lst_supply` always holds; SUI/LST exchange rate is non-decreasing +- **Total SUI Supply Accounting** (`accounting_total_sui_supply.move`, `accounting_total_sui_supply.conf`): `total_sui_supply` equals the sum of the liquid SUI pool, active stake (via exchange rate), and inactive stake principal +- **Token Supply Initialization Invariants** (`accounting_no_lst_no_sui.move`, `accounting_no_lst_no_sui.conf`): zero LST implies zero SUI backing and vice versa +- **Value Conservation** (`accounting_value_conservation.move`, `accounting_value_conservation.conf`): no value is created or destroyed; on `mint`, deposited SUI equals backing increase plus fees; on `redeem`, SUI decrease equals SUI returned plus fees +- **Fee Accounting Integrity** (`fees.move`, `fees.conf`): accrued fees never exceed total SUI supply, grow monotonically except during collection, and never fully consume a deposit or redemption +- **Supply Control Authorization** (`supply_control.move`, `supply_control_decreases.conf`, `supply_control_increases_p1/p2.conf`): only `mint` can increase supplies; only `redeem`/`custom_redeem` can decrease them +- **No Arbitrage** (`no_arbitrage.move`, `no_arbitrage.conf`): a back-to-back `mint` then `redeem` never yields more SUI than was deposited +- **Validator Registry Consistency** (`validators_consistency.move`, `validators_consistency_p1/p2.conf`): no duplicate validators, registry never exceeds `MAX_VALIDATORS`, no-stake validators have zero `total_sui_amount` +- **Validator Registry Integrity** (`validators_integrity.move`, `validators_integrity.conf`): validators added only by authorized operations, removed only by `refresh`, at most one per call; `refresh` leaves no inactive stake or empty validators +- **Assumption Validation** (`assumptions/sources/assumptions.move`, `Assumptions.conf`): validates assumptions made in summaries + +## General Assumptions + +- **Loop unrolling.** All specs use `optimistic_loop: true`. `loop_iter` is set to 2 for most validator-list rules and 6 for `validators_upper_bound_step` (one above the munged `MAX_VALIDATORS = 5`). +- **Validator count reduction.** `storage.patch` reduces `MAX_VALIDATORS` from 50 to 5. Several inductive step rules further restrict to 1 validator for tractability. +- **`setup_fresh` precondition.** Most inductive steps model a post-`refresh` state: no inactive stake, all validators have active stake with matching pool IDs and up-to-date exchange rates, `total_sui_supply` is correct, and `last_refresh_epoch == ctx.epoch()`. Each assumption is justified by a separately verified rule. +- **Solvent exchange rates.** `summaries.move` assumes `sui_amount >= pool_token_amount` for all exchange rates, reflecting Sui system-level pool solvency. +- **`redeem_fungible_staked_sui` summary.** The full proportional split between principal and rewards is simplified to `get_sui_amount(er, value)`. An internal `cvlm_assert` checks this is an underapproximation of the actual withdrawal. diff --git a/certora/assumptions/Assumptions.conf b/certora/assumptions/Assumptions.conf new file mode 100644 index 0000000..07c05bc --- /dev/null +++ b/certora/assumptions/Assumptions.conf @@ -0,0 +1,13 @@ +{ + "optimistic_loop": true, + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + ] +} \ No newline at end of file diff --git a/certora/assumptions/Move.toml b/certora/assumptions/Move.toml new file mode 100644 index 0000000..28f2d82 --- /dev/null +++ b/certora/assumptions/Move.toml @@ -0,0 +1,11 @@ +[package] +name = "assumptions" +edition = "2024.beta" + +[dependencies] +liquid_staking = { local = "../../contracts" } +cvlm = { git = "https://github.com/Certora/cvl-move-proto.git", subdir = "cvlm", rev = "main" } +certora_sui_summaries = { git = "https://github.com/Certora/cvl-move-proto.git", subdir = "certora_sui_summaries", rev = "main" } + +[addresses] +assumptions = "0x0" \ No newline at end of file diff --git a/certora/assumptions/sources/assumptions.move b/certora/assumptions/sources/assumptions.move new file mode 100644 index 0000000..80b9933 --- /dev/null +++ b/certora/assumptions/sources/assumptions.move @@ -0,0 +1,32 @@ +module assumptions::assumptions; + +/* + Here we validate the assumptions we make in the main spec's summaries + */ + +use cvlm::manifest::{rule, function_access}; +use cvlm::asserts::cvlm_assert; +use sui_system::staking_pool::PoolTokenExchangeRate; + +public fun cvlm_manifest() { + rule(b"get_sui_amount_equivalence"); + + function_access(b"ls_get_sui_amount", @liquid_staking, b"storage", b"get_sui_amount"); + function_access(b"ss_get_sui_amount", @sui_system, b"staking_pool", b"get_sui_amount"); +} + +// private function accessors +native fun ls_get_sui_amount(exchange_rate: &PoolTokenExchangeRate, token_amount: u64): u64; +native fun ss_get_sui_amount(exchange_rate: &PoolTokenExchangeRate, token_amount: u64): u64; + +// The main suilend spec's summaries assume that liquid_staking::storage::get_sui_amount is equivalent to +// sui_system::staking_pool::get_sui_amount. We validate that assumption here. +public fun get_sui_amount_equivalence( + exchange_rate: &PoolTokenExchangeRate, + token_amount: u64 +) { + let ls_amount = ls_get_sui_amount(exchange_rate, token_amount); + let ss_amount = ss_get_sui_amount(exchange_rate, token_amount); + cvlm_assert(ls_amount == ss_amount); +} + diff --git a/certora/munges/fees.patch b/certora/munges/fees.patch new file mode 100644 index 0000000..e3ada79 --- /dev/null +++ b/certora/munges/fees.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/sources/fees.move b/contracts/sources/fees.move +index 33df151..caa341c 100644 +--- a/contracts/sources/fees.move ++++ b/contracts/sources/fees.move +@@ -133,7 +133,7 @@ module liquid_staking::fees { + // Note that while it's technically exploitable, we allow lsts to be created with 0 mint/redeem fees. + // This is because having a 0 fee LST is useful in certain cases where mint/redemption can only be done by + // a single party. It is up to the pool creator to ensure that the fees are set correctly. +- fun validate_fees(fees: &FeeConfig) { ++ public fun validate_fees(fees: &FeeConfig) { + assert!(fees.sui_mint_fee_bps <= MAX_BPS, EInvalidFeeConfig); + assert!(fees.staked_sui_mint_fee_bps <= MAX_BPS, EInvalidFeeConfig); + assert!(fees.redeem_fee_bps <= MAX_REDEEM_FEE_BPS, EInvalidFeeConfig); diff --git a/certora/munges/munge.sh b/certora/munges/munge.sh new file mode 100755 index 0000000..ec2072e --- /dev/null +++ b/certora/munges/munge.sh @@ -0,0 +1,2 @@ +git apply -3 certora/munges/fees.patch +git apply -3 certora/munges/storage.patch \ No newline at end of file diff --git a/certora/munges/record_patches.sh b/certora/munges/record_patches.sh new file mode 100755 index 0000000..03ac8fb --- /dev/null +++ b/certora/munges/record_patches.sh @@ -0,0 +1,2 @@ +git diff HEAD:contracts/sources/fees.move contracts/sources/fees.move > certora/munges/fees.patch; +git diff HEAD:contracts/sources/storage.move contracts/sources/storage.move > certora/munges/storage.patch; \ No newline at end of file diff --git a/certora/munges/storage.patch b/certora/munges/storage.patch new file mode 100644 index 0000000..2f3e922 --- /dev/null +++ b/certora/munges/storage.patch @@ -0,0 +1,151 @@ +diff --git a/contracts/sources/storage.move b/contracts/sources/storage.move +index e729823..1023707 100644 +--- a/contracts/sources/storage.move ++++ b/contracts/sources/storage.move +@@ -15,9 +15,13 @@ module liquid_staking::storage { + /* Constants */ + const MIN_STAKE_THRESHOLD: u64 = 1_000_000_000; + const MAX_SUI_SUPPLY: u64 = 10_000_000_000 * 1_000_000_000; +- const MAX_VALIDATORS: u64 = 50; ++ const MAX_VALIDATORS: u64 = 5; + const ACTIVE_STAKE_REDEEM_OFFSET: u64 = 100; + ++ public fun max_validators(): u64 { ++ MAX_VALIDATORS ++ } ++ + /// The Storage struct holds all stake for the LST. + public struct Storage has store { + /// Sui balance. Unstake operations deposit SUI here. +@@ -51,7 +55,7 @@ module liquid_staking::storage { + extra_fields: Bag, + } + +- public(package) fun new(ctx: &mut TxContext): Storage { ++ public fun new(ctx: &mut TxContext): Storage { + Storage { + sui_pool: balance::zero(), + validator_infos: vector::empty(), +@@ -62,43 +66,47 @@ module liquid_staking::storage { + } + + /* Public View Functions */ +- public(package) fun sui_pool(self: &Storage): &Balance { ++ public fun sui_pool(self: &Storage): &Balance { + &self.sui_pool + } + +- public(package) fun validators(self: &Storage): &vector { ++ public fun validators(self: &Storage): &vector { + &self.validator_infos + } + +- public(package) fun total_sui_supply(self: &Storage): u64 { ++ public fun total_sui_supply(self: &Storage): u64 { + self.total_sui_supply + } + +- public(package) fun last_refresh_epoch(self: &Storage): u64 { ++ public fun last_refresh_epoch(self: &Storage): u64 { + self.last_refresh_epoch + } + +- public(package) fun staking_pool_id(self: &ValidatorInfo): ID { ++ public fun staking_pool_id(self: &ValidatorInfo): ID { + self.staking_pool_id + } + +- public(package) fun validator_address(self: &ValidatorInfo): address { ++ public fun validator_address(self: &ValidatorInfo): address { + self.validator_address + } + +- public(package) fun active_stake(self: &ValidatorInfo): &Option { ++ public fun active_stake(self: &ValidatorInfo): &Option { + &self.active_stake + } + +- public(package) fun inactive_stake(self: &ValidatorInfo): &Option { ++ public fun inactive_stake(self: &ValidatorInfo): &Option { + &self.inactive_stake + } + +- public(package) fun exchange_rate(self: &ValidatorInfo): &PoolTokenExchangeRate { ++ public fun exchange_rate(self: &ValidatorInfo): &PoolTokenExchangeRate { ++ &self.exchange_rate ++ } ++ ++ public fun exchange_rate_mut(self: &ValidatorInfo): &PoolTokenExchangeRate { + &self.exchange_rate + } + +- public(package) fun total_sui_amount(self: &ValidatorInfo): u64 { ++ public fun total_sui_amount(self: &ValidatorInfo): u64 { + self.total_sui_amount + } + +@@ -118,7 +126,7 @@ module liquid_staking::storage { + i + } + +- fun is_empty(self: &ValidatorInfo): bool { ++ public fun is_empty(self: &ValidatorInfo): bool { + self.active_stake.is_none() && self.inactive_stake.is_none() && self.total_sui_amount == 0 + } + +@@ -129,10 +137,10 @@ module liquid_staking::storage { + /// - Moves any inactive stake that can be converted to active stake. + /// - Removes validators that have no stake. + /// Returns true if the storage was updated. +- public(package) fun refresh( +- self: &mut Storage, +- system_state: &mut SuiSystemState, +- ctx: &mut TxContext, ++ public fun refresh( ++ self: &mut Storage, ++ system_state: &mut SuiSystemState, ++ ctx: &mut TxContext + ): bool { + if (self.last_refresh_epoch == ctx.epoch()) { + return false +@@ -197,7 +205,7 @@ module liquid_staking::storage { + // this may return none in the case where the staking pool is inactive or + // if sui system is currently in safe mode. In both these cases, the storage + // object has the latest exchange rate already. +- fun get_latest_exchange_rate( ++ public fun get_latest_exchange_rate( + self: &Storage, + staking_pool_id: &ID, + system_state: &mut SuiSystemState, +@@ -219,10 +227,9 @@ module liquid_staking::storage { + + /// Update the total sui amount for the validator and modify the + /// storage sui supply accordingly assumes the exchange rate is up to date +- fun refresh_validator_info(self: &mut Storage, i: u64) { ++ public fun refresh_validator_info(self: &mut Storage, i: u64) { + let validator_info = &mut self.validator_infos[i]; + self.total_sui_supply = self.total_sui_supply - validator_info.total_sui_amount; +- + let mut total_sui_amount = 0; + if (validator_info.active_stake.is_some()) { + let active_stake = validator_info.active_stake.borrow(); +@@ -568,8 +575,8 @@ module liquid_staking::storage { + } + + /* Private functions */ +- fun get_or_add_validator_index_by_staking_pool_id_mut( +- self: &mut Storage, ++ public fun get_or_add_validator_index_by_staking_pool_id_mut( ++ self: &mut Storage, + system_state: &mut SuiSystemState, + staking_pool_id: ID, + ctx: &mut TxContext, +@@ -620,7 +627,7 @@ module liquid_staking::storage { + } + + /// copied directly from staking_pool.move +- fun get_sui_amount(exchange_rate: &PoolTokenExchangeRate, token_amount: u64): u64 { ++ public fun get_sui_amount(exchange_rate: &PoolTokenExchangeRate, token_amount: u64): u64 { + // When either amount is 0, that means we have no stakes with this pool. + // The other amount might be non-zero when there's dust left in the pool. + if (exchange_rate.sui_amount() == 0 || exchange_rate.pool_token_amount() == 0) { diff --git a/certora/munges/unmunge.sh b/certora/munges/unmunge.sh new file mode 100755 index 0000000..a51feb2 --- /dev/null +++ b/certora/munges/unmunge.sh @@ -0,0 +1,3 @@ +git apply -R certora/munges/liquid_staking.patch +git apply -R certora/munges/fees.patch +git apply -R certora/munges/storage.patch \ No newline at end of file diff --git a/certora/spec/Move.toml b/certora/spec/Move.toml new file mode 100644 index 0000000..f9f89a9 --- /dev/null +++ b/certora/spec/Move.toml @@ -0,0 +1,9 @@ +[package] +name = "spec" +edition = "2024.beta" + +[dependencies] +liquid_staking = { local = "../../contracts" } +cvlm = { git = "https://github.com/Certora/cvl-move-proto.git", subdir = "cvlm", rev = "sui-v1.55.0-no-contains" } +certora_sui_summaries = { git = "https://github.com/Certora/cvl-move-proto.git", subdir = "certora_sui_summaries", rev = "sui-v1.55.0-no-contains", rename-from = "certora" } +sui_system = { override = true, git = "https://github.com/MystenLabs/sui.git", subdir = "crates/sui-framework/packages/sui-system", rev = "framework/testnet" } \ No newline at end of file diff --git a/certora/spec/confs/accounting_no_lst_no_sui.conf b/certora/spec/confs/accounting_no_lst_no_sui.conf new file mode 100644 index 0000000..8b4730d --- /dev/null +++ b/certora/spec/confs/accounting_no_lst_no_sui.conf @@ -0,0 +1,25 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*accounting_no_lst_no_sui*" + ], + "msg": "Accounting: No LST iff No SUI", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-depth 20", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ], + "smt_timeout": 1800 +} \ No newline at end of file diff --git a/certora/spec/confs/accounting_total_sui_supply.conf b/certora/spec/confs/accounting_total_sui_supply.conf new file mode 100644 index 0000000..adc7597 --- /dev/null +++ b/certora/spec/confs/accounting_total_sui_supply.conf @@ -0,0 +1,19 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*accounting_total_sui_supply*" + ], + "msg": "Correct accounting of total sui supply", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/accounting_value_conservation.conf b/certora/spec/confs/accounting_value_conservation.conf new file mode 100644 index 0000000..8cbb50b --- /dev/null +++ b/certora/spec/confs/accounting_value_conservation.conf @@ -0,0 +1,24 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*accounting_value_conservation*" + ], + "msg": "LST and SUI value conservation", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-depth 20", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/fees.conf b/certora/spec/confs/fees.conf new file mode 100644 index 0000000..cd8f423 --- /dev/null +++ b/certora/spec/confs/fees.conf @@ -0,0 +1,19 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*fees*" + ], + "msg": "Integrity of fees", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/no_arbitrage.conf b/certora/spec/confs/no_arbitrage.conf new file mode 100644 index 0000000..c908593 --- /dev/null +++ b/certora/spec/confs/no_arbitrage.conf @@ -0,0 +1,21 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*no_arbitrage*" + ], + "msg": "No arbitrage opportunity", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-splitParallel true", + "-dontStopAtFirstSplitTimeout true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/solvency.conf b/certora/spec/confs/solvency.conf new file mode 100644 index 0000000..06f05e3 --- /dev/null +++ b/certora/spec/confs/solvency.conf @@ -0,0 +1,25 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*solvency_base*", + "*solvency_step" + ], + "msg": "LST solvency", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-depth 20", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/solvency_monotonicity.conf b/certora/spec/confs/solvency_monotonicity.conf new file mode 100644 index 0000000..61c9fbc --- /dev/null +++ b/certora/spec/confs/solvency_monotonicity.conf @@ -0,0 +1,24 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*solvency*monotonicity" + ], + "msg": "LST to SUI ratio monotonicity", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-depth 20", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/supply_control_decreases.conf b/certora/spec/confs/supply_control_decreases.conf new file mode 100644 index 0000000..a7920c5 --- /dev/null +++ b/certora/spec/confs/supply_control_decreases.conf @@ -0,0 +1,30 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*only_redemption_decreases_sui_supply", + "*only_redemption_decreases_lst_supply" + ], + "msg": "Supply control: decrease rules", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-oldSplitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true", + "-splitParallelTimelimit", + "7000", + "-splitParallelInitialDepth", + "3", + "-numOfParallelSplits", + "7" + ] +} diff --git a/certora/spec/confs/supply_control_increases_p1.conf b/certora/spec/confs/supply_control_increases_p1.conf new file mode 100644 index 0000000..5fc2f6a --- /dev/null +++ b/certora/spec/confs/supply_control_increases_p1.conf @@ -0,0 +1,32 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*only_minting_increases_sui_supply", + "*only_minting_increases_lst_supply" + ], + "method": [ + "spec::dummy::mint", + "spec::dummy::custom_redeem_request", + "spec::dummy::custom_redeem", + "spec::dummy::change_validator_priority", + "spec::dummy::decrease_validator_stake", + "spec::dummy::increase_validator_stake", + "spec::dummy::update_fees", + "spec::dummy::refresh", + "spec::dummy::update_metadata" + ], + "msg": "Supply control - increase rules (I)", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true" + ], + "smt_timeout": 1800 +} \ No newline at end of file diff --git a/certora/spec/confs/supply_control_increases_p2.conf b/certora/spec/confs/supply_control_increases_p2.conf new file mode 100644 index 0000000..56dce38 --- /dev/null +++ b/certora/spec/confs/supply_control_increases_p2.conf @@ -0,0 +1,36 @@ +{ + "optimistic_loop": true, + "server": "prover", + "prover_version": "master", + "rule": [ + "*only_minting_increases_sui_supply", + "*only_minting_increases_lst_supply" + ], + "method" : [ + "spec::dummy::redeem", + "spec::dummy::collect_fees" + ], + "msg": "Supply control - increase rules (II)", + + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true", + "-oldSplitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true", + "-splitParallelTimelimit", + "7000", + "-splitParallelInitialDepth", + "3", + "-numOfParallelSplits", + "7" + ], + "smt_timeout": 1800 +} diff --git a/certora/spec/confs/validators_consistency_p1.conf b/certora/spec/confs/validators_consistency_p1.conf new file mode 100644 index 0000000..539837d --- /dev/null +++ b/certora/spec/confs/validators_consistency_p1.conf @@ -0,0 +1,21 @@ +{ + "optimistic_loop": true, + "loop_iter": 2, + "server": "prover", + "prover_version": "master", + "rule": [ + "*validators_consistency*no_duplicate_validators", + "*validators_consistency*no_stake_no_sui*" + ], + "msg": "Validators' consistency ", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/validators_consistency_p2.conf b/certora/spec/confs/validators_consistency_p2.conf new file mode 100644 index 0000000..db6e30a --- /dev/null +++ b/certora/spec/confs/validators_consistency_p2.conf @@ -0,0 +1,21 @@ +{ + "optimistic_loop": true, // Cannot be pessimistic because there are internal loops that are not bounded + "loop_iter": 6, // one more than the upper bound, munged to 5, + "rule_sanity": "none", // vacuity checks tend to time out for this rule + "server": "prover", + "prover_version": "master", + "rule": [ + "*validators_consistency*validators_upper_bound*" + ], + "msg": "Validators' consistency: List is upper bounded", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true" + ] +} \ No newline at end of file diff --git a/certora/spec/confs/validators_integrity.conf b/certora/spec/confs/validators_integrity.conf new file mode 100644 index 0000000..8844812 --- /dev/null +++ b/certora/spec/confs/validators_integrity.conf @@ -0,0 +1,24 @@ +{ + "optimistic_loop": true, + "loop_iter": 2, + "server": "prover", + "prover_version": "master", + "rule": [ + "*validators_integrity*can_add_correct", + "*validators_integrity*can_remove_correct", + "*validators_integrity*add_at_most_one", + "*validators_integrity*no_inactive_stake_after_refresh", + "*validators_integrity*no_empty_validators_after_refresh" + ], + "msg": "Validator management integrity", + "prover_args": [ + "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1", + "-disabledTransformations HOIST_LOOPS", + "-maxMergedBranchSize 1000000", + "-maxCommandCount 10000000", + "-maxBlockCount 1000000", + "-tacDumpsWithInternalFunctions true", + "-callTraceVecElemCount 0", + "-dumpCodeSizeAnalysis true" + ] +} \ No newline at end of file diff --git a/certora/spec/sources/accounting_no_lst_no_sui.move b/certora/spec/sources/accounting_no_lst_no_sui.move new file mode 100644 index 0000000..3199f09 --- /dev/null +++ b/certora/spec/sources/accounting_no_lst_no_sui.move @@ -0,0 +1,184 @@ +/// Property: Token Supply Initialization Invariants +/// Description: Verifies that the liquid staking protocol maintains proper relationships between +/// LST (liquid staking token) and SUI supply. Specifically, this +/// ensures that an empty LST supply implies an empty SUI reserve (preventing orphaned SUI), and +/// conversely, that an empty SUI reserve implies no outstanding LST tokens (preventing unbacked tokens). + +module spec::accounting_no_lst_no_sui; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::manifest::{target, invoker, rule}; +use liquid_staking::liquid_staking::{LiquidStakingInfo}; +use spec::dummy::DummyToken; +use sui_system::sui_system::SuiSystemState; +use spec::common::setup_fresh; +use spec::solvency::is_solvent; +use spec::accounting_total_sui_supply::total_supply_correct; +use cvlm::ghost::ghost_destroy; +use liquid_staking::liquid_staking::create_lst; +use cvlm::nondet::nondet; +use liquid_staking::liquid_staking::create_lst_with_stake; + +public fun cvlm_manifest() { + // Public mut functions + target(@spec, b"dummy", b"mint"); + target(@spec, b"dummy", b"redeem"); + target(@spec, b"dummy", b"custom_redeem_request"); + target(@spec, b"dummy", b"custom_redeem"); + target(@spec, b"dummy", b"change_validator_priority"); + target(@spec, b"dummy", b"increase_validator_stake"); + target(@spec, b"dummy", b"decrease_validator_stake"); + target(@spec, b"dummy", b"collect_fees"); + target(@spec, b"dummy", b"update_fees"); + target(@spec, b"dummy", b"refresh"); + target(@spec, b"dummy", b"update_metadata"); + + invoker(b"invoke"); + + rule(b"no_lst_no_sui_step"); + rule(b"no_lst_no_sui_base"); + + rule(b"no_sui_no_lst_base"); + rule(b"no_sui_no_lst_step"); +} + +const MAX_VALIDATORS: u64 = 1; + +native fun invoke( + target: Function, + lis: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + + +/// Checks that if there is no LST supply, then there is no SUI supply. +/// This prevents orphaned SUI that cannot be claimed through LST tokens. +public fun no_lst_no_sui

(lsi: &LiquidStakingInfo

): bool { + let lst = lsi.total_lst_supply(); + let sui = lsi.total_sui_supply(); + // lst == 0 -> sui == 0 <==> lst != 0 || sui == 0 + lst != 0 || sui == 0 +} + +/// Checks that if there is no SUI supply, then there is no LST supply. +/// This prevents unbacked LST tokens that cannot be redeemed for SUI. +public fun no_sui_no_lst

(lsi: &LiquidStakingInfo

): bool { + let lst = lsi.total_lst_supply(); + let sui = lsi.total_sui_supply(); + // sui == 0 -> lst == 0 <==> sui != 0 || lst == 0 + sui != 0 || lst == 0 +} + +/// Base case: Verifies that newly created liquid staking pools (both empty and with initial stake) +/// satisfy the invariant that zero LST supply implies zero SUI supply. +public fun no_lst_no_sui_base( + ctx: &mut TxContext, +) { + let fee_config = nondet(); + let lst_treasury_cap = nondet(); + let (_cap, lsi) = create_lst(fee_config, lst_treasury_cap, ctx); + cvlm_assert(no_lst_no_sui(&lsi)); + + ghost_destroy(lsi); + ghost_destroy(_cap); + + let fee_config = nondet(); + let lst_treasury_cap = nondet(); + let mut system_state = nondet(); + let fungible_staked_suis = nondet(); + let sui = nondet(); + let (_cap, lsi) = create_lst_with_stake(&mut system_state, fee_config, lst_treasury_cap, fungible_staked_suis, sui, ctx); + cvlm_assert(no_lst_no_sui(&lsi)); + + ghost_destroy(lsi); + ghost_destroy(_cap); + ghost_destroy(system_state); + +} + +/// Inductive step: Verifies that all state-modifying operations preserve the invariant that +/// zero LST supply implies zero SUI supply. Assumes the system is solvent and has correct accounting +/// in the pre-state. +public fun no_lst_no_sui_step( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg( + lsi.storage().validators().length() <= MAX_VALIDATORS, + b"Restrict number of validators", + ); + setup_fresh(lsi, system_state, ctx); + + cvlm_assume_msg(is_solvent(lsi), b"Assume solvency in pre state"); + + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Correct accounting"); + + + cvlm_assume_msg(no_lst_no_sui(lsi), b"Assume in pre-state"); + + + invoke(target, lsi, system_state, ctx); + + + + cvlm_assert(no_lst_no_sui(lsi)); +} + + +/// Base case: Verifies that newly created liquid staking pools (both empty and with initial stake) +/// satisfy the invariant that zero SUI supply implies zero LST supply. +public fun no_sui_no_lst_base( + ctx: &mut TxContext, +) { + let fee_config = nondet(); + let lst_treasury_cap = nondet(); + let (_cap, lsi) = create_lst(fee_config, lst_treasury_cap, ctx); + cvlm_assert(no_sui_no_lst(&lsi)); + + ghost_destroy(lsi); + ghost_destroy(_cap); + + let fee_config = nondet(); + let lst_treasury_cap = nondet(); + let mut system_state = nondet(); + let fungible_staked_suis = nondet(); + let sui = nondet(); + let (_cap, lsi) = create_lst_with_stake(&mut system_state, fee_config, lst_treasury_cap, fungible_staked_suis, sui, ctx); + cvlm_assert(no_sui_no_lst(&lsi)); + + ghost_destroy(lsi); + ghost_destroy(_cap); + ghost_destroy(system_state); + +} + +/// Inductive step: Verifies that all state-modifying operations preserve the invariant that +/// zero SUI supply implies zero LST supply. Assumes the system is solvent and has correct accounting +/// in the pre-state. +public fun no_sui_no_lst_step( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg( + lsi.storage().validators().length() <= MAX_VALIDATORS, + b"Restrict number of validators", + ); + setup_fresh(lsi, system_state, ctx); + + cvlm_assume_msg(is_solvent(lsi), b"Assume solvency in pre state"); + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Correct accounting"); + + + cvlm_assume_msg(no_sui_no_lst(lsi), b"Assume in pre-state"); + + invoke(target, lsi, system_state, ctx); + + + cvlm_assert(no_sui_no_lst(lsi)); +} \ No newline at end of file diff --git a/certora/spec/sources/accounting_total_sui_supply.move b/certora/spec/sources/accounting_total_sui_supply.move new file mode 100644 index 0000000..62a1275 --- /dev/null +++ b/certora/spec/sources/accounting_total_sui_supply.move @@ -0,0 +1,143 @@ +/// Property: Total SUI Supply Accounting Accuracy +/// Description: Verifies that the total SUI supply tracked by the storage module precisely matches +/// the sum of all SUI held across different locations: the liquid pool, active stake across all validators, +/// and inactive stake awaiting activation. This property ensures that the protocol's internal accounting +/// accurately reflects the actual SUI holdings, preventing discrepancies that could lead to insolvency +/// or incorrect exchange rate calculations. The invariant is maintained across all storage operations +/// through inductive verification. + +module spec::accounting_total_sui_supply; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::{target, invoker, rule}; +use liquid_staking::storage::{Self, Storage, get_sui_amount, active_stake}; +use sui_system::sui_system::SuiSystemState; +use cvlm::nondet::nondet; + +public fun cvlm_manifest() { + // Public mut functions + + target(@liquid_staking, b"storage", b"refresh"); + target(@liquid_staking, b"storage", b"change_validator_priority"); + target(@liquid_staking, b"storage", b"join_to_sui_pool"); + target(@liquid_staking, b"storage", b"join_stake"); + target(@liquid_staking, b"storage", b"join_fungible_stake"); + target(@liquid_staking, b"storage", b"join_inactive_stake_to_validator"); + target(@liquid_staking, b"storage", b"join_fungible_staked_sui_to_validator"); + target(@liquid_staking, b"storage", b"split_up_to_n_sui_from_sui_pool"); + target(@liquid_staking, b"storage", b"split_from_sui_pool"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_validator"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_active_stake"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_inactive_stake"); + target(@liquid_staking, b"storage", b"split_n_sui"); + target(@liquid_staking, b"storage", b"get_or_add_validator_index_by_staking_pool_id_mut"); + + invoker(b"invoke"); + + rule(b"total_sui_supply_correct_base"); + rule(b"total_sui_supply_correct_step"); +} + +native fun invoke( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + +/// Computes the SUI value of active stake for a specific validator, accounting for exchange rate. +fun staked_active(strg: &Storage, i: u64): u64 { + let validator_info = &strg.validators()[i]; + if (validator_info.active_stake().is_some()) { + let active_stake = validator_info.active_stake().borrow(); + get_sui_amount( + validator_info.exchange_rate(), + active_stake.value(), + ) + } else { + 0 + } +} + +/// Computes the SUI value of inactive stake for a specific validator. +fun staked_inactive(strg: &Storage, i: u64): u64 { + let validator_info = &strg.validators()[i]; + if (validator_info.inactive_stake().is_some()) { + let inactive_stake = validator_info.inactive_stake().borrow(); + inactive_stake.staked_sui_amount() + } else { + 0 + } +} + +/// Computes the total SUI value (active + inactive) for a specific validator. +fun validator_sui_supply(strg: &Storage, i: u64): u64 { + let active_stake = staked_active(strg, i); + let inactive_stake = staked_inactive(strg, i); + + active_stake + inactive_stake +} + +/// Computes the actual total SUI supply by summing the liquid pool and all validator stakes. +/// This is the ground truth used to verify the stored total_sui_supply value. +fun current_supply(strg: &Storage): u64 { + let mut i = 0; + let mut v = strg.sui_pool().value(); + + while (i < strg.validators().length()) { + v = v + validator_sui_supply(strg, i); + i = i+1; + }; + v +} + +/// Checks whether the stored total SUI supply matches the computed actual supply across all locations. +public fun total_supply_correct(strg: &Storage): bool { + let expected = current_supply(strg); + let actual = strg.total_sui_supply(); + expected == actual +} + +/// Base case: Verifies that newly created storage has correct total SUI supply accounting, +/// establishing the initial state for the invariant. +public fun total_sui_supply_correct_base(ctx: &mut TxContext) { + let strg = storage::new(ctx); + cvlm_assert(total_supply_correct(&strg)); + ghost_destroy(strg); +} + +/// Inductive step: Verifies that all storage operations preserve the invariant that the stored +/// total SUI supply matches the actual sum across all locations. Ensures accounting accuracy is maintained. +/// +/// Note: This invariant only holds across epoch boundaries after refresh, as accounting can +/// temporarily drift within an epoch. The drift occurs because refresh_validator_info sets +/// total_sui_amount via get_sui_amount(...) which floors division, while unstaking paths (calling +/// redeem_and_update_accounting) debit total_sui_supply by the actual redeemed SUI from +/// redeem_fungible_staked_sui. Since flooring is not additive, partial unstakes can leave dust, +/// causing the stored total_sui_supply to be higher than the recomputed actual supply until refresh() +/// recomputes and reconciles it at the next epoch boundary. +public fun total_sui_supply_correct_step( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg(strg.validators().length() <= 1, b"Only one validator"); + + cvlm_assume_msg(ctx.epoch() > strg.last_refresh_epoch(), b"Assume fresh state"); + strg.refresh(system_state, ctx); + + cvlm_assume_msg(total_supply_correct(strg), b"Assume invariant holds in pre state"); + + invoke(target, strg, system_state, ctx); + + // Force refresh at next epoch boundary to verify invariant holds + let mut ctx2: TxContext = nondet(); + cvlm_assume_msg(ctx2.epoch() > strg.last_refresh_epoch(), b"Advance epoch so refresh can run"); + strg.refresh(system_state, &mut ctx2); + + + cvlm_assert(total_supply_correct(strg)); +} diff --git a/certora/spec/sources/accounting_value_conservation.move b/certora/spec/sources/accounting_value_conservation.move new file mode 100644 index 0000000..8230958 --- /dev/null +++ b/certora/spec/sources/accounting_value_conservation.move @@ -0,0 +1,148 @@ +/// Property: Value Conservation +/// Description: Ensures that the liquid staking protocol conserves value across all operations. +/// For operations that do not involve deposits or redemptions, the total SUI and LST supplies must +/// be non-decreasing. For mint operations, the deposited SUI value must equal the sum of the LST backing +/// increase and protocol fees collected. For redeem operations, the burned LST value must equal the sum +/// of SUI returned to users and protocol fees. This comprehensive value conservation prevents any loss +/// or creation of value through protocol operations. + +module spec::accounting_value_conservation; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::{target, invoker, rule}; +use cvlm::nondet::nondet; +use liquid_staking::liquid_staking::LiquidStakingInfo; +use spec::accounting_total_sui_supply::total_supply_correct; +use spec::common::{setup_fresh, log, can_decrease_supply}; +use spec::dummy::DummyToken; +use sui::coin::Coin; +use sui::sui::SUI; +use sui_system::sui_system::SuiSystemState; + +public fun cvlm_manifest() { + // Public mut functions + target(@spec, b"dummy", b"mint"); + target(@spec, b"dummy", b"redeem"); + target(@spec, b"dummy", b"custom_redeem_request"); + target(@spec, b"dummy", b"custom_redeem"); + target(@spec, b"dummy", b"change_validator_priority"); + target(@spec, b"dummy", b"increase_validator_stake"); + target(@spec, b"dummy", b"decrease_validator_stake"); + target(@spec, b"dummy", b"collect_fees"); + target(@spec, b"dummy", b"update_fees"); + target(@spec, b"dummy", b"refresh"); + target(@spec, b"dummy", b"update_metadata"); + + invoker(b"invoke"); + + rule(b"sui_value_conservation"); + rule(b"lst_value_conservation"); + + rule(b"deposit_value_conservation"); + rule(b"redeem_value_conservation"); +} + +native fun invoke( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + +/// Verifies that for operations that cannot decrease SUI supply (non-redemption operations), +/// the total SUI backing remains non-decreasing. This prevents unauthorized SUI withdrawals. +public fun sui_value_conservation( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + let sui_pre = lsi.total_sui_supply(); + + cvlm_assume_msg(!can_decrease_supply(target), b"Cannot decrease sui supply"); + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Sound state"); + invoke(target, lsi, system_state, ctx); + + let sui_post = lsi.total_sui_supply(); + + cvlm_assert(sui_post >= sui_pre); +} + +/// Verifies that for operations that cannot decrease LST supply (non-redemption operations), +/// the total LST supply remains non-decreasing. This prevents unauthorized token burns. +public fun lst_value_conservation( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + let lst_pre = lsi.total_lst_supply(); + cvlm_assume_msg(!can_decrease_supply(target), b"Cannot decrease sui supply"); + invoke(target, lsi, system_state, ctx); + + let lst_post = lsi.total_lst_supply(); + + cvlm_assert(lst_post >= lst_pre); +} + +/// Verifies that during mint operations, the deposited SUI value is fully accounted for as either +/// an increase in the SUI backing or as protocol fees. This ensures no value is lost during deposits. +public fun deposit_value_conservation( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Sound state"); + + let sui: Coin = nondet(); + let sui_value = sui.value(); + let fees_pre = lsi.fees(); + let sui_pre = lsi.total_sui_supply(); + let lst = lsi.mint(system_state, sui, ctx); + + cvlm_assert(lsi.total_sui_supply() >= sui_pre); + cvlm_assert(lsi.fees() >= fees_pre); + let sui_increase = lsi.total_sui_supply() - sui_pre; + let fee_increase = lsi.fees() - fees_pre; + + cvlm_assert(sui_increase + fee_increase == sui_value); + + ghost_destroy(lst); +} + +/// Verifies that during redemption operations, the decrease in SUI backing equals the sum of +/// SUI returned to the user and protocol fees collected. This ensures no value is lost during redemptions. +public fun redeem_value_conservation( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Sound state"); + + let lst: Coin = nondet(); + + let fees_pre = lsi.fees(); + let sui_pre = lsi.total_sui_supply(); + + let sui = lsi.redeem(lst, system_state, ctx); + + cvlm_assert(lsi.total_sui_supply() <= sui_pre); + cvlm_assert(lsi.fees() >= fees_pre); + + let sui_decrease = sui_pre - lsi.total_sui_supply(); + let fee_increase = lsi.fees() - fees_pre; + + log(&fee_increase); + log(&sui.value()); + log(&(fee_increase + sui.value())); + log(&sui_decrease); + cvlm_assert(fee_increase + sui.value() == sui_decrease); + + ghost_destroy(sui); +} diff --git a/certora/spec/sources/common.move b/certora/spec/sources/common.move new file mode 100644 index 0000000..eba76b2 --- /dev/null +++ b/certora/spec/sources/common.move @@ -0,0 +1,95 @@ +module spec::common; + +use cvlm::asserts::cvlm_assume_msg; +use cvlm::function::Function; +use liquid_staking::liquid_staking::LiquidStakingInfo; +use spec::summaries::{active_validators}; +use sui_system::sui_system::SuiSystemState; +use liquid_staking::storage::inactive_stake; +use liquid_staking::storage::get_sui_amount; + +public fun setup( + lsi: &mut LiquidStakingInfo, +) { + let mut i = 0; + while (i < lsi.storage().validators().length()) { + let validator = &lsi.storage().validators()[i]; + let pool_id = validator.staking_pool_id(); + let active = validator.active_stake(); + let inactive = lsi.storage().validators()[i].inactive_stake(); + if (active.is_some()) { + cvlm_assume_msg(active.borrow().pool_id() == pool_id, b"Matching pool ids"); + }; + if (inactive.is_some()) { + cvlm_assume_msg(inactive.borrow().pool_id() == pool_id, b"Matching pool ids"); + }; + + i = i+1; + }; +} + + +public fun setup_fresh( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + let mut total_sui_supply = 0; + + let validator_addresses = active_validators(); + + let mut i = 0; + while (i < lsi.storage().validators().length()) { + let validator = &lsi.storage().validators()[i]; + let pool_id = validator.staking_pool_id(); + let active = validator.active_stake(); + let inactive = lsi.storage().validators()[i].inactive_stake(); + + // There is no inactive state after a call to refresh + // This is verified in the rule "no_inactive_stake_after_refresh" + cvlm_assume_msg(inactive.is_none(), b"No inactive stake"); + + // There are no empty validators after a call to refresh. + // This is verified in the rule "no_empty_validators_after_refresh" + // Since there is no inactive stake for this validator, not empty is equivalent to non-zero active stake. + // This is verified in the invariant "no_stake_no_sui" + cvlm_assume_msg(active.is_some(), b"No empty validator"); + let active = active.borrow(); + cvlm_assume_msg(active.pool_id() == pool_id, b"Matching pool ids"); + + + cvlm_assume_msg( + validator_addresses.contains(&validator.validator_address()), + b"Validator is active", + ); + + + // We assume an exchange rate for this epoch exists + let er = lsi + .storage() + .get_latest_exchange_rate(&validator.staking_pool_id(), system_state, ctx) + .destroy_some(); + cvlm_assume_msg(validator.exchange_rate() == er, b"Validator has latest exchange rate"); + + let active_sui_amount = get_sui_amount(&er, active.value()); + cvlm_assume_msg(validator.total_sui_amount() == active_sui_amount, b"Valid amount"); + + total_sui_supply = total_sui_supply + active_sui_amount; + + i = i+1; + }; + + cvlm_assume_msg(lsi.storage().total_sui_supply() == total_sui_supply, b"Correct total sui supply"); + cvlm_assume_msg(lsi.storage().last_refresh_epoch() == ctx.epoch(), b"Set last refresh"); +} + + +public fun log(_: &T) {} + +public fun can_decrease_supply(f: Function): bool { + f.name() == b"redeem" || f.name() == b"custom_redeem" +} + +public fun can_increase_supply(f: Function): bool { + f.name() == b"mint" +} diff --git a/certora/spec/sources/dummy.move b/certora/spec/sources/dummy.move new file mode 100644 index 0000000..dacff3a --- /dev/null +++ b/certora/spec/sources/dummy.move @@ -0,0 +1,143 @@ +module spec::dummy; + + +use liquid_staking::fees::FeeConfig; +use liquid_staking::liquid_staking::{LiquidStakingInfo, AdminCap, CustomRedeemRequest}; +use std::ascii; +use std::string::String; +use sui::coin::{Coin, CoinMetadata}; +use sui::sui::SUI; +use sui_system::sui_system::SuiSystemState; + +public struct DummyToken has drop {} + +public fun mint( + self: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + sui: Coin, + ctx: &mut TxContext, +): Coin { + liquid_staking::liquid_staking::mint(self, system_state, sui, ctx) +} + +public fun redeem( + self: &mut LiquidStakingInfo, + lst: Coin, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +): Coin { + liquid_staking::liquid_staking::redeem(self, lst, system_state, ctx) +} + +public fun custom_redeem_request( + self: &mut LiquidStakingInfo, + lst: Coin, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +): CustomRedeemRequest { + liquid_staking::liquid_staking::custom_redeem_request(self, lst, system_state, ctx) +} + +public fun custom_redeem( + self: &mut LiquidStakingInfo, + request: CustomRedeemRequest, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +): Coin { + liquid_staking::liquid_staking::custom_redeem(self, request, system_state, ctx) +} + +public fun change_validator_priority( + self: &mut LiquidStakingInfo, + cap: &AdminCap, + validator_index: u64, + new_validator_index: u64, +) { + liquid_staking::liquid_staking::change_validator_priority( + self, + cap, + validator_index, + new_validator_index, + ) +} + +public fun increase_validator_stake( + self: &mut LiquidStakingInfo, + cap: &AdminCap, + system_state: &mut SuiSystemState, + validator_address: address, + sui_amount: u64, + ctx: &mut TxContext, +): u64 { + liquid_staking::liquid_staking::increase_validator_stake( + self, + cap, + system_state, + validator_address, + sui_amount, + ctx, + ) +} + +public fun decrease_validator_stake( + self: &mut LiquidStakingInfo, + cap: &AdminCap, + system_state: &mut SuiSystemState, + validator_address: address, + target_unstake_sui_amount: u64, + ctx: &mut TxContext, +): u64 { + liquid_staking::liquid_staking::decrease_validator_stake( + self, + cap, + system_state, + validator_address, + target_unstake_sui_amount, + ctx, + ) +} + +public fun collect_fees( + self: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + _admin_cap: &AdminCap, + ctx: &mut TxContext, +): Coin { + liquid_staking::liquid_staking::collect_fees(self, system_state, _admin_cap, ctx) +} + +public fun update_fees( + self: &mut LiquidStakingInfo, + _admin_cap: &AdminCap, + fee_config: FeeConfig, +) { + liquid_staking::liquid_staking::update_fees(self, _admin_cap, fee_config) +} + +public fun refresh( + self: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +): bool { + liquid_staking::liquid_staking::refresh(self, system_state, ctx) +} + +public fun update_metadata( + self: &mut LiquidStakingInfo, + cap: &AdminCap, + metadata: &mut CoinMetadata, + name: Option, + symbol: Option, + description: Option, + icon_url: Option, +) { + liquid_staking::liquid_staking::update_metadata( + self, + cap, + metadata, + name, + symbol, + description, + icon_url, + ) +} diff --git a/certora/spec/sources/fees.move b/certora/spec/sources/fees.move new file mode 100644 index 0000000..41cd53d --- /dev/null +++ b/certora/spec/sources/fees.move @@ -0,0 +1,165 @@ +/// Property: Fee Accounting Integrity +/// Description: Verifies that the protocol's fee accounting maintains critical invariants across all +/// operations. Accrued spread fees must never exceed the total SUI supply (preventing over-collection), +/// fees must grow monotonically except during collection operations (ensuring they are not lost), and +/// fees must never completely consume user deposits or redemptions (guaranteeing users always receive value). +/// These properties ensure the fee mechanism operates correctly without compromising user funds or +/// protocol accounting. + +module spec::fees; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::{rule, target, invoker}; +use cvlm::nondet::nondet; +use liquid_staking::fees::validate_fees; +use liquid_staking::liquid_staking::LiquidStakingInfo; +use spec::common::setup_fresh; +use spec::dummy::DummyToken; +use sui::coin::Coin; +use sui::sui::SUI; +use sui_system::sui_system::SuiSystemState; +use liquid_staking::liquid_staking::create_lst; + +public fun cvlm_manifest() { + target(@spec, b"dummy", b"mint"); + target(@spec, b"dummy", b"redeem"); + target(@spec, b"dummy", b"custom_redeem_request"); + target(@spec, b"dummy", b"custom_redeem"); + target(@spec, b"dummy", b"change_validator_priority"); + target(@spec, b"dummy", b"increase_validator_stake"); + target(@spec, b"dummy", b"decrease_validator_stake"); + target(@spec, b"dummy", b"collect_fees"); + target(@spec, b"dummy", b"update_fees"); + target(@spec, b"dummy", b"refresh"); + target(@spec, b"dummy", b"update_metadata"); + + invoker(b"invoke"); + + rule(b"spread_fees_dont_exceed_sui_supply_base"); + rule(b"spread_fees_dont_exceed_sui_supply_step"); + + rule(b"fees_grow_monotonically"); + + rule(b"fees_dont_eat_deposit"); + rule(b"fees_dont_eat_redemption"); +} + +native fun invoke( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + +/// Base case: Verifies that for newly created pools, accrued spread fees do not exceed the total SUI supply. +/// This establishes the initial state for the fee accounting invariant. +public fun spread_fees_dont_exceed_sui_supply_base( + ctx: &mut TxContext, +) { + let fee_config = nondet(); + let lst_treasury_cap = nondet(); + let (_cap, lsi) = create_lst(fee_config, lst_treasury_cap, ctx); + let spread_fees = lsi.fees(); + let sui = lsi.storage().total_sui_supply(); + cvlm_assert(spread_fees <= sui); + + ghost_destroy(_cap); + ghost_destroy(lsi); + +} + +/// Inductive step: Verifies that all operations preserve the invariant that accrued spread fees +/// do not exceed the total SUI supply. This prevents the protocol from claiming fees it cannot honor. +public fun spread_fees_dont_exceed_sui_supply_step( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + // This already assumes spread_fees < storage.sui_supply, we'll make it explicit nevertheless + setup_fresh(lsi, system_state, ctx); + validate_fees(lsi.fee_config()); + let spread_fees_pre = lsi.accrued_spread_fees(); + let sui_pre = lsi.storage().total_sui_supply(); + + cvlm_assume_msg(spread_fees_pre <= sui_pre, b"Assume in precondition"); + + invoke(target, lsi, system_state, ctx); + + let spread_fees_post = lsi.accrued_spread_fees(); + let sui_post = lsi.storage().total_sui_supply(); + + cvlm_assert(spread_fees_post <= sui_post); +} + +/// Verifies that accrued fees either remain constant or increase across all operations, except +/// during explicit fee collection. This ensures fees are not lost or incorrectly reduced during operations. +public fun fees_grow_monotonically( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + validate_fees(lsi.fee_config()); + let spread_fees_pre = lsi.fees(); + + invoke(target, lsi, system_state, ctx); + + let spread_fees_post = lsi.fees(); + + let collected = target.name() == b"collect_fees"; + let increased = spread_fees_post >= spread_fees_pre; + + // !collected -> increased <==> collected || increased + cvlm_assert(collected || increased); +} + +/// Verifies that redemption fees do not completely consume the user's redemption, ensuring users +/// always receive a non-zero amount of SUI when redeeming non-zero LST tokens. +public fun fees_dont_eat_redemption( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + validate_fees(lsi.fee_config()); + + let coin: Coin = nondet(); + + let fees_pre = lsi.fees(); + + cvlm_assume_msg(coin.value() > 0, b"Non-zero value"); + let sui = lsi.redeem(coin, system_state, ctx); + + let fees = lsi.fees() - fees_pre; + + cvlm_assume_msg(sui.value() + fees > 0, b"No lost funds"); + cvlm_assert(sui.value() > 0); + ghost_destroy(sui); +} + +/// Verifies that deposit fees do not completely consume the user's deposit, ensuring users +/// always receive a non-zero amount of LST tokens when depositing non-zero SUI. +public fun fees_dont_eat_deposit( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + validate_fees(lsi.fee_config()); + + let coin: Coin = nondet(); + + let fees_pre = lsi.fees(); + + cvlm_assume_msg(coin.value() > 0, b"Non-zero value"); + let lst = lsi.mint(system_state, coin, ctx); + let fees = lsi.fees() - fees_pre; + + cvlm_assume_msg(lst.value()+fees > 0, b"No lost funds"); + cvlm_assert(lst.value() > 0); + ghost_destroy(lst); +} diff --git a/certora/spec/sources/liquid_staking_sanity.move b/certora/spec/sources/liquid_staking_sanity.move new file mode 100644 index 0000000..ab48c17 --- /dev/null +++ b/certora/spec/sources/liquid_staking_sanity.move @@ -0,0 +1,27 @@ +/// Property: Sanity Checks +/// Description: Performs basic sanity verification on all liquid staking protocol functions to ensure +/// they can execute without reverting under valid preconditions. This serves as a smoke test to catch +/// fundamental implementation errors such as incorrect assertions, type mismatches, or logic errors that +/// would cause functions to always fail. Passing these checks confirms that the protocol's core operations +/// are at least executable under normal conditions. + +module spec::liquid_staking_sanity; + +use cvlm::manifest::{ target, target_sanity }; + +public fun cvlm_manifest() { + target(@liquid_staking, b"liquid_staking", b"create_lst"); + target(@liquid_staking, b"liquid_staking", b"create_lst_with_stake"); + target(@liquid_staking, b"liquid_staking", b"mint"); + target(@liquid_staking, b"liquid_staking", b"redeem"); + target(@liquid_staking, b"liquid_staking", b"custom_redeem_request"); + target(@liquid_staking, b"liquid_staking", b"custom_redeem"); + target(@liquid_staking, b"liquid_staking", b"change_validator_priority"); + target(@liquid_staking, b"liquid_staking", b"increase_validator_stake"); + target(@liquid_staking, b"liquid_staking", b"decrease_validator_stake"); + target(@liquid_staking, b"liquid_staking", b"collect_fees"); + target(@liquid_staking, b"liquid_staking", b"update_fees"); + target(@liquid_staking, b"liquid_staking", b"refresh"); + target(@liquid_staking, b"liquid_staking", b"update_metadata"); + target_sanity(); +} \ No newline at end of file diff --git a/certora/spec/sources/no_arbitrage.move b/certora/spec/sources/no_arbitrage.move new file mode 100644 index 0000000..b2c7352 --- /dev/null +++ b/certora/spec/sources/no_arbitrage.move @@ -0,0 +1,51 @@ +/// Property: Mint and Redemption Integrity +/// Description: Ensures the core deposit and withdrawal operations maintain fundamental integrity properties. +/// Users depositing non-zero amounts must receive non-zero value in return (either LST tokens or SUI plus fees), +/// preventing complete value loss. Additionally, this property verifies that there are no arbitrage opportunities +/// where a user could mint LST and immediately redeem it for more SUI than initially deposited. These guarantees +/// ensure fair pricing and protect users from loss of funds during the fundamental protocol operations. + +module spec::no_arbitrage; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::rule; +use cvlm::nondet::nondet; +use liquid_staking::fees::validate_fees; +use liquid_staking::liquid_staking::{LiquidStakingInfo}; +use spec::dummy::DummyToken; +use sui_system::sui_system::SuiSystemState; +use spec::common::setup_fresh; +use sui::coin::Coin; + +use sui::sui::SUI; + + +public fun cvlm_manifest() { + rule(b"no_arbitrage_opportunity"); +} + + +/// Verifies that no arbitrage opportunity exists where a user could deposit SUI, immediately redeem +/// the received LST tokens, and receive more SUI than initially deposited. This ensures fair pricing. +public fun no_arbitrage_opportunity( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + validate_fees(lsi.fee_config()); + + // The rule fails if we have 0 LST but non-zero SUI supply + // This state, however, is not reachable (check rule `no_lst_no_sui` in `solvency.move`) + cvlm_assume_msg(lsi.total_lst_supply() != 0 || lsi.total_sui_supply() == 0, b"No LST means no SUI supply"); + + let sui_in: Coin = nondet(); + let sui_in_value = sui_in.value(); + + let lst = lsi.mint(system_state, sui_in, ctx); + let sui_out = lsi.redeem(lst, system_state, ctx); + + cvlm_assert(sui_out.value() <= sui_in_value); + ghost_destroy(sui_out); +} diff --git a/certora/spec/sources/solvency.move b/certora/spec/sources/solvency.move new file mode 100644 index 0000000..7b8a87b --- /dev/null +++ b/certora/spec/sources/solvency.move @@ -0,0 +1,190 @@ +/// Property: Protocol Solvency and Exchange Rate Monotonicity +/// Description: Verifies that the liquid staking protocol maintains solvency throughout its lifecycle, +/// ensuring that the SUI backing always meets or exceeds the LST supply (maintaining an exchange rate >= 1). +/// Additionally, this property verifies that the SUI/LST exchange rate is non-decreasing across operations, +/// protecting users from value dilution. Solvency is established at initialization and preserved through +/// induction across all state-modifying operations. The monotonic exchange rate ensures that LST tokens +/// never lose purchasing power relative to SUI over time. + +module spec::solvency; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::{target, invoker, rule}; +use cvlm::nondet::nondet; +use liquid_staking::fees::validate_fees; +use liquid_staking::liquid_staking::{Self, LiquidStakingInfo}; +use spec::dummy::DummyToken; +use sui_system::sui_system::SuiSystemState; +use spec::common::setup_fresh; +use spec::accounting_total_sui_supply::total_supply_correct; + +public fun cvlm_manifest() { + // Public mut functions + + target(@spec, b"dummy", b"mint"); + target(@spec, b"dummy", b"redeem"); + target(@spec, b"dummy", b"custom_redeem_request"); + target(@spec, b"dummy", b"custom_redeem"); + target(@spec, b"dummy", b"change_validator_priority"); + target(@spec, b"dummy", b"increase_validator_stake"); + target(@spec, b"dummy", b"decrease_validator_stake"); + target(@spec, b"dummy", b"collect_fees"); + target(@spec, b"dummy", b"update_fees"); + target(@spec, b"dummy", b"refresh"); + target(@spec, b"dummy", b"update_metadata"); + + invoker(b"invoke"); + + rule(b"solvency_base"); + rule(b"solvency_base_staker"); + rule(b"solvency_step"); + + // This rule verifies an upper bound of 1 for insolvency per operation + // rule(b"insolvency_bound"); + + rule(b"monotonicity"); +} + +const MAX_VALIDATORS: u64 = 1; + +native fun invoke( + target: Function, + lis: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + + + +/// Checks whether the protocol is solvent by verifying that the total SUI backing is at least +/// equal to the total LST supply. This ensures the exchange rate (SUI/LST) is at least 1:1. +/// lsi.total_sui_supply()/lsi.total_lst_supply() >= 1 +/// <==> lsi.total_sui_supply() >= lsi.total_lst_supply() +public fun is_solvent(lsi: &LiquidStakingInfo): bool { + let sui_supply = lsi.total_sui_supply(); + let lst_supply = lsi.total_lst_supply(); + + sui_supply >= lst_supply +} + +/// Base case: Verifies that newly created empty liquid staking pools are solvent. +/// This establishes the initial solvency invariant at pool creation. +public fun solvency_base() { + let fee_config = nondet(); + let lst_treasury_cap = nondet(); + let mut ctx = nondet(); + let (cap, lsi) = liquid_staking::create_lst

(fee_config, lst_treasury_cap, &mut ctx); + + cvlm_assert(is_solvent(&lsi)); + + ghost_destroy(cap); + ghost_destroy(lsi); +} + +/// Base case: Verifies that newly created liquid staking pools initialized with existing stake are solvent. +/// This establishes the initial solvency invariant for pools created with pre-existing staked SUI. +public fun solvency_base_staker() { + let fee_config = nondet(); + let mut system_state = nondet(); + let lst_treasury_cap = nondet(); + let mut ctx = nondet(); + let fungible_staked_suis = nondet(); + let sui = nondet(); + let (cap, lsi) = liquid_staking::create_lst_with_stake

( + &mut system_state, + fee_config, + lst_treasury_cap, + fungible_staked_suis, + sui, + &mut ctx, + ); + + cvlm_assert(is_solvent(&lsi)); + + ghost_destroy(cap); + ghost_destroy(lsi); + ghost_destroy(system_state); +} + + +/// Inductive step: Verifies that all state-modifying operations preserve protocol solvency. +/// Assumes the protocol is solvent in the pre-state and proves it remains solvent after the operation. +public fun solvency_step( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg( + lsi.storage().validators().length() <= MAX_VALIDATORS, + b"Restrict number of validators", + ); + setup_fresh(lsi, system_state, ctx); + + cvlm_assume_msg(is_solvent(lsi), b"Assume solvency in pre state"); + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Correct accounting"); + + validate_fees(lsi.fee_config()); + + invoke(target, lsi, system_state, ctx); + + cvlm_assert(is_solvent(lsi)); +} + +public fun insolvency_bound( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg( + lsi.storage().validators().length() <= MAX_VALIDATORS, + b"Restrict number of validators", + ); + setup_fresh(lsi, system_state, ctx); + + cvlm_assume_msg(is_solvent(lsi), b"Assume solvency in pre state"); + + validate_fees(lsi.fee_config()); + + invoke(target, lsi, system_state, ctx); + + cvlm_assert(lsi.total_lst_supply() +1 >= lsi.total_lst_supply()); +} + + +/// Verifies that the SUI/LST exchange rate is non-decreasing across all operations. +/// This ensures LST holders never experience value dilution, as each LST token can always be +/// redeemed for at least as much SUI as it could previously. +public fun monotonicity( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg( + lsi.storage().validators().length() <= MAX_VALIDATORS, + b"Restrict number of validators", + ); + setup_fresh(lsi, system_state, ctx); + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Correct accounting"); + + //cvlm_assume_msg(is_solvent(lsi), b"Assume solvency in pre state"); + + let lst_pre = lsi.total_lst_supply(); + let sui_pre = lsi.total_sui_supply(); + + cvlm_assume_msg(lst_pre > 0 && sui_pre > 0, b"Non-empty reserve"); + + invoke(target, lsi, system_state, ctx); + + let lst_post = lsi.total_lst_supply(); + let sui_post = lsi.total_sui_supply(); + + // sui_pre/lst_pre <= sui_post/lst_post + // <==> sui_pre*lst_post <= sui_post*lst_pre + + cvlm_assert(sui_pre*lst_post <= sui_post*lst_pre); +} diff --git a/certora/spec/sources/summaries.move b/certora/spec/sources/summaries.move new file mode 100644 index 0000000..6065ea1 --- /dev/null +++ b/certora/spec/sources/summaries.move @@ -0,0 +1,265 @@ +module spec::summaries; + +use cvlm::asserts::{cvlm_assume_msg, cvlm_assert}; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::{summary, ghost}; +use cvlm::nondet::nondet; +use liquid_staking::storage::{Self, Storage}; +use liquid_staking::version::Version; +use std::option::some; +use sui::balance::Balance; +use sui::object::id; +use sui::sui::SUI; +use sui::tx_context::epoch; +use sui_system::staking_pool::{PoolTokenExchangeRate, StakedSui, StakingPool, FungibleStakedSui}; +use sui_system::sui_system::SuiSystemState; + +public fun cvlm_manifest() { + ghost(b"exchange_rate"); + summary(b"get_latest_exchange_rate", @liquid_staking, b"storage", b"get_latest_exchange_rate"); + ghost(b"validator_index"); + summary( + b"find_validator_index_by_address", + @liquid_staking, + b"storage", + b"find_validator_index_by_address", + ); + + summary( + b"pool_token_exchange_rate_at_epoch", + @sui_system, + b"staking_pool", + b"pool_token_exchange_rate_at_epoch", + ); + + ghost(b"fungible_total_supply"); + ghost(b"fungible_total_principal"); + + summary( + b"convert_to_fungible_staked_sui", + @sui_system, + b"sui_system", + b"convert_to_fungible_staked_sui", + ); + summary( + b"redeem_fungible_staked_sui", + @sui_system, + b"sui_system", + b"redeem_fungible_staked_sui", + ); + ghost(b"active_validators"); + summary( + b"active_validator_addresses", + @sui_system, + b"sui_system", + b"active_validator_addresses", + ); + summary( + b"request_withdraw_stake_non_entry", + @sui_system, + b"sui_system", + b"request_withdraw_stake_non_entry", + ); + + summary( + b"assert_version_and_upgrade", + @liquid_staking, + b"version", + b"assert_version_and_upgrade", + ); +} + +native fun validator_index(validator_address: address): u64; +public(package) fun find_validator_index_by_address( + self: &Storage, + validator_address: address, +): u64 { + let i = validator_index(validator_address); + cvlm_assume_msg(i < self.validators().length(), b"Validator exists"); + cvlm_assume_msg( + self.validators()[i].validator_address() == validator_address, + b"Address is consistent", + ); + return i +} + +native fun exchange_rate(epoch: u64, staking_pool_id: &ID): PoolTokenExchangeRate; + +fun get_exr(epoch: u64, staking_pool_id: &ID): PoolTokenExchangeRate { + let er: PoolTokenExchangeRate = exchange_rate(epoch, staking_pool_id); + cvlm_assume_msg(er.sui_amount() >= er.pool_token_amount(), b"solvent"); + er +} + +native fun fungible_total_supply(pool: ID): &mut u64; +native fun fungible_total_principal(pool: ID): &mut u64; + +public fun convert_to_fungible_staked_sui( + _: &mut SuiSystemState, + staked_sui: StakedSui, + ctx: &mut TxContext, +): FungibleStakedSui { + let id = staked_sui.pool_id(); + let epoch = ctx.epoch(); + + let principal = staked_sui.staked_sui_amount(); + + let fss: FungibleStakedSui = nondet(); + + let er = get_exr(epoch, &id); + let pool_token_amount = get_token_amount(&er, principal); + + cvlm_assume_msg(fss.pool_id() == id, b"Correct id"); + cvlm_assume_msg(fss.value() == pool_token_amount, b"Correct value"); + + // Update fungible token data + let f_total = fungible_total_supply(id); + let f_principal = fungible_total_supply(id); + *f_total = *f_total + pool_token_amount; + *f_principal = *f_principal + principal; + + ghost_destroy(staked_sui); + + fss +} + +public fun redeem_fungible_staked_sui( + _wrapper: &mut SuiSystemState, + fungible_staked_sui: FungibleStakedSui, + ctx: &TxContext, +): Balance { + let id = fungible_staked_sui.pool_id(); + let epoch = ctx.epoch(); + let value = fungible_staked_sui.value(); + + let principal = *fungible_total_principal(id); + cvlm_assume_msg(principal >= value, b""); + + let total_supply = *fungible_total_supply(id); + cvlm_assume_msg(total_supply >= principal, b""); + + let er = get_exr(epoch, &id); + + // let ( + // principal_amount, + // rewards_amount, + // ) = calculate_fungible_staked_sui_withdraw_amount( + // er, + // value, + // principal, + // total_supply, + // ); + //let total_withdraw = principal_amount+rewards_amount; + + let total_withdraw = get_sui_amount(er, value); + + //fungible_staked_sui_data.total_supply = fungible_staked_sui_data.total_supply - value; + + let sui_out: Balance = nondet(); + cvlm_assume_msg(sui_out.value() == total_withdraw, b""); + // = fungible_staked_sui_data.principal.split(principal_amount); + // sui_out.join(pool.rewards_pool.split(rewards_amount)); + + // pool.pending_total_sui_withdraw = pool.pending_total_sui_withdraw + sui_out.value(); + // pool.pending_pool_token_withdraw = pool.pending_pool_token_withdraw + value; + ghost_destroy(fungible_staked_sui); + sui_out +} + +public(package) fun calculate_fungible_staked_sui_withdraw_amount( + latest_exchange_rate: PoolTokenExchangeRate, + fungible_staked_sui_value: u64, + fungible_staked_sui_data_principal_amount: u64, // fungible_staked_sui_data.principal.value() + fungible_staked_sui_data_total_supply: u64, // fungible_staked_sui_data.total_supply +): (u64, u64) { + // 1. if the entire FungibleStakedSuiData supply is redeemed, how much sui should we receive? + let total_sui_amount = get_sui_amount( + latest_exchange_rate, + fungible_staked_sui_data_total_supply, + ); // == fungible_staked_sui_data_principal_amount + rewards + + // min with total_sui_amount to prevent underflow + // let fungible_staked_sui_data_principal_amount = fungible_staked_sui_data_principal_amount.min( + // total_sui_amount, + // ); + + cvlm_assume_msg( + fungible_staked_sui_data_principal_amount <= total_sui_amount, + b"Principal amount is less than total sui amount", + ); + + // 2. how much do we need to withdraw from the rewards pool? + let total_rewards = total_sui_amount - fungible_staked_sui_data_principal_amount; + + // 3. proportionally withdraw from both wrt the fungible_staked_sui_value. + let principal_withdraw_amount = + (fungible_staked_sui_value*fungible_staked_sui_data_principal_amount)/fungible_staked_sui_data_total_supply; + + let rewards_withdraw_amount = + (fungible_staked_sui_value*total_rewards)/fungible_staked_sui_data_total_supply; + + // invariant check, just in case + let expected_sui_amount = get_sui_amount(latest_exchange_rate, fungible_staked_sui_value); + cvlm_assert( + principal_withdraw_amount + rewards_withdraw_amount <= expected_sui_amount, + ); + + (principal_withdraw_amount, rewards_withdraw_amount) +} + +fun get_token_amount(exchange_rate: &PoolTokenExchangeRate, sui_amount: u64): u64 { + // When either amount is 0, that means we have no stakes with this pool. + // The other amount might be non-zero when there's dust left in the pool. + if (exchange_rate.sui_amount() == 0 || exchange_rate.pool_token_amount() == 0) { + return sui_amount + }; + + (exchange_rate.pool_token_amount()* sui_amount) / exchange_rate.sui_amount() +} + +fun get_sui_amount(exchange_rate: PoolTokenExchangeRate, token_amount: u64): u64 { + // When either amount is 0, that means we have no stakes with this pool. + // The other amount might be non-zero when there's dust left in the pool. + if (exchange_rate.sui_amount() == 0 || exchange_rate.pool_token_amount() == 0) { + return token_amount + }; + + (exchange_rate.sui_amount()* token_amount) / exchange_rate.pool_token_amount() +} + +public(package) fun get_latest_exchange_rate( + _self: &Storage, + staking_pool_id: &ID, + _system_state: &mut SuiSystemState, + ctx: &TxContext, +): Option { some(get_exr(ctx.epoch(), staking_pool_id)) } + +public fun pool_token_exchange_rate_at_epoch( + pool: &StakingPool, + epoch: u64, +): PoolTokenExchangeRate { + let id = id(pool); + some(get_exr(epoch, &id)).destroy_some() +} + +public native fun active_validators(): vector

; + +public fun active_validator_addresses(_wrapper: &mut SuiSystemState): vector
{ + active_validators() +} + +public fun request_withdraw_stake_non_entry( + _wrapper: &mut SuiSystemState, + staked_sui: StakedSui, + ctx: &mut TxContext, +): Balance { + let exr = get_exr(ctx.epoch(), &staked_sui.pool_id()); + let am = storage::get_sui_amount(&exr, staked_sui.amount()); + + let w: Balance = nondet(); + cvlm_assume_msg(w.value() == am, b"Exchange"); + ghost_destroy(staked_sui); + w +} + +public(package) fun assert_version_and_upgrade(_version: &mut Version, _current_version: u16) {} diff --git a/certora/spec/sources/supply_control.move b/certora/spec/sources/supply_control.move new file mode 100644 index 0000000..f4116b9 --- /dev/null +++ b/certora/spec/sources/supply_control.move @@ -0,0 +1,143 @@ +/// Property: Supply Control Authorization +/// Description: Enforces strict access control on token supply modifications by verifying that only +/// authorized operations can increase or decrease the SUI and LST supplies. Specifically, only mint +/// operations can increase supplies, and only redemption operations can decrease supplies. This prevents +/// unauthorized minting or burning of tokens through administrative or operational functions, ensuring +/// that supply changes only occur through the intended user-facing deposit and withdrawal flows. + +module spec::supply_control; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; + +use cvlm::manifest::{target, invoker, rule}; + +use liquid_staking::liquid_staking::LiquidStakingInfo; +use spec::accounting_total_sui_supply::total_supply_correct; +use spec::common::{setup_fresh, can_decrease_supply, can_increase_supply}; +use spec::dummy::DummyToken; +use sui_system::sui_system::SuiSystemState; + + +public fun cvlm_manifest() { + // Public mut functions + target(@spec, b"dummy", b"mint"); + target(@spec, b"dummy", b"redeem"); + target(@spec, b"dummy", b"custom_redeem_request"); + target(@spec, b"dummy", b"custom_redeem"); + target(@spec, b"dummy", b"change_validator_priority"); + target(@spec, b"dummy", b"increase_validator_stake"); + target(@spec, b"dummy", b"decrease_validator_stake"); + target(@spec, b"dummy", b"collect_fees"); + target(@spec, b"dummy", b"update_fees"); + target(@spec, b"dummy", b"refresh"); + target(@spec, b"dummy", b"update_metadata"); + + invoker(b"invoke"); + + rule(b"only_redemption_decreases_sui_supply"); + rule(b"only_redemption_decreases_lst_supply"); + rule(b"only_minting_increases_sui_supply"); + rule(b"only_minting_increases_lst_supply"); + +} + +native fun invoke( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + +/// Verifies that only authorized redemption operations can decrease the total SUI supply. +/// This prevents unauthorized withdrawal of SUI backing through non-redemption functions. +public fun only_redemption_decreases_sui_supply( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + let sui_pre = lsi.total_sui_supply(); + + cvlm_assume_msg(total_supply_correct(lsi.storage()), b"Sound state"); + invoke(target, lsi, system_state, ctx); + + let sui_post = lsi.total_sui_supply(); + + let sui_decrease = sui_post < sui_pre; + + + let decreased = sui_decrease; + + cvlm_assert(!decreased || can_decrease_supply(target)); +} + +/// Verifies that only authorized redemption operations can decrease the total LST supply. +/// This prevents unauthorized burning of LST tokens through non-redemption functions. +public fun only_redemption_decreases_lst_supply( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + let lst_pre = lsi.total_lst_supply(); + + invoke(target, lsi, system_state, ctx); + + let lst_post = lsi.total_lst_supply(); + let lst_decrease = lst_post < lst_pre; + + let decreased = lst_decrease; + + cvlm_assert(!decreased || can_decrease_supply(target)); +} + +/// Verifies that only authorized mint operations can increase the total LST supply. +/// This prevents unauthorized creation of LST tokens through non-mint functions. +public fun only_minting_increases_lst_supply( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + + let lst_pre = lsi.total_lst_supply(); + + invoke(target, lsi, system_state, ctx); + + let lst_post = lsi.total_lst_supply(); + + let lst_increase = lst_post > lst_pre; + + let increased = lst_increase; + + cvlm_assert(!increased || can_increase_supply(target)); +} + +/// Verifies that only authorized mint operations can increase the total SUI supply backing. +/// This prevents unauthorized injection of SUI backing through non-mint functions. +public fun only_minting_increases_sui_supply( + target: Function, + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup_fresh(lsi, system_state, ctx); + + let sui_pre = lsi.total_sui_supply(); + + + invoke(target, lsi, system_state, ctx); + + let sui_post = lsi.total_sui_supply(); + + let sui_increase = sui_post > sui_pre; + + + let increased = sui_increase; + + cvlm_assert(!increased || can_increase_supply(target)); +} diff --git a/certora/spec/sources/validators_consistency.move b/certora/spec/sources/validators_consistency.move new file mode 100644 index 0000000..2589cfd --- /dev/null +++ b/certora/spec/sources/validators_consistency.move @@ -0,0 +1,171 @@ +/// Property: Validator Registry Consistency +/// Description: Ensures the internal validator registry maintains structural invariants critical for +/// correct protocol operation. Validates that: (1) no duplicate validators exist by staking pool ID +/// or validator address; (2) the registry size never exceeds the maximum validators limit; (3) after +/// any operation followed by a forced epoch transition and refresh, validators with no active or inactive +/// stake have zero total SUI recorded, preventing phantom stake across epoch boundaries. +/// These properties guarantee accurate stake accounting and structural integrity of the validator management system. + +module spec::validators_consistency; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::ghost::ghost_destroy; +use cvlm::manifest::{target, invoker, rule}; +use liquid_staking::storage::{Self, Storage, active_stake, ValidatorInfo}; +use spec::common::{log}; +use sui_system::sui_system::SuiSystemState; +use liquid_staking::storage::max_validators; +use cvlm::nondet::nondet; + +public fun cvlm_manifest() { + // Public mut functions + + target(@liquid_staking, b"storage", b"refresh"); + target(@liquid_staking, b"storage", b"change_validator_priority"); + target(@liquid_staking, b"storage", b"join_to_sui_pool"); + target(@liquid_staking, b"storage", b"join_stake"); + target(@liquid_staking, b"storage", b"join_fungible_stake"); + target(@liquid_staking, b"storage", b"join_inactive_stake_to_validator"); + target(@liquid_staking, b"storage", b"join_fungible_staked_sui_to_validator"); + target(@liquid_staking, b"storage", b"split_up_to_n_sui_from_sui_pool"); + target(@liquid_staking, b"storage", b"split_from_sui_pool"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_validator"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_active_stake"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_inactive_stake"); + target(@liquid_staking, b"storage", b"split_n_sui"); + target(@liquid_staking, b"storage", b"get_or_add_validator_index_by_staking_pool_id_mut"); + + invoker(b"invoke"); + + rule(b"no_duplicate_validators"); + + rule(b"validators_upper_bound_base"); + rule(b"validators_upper_bound_step"); + + rule(b"no_stake_no_sui_base"); + rule(b"no_stake_no_sui_step"); + + +} + +native fun invoke( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + +/// Verifies that adding a validator to the registry only occurs if neither its staking pool ID +/// nor its validator address already exists, preventing duplicate entries and double-counting. +public fun no_duplicate_validators( + strg: &mut Storage, + staking_pool_id: ID, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + let validator_address = system_state.validator_address_by_pool_id(&staking_pool_id); + + let mut id_exists = false; + let mut address_exists = false; + + let infos_pre = strg.validators().length(); + + let mut i = 0; + while (i < infos_pre) { + let v = &strg.validators()[i]; + id_exists = id_exists || v.staking_pool_id() == staking_pool_id; + address_exists = address_exists || v.validator_address() == validator_address; + i = i + 1; + }; + + let index = strg.get_or_add_validator_index_by_staking_pool_id_mut( + system_state, + staking_pool_id, + ctx, + ); + let appended = index == infos_pre; + + log(&id_exists); + log(&address_exists); + log(&appended); + + // appended -> !id_exists && !address_exists + cvlm_assert(!appended || (!id_exists && !address_exists )); +} + + +/// Base case: Verifies that newly created storage has a validator count within the maximum limit. +public fun validators_upper_bound_base(ctx: &mut TxContext) { + let strg = storage::new(ctx); + cvlm_assert(strg.validators().length() <= max_validators()); + ghost_destroy(strg); +} + +/// Inductive step: Verifies that all operations preserve the invariant that the validator count +/// never exceeds the maximum validators limit. +public fun validators_upper_bound_step( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg(strg.validators().length() <= max_validators(), b"Assume in pre state"); + invoke(target, strg, system_state, ctx); + cvlm_assert(strg.validators().length() <= max_validators()); +} + +fun validator_no_stake_no_sui(v: &ValidatorInfo): bool { + let no_active = v.active_stake().is_none(); + let no_inactive = v.inactive_stake().is_none(); + // (no active && no_inactive) => no sui + !(no_active && no_inactive) || v.total_sui_amount() == 0 +} + +public fun no_stake_no_sui(strg: &Storage): bool { + let mut ret = true; + let mut i = 0; + while (i < strg.validators().length()) { + let v_i = &strg.validators()[i]; + ret = ret && validator_no_stake_no_sui(v_i); + i = i+1; + }; + ret +} + +/// Base case: Verifies that for newly created storage, validators with no active or inactive stake +/// have zero total SUI amount recorded. +public fun no_stake_no_sui_base(ctx: &mut TxContext) { + let strg = storage::new(ctx); + cvlm_assert(no_stake_no_sui(&strg)); + ghost_destroy(strg); +} + +/// Inductive step: Verifies that all operations preserve the invariant that validators with no +/// active or inactive stake have zero total SUI recorded, preventing phantom stake. +/// +/// Note: This invariant only holds across epoch boundaries after refresh, as accounting can +/// temporarily drift within an epoch. The drift occurs because refresh_validator_info sets +/// total_sui_amount via get_sui_amount(...) which floors division, while unstaking paths (calling +/// redeem_and_update_accounting) debit total_sui_amount by the actual redeemed SUI from +/// redeem_fungible_staked_sui. Since flooring is not additive, partial unstakes can leave dust, +/// and after the last stake object is removed, total_sui_amount may still be > 0 until refresh() +/// recomputes and zeroes it at the next epoch boundary. +public fun no_stake_no_sui_step( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + cvlm_assume_msg(no_stake_no_sui(strg), b"Assume in pre state"); + invoke(target, strg, system_state, ctx); + + // Force refresh at next epoch boundary to verify invariant holds + let mut ctx2: TxContext = nondet(); + cvlm_assume_msg(ctx2.epoch() < ctx.epoch(), b"Force refresh"); + strg.refresh(system_state, &mut ctx2); + + + cvlm_assert(no_stake_no_sui(strg)); +} + diff --git a/certora/spec/sources/validators_integrity.move b/certora/spec/sources/validators_integrity.move new file mode 100644 index 0000000..c736cec --- /dev/null +++ b/certora/spec/sources/validators_integrity.move @@ -0,0 +1,161 @@ +/// Property: Validator Registry Integrity +/// Description: Verifies integrity properties of validator registry operations. Rules check that: +/// (1) validators can only be added through authorized staking operations (join_stake, join_fungible_stake) +/// or explicit validator addition (get_or_add_validator_index_by_staking_pool_id_mut), preventing +/// unauthorized registry modifications; (2) validators can only be removed through refresh operations; +/// (3) at most one validator can be added per operation; (4) after refresh, no inactive stake remains +/// in the registry; (5) after refresh, no empty validators remain in the registry. +/// These rules verify correct authorization and post-conditions for validator registry modifications. + +module spec::validators_integrity; + +use cvlm::asserts::{cvlm_assert, cvlm_assume_msg}; +use cvlm::function::Function; +use cvlm::manifest::{target, invoker, rule}; +use cvlm::nondet::nondet; +use liquid_staking::liquid_staking::LiquidStakingInfo; +use liquid_staking::storage::{Storage}; +use spec::common::{setup}; +use spec::dummy::DummyToken; +use sui_system::sui_system::SuiSystemState; +use spec::validators_consistency::no_stake_no_sui; + +public fun cvlm_manifest() { + // Public mut functions + + target(@liquid_staking, b"storage", b"refresh"); + target(@liquid_staking, b"storage", b"change_validator_priority"); + target(@liquid_staking, b"storage", b"join_to_sui_pool"); + target(@liquid_staking, b"storage", b"join_stake"); + target(@liquid_staking, b"storage", b"join_fungible_stake"); + target(@liquid_staking, b"storage", b"join_inactive_stake_to_validator"); + target(@liquid_staking, b"storage", b"join_fungible_staked_sui_to_validator"); + target(@liquid_staking, b"storage", b"split_up_to_n_sui_from_sui_pool"); + target(@liquid_staking, b"storage", b"split_from_sui_pool"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_validator"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_active_stake"); + target(@liquid_staking, b"storage", b"unstake_approx_n_sui_from_inactive_stake"); + target(@liquid_staking, b"storage", b"split_n_sui"); + target(@liquid_staking, b"storage", b"get_or_add_validator_index_by_staking_pool_id_mut"); + + invoker(b"invoke"); + + rule(b"can_add_correct"); + rule(b"can_remove_correct"); + rule(b"add_at_most_one"); + + rule(b"no_inactive_stake_after_refresh"); + rule(b"no_empty_validators_after_refresh"); +} + +native fun invoke( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +); + + +fun can_add_validator(target: Function): bool { + target.name() == b"get_or_add_validator_index_by_staking_pool_id_mut" + || target.name() == b"join_stake" + || target.name() == b"join_fungible_stake" +} + +fun can_remove_validator(target: Function): bool { + target.name() == b"refresh" +} + +/// Verifies that validators can only be added to the registry through explicitly authorized operations +/// (staking operations and direct validator addition), preventing unauthorized registry modifications. +public fun can_add_correct( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + let validators_pre = strg.validators().length(); + invoke(target, strg, system_state, ctx); + let validators_post = strg.validators().length(); + + let appended = validators_post > validators_pre; + let allowed = can_add_validator(target); + + cvlm_assert(!appended || allowed); +} + +/// Verifies that validators can only be removed from the registry through the refresh operation, +/// which cleans up empty validators, preventing unauthorized validator removal. +public fun can_remove_correct( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + let validators_pre = strg.validators().length(); + invoke(target, strg, system_state, ctx); + let validators_post = strg.validators().length(); + + let removed = validators_post < validators_pre; + let allowed = can_remove_validator(target); + + cvlm_assert(!removed || allowed); +} + + + +/// Verifies that any single operation can add at most one validator to the registry, +/// preventing bulk additions that could bypass validation logic. +public fun add_at_most_one( + target: Function, + strg: &mut Storage, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + let validators_pre = strg.validators().length(); + invoke(target, strg, system_state, ctx); + let validators_post = strg.validators().length(); + + cvlm_assert(validators_post <= validators_pre + 1); +} + + +/// Verifies that after a refresh operation completes, no validators in the registry contain +/// inactive stake, ensuring all stake has been properly activated or removed. +public fun no_inactive_stake_after_refresh( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup(lsi); + cvlm_assume_msg(ctx.epoch() > lsi.storage().last_refresh_epoch(), b"Force refresh"); + + lsi.refresh(system_state, ctx); + + let i = nondet(); + cvlm_assume_msg(i < lsi.storage().validators().length(), b""); + + let inactive = lsi.storage().validators()[i].inactive_stake(); + cvlm_assert(inactive.is_none()); +} + +/// Verifies that after a refresh operation completes, no validators in the registry are empty +/// (containing no stake), ensuring clean state and accurate registry size. +public fun no_empty_validators_after_refresh( + lsi: &mut LiquidStakingInfo, + system_state: &mut SuiSystemState, + ctx: &mut TxContext, +) { + setup(lsi); + cvlm_assume_msg(ctx.epoch() > lsi.storage().last_refresh_epoch(), b"Force refresh"); + cvlm_assume_msg(no_stake_no_sui(lsi.storage()), b"Assume in pre state"); + + + lsi.refresh(system_state, ctx); + + let i = nondet(); + cvlm_assume_msg(i < lsi.storage().validators().length(), b""); + let validator = &lsi.storage().validators()[i]; + + cvlm_assert(!validator.is_empty()); +}