From 5cbb160138286f89cde00b732363bd51e1695626 Mon Sep 17 00:00:00 2001 From: Igor Date: Fri, 9 Aug 2024 22:02:09 -0700 Subject: [PATCH] [framework][object] Introduce ability to recreate objects after deletion --- .../framework/aptos-framework/doc/event.md | 10 +- .../framework/aptos-framework/doc/object.md | 360 ++++++++++++++++-- .../aptos-framework/sources/event.move | 6 +- .../aptos-framework/sources/object.move | 130 ++++++- .../aptos-framework/sources/object.spec.move | 18 +- 5 files changed, 472 insertions(+), 52 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/event.md b/aptos-move/framework/aptos-framework/doc/event.md index 7bf257ff41fe7..215b41ed9e6e3 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 cb633a173bf6c..243b780a1626d 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,
+    }
 }
 
@@ -2573,14 +2885,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;
 
@@ -2955,15 +3267,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 };
 
@@ -3043,14 +3355,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 542808163e88e..9cad393cfc9e4 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 abca67bb2451a..3786f82b9a8c3 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 = 10; /// 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 51ae05b568368..43911e812aa49 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) {