Enable the max object nesting check

aptos-move/aptos-release-builder/src/components/feature_flags.rs

@@ -103,6 +103,7 @@ pub enum FeatureFlag {
     ConcurrentFungibleAssets,
     RefundableBytes,
     ObjectCodeDeployment,
+    MaxObjectNestingCheck,
 }
 
 fn generate_features_blob(writer: &CodeWriter, data: &[u64]) {
@@ -264,6 +265,7 @@ impl From<FeatureFlag> for AptosFeatureFlag {
             FeatureFlag::ConcurrentFungibleAssets => AptosFeatureFlag::CONCURRENT_FUNGIBLE_ASSETS,
             FeatureFlag::RefundableBytes => AptosFeatureFlag::REFUNDABLE_BYTES,
             FeatureFlag::ObjectCodeDeployment => AptosFeatureFlag::OBJECT_CODE_DEPLOYMENT,
+            FeatureFlag::MaxObjectNestingCheck => AptosFeatureFlag::MAX_OBJECT_NESTING_CHECK,
         }
     }
 }
@@ -348,6 +350,7 @@ impl From<AptosFeatureFlag> for FeatureFlag {
             AptosFeatureFlag::CONCURRENT_FUNGIBLE_ASSETS => FeatureFlag::ConcurrentFungibleAssets,
             AptosFeatureFlag::REFUNDABLE_BYTES => FeatureFlag::RefundableBytes,
             AptosFeatureFlag::OBJECT_CODE_DEPLOYMENT => FeatureFlag::ObjectCodeDeployment,
+            AptosFeatureFlag::MAX_OBJECT_NESTING_CHECK => FeatureFlag::MaxObjectNestingCheck,
         }
     }
 }

aptos-move/framework/aptos-framework/doc/object.md

