diff --git a/crates/move-model/src/model.rs b/crates/move-model/src/model.rs index 8fd2f132ea..e68a2656e8 100644 --- a/crates/move-model/src/model.rs +++ b/crates/move-model/src/model.rs @@ -1539,6 +1539,8 @@ impl GlobalEnv { "vdf_spec", "zklogin_verified_id_spec", "zklogin_verified_issuer_spec", + "derived_object_spec", + "funds_accumulator_spec", ]; const LOG_MODULE_NAME: &'static str = "log"; const VECTOR_MODULE_NAME: &'static str = "vector"; diff --git a/packages/sui-specs/sources/sui-framework/accumulator.move b/packages/sui-specs/sources/sui-framework/accumulator.move index fd514304a8..61960c7bd2 100644 --- a/packages/sui-specs/sources/sui-framework/accumulator.move +++ b/packages/sui-specs/sources/sui-framework/accumulator.move @@ -1,6 +1,6 @@ module specs::accumulator_spec; -use sui::accumulator::{emit_deposit_event, emit_withdraw_event}; +use sui::accumulator::{emit_deposit_event, emit_withdraw_event, accumulator_address}; #[spec(target = sui::accumulator::emit_deposit_event)] public fun emit_deposit_event_spec( @@ -19,3 +19,8 @@ public fun emit_withdraw_event_spec( ) { emit_withdraw_event(accumulator, owner, amount) } + +#[spec(target = sui::accumulator::accumulator_address)] +public fun accumulator_address_spec(address: address): address { + accumulator_address(address) +} diff --git a/packages/sui-specs/sources/sui-framework/derived_object.move b/packages/sui-specs/sources/sui-framework/derived_object.move new file mode 100644 index 0000000000..8b1a43eb3a --- /dev/null +++ b/packages/sui-specs/sources/sui-framework/derived_object.move @@ -0,0 +1,8 @@ +module specs::derived_object_spec; + +use sui::derived_object::derive_address; + +#[spec(target = sui::derived_object::derive_address)] +public fun derive_address_spec(parent: ID, key: K): address { + derive_address(parent, key) +} diff --git a/packages/sui-specs/sources/sui-framework/funds_accumulator.move b/packages/sui-specs/sources/sui-framework/funds_accumulator.move new file mode 100644 index 0000000000..6f1064be0a --- /dev/null +++ b/packages/sui-specs/sources/sui-framework/funds_accumulator.move @@ -0,0 +1,22 @@ +module specs::funds_accumulator_spec; + +use sui::funds_accumulator::{add_to_accumulator_address, withdraw_from_accumulator_address}; + + +#[spec(target = sui::funds_accumulator::add_to_accumulator_address)] +public fun add_to_accumulator_address_spec( + accumulator: address, + recipient: address, + value: T, +) { + add_to_accumulator_address(accumulator, recipient, value) +} + +#[spec(target = sui::funds_accumulator::withdraw_from_accumulator_address)] +public fun withdraw_from_accumulator_address_spec( + accumulator: address, + owner: address, + value: u256, +): T { + withdraw_from_accumulator_address(accumulator, owner, value) +}