From 552a5a10431b4a55dcddaa3f7d27bb479b9648f8 Mon Sep 17 00:00:00 2001 From: Junkil Park Date: Wed, 30 Nov 2022 22:38:21 -0800 Subject: [PATCH] [Spec] Completed the spec of `from_bcs`, `any`, `copyable_any` and `type_info` (#5712) Added the spec of the following modules: - `from_bcs` - `any` - `copyable_any` - `type_info` There are TODOs which should be filed as separate Github issues. --- aptos-move/framework/aptos-stdlib/doc/any.md | 63 +++++++++++++++++++ .../aptos-stdlib/doc/copyable_any.md | 63 +++++++++++++++++++ .../framework/aptos-stdlib/doc/from_bcs.md | 13 ++++ .../framework/aptos-stdlib/doc/type_info.md | 37 +++++++++++ .../aptos-stdlib/sources/any.spec.move | 30 ++++++++- .../sources/copyable_any.spec.move | 29 +++++++++ .../aptos-stdlib/sources/from_bcs.spec.move | 35 ++++++++++- .../aptos-stdlib/sources/type_info.move | 3 + .../aptos-stdlib/sources/type_info.spec.move | 10 ++- 9 files changed, 278 insertions(+), 5 deletions(-) create mode 100644 aptos-move/framework/aptos-stdlib/sources/copyable_any.spec.move diff --git a/aptos-move/framework/aptos-stdlib/doc/any.md b/aptos-move/framework/aptos-stdlib/doc/any.md index 1893839049b17..1f9e53191d6e6 100644 --- a/aptos-move/framework/aptos-stdlib/doc/any.md +++ b/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) 
use 0x1::bcs;
@@ -160,5 +164,64 @@ Returns the type name of this Any
 
 
 
+
+
+## Specification
+
+
+
+
+### Function `pack`
+
+
+
public fun pack<T: drop, store>(x: T): any::Any
+

+
+
+
+
+
aborts_if false;
+ensures result == Any {
+    type_name: type_info::type_name<T>(),
+    data: bcs::serialize<T>(x)
+};
+

+
+
+
+
+
+### Function `unpack`
+
+
+
public fun unpack<T>(x: any::Any): T
+

+
+
+
+
+
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);
+

+
+
+
+
+
+### Function `type_name`
+
+
+
public fun type_name(x: &any::Any): &string::String
+

+
+
+
+
+
aborts_if false;
+ensures result == x.type_name;
+

+
 
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-stdlib/doc/copyable_any.md b/aptos-move/framework/aptos-stdlib/doc/copyable_any.md
index 6c1b583d5f91e..10787b97bd27a 100644
--- a/aptos-move/framework/aptos-stdlib/doc/copyable_any.md
+++ b/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)
 
 
 
use 0x1::bcs;
@@ -150,5 +154,64 @@ Returns the type name of this Any
 
 
 
+
+
+## Specification
+
+
+
+
+### Function `pack`
+
+
+
public fun pack<T: copy, drop, store>(x: T): copyable_any::Any
+

+
+
+
+
+
aborts_if false;
+ensures result == Any {
+    type_name: type_info::type_name<T>(),
+    data: bcs::serialize<T>(x)
+};
+

+
+
+
+
+
+### Function `unpack`
+
+
+
public fun unpack<T>(x: copyable_any::Any): T
+

+
+
+
+
+
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);
+

+
+
+
+
+
+### Function `type_name`
+
+
+
public fun type_name(x: &copyable_any::Any): &string::String
+

+
+
+
+
+
aborts_if false;
+ensures result == x.type_name;
+

+
 
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-stdlib/doc/from_bcs.md b/aptos-move/framework/aptos-stdlib/doc/from_bcs.md
index 6ee7866e0eb45..5f5ee2191db6e 100644
--- a/aptos-move/framework/aptos-stdlib/doc/from_bcs.md
+++ b/aptos-move/framework/aptos-stdlib/doc/from_bcs.md
@@ -228,6 +228,17 @@ owned.
 ## Specification
 
 
+
+
+
+
+
fun deserialize<T>(bytes: vector<u8>): T;
+
+fun deserializable<T>(bytes: vector<u8>): bool;
+

+
+
+
 
 
 ### Function `from_bytes`
@@ -240,6 +251,8 @@ owned.
 
 
 
pragma opaque;
+aborts_if !deserializable<T>(bytes);
+ensures result == deserialize<T>(bytes);
 

 
 
diff --git a/aptos-move/framework/aptos-stdlib/doc/type_info.md b/aptos-move/framework/aptos-stdlib/doc/type_info.md
index ab46f716682c5..34eaff24de6ea 100644
--- a/aptos-move/framework/aptos-stdlib/doc/type_info.md
+++ b/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)
 
 
 
use 0x1::bcs;
@@ -364,6 +365,42 @@ analysis of vector size dynamism.
 
 
 
pragma opaque;
+aborts_if false;
+ensures result == spec_chain_id_internal();
+

