-
Notifications
You must be signed in to change notification settings - Fork 3.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Spec] Completed the spec of
from_bcs, any, copyable_any and `t…
…ype_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.
- Loading branch information
1 parent
fd70fb6
commit 0c21d91
Showing
9 changed files
with
278 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; | ||
| } | ||
| } |
29 changes: 29 additions & 0 deletions
29
aptos-move/framework/aptos-stdlib/sources/copyable_any.spec.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; | ||
| } | ||
| } |
35 changes: 33 additions & 2 deletions
35
aptos-move/framework/aptos-stdlib/sources/from_bcs.spec.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
10 changes: 8 additions & 2 deletions
10
aptos-move/framework/aptos-stdlib/sources/type_info.spec.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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(); | ||
| } | ||
| } |