More system specs

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";

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<T>(
@@ -19,3 +19,8 @@ public fun emit_withdraw_event_spec<T>(
 ) {
     emit_withdraw_event<T>(accumulator, owner, amount)
 }
+
+#[spec(target = sui::accumulator::accumulator_address)]
+public fun accumulator_address_spec<T>(address: address): address {
+    accumulator_address<T>(address)
+}

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<K: copy + drop + store>(parent: ID, key: K): address {
+    derive_address(parent, key)
+}

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<T: store>(
+    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<T: store>(
+    accumulator: address,
+    owner: address,
+    value: u256,
+): T {
+    withdraw_from_accumulator_address(accumulator, owner, value)
+}