[Spec] Fix the broken spec (#6659)

- This PR fix the broken spec by mocking up the `aptos_framework::object::exists_at`.
- It's because a correct spec is not supported by Prover. This is a TODO and filed as an issue: aptos-labs/aptos-core#6658

GitOrigin-RevId: 74f6790f32b4fc09729d8c0e7930f9f93b534e2a

aptos-framework/doc/object.md

@@ -61,6 +61,8 @@ make it so that a reference to a global object can be returned from a function.
 -  [Function `verify_ungated_and_descendant`](#0x1_object_verify_ungated_and_descendant)
 -  [Function `owner`](#0x1_object_owner)
 -  [Function `is_owner`](#0x1_object_is_owner)
+-  [Specification](#@Specification_1)
+    -  [Function `exists_at`](#@Specification_1_exists_at)
 
 
 <pre><code><b>use</b> <a href="account.md#0x1_account">0x1::account</a>;
@@ -1377,5 +1379,25 @@ Return true if the provided address is the current owner.
 
 </details>
 
+<a name="@Specification_1"></a>
+
+## Specification
+
+
+<a name="@Specification_1_exists_at"></a>
+
+### Function `exists_at`
+
+
+<pre><code><b>fun</b> <a href="object.md#0x1_object_exists_at">exists_at</a>&lt;T: key&gt;(<a href="object.md#0x1_object">object</a>: <b>address</b>): bool
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> <b>false</b>;
+</code></pre>
+
 
 [move-book]: https://move-language.github.io/move/introduction.html

aptos-framework/sources/object.spec.move

@@ -0,0 +1,9 @@
+spec aptos_framework::object {
+    spec exists_at {
+        pragma opaque;
+        aborts_if false;
+        // TODO: Disabled the following post-condition due to an issue with
+        // the use of a type parameter in `exists` in spec.
+        // ensures result == exists<T>(object);
+    }
+}