diff --git a/aptos-move/framework/aptos-framework/doc/event.md b/aptos-move/framework/aptos-framework/doc/event.md
index 7bf257ff41fe76..215b41ed9e6e32 100644
--- a/aptos-move/framework/aptos-framework/doc/event.md
+++ b/aptos-move/framework/aptos-framework/doc/event.md
@@ -46,7 +46,7 @@ A handle for an event such that:
#[deprecated]
-struct EventHandle<T: drop, store> has store
+struct EventHandle<T: drop, store> has drop, store
@@ -264,7 +264,7 @@ Destroy a unique handle.
#[deprecated]
-public fun destroy_handle<T: drop, store>(handle: event::EventHandle<T>)
+public fun destroy_handle<T: drop, store>(self: event::EventHandle<T>)
@@ -273,8 +273,8 @@ Destroy a unique handle.
Implementation
-public fun destroy_handle<T: drop + store>(handle: EventHandle<T>) {
- EventHandle<T> { counter: _, guid: _ } = handle;
+public fun destroy_handle<T: drop + store>(self: EventHandle<T>) {
+ EventHandle<T> { counter: _, guid: _ } = self;
}
@@ -466,7 +466,7 @@ Native function use opaque.
#[deprecated]
-public fun destroy_handle<T: drop, store>(handle: event::EventHandle<T>)
+public fun destroy_handle<T: drop, store>(self: event::EventHandle<T>)
diff --git a/aptos-move/framework/aptos-framework/doc/object.md b/aptos-move/framework/aptos-framework/doc/object.md
index 7ae33a425ee25f..4b8164d0b4ef61 100644
--- a/aptos-move/framework/aptos-framework/doc/object.md
+++ b/aptos-move/framework/aptos-framework/doc/object.md
@@ -28,10 +28,12 @@ make it so that a reference to a global object can be returned from a function.
- [Struct `Object`](#0x1_object_Object)
- [Struct `ConstructorRef`](#0x1_object_ConstructorRef)
- [Struct `DeleteRef`](#0x1_object_DeleteRef)
+- [Struct `DeleteAndRecreateRef`](#0x1_object_DeleteAndRecreateRef)
- [Struct `ExtendRef`](#0x1_object_ExtendRef)
- [Struct `TransferRef`](#0x1_object_TransferRef)
- [Struct `LinearTransferRef`](#0x1_object_LinearTransferRef)
- [Struct `DeriveRef`](#0x1_object_DeriveRef)
+- [Enum `CreateAtAddressRef`](#0x1_object_CreateAtAddressRef)
- [Struct `TransferEvent`](#0x1_object_TransferEvent)
- [Struct `Transfer`](#0x1_object_Transfer)
- [Constants](#@Constants_0)
@@ -50,6 +52,7 @@ make it so that a reference to a global object can be returned from a function.
- [Function `create_named_object`](#0x1_object_create_named_object)
- [Function `create_user_derived_object`](#0x1_object_create_user_derived_object)
- [Function `create_object`](#0x1_object_create_object)
+- [Function `create_object_at_address_from_ref`](#0x1_object_create_object_at_address_from_ref)
- [Function `create_sticky_object`](#0x1_object_create_sticky_object)
- [Function `create_sticky_object_at_address`](#0x1_object_create_sticky_object_at_address)
- [Function `create_object_from_account`](#0x1_object_create_object_from_account)
@@ -57,6 +60,7 @@ make it so that a reference to a global object can be returned from a function.
- [Function `create_object_from_guid`](#0x1_object_create_object_from_guid)
- [Function `create_object_internal`](#0x1_object_create_object_internal)
- [Function `generate_delete_ref`](#0x1_object_generate_delete_ref)
+- [Function `generate_delete_and_recreate_ref`](#0x1_object_generate_delete_and_recreate_ref)
- [Function `generate_extend_ref`](#0x1_object_generate_extend_ref)
- [Function `generate_transfer_ref`](#0x1_object_generate_transfer_ref)
- [Function `generate_derive_ref`](#0x1_object_generate_derive_ref)
@@ -64,11 +68,15 @@ make it so that a reference to a global object can be returned from a function.
- [Function `address_from_constructor_ref`](#0x1_object_address_from_constructor_ref)
- [Function `object_from_constructor_ref`](#0x1_object_object_from_constructor_ref)
- [Function `can_generate_delete_ref`](#0x1_object_can_generate_delete_ref)
+- [Function `address_from_create_at_ref`](#0x1_object_address_from_create_at_ref)
- [Function `create_guid`](#0x1_object_create_guid)
- [Function `new_event_handle`](#0x1_object_new_event_handle)
- [Function `address_from_delete_ref`](#0x1_object_address_from_delete_ref)
- [Function `object_from_delete_ref`](#0x1_object_object_from_delete_ref)
- [Function `delete`](#0x1_object_delete)
+- [Function `address_from_delete_and_recreate_ref`](#0x1_object_address_from_delete_and_recreate_ref)
+- [Function `object_from_delete_and_recreate_ref`](#0x1_object_object_from_delete_and_recreate_ref)
+- [Function `delete_and_can_recreate`](#0x1_object_delete_and_can_recreate)
- [Function `generate_signer_for_extending`](#0x1_object_generate_signer_for_extending)
- [Function `address_from_extend_ref`](#0x1_object_address_from_extend_ref)
- [Function `disable_ungated_transfer`](#0x1_object_disable_ungated_transfer)
@@ -363,6 +371,34 @@ Used to remove an object from storage.
+
+Fields
+
+
+
+-
+
self: address
+
+-
+
+
+
+
+
+
+
+
+
+## Struct `DeleteAndRecreateRef`
+
+Used to remove an object from storage, such that it can be created again
+
+
+struct DeleteAndRecreateRef has drop, store
+
+
+
+
Fields
@@ -496,6 +532,70 @@ Used to create derived objects from a given objects.
+
+
+
+
+## Enum `CreateAtAddressRef`
+
+Used to (re)create object at a given address
+
+
+enum CreateAtAddressRef has drop, store
+
+
+
+
+
+Variants
+
+
+
+RecreateV1
+
+
+
+Fields
+
+
+
+-
+
object: address
+
+-
+
+
+-
+
owner: address
+
+-
+
+
+-
+
guid_creation_num: u64
+
+-
+
+
+-
+
untransferable: bool
+
+-
+
+
+-
+
allow_ungated_transfer: bool
+
+-
+
+
+
+
+
+
+
+
+
@@ -704,6 +804,16 @@ The resource is not stored at the specified address.
+
+
+Cannot delete_and_can_recreate with TombStone present.
+
+
+const ETOMBSTONE_CANNOT_BE_PRESENT: u64 = 10;
+
+
+
+
Explicitly separate the GUID space between Object and Account to prevent accidental overlap.
@@ -1040,7 +1150,7 @@ Derives an object from an Account GUID.
Returns the address of within an ObjectId.
-public fun object_address<T: key>(object: &object::Object<T>): address
+public fun object_address<T: key>(self: &object::Object<T>): address
@@ -1049,8 +1159,8 @@ Returns the address of within an ObjectId.
Implementation
-public fun object_address<T: key>(object: &Object<T>): address {
- object.inner
+public fun object_address<T: key>(self: &Object<T>): address {
+ self.inner
}
@@ -1165,6 +1275,54 @@ never be regenerated with future txs.
+
+
+
+
+## Function `create_object_at_address_from_ref`
+
+
+
+public fun create_object_at_address_from_ref(create_ref: object::CreateAtAddressRef): object::ConstructorRef
+
+
+
+
+
+Implementation
+
+
+public fun create_object_at_address_from_ref(create_ref: CreateAtAddressRef): ConstructorRef {
+ let CreateAtAddressRef::RecreateV1 {
+ object, owner, guid_creation_num, untransferable, allow_ungated_transfer,
+ } = create_ref;
+
+ assert!(!exists<ObjectCore>(object), error::already_exists(EOBJECT_EXISTS));
+
+ let object_signer = create_signer(object);
+ let transfer_events_guid = guid::create(object, &mut guid_creation_num);
+
+ move_to(
+ &object_signer,
+ ObjectCore {
+ guid_creation_num,
+ owner,
+ allow_ungated_transfer,
+ // since transfer_events is not used any more, it is perfectly fine
+ // to create a new handle, when recreating.
+ transfer_events: event::new_event_handle(transfer_events_guid),
+ },
+ );
+
+ if (untransferable) {
+ move_to(&object_signer, Untransferable {});
+ };
+ ConstructorRef { self: object, can_delete: true }
+}
+
+
+
+
@@ -1379,6 +1537,31 @@ Generates the DeleteRef, which can be used to remove ObjectCore from global stor
+
+
+
+
+## Function `generate_delete_and_recreate_ref`
+
+
+
+public fun generate_delete_and_recreate_ref(self: &object::ConstructorRef): object::DeleteAndRecreateRef
+
+
+
+
+
+Implementation
+
+
+public fun generate_delete_and_recreate_ref(self: &ConstructorRef): DeleteAndRecreateRef {
+ assert!(self.can_delete, error::permission_denied(ECANNOT_DELETE));
+ DeleteAndRecreateRef { self: self.self }
+}
+
+
+
+
@@ -1489,7 +1672,7 @@ Create a signer for the ConstructorRef
Returns the address associated with the constructor
-public fun address_from_constructor_ref(ref: &object::ConstructorRef): address
+public fun address_from_constructor_ref(self: &object::ConstructorRef): address
@@ -1498,8 +1681,8 @@ Returns the address associated with the constructor
Implementation
-public fun address_from_constructor_ref(ref: &ConstructorRef): address {
- ref.self
+public fun address_from_constructor_ref(self: &ConstructorRef): address {
+ self.self
}
@@ -1514,7 +1697,7 @@ Returns the address associated with the constructor
Returns an Object from within a ConstructorRef
-public fun object_from_constructor_ref<T: key>(ref: &object::ConstructorRef): object::Object<T>
+public fun object_from_constructor_ref<T: key>(self: &object::ConstructorRef): object::Object<T>
@@ -1523,8 +1706,8 @@ Returns an Object from within a ConstructorRef
Implementation
-public fun object_from_constructor_ref<T: key>(ref: &ConstructorRef): Object<T> {
- address_to_object<T>(ref.self)
+public fun object_from_constructor_ref<T: key>(self: &ConstructorRef): Object<T> {
+ address_to_object<T>(self.self)
}
@@ -1555,6 +1738,30 @@ Returns whether or not the ConstructorRef can be used to create DeleteRef
+
+
+
+
+## Function `address_from_create_at_ref`
+
+
+
+public fun address_from_create_at_ref(ref: &object::CreateAtAddressRef): address
+
+
+
+
+
+Implementation
+
+
+public fun address_from_create_at_ref(ref: &CreateAtAddressRef): address {
+ ref.object
+}
+
+
+
+
@@ -1668,7 +1875,7 @@ Returns an Object from within a DeleteRef.
Removes from the specified Object from global storage.
-public fun delete(ref: object::DeleteRef)
+public fun delete(self: object::DeleteRef)
@@ -1677,8 +1884,8 @@ Removes from the specified Object from global storage.
Implementation
-public fun delete(ref: DeleteRef) acquires Untransferable, ObjectCore {
- let object_core = move_from<ObjectCore>(ref.self);
+public fun delete(self: DeleteRef) acquires Untransferable, ObjectCore, TombStone {
+ let object_core = move_from<ObjectCore>(self.self);
let ObjectCore {
guid_creation_num: _,
owner: _,
@@ -1686,11 +1893,116 @@ Removes from the specified Object from global storage.
transfer_events,
} = object_core;
- if (exists<Untransferable>(ref.self)) {
- let Untransferable {} = move_from<Untransferable>(ref.self);
+ transfer_events.destroy_handle();
+
+ if (exists<Untransferable>(self.self)) {
+ let Untransferable {} = move_from<Untransferable>(self.self);
};
- event::destroy_handle(transfer_events);
+ // Since we are fully deleting the object, remove TombStone
+ if (exists<TombStone>(self.self)) {
+ let TombStone { original_owner: _ } = move_from<TombStone>(self.self);
+ };
+}
+
+
+
+
+
+
+
+
+## Function `address_from_delete_and_recreate_ref`
+
+Returns the address associated with the constructor
+
+
+public fun address_from_delete_and_recreate_ref(self: &object::DeleteAndRecreateRef): address
+
+
+
+
+
+Implementation
+
+
+public fun address_from_delete_and_recreate_ref(self: &DeleteAndRecreateRef): address {
+ self.self
+}
+
+
+
+
+
+
+
+
+## Function `object_from_delete_and_recreate_ref`
+
+Returns an Object from within a DeleteRef.
+
+
+public fun object_from_delete_and_recreate_ref<T: key>(self: &object::DeleteAndRecreateRef): object::Object<T>
+
+
+
+
+
+Implementation
+
+
+public fun object_from_delete_and_recreate_ref<T: key>(self: &DeleteAndRecreateRef): Object<T> {
+ address_to_object<T>(self.self)
+}
+
+
+
+
+
+
+
+
+## Function `delete_and_can_recreate`
+
+Removes from the specified Object from global storage, and returns a handle to be able to recreate it
+
+
+public fun delete_and_can_recreate(self: object::DeleteAndRecreateRef): object::CreateAtAddressRef
+
+
+
+
+
+Implementation
+
+
+public fun delete_and_can_recreate(self: DeleteAndRecreateRef): CreateAtAddressRef acquires Untransferable, ObjectCore {
+ // We don't want to track TombStone through delete_and_can_recreate, and since TombStone is deprecated,
+ // don't support objects with it.
+ assert!(!exists<TombStone>(self.self), error::invalid_state(ETOMBSTONE_CANNOT_BE_PRESENT));
+
+ let object_core = move_from<ObjectCore>(self.self);
+ let ObjectCore {
+ guid_creation_num,
+ owner,
+ allow_ungated_transfer,
+ transfer_events,
+ } = object_core;
+
+ transfer_events.destroy_handle();
+
+ let untransferable = exists<Untransferable>(self.self);
+ if (untransferable) {
+ let Untransferable {} = move_from<Untransferable>(self.self);
+ };
+
+ CreateAtAddressRef::RecreateV1 {
+ object: self.self,
+ owner,
+ guid_creation_num,
+ untransferable,
+ allow_ungated_transfer,
+ }
}
@@ -2574,14 +2886,14 @@ to determine the identity of the starting point of ownership.
### Function `object_address`
-public fun object_address<T: key>(object: &object::Object<T>): address
+public fun object_address<T: key>(self: &object::Object<T>): address
aborts_if false;
-ensures result == object.inner;
+ensures result == self.inner;
@@ -2956,15 +3268,15 @@ to determine the identity of the starting point of ownership.
### Function `object_from_constructor_ref`
-public fun object_from_constructor_ref<T: key>(ref: &object::ConstructorRef): object::Object<T>
+public fun object_from_constructor_ref<T: key>(self: &object::ConstructorRef): object::Object<T>
-aborts_if !exists<ObjectCore>(ref.self);
-aborts_if !spec_exists_at<T>(ref.self);
-ensures result == Object<T> { inner: ref.self };
+aborts_if !exists<ObjectCore>(self.self);
+aborts_if !spec_exists_at<T>(self.self);
+ensures result == Object<T> { inner: self.self };
@@ -3044,14 +3356,14 @@ to determine the identity of the starting point of ownership.
### Function `delete`
-public fun delete(ref: object::DeleteRef)
+public fun delete(self: object::DeleteRef)
-aborts_if !exists<ObjectCore>(ref.self);
-ensures !exists<ObjectCore>(ref.self);
+aborts_if !exists<ObjectCore>(self.self);
+ensures !exists<ObjectCore>(self.self);
diff --git a/aptos-move/framework/aptos-framework/sources/event.move b/aptos-move/framework/aptos-framework/sources/event.move
index 542808163e88ea..9cad393cfc9e4e 100644
--- a/aptos-move/framework/aptos-framework/sources/event.move
+++ b/aptos-move/framework/aptos-framework/sources/event.move
@@ -31,7 +31,7 @@ module aptos_framework::event {
/// A handle for an event such that:
/// 1. Other modules can emit events to this handle.
/// 2. Storage can use this handle to prove the total number of events that happened in the past.
- struct EventHandle has store {
+ struct EventHandle has drop, store {
/// Total number of events emitted to this event stream.
counter: u64,
/// A globally unique ID for this event stream.
@@ -75,8 +75,8 @@ module aptos_framework::event {
#[deprecated]
/// Destroy a unique handle.
- public fun destroy_handle(handle: EventHandle) {
- EventHandle { counter: _, guid: _ } = handle;
+ public fun destroy_handle(self: EventHandle) {
+ EventHandle { counter: _, guid: _ } = self;
}
#[deprecated]
diff --git a/aptos-move/framework/aptos-framework/sources/object.move b/aptos-move/framework/aptos-framework/sources/object.move
index bb6684ff6f430c..239fa88d468761 100644
--- a/aptos-move/framework/aptos-framework/sources/object.move
+++ b/aptos-move/framework/aptos-framework/sources/object.move
@@ -52,6 +52,8 @@ module aptos_framework::object {
const EOBJECT_NOT_TRANSFERRABLE: u64 = 9;
/// Objects cannot be burnt
const EBURN_NOT_ALLOWED: u64 = 10;
+ /// Cannot delete_and_can_recreate with TombStone present.
+ const ETOMBSTONE_CANNOT_BE_PRESENT: u64 = 11;
/// Explicitly separate the GUID space between Object and Account to prevent accidental overlap.
const INIT_GUID_CREATION_NUM: u64 = 0x4000000000000;
@@ -143,6 +145,11 @@ module aptos_framework::object {
self: address,
}
+ /// Used to remove an object from storage, such that it can be created again
+ struct DeleteAndRecreateRef has drop, store {
+ self: address,
+ }
+
/// Used to create events or move additional resources into object storage.
struct ExtendRef has drop, store {
self: address,
@@ -165,6 +172,17 @@ module aptos_framework::object {
self: address,
}
+ /// Used to (re)create object at a given address
+ enum CreateAtAddressRef has drop, store {
+ RecreateV1 {
+ object: address,
+ owner: address,
+ guid_creation_num: u64,
+ untransferable: bool,
+ allow_ungated_transfer: bool,
+ },
+ }
+
/// Emitted whenever the object's owner field is changed.
struct TransferEvent has drop, store {
object: address,
@@ -240,8 +258,8 @@ module aptos_framework::object {
native fun exists_at(object: address): bool;
/// Returns the address of within an ObjectId.
- public fun object_address(object: &Object): address {
- object.inner
+ public fun object_address(self: &Object): address {
+ self.inner
}
/// Convert Object to Object.
@@ -273,6 +291,42 @@ module aptos_framework::object {
create_object_internal(owner_address, unique_address, true)
}
+ // TODO this should probably not return ConstructorRef
+ public fun create_object_at_address_from_ref(create_ref: CreateAtAddressRef): ConstructorRef {
+ let CreateAtAddressRef::RecreateV1 {
+ object, owner, guid_creation_num, untransferable, allow_ungated_transfer,
+ } = create_ref;
+
+ assert!(!exists(object), error::already_exists(EOBJECT_EXISTS));
+
+ let object_signer = create_signer(object);
+ let transfer_events_guid = guid::create(object, &mut guid_creation_num);
+
+ move_to(
+ &object_signer,
+ ObjectCore {
+ guid_creation_num,
+ owner,
+ allow_ungated_transfer,
+ // since transfer_events is not used any more, it is perfectly fine
+ // to create a new handle, when recreating.
+ transfer_events: event::new_event_handle(transfer_events_guid),
+ },
+ );
+
+ if (untransferable) {
+ move_to(&object_signer, Untransferable {});
+ };
+ ConstructorRef { self: object, can_delete: true }
+ }
+
+ // /// Create an address where we can create an object in the future.
+ // public fun create_at_address_ref(): CreateAtAddressRef {
+ // CreateAtAddressRef {
+ // object: transaction_context::generate_auid_address(),
+ // }
+ // }
+
/// Same as `create_object` except the object to be created will be undeletable.
public fun create_sticky_object(owner_address: address): ConstructorRef {
let unique_address = transaction_context::generate_auid_address();
@@ -349,6 +403,11 @@ module aptos_framework::object {
DeleteRef { self: ref.self }
}
+ public fun generate_delete_and_recreate_ref(self: &ConstructorRef): DeleteAndRecreateRef {
+ assert!(self.can_delete, error::permission_denied(ECANNOT_DELETE));
+ DeleteAndRecreateRef { self: self.self }
+ }
+
/// Generates the ExtendRef, which can be used to add new events and resources to the object.
public fun generate_extend_ref(ref: &ConstructorRef): ExtendRef {
ExtendRef { self: ref.self }
@@ -371,13 +430,13 @@ module aptos_framework::object {
}
/// Returns the address associated with the constructor
- public fun address_from_constructor_ref(ref: &ConstructorRef): address {
- ref.self
+ public fun address_from_constructor_ref(self: &ConstructorRef): address {
+ self.self
}
/// Returns an Object from within a ConstructorRef
- public fun object_from_constructor_ref(ref: &ConstructorRef): Object {
- address_to_object(ref.self)
+ public fun object_from_constructor_ref(self: &ConstructorRef): Object {
+ address_to_object(self.self)
}
/// Returns whether or not the ConstructorRef can be used to create DeleteRef
@@ -385,6 +444,10 @@ module aptos_framework::object {
ref.can_delete
}
+ public fun address_from_create_at_ref(ref: &CreateAtAddressRef): address {
+ ref.object
+ }
+
// Signer required functions
/// Create a guid for the object, typically used for events
@@ -414,8 +477,8 @@ module aptos_framework::object {
}
/// Removes from the specified Object from global storage.
- public fun delete(ref: DeleteRef) acquires Untransferable, ObjectCore {
- let object_core = move_from(ref.self);
+ public fun delete(self: DeleteRef) acquires Untransferable, ObjectCore, TombStone {
+ let object_core = move_from(self.self);
let ObjectCore {
guid_creation_num: _,
owner: _,
@@ -423,11 +486,56 @@ module aptos_framework::object {
transfer_events,
} = object_core;
- if (exists(ref.self)) {
- let Untransferable {} = move_from(ref.self);
+ transfer_events.destroy_handle();
+
+ if (exists(self.self)) {
+ let Untransferable {} = move_from(self.self);
};
- event::destroy_handle(transfer_events);
+ // Since we are fully deleting the object, remove TombStone
+ if (exists(self.self)) {
+ let TombStone { original_owner: _ } = move_from(self.self);
+ };
+ }
+
+ /// Returns the address associated with the constructor
+ public fun address_from_delete_and_recreate_ref(self: &DeleteAndRecreateRef): address {
+ self.self
+ }
+
+ /// Returns an Object from within a DeleteRef.
+ public fun object_from_delete_and_recreate_ref(self: &DeleteAndRecreateRef): Object {
+ address_to_object(self.self)
+ }
+
+ /// Removes from the specified Object from global storage, and returns a handle to be able to recreate it
+ public fun delete_and_can_recreate(self: DeleteAndRecreateRef): CreateAtAddressRef acquires Untransferable, ObjectCore {
+ // We don't want to track TombStone through delete_and_can_recreate, and since TombStone is deprecated,
+ // don't support objects with it.
+ assert!(!exists(self.self), error::invalid_state(ETOMBSTONE_CANNOT_BE_PRESENT));
+
+ let object_core = move_from(self.self);
+ let ObjectCore {
+ guid_creation_num,
+ owner,
+ allow_ungated_transfer,
+ transfer_events,
+ } = object_core;
+
+ transfer_events.destroy_handle();
+
+ let untransferable = exists(self.self);
+ if (untransferable) {
+ let Untransferable {} = move_from(self.self);
+ };
+
+ CreateAtAddressRef::RecreateV1 {
+ object: self.self,
+ owner,
+ guid_creation_num,
+ untransferable,
+ allow_ungated_transfer,
+ }
}
// Extension helpers
diff --git a/aptos-move/framework/aptos-framework/sources/object.spec.move b/aptos-move/framework/aptos-framework/sources/object.spec.move
index 51ae05b568368d..43911e812aa498 100644
--- a/aptos-move/framework/aptos-framework/sources/object.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/object.spec.move
@@ -139,9 +139,9 @@ spec aptos_framework::object {
ensures [abstract] result == spec_create_guid_object_address(source, creation_num);
}
- spec object_address(object: &Object): address {
+ spec object_address(self: &Object): address {
aborts_if false;
- ensures result == object.inner;
+ ensures result == self.inner;
}
spec convert(object: Object): Object {
@@ -335,10 +335,10 @@ spec aptos_framework::object {
ensures global(ref.self).allow_ungated_transfer == false;
}
- spec object_from_constructor_ref(ref: &ConstructorRef): Object {
- aborts_if !exists(ref.self);
- aborts_if !spec_exists_at(ref.self);
- ensures result == Object { inner: ref.self };
+ spec object_from_constructor_ref(self: &ConstructorRef): Object {
+ aborts_if !exists(self.self);
+ aborts_if !spec_exists_at(self.self);
+ ensures result == Object { inner: self.self };
}
spec create_guid(object: &signer): guid::GUID {
@@ -381,9 +381,9 @@ spec aptos_framework::object {
ensures result == Object { inner: ref.self };
}
- spec delete(ref: DeleteRef) {
- aborts_if !exists(ref.self);
- ensures !exists(ref.self);
+ spec delete(self: DeleteRef) {
+ aborts_if !exists(self.self);
+ ensures !exists(self.self);
}
spec set_untransferable(ref: &ConstructorRef) {