[Spec] Completed the spec of from_bcs, any, copyable_any and type_info

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

@@ -10,6 +10,10 @@
 -  [Function `pack`](#0x1_any_pack)
 -  [Function `unpack`](#0x1_any_unpack)
 -  [Function `type_name`](#0x1_any_type_name)
+-  [Specification](#@Specification_1)
+    -  [Function `pack`](#@Specification_1_pack)
+    -  [Function `unpack`](#@Specification_1_unpack)
+    -  [Function `type_name`](#@Specification_1_type_name)
 
 
 <pre><code><b>use</b> <a href="../../move-stdlib/doc/bcs.md#0x1_bcs">0x1::bcs</a>;
@@ -160,5 +164,64 @@ Returns the type name of this Any
 
 </details>
 
+<a name="@Specification_1"></a>
+
+## Specification
+
+
+<a name="@Specification_1_pack"></a>
+
+### Function `pack`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="any.md#0x1_any_pack">pack</a>&lt;T: drop, store&gt;(x: T): <a href="any.md#0x1_any_Any">any::Any</a>
+</code></pre>
+
+
+
+
+<pre><code><b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == <a href="any.md#0x1_any_Any">Any</a> {
+    type_name: <a href="type_info.md#0x1_type_info_type_name">type_info::type_name</a>&lt;T&gt;(),
+    data: <a href="../../move-stdlib/doc/bcs.md#0x1_bcs_serialize">bcs::serialize</a>&lt;T&gt;(x)
+};
+</code></pre>
+
+
+
+<a name="@Specification_1_unpack"></a>
+
+### Function `unpack`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="any.md#0x1_any_unpack">unpack</a>&lt;T&gt;(x: <a href="any.md#0x1_any_Any">any::Any</a>): T
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>aborts_if</b> <a href="type_info.md#0x1_type_info_type_name">type_info::type_name</a>&lt;T&gt;() != x.type_name;
+<b>aborts_if</b> !<a href="from_bcs.md#0x1_from_bcs_deserializable">from_bcs::deserializable</a>&lt;T&gt;(x.data);
+<b>ensures</b> result == <a href="from_bcs.md#0x1_from_bcs_deserialize">from_bcs::deserialize</a>&lt;T&gt;(x.data);
+</code></pre>
+
+
+
+<a name="@Specification_1_type_name"></a>
+
+### Function `type_name`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="any.md#0x1_any_type_name">type_name</a>(x: &<a href="any.md#0x1_any_Any">any::Any</a>): &<a href="../../move-stdlib/doc/string.md#0x1_string_String">string::String</a>
+</code></pre>
+
+
+
+
+<pre><code><b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == x.type_name;
+</code></pre>
+
 
 [move-book]: https://move-language.github.io/move/introduction.html

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

@@ -10,6 +10,10 @@
 -  [Function `pack`](#0x1_copyable_any_pack)
 -  [Function `unpack`](#0x1_copyable_any_unpack)
 -  [Function `type_name`](#0x1_copyable_any_type_name)
+-  [Specification](#@Specification_1)
+    -  [Function `pack`](#@Specification_1_pack)
+    -  [Function `unpack`](#@Specification_1_unpack)
+    -  [Function `type_name`](#@Specification_1_type_name)
 
 
 <pre><code><b>use</b> <a href="../../move-stdlib/doc/bcs.md#0x1_bcs">0x1::bcs</a>;
@@ -150,5 +154,64 @@ Returns the type name of this Any
 
 </details>
 
+<a name="@Specification_1"></a>
+
+## Specification
+
+
+<a name="@Specification_1_pack"></a>
+
+### Function `pack`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="copyable_any.md#0x1_copyable_any_pack">pack</a>&lt;T: <b>copy</b>, drop, store&gt;(x: T): <a href="copyable_any.md#0x1_copyable_any_Any">copyable_any::Any</a>
+</code></pre>
+
+
+
+
+<pre><code><b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == <a href="copyable_any.md#0x1_copyable_any_Any">Any</a> {
+    type_name: <a href="type_info.md#0x1_type_info_type_name">type_info::type_name</a>&lt;T&gt;(),
+    data: <a href="../../move-stdlib/doc/bcs.md#0x1_bcs_serialize">bcs::serialize</a>&lt;T&gt;(x)
+};
+</code></pre>
+
+
+
+<a name="@Specification_1_unpack"></a>
+
+### Function `unpack`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="copyable_any.md#0x1_copyable_any_unpack">unpack</a>&lt;T&gt;(x: <a href="copyable_any.md#0x1_copyable_any_Any">copyable_any::Any</a>): T
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>aborts_if</b> <a href="type_info.md#0x1_type_info_type_name">type_info::type_name</a>&lt;T&gt;() != x.type_name;
+<b>aborts_if</b> !<a href="from_bcs.md#0x1_from_bcs_deserializable">from_bcs::deserializable</a>&lt;T&gt;(x.data);
+<b>ensures</b> result == <a href="from_bcs.md#0x1_from_bcs_deserialize">from_bcs::deserialize</a>&lt;T&gt;(x.data);
+</code></pre>
+
+
+
+<a name="@Specification_1_type_name"></a>
+
+### Function `type_name`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="copyable_any.md#0x1_copyable_any_type_name">type_name</a>(x: &<a href="copyable_any.md#0x1_copyable_any_Any">copyable_any::Any</a>): &<a href="../../move-stdlib/doc/string.md#0x1_string_String">string::String</a>
+</code></pre>
+
+
+
+
+<pre><code><b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == x.type_name;
+</code></pre>
+
 
 [move-book]: https://move-language.github.io/move/introduction.html

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

@@ -228,6 +228,17 @@ owned.
 ## Specification
 
 
+
+<a name="0x1_from_bcs_deserialize"></a>
+
+
+<pre><code><b>fun</b> <a href="from_bcs.md#0x1_from_bcs_deserialize">deserialize</a>&lt;T&gt;(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): T;
+<a name="0x1_from_bcs_deserializable"></a>
+<b>fun</b> <a href="from_bcs.md#0x1_from_bcs_deserializable">deserializable</a>&lt;T&gt;(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): bool;
+</code></pre>
+
+
+
 <a name="@Specification_1_from_bytes"></a>
 
 ### Function `from_bytes`
@@ -240,6 +251,8 @@ owned.
 
 
 <pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> !<a href="from_bcs.md#0x1_from_bcs_deserializable">deserializable</a>&lt;T&gt;(bytes);
+<b>ensures</b> result == <a href="from_bcs.md#0x1_from_bcs_deserialize">deserialize</a>&lt;T&gt;(bytes);
 </code></pre>
 
 

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

@@ -19,6 +19,7 @@
 -  [Function `verify_type_of_generic`](#0x1_type_info_verify_type_of_generic)
 -  [Specification](#@Specification_1)
     -  [Function `chain_id_internal`](#@Specification_1_chain_id_internal)
+    -  [Function `verify_type_of_generic`](#@Specification_1_verify_type_of_generic)
 
 
 <pre><code><b>use</b> <a href="../../move-stdlib/doc/bcs.md#0x1_bcs">0x1::bcs</a>;
@@ -364,6 +365,42 @@ analysis of vector size dynamism.
 
 
 <pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == <a href="type_info.md#0x1_type_info_spec_chain_id_internal">spec_chain_id_internal</a>();
+</code></pre>
+
+
+
+<a name="@Specification_1_verify_type_of_generic"></a>
+
+### Function `verify_type_of_generic`
+
+
+<pre><code><b>fun</b> <a href="type_info.md#0x1_type_info_verify_type_of_generic">verify_type_of_generic</a>&lt;T&gt;()
+</code></pre>
+
+
+
+
+<pre><code><b>aborts_if</b> !<a href="type_info.md#0x1_type_info_spec_is_struct">spec_is_struct</a>&lt;T&gt;();
+</code></pre>
+
+
+
+
+<a name="0x1_type_info_spec_is_struct"></a>
+
+
+<pre><code><b>native</b> <b>fun</b> <a href="type_info.md#0x1_type_info_spec_is_struct">spec_is_struct</a>&lt;T&gt;(): bool;
+</code></pre>
+
+
+
+
+<a name="0x1_type_info_spec_chain_id_internal"></a>
+
+
+<pre><code><b>fun</b> <a href="type_info.md#0x1_type_info_spec_chain_id_internal">spec_chain_id_internal</a>(): u8;
 </code></pre>
 
 

aptos-move/framework/aptos-stdlib/sources/any.spec.move

@@ -1 +1,29 @@
-spec aptos_std::any {}
+spec aptos_std::any {
+
+    // -----------------------
+    // Function specifications
+    // -----------------------
+
+    spec pack<T: drop + store>(x: T): Any {
+        use std::bcs;
+        aborts_if false;
+        ensures result == Any {
+            type_name: type_info::type_name<T>(),
+            data: bcs::serialize<T>(x)
+        };
+    }
+
+    spec unpack<T>(x: Any): T {
+        use aptos_std::from_bcs;
+        // TODO: timeout without this.
+        pragma aborts_if_is_partial;
+        aborts_if type_info::type_name<T>() != x.type_name;
+        aborts_if !from_bcs::deserializable<T>(x.data);
+        ensures result == from_bcs::deserialize<T>(x.data);
+    }
+
+    spec type_name(x: &Any): &String {
+        aborts_if false;
+        ensures result == x.type_name;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/copyable_any.spec.move

@@ -0,0 +1,29 @@
+spec aptos_std::copyable_any {
+
+    // -----------------------
+    // Function specifications
+    // -----------------------
+
+    spec pack<T: drop + store>(x: T): Any {
+        use std::bcs;
+        aborts_if false;
+        ensures result == Any {
+            type_name: type_info::type_name<T>(),
+            data: bcs::serialize<T>(x)
+        };
+    }
+
+    spec unpack<T>(x: Any): T {
+        use aptos_std::from_bcs;
+        // TODO: timeout without this.
+        pragma aborts_if_is_partial;
+        aborts_if type_info::type_name<T>() != x.type_name;
+        aborts_if !from_bcs::deserializable<T>(x.data);
+        ensures result == from_bcs::deserialize<T>(x.data);
+    }
+
+    spec type_name(x: &Any): &String {
+        aborts_if false;
+        ensures result == x.type_name;
+    }
+}

aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move

@@ -1,6 +1,37 @@
 spec aptos_std::from_bcs {
-    spec from_bytes {
-        // TODO: temporary mockup.
+    // ----------------------------------
+    // Uninterpreted functions and axioms
+    // ----------------------------------
+    spec module {
+        // An uninterpreted function to represent the desrialization.
+        fun deserialize<T>(bytes: vector<u8>): T;
+
+        // Checks if `bytes` is valid so that it can be deserialized into type T.
+        // This is modeled as an uninterpreted function.
+        fun deserializable<T>(bytes: vector<u8>): bool;
+
+        // `deserialize` is an injective function.
+        // TODO: disabled due to the issue with generic axioms.
+        // axiom<T> forall b1: vector<u8>, b2: vector<u8>:
+        //     (deserialize<T>(b1) == deserialize<T>(b2) ==> b1 == b2);
+
+        // `deserialize` is an inverse function of `bcs::serialize`.
+        // TODO: disabled due to the issue with generic axioms.
+        // axiom<T> forall v: T: deserialize<T>(bcs::serialize(v)) == v;
+
+        // All serialized bytes are deserializable.
+        // TODO: disabled due to the issue with generic axioms.
+        // axiom<T> forall v: T: deserializable<T>(bcs::serialize(v));
+    }
+
+
+    // -----------------------
+    // Function specifications
+    // -----------------------
+
+    spec from_bytes<T>(bytes: vector<u8>): T {
         pragma opaque;
+        aborts_if !deserializable<T>(bytes);
+        ensures result == deserialize<T>(bytes);
     }
 }

aptos-move/framework/aptos-stdlib/sources/type_info.move

@@ -134,6 +134,9 @@ module aptos_std::type_info {
             assert struct_name == type_of<T>().struct_name;
         };
     }
+    spec verify_type_of_generic {
+        aborts_if !spec_is_struct<T>();
+    }
 
     #[test_only]
     struct CustomType has drop {}

aptos-move/framework/aptos-stdlib/sources/type_info.spec.move

@@ -1,8 +1,14 @@
 spec aptos_std::type_info {
     // Move Prover natively supports `type_of` and `type_name`.
 
-    spec chain_id_internal {
-        // TODO: temporary mockup.
+    spec native fun spec_is_struct<T>(): bool;
+
+    // The chain ID is modeled as an uninterpreted function.
+    spec fun spec_chain_id_internal(): u8;
+
+    spec chain_id_internal(): u8 {
         pragma opaque;
+        aborts_if false;
+        ensures result == spec_chain_id_internal();
     }
 }