From daa97f07a7b70c3704207379540be1207a26f38f Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 19 Aug 2025 16:06:41 +0300 Subject: [PATCH 1/3] cherry-pick: sui-system-no-abort-specs --- .../packages/sui-framework/Move.toml | 2 +- .../packages/sui-system/Move.lock | 67 +++++++++++-- .../packages/sui-system/Move.toml | 4 +- .../packages/sui-system/sources/helpers.move | 74 +++++++++++++++ .../sui-system/sources/other_specs.move | 16 ++++ .../sui-system/sources/stake_subsidy.move | 16 ++++ .../sui-system/sources/staking_pool.move | 95 +++++++++++++++++++ .../sui-system/sources/storage_fund.move | 21 ++++ .../sui-system/sources/validator.move | 39 ++++++++ 9 files changed, 321 insertions(+), 13 deletions(-) create mode 100644 crates/sui-framework/packages/sui-system/sources/helpers.move create mode 100644 crates/sui-framework/packages/sui-system/sources/other_specs.move diff --git a/crates/sui-framework/packages/sui-framework/Move.toml b/crates/sui-framework/packages/sui-framework/Move.toml index 90a026948a7e..30de79561d77 100644 --- a/crates/sui-framework/packages/sui-framework/Move.toml +++ b/crates/sui-framework/packages/sui-framework/Move.toml @@ -5,7 +5,7 @@ published-at = "0x2" edition = "2024.beta" [dependencies] -MoveStdlib = { local = "../move-stdlib", override = true } +# MoveStdlib = { local = "../move-stdlib", override = true } [addresses] sui = "0x2" diff --git a/crates/sui-framework/packages/sui-system/Move.lock b/crates/sui-framework/packages/sui-system/Move.lock index af204d00c799..01df77464e50 100644 --- a/crates/sui-framework/packages/sui-system/Move.lock +++ b/crates/sui-framework/packages/sui-system/Move.lock @@ -1,27 +1,74 @@ # @generated by Move, please check-in and do not edit manually. [move] -version = 1 -manifest_digest = "68AEB9354EE1D616F6D2293EC721FE3D7E810FEC4FE34197676ECFA3DA72CAE3" -deps_digest = "3C4103934B1E040BB6B23F1D610B4EF9F2F1166A50A104EADCF77467C004C600" +version = 3 +manifest_digest = "05062993DFF0CEB4183CF4B07640698C2BFD8B7B66CEAE02DE3B49334C09F07F" +deps_digest = "E3B0C44298FC1C149AFBF4C8996FB92427AE41E4649B934CA495991B7852B855" dependencies = [ - { name = "MoveStdlib" }, - { name = "Sui" }, + { id = "DeepBook", name = "DeepBook" }, + { id = "MoveStdlib", name = "MoveStdlib" }, + { id = "Sui", name = "Sui" }, + { id = "SuiProver", name = "SuiProver" }, + # { id = "SuiSystem", name = "SuiSystem" }, ] [[move.package]] -name = "MoveStdlib" -source = { local = "../move-stdlib" } +id = "DeepBook" +source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/deepbook" } + +dependencies = [ + { id = "MoveStdlib", name = "MoveStdlib" }, + { id = "Sui", name = "Sui" }, +] + +[[move.package]] +id = "MoveStdlib" +source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/move-stdlib" } + +[[move.package]] +id = "Prover" +source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/prover" } + +dependencies = [ + { id = "MoveStdlib", name = "MoveStdlib" }, +] [[move.package]] -name = "Sui" -source = { local = "../sui-framework" } +id = "Sui" +source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/sui-framework" } dependencies = [ - { name = "MoveStdlib" }, + { id = "MoveStdlib", name = "MoveStdlib" }, ] +[[move.package]] +id = "SuiProver" +source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-prover" } + +dependencies = [ + { id = "SuiSpecs", name = "SuiSpecs" }, +] + +[[move.package]] +id = "SuiSpecs" +source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-framework-specs" } + +dependencies = [ + { id = "Prover", name = "Prover" }, + { id = "Sui", name = "Sui" }, +] + +# [[move.package]] +# id = "SuiSystem" +# source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/sui-system" } + +# dependencies = [ +# { id = "MoveStdlib", name = "MoveStdlib" }, +# { id = "Sui", name = "Sui" }, +#] + + [move.toolchain-version] compiler-version = "1.22.0" edition = "legacy" diff --git a/crates/sui-framework/packages/sui-system/Move.toml b/crates/sui-framework/packages/sui-system/Move.toml index 98e9236ff9b0..77101056d9f0 100644 --- a/crates/sui-framework/packages/sui-system/Move.toml +++ b/crates/sui-framework/packages/sui-system/Move.toml @@ -5,8 +5,8 @@ published-at = "0x3" edition = "2024.beta" [dependencies] -MoveStdlib = { local = "../move-stdlib" } -Sui = { local = "../sui-framework" } +# MoveStdlib = { local = "../move-stdlib" } +# Sui = { local = "../sui-framework" } [addresses] sui_system = "0x3" diff --git a/crates/sui-framework/packages/sui-system/sources/helpers.move b/crates/sui-framework/packages/sui-system/sources/helpers.move new file mode 100644 index 000000000000..a2eb5cbf4587 --- /dev/null +++ b/crates/sui-framework/packages/sui-system/sources/helpers.move @@ -0,0 +1,74 @@ +module sui_system::helpers; + +#[spec_only] +use std::{u64,u32,u16,u8}; +#[spec_only] +use prover::prover::{ensures, invariant}; + +#[spec_only] +/// x+y will not abort (u64) +fun can_add_u64(x: u64, y: u64): bool { + x.to_int().add(y.to_int()).lte(u64::max_value!().to_int()) +} + +#[spec_only] +/// x+y will not abort (u32) +fun can_add_u32(x: u32, y: u32): bool { + x.to_int().add(y.to_int()).lte(u32::max_value!().to_int()) +} + +#[spec_only] +/// x-y will not abort +fun can_sub_u64(x: u64, y: u64): bool { + y <= x +} + +#[spec_only] +/// x-y will not abort +fun can_sub_u32(x: u32, y: u32): bool { + y <= x +} + +// iteration macros have expansions that wrap up the contained loop, +// so that an invariant cannot be attached. the versions here have a +// parameter that will give the loop invarant, which gets placed in +// the correct spot. + +/// like `std::macros::range_do`, but allows for an invariant. +/// The supplied function takes one parameter, the loop index +public macro fun range_do_with_invariant<$T, $R: drop>($start: $T, $stop: $T, $f: |$T| -> $R, $g: |$T| -> bool) { + let mut i = $start; + let stop = $stop; + invariant!(|| { ensures( $g(i) ); }); + while (i < stop) { + $f(i); + i = i + 1; + } +} + +/// like `std::macros::do`, but allows for an invariant. +/// The supplied function takes one parameter, the loop index +public macro fun do_with_invariant<$T, $R: drop>($stop: $T, $f: |$T| -> $R, $g: |$T| -> bool) { + range_do_with_invariant!(0, $stop, $f, $g) +} + +/// like `std:vectors::do`, but allows for an invariant. +/// The supplied function takes one parameter, the loop index +/// (which is also used as the index into the vector in the loop) +public macro fun vector_do_ref_with_invariant<$T, $R: drop>($v: &vector<$T>, $f: |&$T| -> $R, $g: |u64| -> bool) { + let v = $v; + do_with_invariant!(v.length(), |i| $f(&v[i]), |i| i <= v.length() && ($g(i))) +} + +/// like `std::vectors::find_index`, but allows for an invariant. +public macro fun vector_find_index_with_invariant<$T>($v: &vector<$T>, + $f: |&$T| -> bool, + $g: |u64| -> bool): Option { + let v = $v; + 'find_index: { + do_with_invariant!(v.length(), + (|i| if ($f(&v[i])) return 'find_index std::option::some(i)), // do this + (|i| i <= v.length() && ($g(i)))); // using this invariant + std::option::none() + } +} diff --git a/crates/sui-framework/packages/sui-system/sources/other_specs.move b/crates/sui-framework/packages/sui-system/sources/other_specs.move new file mode 100644 index 000000000000..61803c8b8781 --- /dev/null +++ b/crates/sui-framework/packages/sui-system/sources/other_specs.move @@ -0,0 +1,16 @@ +/// Specifications for modules used by sui_system, and in particular for functions +/// that cause problems. + +module sui_system::other_specs; + +use sui::tx_context::TxContext; + +#[spec(target=sui::tx_context::epoch)] +public fun epoch_spec(self: &TxContext): u64 { + sui::tx_context::epoch(self) +} + +#[spec(target=sui::tx_context::sender)] +public fun sender_spec(self: &TxContext): address { + sui::tx_context::sender(self) +} diff --git a/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move b/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move index bf013e7e11f5..7f0f4650fc26 100644 --- a/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move +++ b/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move @@ -89,3 +89,19 @@ public(package) fun get_distribution_counter(self: &StakeSubsidy): u64 { public(package) fun set_distribution_counter(self: &mut StakeSubsidy, distribution_counter: u64) { self.distribution_counter = distribution_counter; } + +// === specifications === + +// This invariant is needed to prove no abort in some of the non-public functions, +// so can be skipped for now. + +// #[spec_only] +// fun StakeSubsidy_inv(x: &StakeSubsidy): bool { +// x.stake_subsidy_decrease_rate <= BASIS_POINT_DENOMINATOR as u16 && +// x.stake_subsidy_period_length > 0 +// } + +#[spec(prove, no_opaque)] +public fun current_epoch_subsidy_amount_spec(self: &StakeSubsidy): u64 { + current_epoch_subsidy_amount(self) +} diff --git a/crates/sui-framework/packages/sui-system/sources/staking_pool.move b/crates/sui-framework/packages/sui-system/sources/staking_pool.move index 0fc77a9ca028..64925d7a7ebc 100644 --- a/crates/sui-framework/packages/sui-system/sources/staking_pool.move +++ b/crates/sui-framework/packages/sui-system/sources/staking_pool.move @@ -774,3 +774,98 @@ fun test_calculate_fungible_staked_sui_withdraw_amount( let min_out = if (expected_out > 2) expected_out - 2 else 0; assert!(principal_amount + rewards_amount >= min_out, 0); } + +// === specifications === + +#[spec_only] +use prover::prover::{requires, ensures}; + +#[spec_only] +use prover::ghost; + +#[spec_only] +use sui_system::helpers::{can_add_u64}; + + +#[spec(prove, no_opaque)] +public fun staked_sui_amount_spec(staked_sui: &StakedSui): u64 { + staked_sui_amount(staked_sui) +} + +#[spec(prove, no_opaque)] +public fun is_preactive_spec(pool: &StakingPool): bool { + is_preactive(pool) +} + +#[spec(prove, no_opaque)] +public fun is_inactive_spec(pool: &StakingPool): bool { + is_inactive(pool) +} + +#[spec(prove)] +public fun split_fungible_staked_sui_spec( + fungible_staked_sui: &mut FungibleStakedSui, + split_amount: u64, + ctx: &mut TxContext, +): FungibleStakedSui { + requires(split_amount <= fungible_staked_sui_value(fungible_staked_sui)); + split_fungible_staked_sui(fungible_staked_sui, split_amount, ctx) +} + +#[spec(prove)] +public fun join_fungible_staked_sui_spec(self: &mut FungibleStakedSui, other: FungibleStakedSui) { + requires(self.pool_id() == other.pool_id()); + requires(can_add_u64(self.value(), other.value())); + join_fungible_staked_sui(self, other); +} + +#[spec(prove)] +public fun split_spec(self: &mut StakedSui, split_amount: u64, ctx: &mut TxContext): StakedSui { + requires(split_amount <= self.principal.value()); + requires(split_amount >= MIN_STAKING_THRESHOLD); + requires(self.principal.value() - split_amount >= MIN_STAKING_THRESHOLD); + split(self, split_amount, ctx) +} + +#[spec(prove, no_opaque)] +public fun is_equal_staking_metadata_spec(self: &StakedSui, other: &StakedSui): bool { + is_equal_staking_metadata(self, other) +} + +#[spec_only] +/// function needed to make the requirements of `pool_token_exchange_rate_at_epoch_spec` +/// expressible outside this module. +public fun activation_epoch_is_positive(pool: &StakingPool): bool { + pool.activation_epoch.is_some() && + *pool.activation_epoch.borrow() > 0 +} + +#[spec(prove)] +public fun pool_token_exchange_rate_at_epoch_spec( + pool: &StakingPool, + epoch: u64, +): PoolTokenExchangeRate { + requires(! pool.is_preactive()); + // requires(*pool.activation_epoch.borrow() > 0); // visible? add to invariant? + requires(activation_epoch_is_positive(pool)); + pool_token_exchange_rate_at_epoch(pool, epoch) +} + +#[spec(prove)] +public fun split_staked_sui_spec(stake: &mut StakedSui, split_amount: u64, ctx: &mut TxContext) { + use specs::transfer_spec::{SpecTransferAddress,SpecTransferAddressExists}; + ghost::declare_global_mut(); + ghost::declare_global_mut(); + // preconditions from the call to split: + requires(split_amount <= stake.principal.value()); + requires(split_amount >= MIN_STAKING_THRESHOLD); + requires(stake.principal.value() - split_amount >= MIN_STAKING_THRESHOLD); + split_staked_sui(stake, split_amount, ctx); +} + +#[spec(prove)] +public fun join_staked_sui_spec(self: &mut StakedSui, other: StakedSui) { + requires(is_equal_staking_metadata(self, &other)); + requires(can_add_u64(self.principal.value(), other.principal.value())); // or the join overflows + join_staked_sui(self, other); +} diff --git a/crates/sui-framework/packages/sui-system/sources/storage_fund.move b/crates/sui-framework/packages/sui-system/sources/storage_fund.move index 5cfae4038f0a..bf9cb90d4f48 100644 --- a/crates/sui-framework/packages/sui-system/sources/storage_fund.move +++ b/crates/sui-framework/packages/sui-system/sources/storage_fund.move @@ -69,3 +69,24 @@ public fun total_object_storage_rebates(self: &StorageFund): u64 { public fun total_balance(self: &StorageFund): u64 { self.total_object_storage_rebates.value() + self.non_refundable_balance.value() } + +// === specifications === + +#[spec_only] +use prover::prover::requires; + +#[spec_only] +use sui_system::helpers::can_add_u64; + +#[spec(prove, no_opaque)] +public fun total_object_storage_rebates_spec(self: &StorageFund): u64 { + total_object_storage_rebates(self) +} + +// This precondition is not useful to a caller; it mentions fields that are not caller-visible +#[spec(prove)] +public fun total_balance_spec(self: &StorageFund): u64 { + requires(can_add_u64(self.total_object_storage_rebates.value(), + self.non_refundable_balance.value())); + total_balance(self) +} diff --git a/crates/sui-framework/packages/sui-system/sources/validator.move b/crates/sui-framework/packages/sui-system/sources/validator.move index 9b6aedb64827..05950745f906 100644 --- a/crates/sui-framework/packages/sui-system/sources/validator.move +++ b/crates/sui-framework/packages/sui-system/sources/validator.move @@ -995,3 +995,42 @@ public(package) fun new_for_testing( validator } + +// === specifications and proofs === + +#[spec_only] +use prover::prover::{requires, ensures}; + +#[spec(prove, no_opaque)] +public fun is_preactive_spec(self: &Validator): bool { + is_preactive(self) +} + +#[spec(prove)] +public fun pool_token_exchange_rate_at_epoch_spec(self: &Validator, epoch: u64): PoolTokenExchangeRate { + requires(! self.is_preactive()); + requires(staking_pool::activation_epoch_is_positive(&self.staking_pool)); + pool_token_exchange_rate_at_epoch(self, epoch) +} + +#[spec(prove, no_opaque)] +public fun staking_pool_id_spec(self: &Validator): ID { + staking_pool_id(self) +} + +#[spec(prove)] +public fun is_duplicate_spec(self: &Validator, other: &Validator): bool { + is_duplicate(self, other) +} + +#[spec(prove)] +public fun validate_metadata_spec(metadata: &ValidatorMetadata) { + validate_metadata(metadata); +} +// + +// "aborts if metadata is not valid" -- how to capture? +#[spec] +public fun validate_metadata_bcs_spec(metadata: vector) { + validate_metadata_bcs(metadata); +} From c234c797179372bcdb38ddea46625b7f5db01e6a Mon Sep 17 00:00:00 2001 From: Andrii Date: Wed, 20 Aug 2025 13:27:07 +0300 Subject: [PATCH 2/3] feat: moved specs to different package --- .../packages/sui-framework/Move.lock | 13 +- .../packages/sui-framework/Move.toml | 2 +- .../packages/sui-system-specs/Move.toml | 11 ++ .../sources/helpers.move | 2 +- .../sui-system-specs/sources/other_specs.move | 11 ++ .../sources/stake_subsidy.move | 21 ++++ .../sources/staking_pool.move | 119 ++++++++++++++++++ .../sources/storage_fund.move | 27 ++++ .../sui-system-specs/sources/validator.move | 65 ++++++++++ .../packages/sui-system/Move.lock | 35 +----- .../packages/sui-system/Move.toml | 4 +- .../sui-system/sources/other_specs.move | 16 --- .../sui-system/sources/stake_subsidy.move | 16 --- .../sui-system/sources/staking_pool.move | 95 -------------- .../sui-system/sources/storage_fund.move | 20 +-- .../sui-system/sources/validator.move | 39 +----- 16 files changed, 272 insertions(+), 224 deletions(-) create mode 100644 crates/sui-framework/packages/sui-system-specs/Move.toml rename crates/sui-framework/packages/{sui-system => sui-system-specs}/sources/helpers.move (98%) create mode 100644 crates/sui-framework/packages/sui-system-specs/sources/other_specs.move create mode 100644 crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move create mode 100644 crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move create mode 100644 crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move create mode 100644 crates/sui-framework/packages/sui-system-specs/sources/validator.move delete mode 100644 crates/sui-framework/packages/sui-system/sources/other_specs.move diff --git a/crates/sui-framework/packages/sui-framework/Move.lock b/crates/sui-framework/packages/sui-framework/Move.lock index 999fa85693d7..1bacad6d8baa 100644 --- a/crates/sui-framework/packages/sui-framework/Move.lock +++ b/crates/sui-framework/packages/sui-framework/Move.lock @@ -2,18 +2,9 @@ [move] version = 3 -manifest_digest = "06FD8F5C2B5CB25BBFF27D5AF3EEEC284C453E7190F2FA22CEC3FB4270B4B5D4" -deps_digest = "3C4103934B1E040BB6B23F1D610B4EF9F2F1166A50A104EADCF77467C004C600" - -dependencies = [ - { id = "MoveStdlib", name = "MoveStdlib" }, -] +manifest_digest = "CD04B0AFFBEA9E38D757D76D077FCB8D9F7E69A99F98F542A4F6D5DBBB6B84A0" +deps_digest = "E3B0C44298FC1C149AFBF4C8996FB92427AE41E4649B934CA495991B7852B855" [[move.package]] id = "MoveStdlib" source = { local = "../move-stdlib" } - -[move.toolchain-version] -compiler-version = "1.30.0" -edition = "2024.beta" -flavor = "sui" diff --git a/crates/sui-framework/packages/sui-framework/Move.toml b/crates/sui-framework/packages/sui-framework/Move.toml index 30de79561d77..90a026948a7e 100644 --- a/crates/sui-framework/packages/sui-framework/Move.toml +++ b/crates/sui-framework/packages/sui-framework/Move.toml @@ -5,7 +5,7 @@ published-at = "0x2" edition = "2024.beta" [dependencies] -# MoveStdlib = { local = "../move-stdlib", override = true } +MoveStdlib = { local = "../move-stdlib", override = true } [addresses] sui = "0x2" diff --git a/crates/sui-framework/packages/sui-system-specs/Move.toml b/crates/sui-framework/packages/sui-system-specs/Move.toml new file mode 100644 index 000000000000..788f68464333 --- /dev/null +++ b/crates/sui-framework/packages/sui-system-specs/Move.toml @@ -0,0 +1,11 @@ +[package] +name = "SuiSystemSpecs" +version = "0.0.1" +published-at = "0x31" +edition = "2024.beta" + +[dependencies] +SuiSystem = { local = "../sui-system" } + +[addresses] +sui_system_specs = "0x31" diff --git a/crates/sui-framework/packages/sui-system/sources/helpers.move b/crates/sui-framework/packages/sui-system-specs/sources/helpers.move similarity index 98% rename from crates/sui-framework/packages/sui-system/sources/helpers.move rename to crates/sui-framework/packages/sui-system-specs/sources/helpers.move index a2eb5cbf4587..3e1003318ebd 100644 --- a/crates/sui-framework/packages/sui-system/sources/helpers.move +++ b/crates/sui-framework/packages/sui-system-specs/sources/helpers.move @@ -1,4 +1,4 @@ -module sui_system::helpers; +module sui_system_specs::helpers; #[spec_only] use std::{u64,u32,u16,u8}; diff --git a/crates/sui-framework/packages/sui-system-specs/sources/other_specs.move b/crates/sui-framework/packages/sui-system-specs/sources/other_specs.move new file mode 100644 index 000000000000..bf7a678c0ddc --- /dev/null +++ b/crates/sui-framework/packages/sui-system-specs/sources/other_specs.move @@ -0,0 +1,11 @@ +module sui_system_specs::other_specs; + +#[spec(target = sui::tx_context::epoch)] +public fun epoch_spec(self: &TxContext): u64 { + sui::tx_context::epoch(self) +} + +#[spec(target = sui::tx_context::sender)] +public fun sender_spec(self: &TxContext): address { + sui::tx_context::sender(self) +} diff --git a/crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move b/crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move new file mode 100644 index 000000000000..e08144fb7bf4 --- /dev/null +++ b/crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move @@ -0,0 +1,21 @@ +module sui_system_specs::stake_subsidy; + +#[spec_only] +use sui_system::stake_subsidy::{ + StakeSubsidy, + current_epoch_subsidy_amount +}; + +// This invariant is needed to prove no abort in some of the non-public functions, +// so can be skipped for now. + +// #[spec_only] +// fun StakeSubsidy_inv(x: &StakeSubsidy): bool { +// x.stake_subsidy_decrease_rate <= BASIS_POINT_DENOMINATOR as u16 && +// x.stake_subsidy_period_length > 0 +// } + +#[spec(prove, no_opaque, target = sui_system::stake_subsidy::current_epoch_subsidy_amount)] +public fun current_epoch_subsidy_amount_spec(self: &StakeSubsidy): u64 { + current_epoch_subsidy_amount(self) +} diff --git a/crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move b/crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move new file mode 100644 index 000000000000..f38863ae622a --- /dev/null +++ b/crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move @@ -0,0 +1,119 @@ +#[allow(unused_const)] +module sui_system_specs::staking_pool; + +#[spec_only] +use sui_system::staking_pool::{ + PoolTokenExchangeRate, + StakedSui, + StakingPool, + FungibleStakedSui, + staked_sui_amount, + is_preactive, + is_inactive, + split_fungible_staked_sui, + join_fungible_staked_sui, + is_equal_staking_metadata, + split, + split_staked_sui, + pool_token_exchange_rate_at_epoch, + join_staked_sui, + fungible_staked_sui_value, + activation_epoch, +}; + +#[spec_only] +use sui_system_specs::helpers::can_add_u64; + +#[spec_only] +use prover::prover::{requires, ensures}; + +#[spec_only] +use prover::ghost; + +/// CLONE. +#[spec_only] +const MIN_STAKING_THRESHOLD: u64 = 1_000_000_000; // 1 SUI + +#[spec(prove, no_opaque, target = sui_system::staking_pool::staked_sui_amount)] +public fun staked_sui_amount_spec(staked_sui: &StakedSui): u64 { + staked_sui_amount(staked_sui) +} + +#[spec(prove, no_opaque, target = sui_system::staking_pool::is_preactive)] +public fun is_preactive_spec(pool: &StakingPool): bool { + is_preactive(pool) +} + +#[spec(prove, no_opaque, target = sui_system::staking_pool::is_inactive)] +public fun is_inactive_spec(pool: &StakingPool): bool { + is_inactive(pool) +} + +#[spec(prove, target = sui_system::staking_pool::split_fungible_staked_sui)] +public fun split_fungible_staked_sui_spec( + fungible_staked_sui: &mut FungibleStakedSui, + split_amount: u64, + ctx: &mut TxContext, +): FungibleStakedSui { + requires(split_amount <= fungible_staked_sui_value(fungible_staked_sui)); + split_fungible_staked_sui(fungible_staked_sui, split_amount, ctx) +} + +#[spec(prove, target = sui_system::staking_pool::join_fungible_staked_sui)] +public fun join_fungible_staked_sui_spec(self: &mut FungibleStakedSui, other: FungibleStakedSui) { + requires(self.pool_id() == other.pool_id()); + requires(can_add_u64(self.value(), other.value())); + join_fungible_staked_sui(self, other); +} + +#[spec(prove, target = sui_system::staking_pool::split)] +public fun split_spec(self: &mut StakedSui, split_amount: u64, ctx: &mut TxContext): StakedSui { + requires(split_amount <= staked_sui_amount(self)); + requires(split_amount >= MIN_STAKING_THRESHOLD); + requires(staked_sui_amount(self) - split_amount >= MIN_STAKING_THRESHOLD); + split(self, split_amount, ctx) +} + +#[spec(prove, no_opaque, target = sui_system::staking_pool::is_equal_staking_metadata)] +public fun is_equal_staking_metadata_spec(self: &StakedSui, other: &StakedSui): bool { + is_equal_staking_metadata(self, other) +} + +#[spec_only] +/// function needed to make the requirements of `pool_token_exchange_rate_at_epoch_spec` +/// expressible outside this module. +public fun activation_epoch_is_positive(pool: &StakingPool): bool { + let epoch_opt = activation_epoch(pool); + epoch_opt.is_some() && + *epoch_opt.borrow() > 0 +} + +#[spec(prove, target = sui_system::staking_pool::pool_token_exchange_rate_at_epoch)] +public fun pool_token_exchange_rate_at_epoch_spec( + pool: &StakingPool, + epoch: u64, +): PoolTokenExchangeRate { + requires(! pool.is_preactive()); + // requires(*pool.activation_epoch.borrow() > 0); // visible? add to invariant? + requires(activation_epoch_is_positive(pool)); + pool_token_exchange_rate_at_epoch(pool, epoch) +} + +#[spec(prove, target = sui_system::staking_pool::split_staked_sui)] +public fun split_staked_sui_spec(stake: &mut StakedSui, split_amount: u64, ctx: &mut TxContext) { + use specs::transfer_spec::{SpecTransferAddress,SpecTransferAddressExists}; + ghost::declare_global_mut(); + ghost::declare_global_mut(); + // preconditions from the call to split: + requires(split_amount <= staked_sui_amount(stake)); + requires(split_amount >= MIN_STAKING_THRESHOLD); + requires(staked_sui_amount(stake) - split_amount >= MIN_STAKING_THRESHOLD); + split_staked_sui(stake, split_amount, ctx); +} + +#[spec(prove, target = sui_system::staking_pool::join_staked_sui)] +public fun join_staked_sui_spec(self: &mut StakedSui, other: StakedSui) { + requires(is_equal_staking_metadata(self, &other)); + requires(can_add_u64(staked_sui_amount(self), staked_sui_amount(&other))); // or the join overflows + join_staked_sui(self, other); +} diff --git a/crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move b/crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move new file mode 100644 index 000000000000..16e2d1292fbb --- /dev/null +++ b/crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move @@ -0,0 +1,27 @@ +module sui_system_specs::storage_fund; + +#[spec_only] +use sui_system::storage_fund::{ + StorageFund, + total_object_storage_rebates, + non_refundable_balance, + total_balance, +}; + +#[spec_only] +use sui_system_specs::helpers::can_add_u64; + +#[spec_only] +use prover::prover::requires; + + +#[spec(prove, no_opaque, target = sui_system::storage_fund::total_object_storage_rebates)] +public fun total_object_storage_rebates_spec(self: &StorageFund): u64 { + total_object_storage_rebates(self) +} + +#[spec(prove, target = sui_system::storage_fund::total_balance)] +public fun total_balance_spec(self: &StorageFund): u64 { + requires(can_add_u64(total_object_storage_rebates(self), non_refundable_balance(self))); + total_balance(self) +} diff --git a/crates/sui-framework/packages/sui-system-specs/sources/validator.move b/crates/sui-framework/packages/sui-system-specs/sources/validator.move new file mode 100644 index 000000000000..d3473417eadc --- /dev/null +++ b/crates/sui-framework/packages/sui-system-specs/sources/validator.move @@ -0,0 +1,65 @@ +#[allow(unused_const)] +module sui_system_specs::validator; + +#[spec_only] +use sui_system::staking_pool::{ + PoolTokenExchangeRate, +}; + +#[spec_only] +use sui_system::validator::{ + Validator, + ValidatorMetadata, + is_preactive, + is_duplicate, + validate_metadata, + validate_metadata_bcs, + staking_pool_id, + pool_token_exchange_rate_at_epoch, + pool_activation_epoch, +}; +#[spec_only] +use sui_system::validator_cap::{Self, ValidatorOperationCap}; + +#[spec_only] +use prover::prover::requires; + +#[spec_only] +public fun pool_activation_epoch_is_positive(validator: &Validator): bool { + let epoch_opt = pool_activation_epoch(validator); + epoch_opt.is_some() && + *epoch_opt.borrow() > 0 +} + +#[spec(prove, no_opaque, target = sui_system::validator::is_preactive)] +public fun is_preactive_spec(self: &Validator): bool { + is_preactive(self) +} + +#[spec(prove, target = sui_system::validator::pool_token_exchange_rate_at_epoch)] +public fun pool_token_exchange_rate_at_epoch_spec(self: &Validator, epoch: u64): PoolTokenExchangeRate { + requires(!is_preactive(self)); + requires(pool_activation_epoch_is_positive(self)); + pool_token_exchange_rate_at_epoch(self, epoch) +} + +#[spec(prove, no_opaque, target = sui_system::validator::staking_pool_id)] +public fun staking_pool_id_spec(self: &Validator): ID { + staking_pool_id(self) +} + +#[spec(prove, target = sui_system::validator::is_duplicate)] +public fun is_duplicate_spec(self: &Validator, other: &Validator): bool { + is_duplicate(self, other) +} + +#[spec(prove, target = sui_system::validator::validate_metadata)] +public fun validate_metadata_spec(metadata: &ValidatorMetadata) { + validate_metadata(metadata); +} + +// "aborts if metadata is not valid" -- how to capture? +#[spec(target = sui_system::validator::validate_metadata_bcs)] +public fun validate_metadata_bcs_spec(metadata: vector) { + validate_metadata_bcs(metadata); +} diff --git a/crates/sui-framework/packages/sui-system/Move.lock b/crates/sui-framework/packages/sui-system/Move.lock index 01df77464e50..60beaf60ebad 100644 --- a/crates/sui-framework/packages/sui-system/Move.lock +++ b/crates/sui-framework/packages/sui-system/Move.lock @@ -2,29 +2,17 @@ [move] version = 3 -manifest_digest = "05062993DFF0CEB4183CF4B07640698C2BFD8B7B66CEAE02DE3B49334C09F07F" -deps_digest = "E3B0C44298FC1C149AFBF4C8996FB92427AE41E4649B934CA495991B7852B855" - +manifest_digest = "6F0DE69ABABB50F9E478F492F1AFC330895CDEEBBE3BA097A41A528D4C2815F0" +deps_digest = "060AD7E57DFB13104F21BE5F5C3759D03F0553FC3229247D9A7A6B45F50D03A3" dependencies = [ - { id = "DeepBook", name = "DeepBook" }, { id = "MoveStdlib", name = "MoveStdlib" }, { id = "Sui", name = "Sui" }, { id = "SuiProver", name = "SuiProver" }, - # { id = "SuiSystem", name = "SuiSystem" }, -] - -[[move.package]] -id = "DeepBook" -source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/deepbook" } - -dependencies = [ - { id = "MoveStdlib", name = "MoveStdlib" }, - { id = "Sui", name = "Sui" }, ] [[move.package]] id = "MoveStdlib" -source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/move-stdlib" } +source = { local = "../move-stdlib" } [[move.package]] id = "Prover" @@ -36,7 +24,7 @@ dependencies = [ [[move.package]] id = "Sui" -source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/sui-framework" } +source = { local = "../sui-framework" } dependencies = [ { id = "MoveStdlib", name = "MoveStdlib" }, @@ -58,18 +46,3 @@ dependencies = [ { id = "Prover", name = "Prover" }, { id = "Sui", name = "Sui" }, ] - -# [[move.package]] -# id = "SuiSystem" -# source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/sui-system" } - -# dependencies = [ -# { id = "MoveStdlib", name = "MoveStdlib" }, -# { id = "Sui", name = "Sui" }, -#] - - -[move.toolchain-version] -compiler-version = "1.22.0" -edition = "legacy" -flavor = "sui" diff --git a/crates/sui-framework/packages/sui-system/Move.toml b/crates/sui-framework/packages/sui-system/Move.toml index 77101056d9f0..98e9236ff9b0 100644 --- a/crates/sui-framework/packages/sui-system/Move.toml +++ b/crates/sui-framework/packages/sui-system/Move.toml @@ -5,8 +5,8 @@ published-at = "0x3" edition = "2024.beta" [dependencies] -# MoveStdlib = { local = "../move-stdlib" } -# Sui = { local = "../sui-framework" } +MoveStdlib = { local = "../move-stdlib" } +Sui = { local = "../sui-framework" } [addresses] sui_system = "0x3" diff --git a/crates/sui-framework/packages/sui-system/sources/other_specs.move b/crates/sui-framework/packages/sui-system/sources/other_specs.move deleted file mode 100644 index 61803c8b8781..000000000000 --- a/crates/sui-framework/packages/sui-system/sources/other_specs.move +++ /dev/null @@ -1,16 +0,0 @@ -/// Specifications for modules used by sui_system, and in particular for functions -/// that cause problems. - -module sui_system::other_specs; - -use sui::tx_context::TxContext; - -#[spec(target=sui::tx_context::epoch)] -public fun epoch_spec(self: &TxContext): u64 { - sui::tx_context::epoch(self) -} - -#[spec(target=sui::tx_context::sender)] -public fun sender_spec(self: &TxContext): address { - sui::tx_context::sender(self) -} diff --git a/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move b/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move index 7f0f4650fc26..bf013e7e11f5 100644 --- a/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move +++ b/crates/sui-framework/packages/sui-system/sources/stake_subsidy.move @@ -89,19 +89,3 @@ public(package) fun get_distribution_counter(self: &StakeSubsidy): u64 { public(package) fun set_distribution_counter(self: &mut StakeSubsidy, distribution_counter: u64) { self.distribution_counter = distribution_counter; } - -// === specifications === - -// This invariant is needed to prove no abort in some of the non-public functions, -// so can be skipped for now. - -// #[spec_only] -// fun StakeSubsidy_inv(x: &StakeSubsidy): bool { -// x.stake_subsidy_decrease_rate <= BASIS_POINT_DENOMINATOR as u16 && -// x.stake_subsidy_period_length > 0 -// } - -#[spec(prove, no_opaque)] -public fun current_epoch_subsidy_amount_spec(self: &StakeSubsidy): u64 { - current_epoch_subsidy_amount(self) -} diff --git a/crates/sui-framework/packages/sui-system/sources/staking_pool.move b/crates/sui-framework/packages/sui-system/sources/staking_pool.move index 64925d7a7ebc..0fc77a9ca028 100644 --- a/crates/sui-framework/packages/sui-system/sources/staking_pool.move +++ b/crates/sui-framework/packages/sui-system/sources/staking_pool.move @@ -774,98 +774,3 @@ fun test_calculate_fungible_staked_sui_withdraw_amount( let min_out = if (expected_out > 2) expected_out - 2 else 0; assert!(principal_amount + rewards_amount >= min_out, 0); } - -// === specifications === - -#[spec_only] -use prover::prover::{requires, ensures}; - -#[spec_only] -use prover::ghost; - -#[spec_only] -use sui_system::helpers::{can_add_u64}; - - -#[spec(prove, no_opaque)] -public fun staked_sui_amount_spec(staked_sui: &StakedSui): u64 { - staked_sui_amount(staked_sui) -} - -#[spec(prove, no_opaque)] -public fun is_preactive_spec(pool: &StakingPool): bool { - is_preactive(pool) -} - -#[spec(prove, no_opaque)] -public fun is_inactive_spec(pool: &StakingPool): bool { - is_inactive(pool) -} - -#[spec(prove)] -public fun split_fungible_staked_sui_spec( - fungible_staked_sui: &mut FungibleStakedSui, - split_amount: u64, - ctx: &mut TxContext, -): FungibleStakedSui { - requires(split_amount <= fungible_staked_sui_value(fungible_staked_sui)); - split_fungible_staked_sui(fungible_staked_sui, split_amount, ctx) -} - -#[spec(prove)] -public fun join_fungible_staked_sui_spec(self: &mut FungibleStakedSui, other: FungibleStakedSui) { - requires(self.pool_id() == other.pool_id()); - requires(can_add_u64(self.value(), other.value())); - join_fungible_staked_sui(self, other); -} - -#[spec(prove)] -public fun split_spec(self: &mut StakedSui, split_amount: u64, ctx: &mut TxContext): StakedSui { - requires(split_amount <= self.principal.value()); - requires(split_amount >= MIN_STAKING_THRESHOLD); - requires(self.principal.value() - split_amount >= MIN_STAKING_THRESHOLD); - split(self, split_amount, ctx) -} - -#[spec(prove, no_opaque)] -public fun is_equal_staking_metadata_spec(self: &StakedSui, other: &StakedSui): bool { - is_equal_staking_metadata(self, other) -} - -#[spec_only] -/// function needed to make the requirements of `pool_token_exchange_rate_at_epoch_spec` -/// expressible outside this module. -public fun activation_epoch_is_positive(pool: &StakingPool): bool { - pool.activation_epoch.is_some() && - *pool.activation_epoch.borrow() > 0 -} - -#[spec(prove)] -public fun pool_token_exchange_rate_at_epoch_spec( - pool: &StakingPool, - epoch: u64, -): PoolTokenExchangeRate { - requires(! pool.is_preactive()); - // requires(*pool.activation_epoch.borrow() > 0); // visible? add to invariant? - requires(activation_epoch_is_positive(pool)); - pool_token_exchange_rate_at_epoch(pool, epoch) -} - -#[spec(prove)] -public fun split_staked_sui_spec(stake: &mut StakedSui, split_amount: u64, ctx: &mut TxContext) { - use specs::transfer_spec::{SpecTransferAddress,SpecTransferAddressExists}; - ghost::declare_global_mut(); - ghost::declare_global_mut(); - // preconditions from the call to split: - requires(split_amount <= stake.principal.value()); - requires(split_amount >= MIN_STAKING_THRESHOLD); - requires(stake.principal.value() - split_amount >= MIN_STAKING_THRESHOLD); - split_staked_sui(stake, split_amount, ctx); -} - -#[spec(prove)] -public fun join_staked_sui_spec(self: &mut StakedSui, other: StakedSui) { - requires(is_equal_staking_metadata(self, &other)); - requires(can_add_u64(self.principal.value(), other.principal.value())); // or the join overflows - join_staked_sui(self, other); -} diff --git a/crates/sui-framework/packages/sui-system/sources/storage_fund.move b/crates/sui-framework/packages/sui-system/sources/storage_fund.move index bf9cb90d4f48..5a572b118bd8 100644 --- a/crates/sui-framework/packages/sui-system/sources/storage_fund.move +++ b/crates/sui-framework/packages/sui-system/sources/storage_fund.move @@ -70,23 +70,9 @@ public fun total_balance(self: &StorageFund): u64 { self.total_object_storage_rebates.value() + self.non_refundable_balance.value() } -// === specifications === +// === specs utils === #[spec_only] -use prover::prover::requires; - -#[spec_only] -use sui_system::helpers::can_add_u64; - -#[spec(prove, no_opaque)] -public fun total_object_storage_rebates_spec(self: &StorageFund): u64 { - total_object_storage_rebates(self) -} - -// This precondition is not useful to a caller; it mentions fields that are not caller-visible -#[spec(prove)] -public fun total_balance_spec(self: &StorageFund): u64 { - requires(can_add_u64(self.total_object_storage_rebates.value(), - self.non_refundable_balance.value())); - total_balance(self) +public fun non_refundable_balance(self: &StorageFund): u64 { + self.non_refundable_balance.value() } diff --git a/crates/sui-framework/packages/sui-system/sources/validator.move b/crates/sui-framework/packages/sui-system/sources/validator.move index 05950745f906..094778439656 100644 --- a/crates/sui-framework/packages/sui-system/sources/validator.move +++ b/crates/sui-framework/packages/sui-system/sources/validator.move @@ -996,41 +996,12 @@ public(package) fun new_for_testing( validator } -// === specifications and proofs === +// === specs utils === #[spec_only] -use prover::prover::{requires, ensures}; +use sui_system::staking_pool::activation_epoch; -#[spec(prove, no_opaque)] -public fun is_preactive_spec(self: &Validator): bool { - is_preactive(self) -} - -#[spec(prove)] -public fun pool_token_exchange_rate_at_epoch_spec(self: &Validator, epoch: u64): PoolTokenExchangeRate { - requires(! self.is_preactive()); - requires(staking_pool::activation_epoch_is_positive(&self.staking_pool)); - pool_token_exchange_rate_at_epoch(self, epoch) -} - -#[spec(prove, no_opaque)] -public fun staking_pool_id_spec(self: &Validator): ID { - staking_pool_id(self) -} - -#[spec(prove)] -public fun is_duplicate_spec(self: &Validator, other: &Validator): bool { - is_duplicate(self, other) -} - -#[spec(prove)] -public fun validate_metadata_spec(metadata: &ValidatorMetadata) { - validate_metadata(metadata); -} -// - -// "aborts if metadata is not valid" -- how to capture? -#[spec] -public fun validate_metadata_bcs_spec(metadata: vector) { - validate_metadata_bcs(metadata); +#[spec_only] +public fun pool_activation_epoch(self: &Validator): Option { + activation_epoch(&self.staking_pool) } From 0fb0e07c309814da2e0bf547899581197e0891fe Mon Sep 17 00:00:00 2001 From: Andrii Date: Wed, 20 Aug 2025 13:30:37 +0300 Subject: [PATCH 3/3] lockfile update --- .../packages/sui-system/Move.lock | 33 ++++--------------- 1 file changed, 6 insertions(+), 27 deletions(-) diff --git a/crates/sui-framework/packages/sui-system/Move.lock b/crates/sui-framework/packages/sui-system/Move.lock index 60beaf60ebad..fb23e91fa4f6 100644 --- a/crates/sui-framework/packages/sui-system/Move.lock +++ b/crates/sui-framework/packages/sui-system/Move.lock @@ -2,26 +2,17 @@ [move] version = 3 -manifest_digest = "6F0DE69ABABB50F9E478F492F1AFC330895CDEEBBE3BA097A41A528D4C2815F0" -deps_digest = "060AD7E57DFB13104F21BE5F5C3759D03F0553FC3229247D9A7A6B45F50D03A3" +manifest_digest = "68AEB9354EE1D616F6D2293EC721FE3D7E810FEC4FE34197676ECFA3DA72CAE3" +deps_digest = "3C4103934B1E040BB6B23F1D610B4EF9F2F1166A50A104EADCF77467C004C600" dependencies = [ { id = "MoveStdlib", name = "MoveStdlib" }, { id = "Sui", name = "Sui" }, - { id = "SuiProver", name = "SuiProver" }, ] [[move.package]] id = "MoveStdlib" source = { local = "../move-stdlib" } -[[move.package]] -id = "Prover" -source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/prover" } - -dependencies = [ - { id = "MoveStdlib", name = "MoveStdlib" }, -] - [[move.package]] id = "Sui" source = { local = "../sui-framework" } @@ -30,19 +21,7 @@ dependencies = [ { id = "MoveStdlib", name = "MoveStdlib" }, ] -[[move.package]] -id = "SuiProver" -source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-prover" } - -dependencies = [ - { id = "SuiSpecs", name = "SuiSpecs" }, -] - -[[move.package]] -id = "SuiSpecs" -source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-framework-specs" } - -dependencies = [ - { id = "Prover", name = "Prover" }, - { id = "Sui", name = "Sui" }, -] +[move.toolchain-version] +compiler-version = "1.54.0" +edition = "2024.beta" +flavor = "sui"