@@ -32,7 +32,6 @@ make it so that a reference to a global object can be returned from a function.
 -  [Struct `LinearTransferRef`](#0x1_object_LinearTransferRef)
 -  [Struct `DeriveRef`](#0x1_object_DeriveRef)
 -  [Struct `TransferEvent`](#0x1_object_TransferEvent)
--  [Resource `Ghost$g_roll`](#0x1_object_Ghost$g_roll)
 -  [Constants](#@Constants_0)
 -  [Function `is_burnt`](#0x1_object_is_burnt)
 -  [Function `address_to_object`](#0x1_object_address_to_object)
@@ -129,6 +128,7 @@ make it so that a reference to a global object can be returned from a function.
 <b>use</b> <a href="create_signer.md#0x1_create_signer">0x1::create_signer</a>;
 <b>use</b> <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error">0x1::error</a>;
 <b>use</b> <a href="event.md#0x1_event">0x1::event</a>;
+<b>use</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features">0x1::features</a>;
 <b>use</b> <a href="../../aptos-stdlib/doc/from_bcs.md#0x1_from_bcs">0x1::from_bcs</a>;
 <b>use</b> <a href="guid.md#0x1_guid">0x1::guid</a>;
 <b>use</b> <a href="../../aptos-stdlib/../move-stdlib/doc/hash.md#0x1_hash">0x1::hash</a>;
@@ -496,33 +496,6 @@ Emitted whenever the object's owner field is changed.
 </dl>
 
 
-</details>
-
-<a id="0x1_object_Ghost$g_roll"></a>
-
-## Resource `Ghost$g_roll`
-
-
-
-<pre><code><b>struct</b> Ghost$<a href="object.md#0x1_object_g_roll">g_roll</a> <b>has</b> <b>copy</b>, drop, store, key
-</code></pre>
-
-
-
-<details>
-<summary>Fields</summary>
-
-
-<dl>
-<dt>
-<code>v: u8</code>
-</dt>
-<dd>
-
-</dd>
-</dl>
-
-
 </details>
 
 <a id="@Constants_0"></a>
@@ -1913,18 +1886,11 @@ objects may have cyclic dependencies.
 
     <b>let</b> current_address = <a href="object.md#0x1_object">object</a>.owner;
     <b>let</b> count = 0;
-    <b>while</b> ({
-        <b>spec</b> {
-            <b>invariant</b> count &lt; <a href="object.md#0x1_object_MAXIMUM_OBJECT_NESTING">MAXIMUM_OBJECT_NESTING</a>;
-            <b>invariant</b> <b>forall</b> i in 0..count:
-                <b>exists</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(current_address) && <b>global</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(current_address).allow_ungated_transfer;
-            // <b>invariant</b> <b>forall</b> i in 0..count:
-            //     current_address == get_transfer_address(<b>global</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(destination).owner, i);
+    <b>while</b> (owner != current_address) {
+        count = count + 1;
+        <b>if</b> (std::features::max_object_nesting_check_enabled()) {
+            <b>assert</b>!(count &lt; <a href="object.md#0x1_object_MAXIMUM_OBJECT_NESTING">MAXIMUM_OBJECT_NESTING</a>, <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_out_of_range">error::out_of_range</a>(<a href="object.md#0x1_object_EMAXIMUM_NESTING">EMAXIMUM_NESTING</a>))
         };
-        owner != current_address
-    }) {
-        <b>let</b> count = count + 1;
-        <b>assert</b>!(count &lt; <a href="object.md#0x1_object_MAXIMUM_OBJECT_NESTING">MAXIMUM_OBJECT_NESTING</a>, <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_out_of_range">error::out_of_range</a>(<a href="object.md#0x1_object_EMAXIMUM_NESTING">EMAXIMUM_NESTING</a>));
         // At this point, the first <a href="object.md#0x1_object">object</a> <b>exists</b> and so the more likely case is that the
         // <a href="object.md#0x1_object">object</a>'s owner is not an <a href="object.md#0x1_object">object</a>. So we <b>return</b> a more sensible <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error">error</a>.
         <b>assert</b>!(
@@ -2124,16 +2090,11 @@ Return true if the provided address has indirect or direct ownership of the prov
     <b>let</b> current_address = <a href="object.md#0x1_object">object</a>.owner;
 
     <b>let</b> count = 0;
-    <b>while</b> ({
-        <b>spec</b> {
-            <b>invariant</b> count &lt; <a href="object.md#0x1_object_MAXIMUM_OBJECT_NESTING">MAXIMUM_OBJECT_NESTING</a>;
-            <b>invariant</b> <b>forall</b> i in 0..count:
-                owner != current_address && <b>exists</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(current_address);
+    <b>while</b> (owner != current_address) {
+        count = count + 1;
+        <b>if</b> (std::features::max_object_nesting_check_enabled()) {
+            <b>assert</b>!(count &lt; <a href="object.md#0x1_object_MAXIMUM_OBJECT_NESTING">MAXIMUM_OBJECT_NESTING</a>, <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_out_of_range">error::out_of_range</a>(<a href="object.md#0x1_object_EMAXIMUM_NESTING">EMAXIMUM_NESTING</a>))
         };
-        owner != current_address
-    }) {
-        <b>let</b> count = count + 1;
-        <b>assert</b>!(count &lt; <a href="object.md#0x1_object_MAXIMUM_OBJECT_NESTING">MAXIMUM_OBJECT_NESTING</a>, <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_out_of_range">error::out_of_range</a>(<a href="object.md#0x1_object_EMAXIMUM_NESTING">EMAXIMUM_NESTING</a>));
         <b>if</b> (!<b>exists</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(current_address)) {
             <b>return</b> <b>false</b>
         };
@@ -2224,8 +2185,6 @@ Return true if the provided address has indirect or direct ownership of the prov
 
 
 <pre><code><b>pragma</b> aborts_if_is_strict;
-<a id="0x1_object_g_roll"></a>
-<b>global</b> <a href="object.md#0x1_object_g_roll">g_roll</a>: u8;
 </code></pre>
 
 
@@ -3058,7 +3017,8 @@ Return true if the provided address has indirect or direct ownership of the prov
 
 
 
-<pre><code><b>let</b> current_address_0 = <a href="object.md#0x1_object">object</a>.inner;
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>let</b> current_address_0 = <a href="object.md#0x1_object">object</a>.inner;
 <b>let</b> object_0 = <b>global</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(current_address_0);
 <b>let</b> current_address = object_0.owner;
 <b>aborts_if</b> <a href="object.md#0x1_object">object</a>.inner != owner && !<b>exists</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(<a href="object.md#0x1_object">object</a>.inner);

aptos-move/framework/aptos-framework/sources/object.move

@@ -532,18 +532,11 @@ module aptos_framework::object {
 
         let current_address = object.owner;
         let count = 0;
-        while ({
-            spec {
-                invariant count < MAXIMUM_OBJECT_NESTING;
-                invariant forall i in 0..count:
-                    exists<ObjectCore>(current_address) && global<ObjectCore>(current_address).allow_ungated_transfer;
-                // invariant forall i in 0..count:
-                //     current_address == get_transfer_address(global<ObjectCore>(destination).owner, i);
+        while (owner != current_address) {
+            count = count + 1;
+            if (std::features::max_object_nesting_check_enabled()) {
+                assert!(count < MAXIMUM_OBJECT_NESTING, error::out_of_range(EMAXIMUM_NESTING))
             };
-            owner != current_address
-        }) {
-            let count = count + 1;
-            assert!(count < MAXIMUM_OBJECT_NESTING, error::out_of_range(EMAXIMUM_NESTING));
             // At this point, the first object exists and so the more likely case is that the
             // object's owner is not an object. So we return a more sensible error.
             assert!(
@@ -623,16 +616,11 @@ module aptos_framework::object {
         let current_address = object.owner;
 
         let count = 0;
-        while ({
-            spec {
-                invariant count < MAXIMUM_OBJECT_NESTING;
-                invariant forall i in 0..count:
-                    owner != current_address && exists<ObjectCore>(current_address);
+        while (owner != current_address) {
+            count = count + 1;
+            if (std::features::max_object_nesting_check_enabled()) {
+                assert!(count < MAXIMUM_OBJECT_NESTING, error::out_of_range(EMAXIMUM_NESTING))
             };
-            owner != current_address
-        }) {
-            let count = count + 1;
-            assert!(count < MAXIMUM_OBJECT_NESTING, error::out_of_range(EMAXIMUM_NESTING));
             if (!exists<ObjectCore>(current_address)) {
                 return false
             };
@@ -816,4 +804,110 @@ module aptos_framework::object {
         let (_, hero) = create_hero(creator);
         unburn(creator, hero);
     }
+
+    #[test_only]
+    fun create_simple_object(creator: &signer, seed: vector<u8>): Object<ObjectCore> {
+        object_from_constructor_ref<ObjectCore>(&create_named_object(creator, seed))
+    }
+
+    #[test(creator = @0x123)]
+    #[expected_failure(abort_code = 131078, location = Self)]
+    fun test_exceeding_maximum_object_nesting_owns_should_fail(creator: &signer) acquires ObjectCore {
+        use std::features;
+        let feature = features::get_max_object_nesting_check_feature();
+        let fx = account::create_signer_for_test(@0x1);
+        features::change_feature_flags(&fx, vector[feature], vector[]);
+
+        let obj1 = create_simple_object(creator, b"1");
+        let obj2 = create_simple_object(creator, b"2");
+        let obj3 = create_simple_object(creator, b"3");
+        let obj4 = create_simple_object(creator, b"4");
+        let obj5 = create_simple_object(creator, b"5");
+        let obj6 = create_simple_object(creator, b"6");
+        let obj7 = create_simple_object(creator, b"7");
+        let obj8 = create_simple_object(creator, b"8");
+        let obj9 = create_simple_object(creator, b"9");
+
+        transfer(creator, obj1, object_address(&obj2));
+        transfer(creator, obj2, object_address(&obj3));
+        transfer(creator, obj3, object_address(&obj4));
+        transfer(creator, obj4, object_address(&obj5));
+        transfer(creator, obj5, object_address(&obj6));
+        transfer(creator, obj6, object_address(&obj7));
+        transfer(creator, obj7, object_address(&obj8));
+        transfer(creator, obj8, object_address(&obj9));
+
+        assert!(owns(obj9, signer::address_of(creator)), 1);
+        assert!(owns(obj8, signer::address_of(creator)), 1);
+        assert!(owns(obj7, signer::address_of(creator)), 1);
+        assert!(owns(obj6, signer::address_of(creator)), 1);
+        assert!(owns(obj5, signer::address_of(creator)), 1);
+        assert!(owns(obj4, signer::address_of(creator)), 1);
+        assert!(owns(obj3, signer::address_of(creator)), 1);
+        assert!(owns(obj2, signer::address_of(creator)), 1);
+
+        // Calling `owns` should fail as the nesting is too deep.
+        assert!(owns(obj1, signer::address_of(creator)), 1);
+    }
+
+    #[test(creator = @0x123)]
+    #[expected_failure(abort_code = 131078, location = Self)]
+    fun test_exceeding_maximum_object_nesting_transfer_should_fail(creator: &signer) acquires ObjectCore {
+        use std::features;
+        let feature = features::get_max_object_nesting_check_feature();
+        let fx = account::create_signer_for_test(@0x1);
+        features::change_feature_flags(&fx, vector[feature], vector[]);
+
+        let obj1 = create_simple_object(creator, b"1");
+        let obj2 = create_simple_object(creator, b"2");
+        let obj3 = create_simple_object(creator, b"3");
+        let obj4 = create_simple_object(creator, b"4");
+        let obj5 = create_simple_object(creator, b"5");
+        let obj6 = create_simple_object(creator, b"6");
+        let obj7 = create_simple_object(creator, b"7");
+        let obj8 = create_simple_object(creator, b"8");
+        let obj9 = create_simple_object(creator, b"9");
+
+        transfer(creator, obj1, object_address(&obj2));
+        transfer(creator, obj2, object_address(&obj3));
+        transfer(creator, obj3, object_address(&obj4));
+        transfer(creator, obj4, object_address(&obj5));
+        transfer(creator, obj5, object_address(&obj6));
+        transfer(creator, obj6, object_address(&obj7));
+        transfer(creator, obj7, object_address(&obj8));
+        transfer(creator, obj8, object_address(&obj9));
+
+        // This should fail as the nesting is too deep.
+        transfer(creator, obj1, @0x1);
+    }
+
+    #[test(creator = @0x123)]
+    #[expected_failure(abort_code = 131078, location = Self)]
+    fun test_cyclic_ownership_transfer_should_fail(creator: &signer) acquires ObjectCore {
+        use std::features;
+        let feature = features::get_max_object_nesting_check_feature();
+        let fx = account::create_signer_for_test(@0x1);
+        features::change_feature_flags(&fx, vector[feature], vector[]);
+
+        let obj1 = create_simple_object(creator, b"1");
+        // This creates a cycle (self-loop) in ownership.
+        transfer(creator, obj1, object_address(&obj1));
+        // This should fails as the ownership is cyclic.
+        transfer(creator, obj1, object_address(&obj1));
+    }
+
+    #[test(creator = @0x123)]
+    #[expected_failure(abort_code = 131078, location = Self)]
+    fun test_cyclic_ownership_owns_should_fail(creator: &signer) acquires ObjectCore {
+        use std::features;
+        let feature = features::get_max_object_nesting_check_feature();
+        let fx = account::create_signer_for_test(@0x1);
+        features::change_feature_flags(&fx, vector[feature], vector[]);
+
+        let obj1 = create_simple_object(creator, b"1");
+        // This creates a cycle (self-loop) in ownership.
+        transfer(creator, obj1, object_address(&obj1));
+        // This should fails as the ownership is cyclic.
+        let _ = owns(obj1, signer::address_of(creator));
+    }
 }

aptos-move/framework/aptos-framework/sources/object.spec.move

@@ -47,8 +47,6 @@ spec aptos_framework::object {
     ///
     spec module {
         pragma aborts_if_is_strict;
-        //ghost variable
-        global g_roll: u8;
     }
 
     spec fun spec_exists_at<T: key>(object: address): bool;
@@ -504,6 +502,7 @@ spec aptos_framework::object {
     }
 
     spec owns<T: key>(object: Object<T>, owner: address): bool {
+        pragma aborts_if_is_partial;
         let current_address_0 = object.inner;
         let object_0 = global<ObjectCore>(current_address_0);
         let current_address = object_0.owner;

aptos-move/framework/move-stdlib/doc/features.md

@@ -95,6 +95,8 @@ return true.
 -  [Function `get_concurrent_fungible_assets_feature`](#0x1_features_get_concurrent_fungible_assets_feature)
 -  [Function `concurrent_fungible_assets_enabled`](#0x1_features_concurrent_fungible_assets_enabled)
 -  [Function `is_object_code_deployment_enabled`](#0x1_features_is_object_code_deployment_enabled)
+-  [Function `get_max_object_nesting_check_feature`](#0x1_features_get_max_object_nesting_check_feature)
+-  [Function `max_object_nesting_check_enabled`](#0x1_features_max_object_nesting_check_enabled)
 -  [Function `change_feature_flags`](#0x1_features_change_feature_flags)
 -  [Function `is_enabled`](#0x1_features_is_enabled)
 -  [Function `set`](#0x1_features_set)
@@ -418,6 +420,16 @@ Lifetime: permanent
 
 
 
+<a id="0x1_features_MAX_OBJECT_NESTING_CHECK"></a>
+
+Whether checking the maximum object nesting is enabled.
+
+
+<pre><code><b>const</b> <a href="features.md#0x1_features_MAX_OBJECT_NESTING_CHECK">MAX_OBJECT_NESTING_CHECK</a>: u64 = 53;
+</code></pre>
+
+
+
 <a id="0x1_features_MODULE_EVENT"></a>
 
 Whether emit function in <code>event.<b>move</b></code> are enabled for module events.
@@ -2139,6 +2151,52 @@ Lifetime: transient
 
 
 
+</details>
+
+<a id="0x1_features_get_max_object_nesting_check_feature"></a>
+
+## Function `get_max_object_nesting_check_feature`
+
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="features.md#0x1_features_get_max_object_nesting_check_feature">get_max_object_nesting_check_feature</a>(): u64
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="features.md#0x1_features_get_max_object_nesting_check_feature">get_max_object_nesting_check_feature</a>(): u64 { <a href="features.md#0x1_features_MAX_OBJECT_NESTING_CHECK">MAX_OBJECT_NESTING_CHECK</a> }
+</code></pre>
+
+
+
+</details>
+
+<a id="0x1_features_max_object_nesting_check_enabled"></a>
+
+## Function `max_object_nesting_check_enabled`
+
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="features.md#0x1_features_max_object_nesting_check_enabled">max_object_nesting_check_enabled</a>(): bool
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="features.md#0x1_features_max_object_nesting_check_enabled">max_object_nesting_check_enabled</a>(): bool <b>acquires</b> <a href="features.md#0x1_features_Features">Features</a> {
+    <a href="features.md#0x1_features_is_enabled">is_enabled</a>(<a href="features.md#0x1_features_MAX_OBJECT_NESTING_CHECK">MAX_OBJECT_NESTING_CHECK</a>)
+}
+</code></pre>
+
+
+
 </details>
 
 <a id="0x1_features_change_feature_flags"></a>