+
+
+
+
+
+### Function `verify_type_of_generic`
+
+
+
fun verify_type_of_generic<T>()
+

+
+
+
+
+
aborts_if !spec_is_struct<T>();
+

+
+
+
+
+
+
+
+
native fun spec_is_struct<T>(): bool;
+

+
+
+
+
+
+
+
+
fun spec_chain_id_internal(): u8;
 

 
 
diff --git a/aptos-move/framework/aptos-stdlib/sources/any.spec.move b/aptos-move/framework/aptos-stdlib/sources/any.spec.move
index b921ec56b0d93..aa697260e7ca3 100644
--- a/aptos-move/framework/aptos-stdlib/sources/any.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/any.spec.move
@@ -1 +1,29 @@
-spec aptos_std::any {}
+spec aptos_std::any {
+
+    // -----------------------
+    // Function specifications
+    // -----------------------
+
+    spec pack(x: T): Any {
+        use std::bcs;
+        aborts_if false;
+        ensures result == Any {
+            type_name: type_info::type_name(),
+            data: bcs::serialize(x)
+        };
+    }
+
+    spec unpack(x: Any): T {
+        use aptos_std::from_bcs;
+        // TODO: timeout without this.
+        pragma aborts_if_is_partial;
+        aborts_if type_info::type_name() != x.type_name;
+        aborts_if !from_bcs::deserializable(x.data);
+        ensures result == from_bcs::deserialize(x.data);
+    }
+
+    spec type_name(x: &Any): &String {
+        aborts_if false;
+        ensures result == x.type_name;
+    }
+}
diff --git a/aptos-move/framework/aptos-stdlib/sources/copyable_any.spec.move b/aptos-move/framework/aptos-stdlib/sources/copyable_any.spec.move
new file mode 100644
index 0000000000000..f8df857dffd12
--- /dev/null
+++ b/aptos-move/framework/aptos-stdlib/sources/copyable_any.spec.move
@@ -0,0 +1,29 @@
+spec aptos_std::copyable_any {
+
+    // -----------------------
+    // Function specifications
+    // -----------------------
+
+    spec pack(x: T): Any {
+        use std::bcs;
+        aborts_if false;
+        ensures result == Any {
+            type_name: type_info::type_name(),
+            data: bcs::serialize(x)
+        };
+    }
+
+    spec unpack(x: Any): T {
+        use aptos_std::from_bcs;
+        // TODO: timeout without this.
+        pragma aborts_if_is_partial;
+        aborts_if type_info::type_name() != x.type_name;
+        aborts_if !from_bcs::deserializable(x.data);
+        ensures result == from_bcs::deserialize(x.data);
+    }
+
+    spec type_name(x: &Any): &String {
+        aborts_if false;
+        ensures result == x.type_name;
+    }
+}
diff --git a/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move b/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move
index ed03b967dc5bf..28415ae9b7258 100644
--- a/aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move
+++ b/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(bytes: vector): T;
+
+        // Checks if `bytes` is valid so that it can be deserialized into type T.
+        // This is modeled as an uninterpreted function.
+        fun deserializable(bytes: vector): bool;
+
+        // `deserialize` is an injective function.
+        // TODO: disabled due to the issue with generic axioms.
+        // axiom forall b1: vector, b2: vector:
+        //     (deserialize(b1) == deserialize(b2) ==> b1 == b2);
+
+        // `deserialize` is an inverse function of `bcs::serialize`.
+        // TODO: disabled due to the issue with generic axioms.
+        // axiom forall v: T: deserialize(bcs::serialize(v)) == v;
+
+        // All serialized bytes are deserializable.
+        // TODO: disabled due to the issue with generic axioms.
+        // axiom forall v: T: deserializable(bcs::serialize(v));
+    }
+
+
+    // -----------------------
+    // Function specifications
+    // -----------------------
+
+    spec from_bytes(bytes: vector): T {
         pragma opaque;
+        aborts_if !deserializable(bytes);
+        ensures result == deserialize(bytes);
     }
 }
diff --git a/aptos-move/framework/aptos-stdlib/sources/type_info.move b/aptos-move/framework/aptos-stdlib/sources/type_info.move
index 035206bcc70f9..c758476426b17 100644
--- a/aptos-move/framework/aptos-stdlib/sources/type_info.move
+++ b/aptos-move/framework/aptos-stdlib/sources/type_info.move
@@ -134,6 +134,9 @@ module aptos_std::type_info {
             assert struct_name == type_of().struct_name;
         };
     }
+    spec verify_type_of_generic {
+        aborts_if !spec_is_struct();
+    }
 
     #[test_only]
     struct CustomType has drop {}
diff --git a/aptos-move/framework/aptos-stdlib/sources/type_info.spec.move b/aptos-move/framework/aptos-stdlib/sources/type_info.spec.move
index 880ad5fd1e652..f73b3f11e2595 100644
--- a/aptos-move/framework/aptos-stdlib/sources/type_info.spec.move
+++ b/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(): 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();
     }
 }