From f4f7a60ac469f9f2305f5a28528e4d19e604f268 Mon Sep 17 00:00:00 2001 From: Junkil Park Date: Thu, 8 Dec 2022 12:45:10 -0800 Subject: [PATCH] [Spec] Added more specs to the `coin` and `account` modules - this PR completes many TODOs in the specs of coin and account modules. --- .../framework/aptos-framework/doc/account.md | 65 ++++++++++++-- .../framework/aptos-framework/doc/coin.md | 4 +- .../aptos-framework/sources/account.spec.move | 64 +++++++++++-- .../aptos-framework/sources/coin.spec.move | 3 +- .../framework/aptos-stdlib/doc/ed25519.md | 89 ++++++++++++++++--- .../aptos-stdlib/doc/multi_ed25519.md | 83 +++++++++++++++-- .../framework/aptos-stdlib/doc/type_info.md | 59 ++++++++++-- .../sources/cryptography/ed25519.spec.move | 40 +++++++-- .../cryptography/multi_ed25519.spec.move | 40 +++++++-- .../aptos-stdlib/sources/type_info.spec.move | 19 +++- .../framework/move-stdlib/doc/option.md | 1 + .../framework/move-stdlib/sources/option.move | 1 + 12 files changed, 407 insertions(+), 61 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/account.md b/aptos-move/framework/aptos-framework/doc/account.md index b51fc35cbdc71..87ee5d31ed2d7 100644 --- a/aptos-move/framework/aptos-framework/doc/account.md +++ b/aptos-move/framework/aptos-framework/doc/account.md @@ -1724,7 +1724,20 @@ The length of new_auth_key is 32. -
pragma aborts_if_is_partial;
+
include scheme == ED25519_SCHEME ==> ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: public_key_bytes };
+include scheme == ED25519_SCHEME ==> ed25519::NewSignatureFromBytesAbortsIf { bytes: signature };
+aborts_if scheme == ED25519_SCHEME && !ed25519::spec_signature_verify_strict_t(
+    ed25519::Signature { bytes: signature },
+    ed25519::UnvalidatedPublicKey { bytes: public_key_bytes },
+    challenge
+);
+include scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: public_key_bytes };
+include scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewSignatureFromBytesAbortsIf { bytes: signature };
+aborts_if scheme == MULTI_ED25519_SCHEME && !multi_ed25519::spec_signature_verify_strict_t(
+    multi_ed25519::Signature { bytes: signature },
+    multi_ed25519::UnvalidatedPublicKey { bytes: public_key_bytes },
+    challenge
+);
 aborts_if scheme != ED25519_SCHEME && scheme != MULTI_ED25519_SCHEME;
 

 
@@ -1767,9 +1780,37 @@ The Account existed under the signer.
 The authentication scheme is ED25519_SCHEME and MULTI_ED25519_SCHEME.
 
 
-
pragma aborts_if_is_partial;
-let source_address = signer::address_of(account);
+
let source_address = signer::address_of(account);
+let account_resource = global<Account>(source_address);
+let proof_challenge = SignerCapabilityOfferProofChallengeV2 {
+    sequence_number: account_resource.sequence_number,
+    source_address,
+    recipient_address,
+};
 aborts_if !exists<Account>(recipient_address);
+aborts_if !exists<Account>(source_address);
+include account_scheme == ED25519_SCHEME ==> ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: account_public_key_bytes };
+aborts_if account_scheme == ED25519_SCHEME && ({
+    let expected_auth_key = ed25519::spec_public_key_bytes_to_authentication_key(account_public_key_bytes);
+    account_resource.authentication_key != expected_auth_key
+});
+include account_scheme == ED25519_SCHEME ==> ed25519::NewSignatureFromBytesAbortsIf { bytes: signer_capability_sig_bytes };
+aborts_if account_scheme == ED25519_SCHEME && !ed25519::spec_signature_verify_strict_t(
+    ed25519::Signature { bytes: signer_capability_sig_bytes },
+    ed25519::UnvalidatedPublicKey { bytes: account_public_key_bytes },
+    proof_challenge
+);
+include account_scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: account_public_key_bytes };
+aborts_if account_scheme == MULTI_ED25519_SCHEME && ({
+    let expected_auth_key = multi_ed25519::spec_public_key_bytes_to_authentication_key(account_public_key_bytes);
+    account_resource.authentication_key != expected_auth_key
+});
+include account_scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewSignatureFromBytesAbortsIf { bytes: signer_capability_sig_bytes };
+aborts_if account_scheme == MULTI_ED25519_SCHEME && !multi_ed25519::spec_signature_verify_strict_t(
+    multi_ed25519::Signature { bytes: signer_capability_sig_bytes },
+    multi_ed25519::UnvalidatedPublicKey { bytes: account_public_key_bytes },
+    proof_challenge
+);
 aborts_if account_scheme != ED25519_SCHEME && account_scheme != MULTI_ED25519_SCHEME;
 modifies global<Account>(source_address);
 

@@ -1853,7 +1894,19 @@ The Account existed under the signer
 The value of signer_capability_offer.for of Account resource under the signer is to_be_revoked_address
 
 
-
pragma verify = false;
+
pragma opaque;
+pragma aborts_if_is_strict = false;
+aborts_if [abstract] false;
+ensures [abstract] result == spec_create_resource_address(source, seed);
+

+
+
+
+
+
+
+
+
fun spec_create_resource_address(source: address, seed: vector<u8>): address;
 

 
 
@@ -1970,8 +2023,8 @@ The guid_creation_num of the Account is up to MAX_U64.
 
 
 
-
pragma aborts_if_is_partial;
-aborts_if !exists<Account>(account_addr);
+
aborts_if !exists<Account>(account_addr);
+aborts_if !type_info::spec_is_struct<CoinType>();
 modifies global<Account>(account_addr);
 

 
diff --git a/aptos-move/framework/aptos-framework/doc/coin.md b/aptos-move/framework/aptos-framework/doc/coin.md
index f92b171f27f94..7030576eebddc 100644
--- a/aptos-move/framework/aptos-framework/doc/coin.md
+++ b/aptos-move/framework/aptos-framework/doc/coin.md
@@ -2235,12 +2235,12 @@ An account can only be registered once.
 Updating Account.guid_creation_num will not overflow.
 
 
-
pragma aborts_if_is_partial;
-let account_addr = signer::address_of(account);
+
let account_addr = signer::address_of(account);
 let acc = global<account::Account>(account_addr);
 aborts_if acc.guid_creation_num + 2 > MAX_U64;
 aborts_if exists<CoinStore<CoinType>>(account_addr);
 aborts_if !exists<account::Account>(account_addr);
+aborts_if !type_info::spec_is_struct<CoinType>();
 ensures exists<CoinStore<CoinType>>(account_addr);
 

 
diff --git a/aptos-move/framework/aptos-framework/sources/account.spec.move b/aptos-move/framework/aptos-framework/sources/account.spec.move
index 1c8d8e022f59d..875532a8a9e90 100644
--- a/aptos-move/framework/aptos-framework/sources/account.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/account.spec.move
@@ -81,8 +81,21 @@ spec aptos_framework::account {
     }
 
     spec assert_valid_signature_and_get_auth_key(scheme: u8, public_key_bytes: vector, signature: vector, challenge: &RotationProofChallenge): vector {
-        // TODO: complex aborts conditions.
-        pragma aborts_if_is_partial;
+        include scheme == ED25519_SCHEME ==> ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: public_key_bytes };
+        include scheme == ED25519_SCHEME ==> ed25519::NewSignatureFromBytesAbortsIf { bytes: signature };
+        aborts_if scheme == ED25519_SCHEME && !ed25519::spec_signature_verify_strict_t(
+            ed25519::Signature { bytes: signature },
+            ed25519::UnvalidatedPublicKey { bytes: public_key_bytes },
+            challenge
+        );
+
+        include scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: public_key_bytes };
+        include scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewSignatureFromBytesAbortsIf { bytes: signature };
+        aborts_if scheme == MULTI_ED25519_SCHEME && !multi_ed25519::spec_signature_verify_strict_t(
+            multi_ed25519::Signature { bytes: signature },
+            multi_ed25519::UnvalidatedPublicKey { bytes: public_key_bytes },
+            challenge
+        );
         aborts_if scheme != ED25519_SCHEME && scheme != MULTI_ED25519_SCHEME;
     }
 
@@ -116,11 +129,43 @@ spec aptos_framework::account {
         account_public_key_bytes: vector,
         recipient_address: address
     ) {
-        // TODO: complex aborts conditions.
-        pragma aborts_if_is_partial;
         let source_address = signer::address_of(account);
+        let account_resource = global(source_address);
+        let proof_challenge = SignerCapabilityOfferProofChallengeV2 {
+            sequence_number: account_resource.sequence_number,
+            source_address,
+            recipient_address,
+        };
+
         aborts_if !exists(recipient_address);
+        aborts_if !exists(source_address);
+
+        include account_scheme == ED25519_SCHEME ==> ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: account_public_key_bytes };
+        aborts_if account_scheme == ED25519_SCHEME && ({
+            let expected_auth_key = ed25519::spec_public_key_bytes_to_authentication_key(account_public_key_bytes);
+            account_resource.authentication_key != expected_auth_key
+        });
+        include account_scheme == ED25519_SCHEME ==> ed25519::NewSignatureFromBytesAbortsIf { bytes: signer_capability_sig_bytes };
+        aborts_if account_scheme == ED25519_SCHEME && !ed25519::spec_signature_verify_strict_t(
+            ed25519::Signature { bytes: signer_capability_sig_bytes },
+            ed25519::UnvalidatedPublicKey { bytes: account_public_key_bytes },
+            proof_challenge
+        );
+
+        include account_scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewUnvalidatedPublicKeyFromBytesAbortsIf { bytes: account_public_key_bytes };
+        aborts_if account_scheme == MULTI_ED25519_SCHEME && ({
+            let expected_auth_key = multi_ed25519::spec_public_key_bytes_to_authentication_key(account_public_key_bytes);
+            account_resource.authentication_key != expected_auth_key
+        });
+        include account_scheme == MULTI_ED25519_SCHEME ==> multi_ed25519::NewSignatureFromBytesAbortsIf { bytes: signer_capability_sig_bytes };
+        aborts_if account_scheme == MULTI_ED25519_SCHEME && !multi_ed25519::spec_signature_verify_strict_t(
+            multi_ed25519::Signature { bytes: signer_capability_sig_bytes },
+            multi_ed25519::UnvalidatedPublicKey { bytes: account_public_key_bytes },
+            proof_challenge
+        );
+
         aborts_if account_scheme != ED25519_SCHEME && account_scheme != MULTI_ED25519_SCHEME;
+
         modifies global(source_address);
     }
 
@@ -160,9 +205,15 @@ spec aptos_framework::account {
     /// The Account existed under the signer
     /// The value of signer_capability_offer.for of Account resource under the signer is to_be_revoked_address
     spec create_resource_address(source: &address, seed: vector): address {
-        pragma verify = false;
+        pragma opaque;
+        pragma aborts_if_is_strict = false;
+        // This function should not abort assuming the result of `sha3_256` is deserializable into an address.
+        aborts_if [abstract] false;
+        ensures [abstract] result == spec_create_resource_address(source, seed);
     }
 
+    spec fun spec_create_resource_address(source: address, seed: vector): address;
+
     spec create_resource_account(source: &signer, seed: vector): (signer, SignerCapability) {
         pragma verify = false;
     }
@@ -210,9 +261,8 @@ spec aptos_framework::account {
     }
 
     spec register_coin(account_addr: address) {
-        // TODO: Add the abort condition about `type_info::type_of`
-        pragma aborts_if_is_partial;
         aborts_if !exists(account_addr);
+        aborts_if !type_info::spec_is_struct();
         modifies global(account_addr);
     }
 
diff --git a/aptos-move/framework/aptos-framework/sources/coin.spec.move b/aptos-move/framework/aptos-framework/sources/coin.spec.move
index f9f6a4591a396..231ad50b0d3fe 100644
--- a/aptos-move/framework/aptos-framework/sources/coin.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/coin.spec.move
@@ -214,13 +214,12 @@ spec aptos_framework::coin {
     /// An account can only be registered once.
     /// Updating `Account.guid_creation_num` will not overflow.
     spec register(account: &signer) {
-        // TODO: Add the abort condition about `type_info::type_of`
-        pragma aborts_if_is_partial;
         let account_addr = signer::address_of(account);
         let acc = global(account_addr);
         aborts_if acc.guid_creation_num + 2 > MAX_U64;
         aborts_if exists>(account_addr);
         aborts_if !exists(account_addr);
+        aborts_if !type_info::spec_is_struct();
         ensures exists>(account_addr);
     }
 
diff --git a/aptos-move/framework/aptos-stdlib/doc/ed25519.md b/aptos-move/framework/aptos-stdlib/doc/ed25519.md
index e217cf024f6b6..b3261a165a3cb 100644
--- a/aptos-move/framework/aptos-stdlib/doc/ed25519.md
+++ b/aptos-move/framework/aptos-stdlib/doc/ed25519.md
@@ -34,6 +34,7 @@ Contains functions for:
     -  [Function `new_unvalidated_public_key_from_bytes`](#@Specification_1_new_unvalidated_public_key_from_bytes)
     -  [Function `new_validated_public_key_from_bytes`](#@Specification_1_new_validated_public_key_from_bytes)
     -  [Function `new_signature_from_bytes`](#@Specification_1_new_signature_from_bytes)
+    -  [Function `public_key_bytes_to_authentication_key`](#@Specification_1_public_key_bytes_to_authentication_key)
     -  [Function `public_key_validate_internal`](#@Specification_1_public_key_validate_internal)
     -  [Function `signature_verify_strict_internal`](#@Specification_1_signature_verify_strict_internal)
 
@@ -689,6 +690,19 @@ Returns false if either:
 ## Specification
 
 
+
+
+
+
+
fun spec_signature_verify_strict_internal(
+   signature: vector<u8>,
+   public_key: vector<u8>,
+   message: vector<u8>
+): bool;
+

+
+
+
 
 
 ### Function `new_unvalidated_public_key_from_bytes`
@@ -700,13 +714,24 @@ Returns false if either:
 
 
 
-
let length = len(bytes);
-aborts_if length != PUBLIC_KEY_NUM_BYTES;
+
include NewUnvalidatedPublicKeyFromBytesAbortsIf;
 ensures result == UnvalidatedPublicKey { bytes };
 

 
 
 
+
+
+
+
+
schema NewUnvalidatedPublicKeyFromBytesAbortsIf {
+    bytes: vector<u8>;
+    aborts_if len(bytes) != PUBLIC_KEY_NUM_BYTES;
+}
+

+
+
+
 
 
 ### Function `new_validated_public_key_from_bytes`
@@ -737,30 +762,38 @@ Returns false if either:
 
 
 
-
aborts_if len(bytes)!= SIGNATURE_NUM_BYTES;
+
include NewSignatureFromBytesAbortsIf;
 ensures result == Signature { bytes };
 

 
 
 
 
-
+
 
 
-
fun spec_public_key_validate_internal(bytes: vector<u8>): bool;
+
schema NewSignatureFromBytesAbortsIf {
+    bytes: vector<u8>;
+    aborts_if len(bytes) != SIGNATURE_NUM_BYTES;
+}
 

 
 
 
+
 
-
+### Function `public_key_bytes_to_authentication_key`
 
 
-
fun spec_signature_verify_strict_internal(
-   signature: vector<u8>,
-   public_key: vector<u8>,
-   message: vector<u8>
-): bool;
+
fun public_key_bytes_to_authentication_key(pk_bytes: vector<u8>): vector<u8>
+

+
+
+
+
+
pragma opaque;
+aborts_if false;
+ensures [abstract] result == spec_public_key_bytes_to_authentication_key(pk_bytes);
 

 
 
@@ -800,4 +833,38 @@ Returns false if either:
 

 
 
+
+
+
+
+
+
fun spec_public_key_validate_internal(bytes: vector<u8>): bool;
+

+
+
+
+
+
+
+
+
fun spec_public_key_bytes_to_authentication_key(pk_bytes: vector<u8>): vector<u8>;
+

+
+
+
+
+
+
+
+
fun spec_signature_verify_strict_t<T>(signature: Signature, public_key: UnvalidatedPublicKey, data: T): bool {
+   let encoded = SignedMessage<T> {
+       type_info: type_info::type_of<T>(),
+       inner: data,
+   };
+   let message = bcs::serialize(encoded);
+   spec_signature_verify_strict_internal(signature.bytes, public_key.bytes, message)
+}
+

+
+
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md b/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md
index 7ed55619a85f1..988ab4d05464f 100644
--- a/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md
+++ b/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md
@@ -31,6 +31,7 @@ This module has the exact same interface as the Ed25519 module.
     -  [Function `new_unvalidated_public_key_from_bytes`](#@Specification_1_new_unvalidated_public_key_from_bytes)
     -  [Function `new_validated_public_key_from_bytes`](#@Specification_1_new_validated_public_key_from_bytes)
     -  [Function `new_signature_from_bytes`](#@Specification_1_new_signature_from_bytes)
+    -  [Function `public_key_bytes_to_authentication_key`](#@Specification_1_public_key_bytes_to_authentication_key)
     -  [Function `public_key_validate_internal`](#@Specification_1_public_key_validate_internal)
     -  [Function `signature_verify_strict_internal`](#@Specification_1_signature_verify_strict_internal)
 
@@ -684,14 +685,26 @@ Returns false if either:
 
 
 
-
let length = len(bytes);
-aborts_if length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
-aborts_if length % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES != THRESHOLD_SIZE_BYTES;
+
include NewUnvalidatedPublicKeyFromBytesAbortsIf;
 ensures result == UnvalidatedPublicKey { bytes };
 

 
 
 
+
+
+
+
+
schema NewUnvalidatedPublicKeyFromBytesAbortsIf {
+    bytes: vector<u8>;
+    let length = len(bytes);
+    aborts_if length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
+    aborts_if length % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES != THRESHOLD_SIZE_BYTES;
+}
+

+
+
+
 
 
 ### Function `new_validated_public_key_from_bytes`
@@ -703,8 +716,7 @@ Returns false if either:
 
 
 
-
aborts_if len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES
-    && len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
+
aborts_if false;
 let cond = len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES
     && spec_public_key_validate_internal(bytes);
 ensures cond ==> result == option::spec_some(ValidatedPublicKey{bytes});
@@ -724,17 +736,38 @@ Returns false if either:
 
 
 
-
aborts_if len(bytes) % INDIVIDUAL_SIGNATURE_NUM_BYTES != BITMAP_NUM_OF_BYTES;
+
include NewSignatureFromBytesAbortsIf;
 ensures result == Signature { bytes };
 

 
 
 
 
-
+
 
 
-
fun spec_public_key_validate_internal(bytes: vector<u8>): bool;
+
schema NewSignatureFromBytesAbortsIf {
+    bytes: vector<u8>;
+    aborts_if len(bytes) % INDIVIDUAL_SIGNATURE_NUM_BYTES != BITMAP_NUM_OF_BYTES;
+}
+

+
+
+
+
+
+### Function `public_key_bytes_to_authentication_key`
+
+
+
fun public_key_bytes_to_authentication_key(pk_bytes: vector<u8>): vector<u8>
+

+
+
+
+
+
pragma opaque;
+aborts_if false;
+ensures [abstract] result == spec_public_key_bytes_to_authentication_key(pk_bytes);
 

 
 
@@ -764,7 +797,8 @@ Returns false if either:
 
 
 
pragma opaque;
-aborts_if len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
+aborts_if false;
+ensures (len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS) ==> (result == false);
 ensures result == spec_public_key_validate_internal(bytes);
 

 
@@ -787,4 +821,35 @@ Returns false if either:
 

 
 
+
+
+
+
+
+
fun spec_public_key_validate_internal(bytes: vector<u8>): bool;
+

+
+
+
+
+
+
+
+
fun spec_public_key_bytes_to_authentication_key(pk_bytes: vector<u8>): vector<u8>;
+

+
+
+
+
+
+
+
+
fun spec_signature_verify_strict_t<T>(signature: Signature, public_key: UnvalidatedPublicKey, data: T): bool {
+   let encoded = ed25519::new_signed_message<T>(data);
+   let message = bcs::serialize(encoded);
+   spec_signature_verify_strict_internal(signature.bytes, public_key.bytes, message)
+}
+

+
+
 [move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-stdlib/doc/type_info.md b/aptos-move/framework/aptos-stdlib/doc/type_info.md
index 34eaff24de6ea..7e7ae74990cb3 100644
--- a/aptos-move/framework/aptos-stdlib/doc/type_info.md
+++ b/aptos-move/framework/aptos-stdlib/doc/type_info.md
@@ -18,6 +18,9 @@
 -  [Function `verify_type_of`](#0x1_type_info_verify_type_of)
 -  [Function `verify_type_of_generic`](#0x1_type_info_verify_type_of_generic)
 -  [Specification](#@Specification_1)
+    -  [Function `chain_id`](#@Specification_1_chain_id)
+    -  [Function `type_of`](#@Specification_1_type_of)
+    -  [Function `type_name`](#@Specification_1_type_name)
     -  [Function `chain_id_internal`](#@Specification_1_chain_id_internal)
     -  [Function `verify_type_of_generic`](#@Specification_1_verify_type_of_generic)
 
@@ -353,6 +356,44 @@ analysis of vector size dynamism.
 ## Specification
 
 
+
+
+### Function `chain_id`
+
+
+
public fun chain_id(): u8
+

+
+
+
+
+
ensures result == spec_chain_id_internal();
+

+
+
+
+
+
+### Function `type_of`
+
+
+
public fun type_of<T>(): type_info::TypeInfo
+

+
+
+
+
+
+
+### Function `type_name`
+
+
+
public fun type_name<T>(): string::String
+

+
+
+
+
 
 
 ### Function `chain_id_internal`
@@ -371,36 +412,36 @@ analysis of vector size dynamism.
 
 
 
-
 
-### Function `verify_type_of_generic`
+
 
 
-
fun verify_type_of_generic<T>()
+
fun spec_chain_id_internal(): u8;
 

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

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

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

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

 
 
diff --git a/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move b/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move
index 8998aa3d0a39f..bf39ec56db8ef 100644
--- a/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move
@@ -5,10 +5,13 @@ spec aptos_std::ed25519 {
     // -----------------------
 
     spec new_unvalidated_public_key_from_bytes(bytes: vector): UnvalidatedPublicKey {
-        let length = len(bytes);
-        aborts_if length != PUBLIC_KEY_NUM_BYTES;
+        include NewUnvalidatedPublicKeyFromBytesAbortsIf;
         ensures result == UnvalidatedPublicKey { bytes };
     }
+    spec schema NewUnvalidatedPublicKeyFromBytesAbortsIf {
+        bytes: vector;
+        aborts_if len(bytes) != PUBLIC_KEY_NUM_BYTES;
+    }
 
     spec new_validated_public_key_from_bytes(bytes: vector): Option {
         aborts_if false;
@@ -18,17 +21,25 @@ spec aptos_std::ed25519 {
     }
 
     spec new_signature_from_bytes(bytes: vector): Signature {
-        aborts_if len(bytes)!= SIGNATURE_NUM_BYTES;
+        include NewSignatureFromBytesAbortsIf;
         ensures result == Signature { bytes };
     }
+    spec schema NewSignatureFromBytesAbortsIf {
+        bytes: vector;
+        aborts_if len(bytes) != SIGNATURE_NUM_BYTES;
+    }
+
+    spec public_key_bytes_to_authentication_key(pk_bytes: vector): vector {
+        pragma opaque;
+        aborts_if false;
+        ensures [abstract] result == spec_public_key_bytes_to_authentication_key(pk_bytes);
+    }
 
 
     // ----------------
     // Native functions
     // ----------------
 
-    spec fun spec_public_key_validate_internal(bytes: vector): bool;
-
     spec fun spec_signature_verify_strict_internal(
         signature: vector,
         public_key: vector,
@@ -50,4 +61,23 @@ spec aptos_std::ed25519 {
         aborts_if false;
         ensures result == spec_signature_verify_strict_internal(signature, public_key, message);
     }
+
+
+    // ----------------
+    // Helper functions
+    // ----------------
+
+    spec fun spec_public_key_validate_internal(bytes: vector): bool;
+
+    spec fun spec_public_key_bytes_to_authentication_key(pk_bytes: vector): vector;
+
+    spec fun spec_signature_verify_strict_t(signature: Signature, public_key: UnvalidatedPublicKey, data: T): bool {
+        let encoded = SignedMessage {
+            type_info: type_info::type_of(),
+            inner: data,
+        };
+        let message = bcs::serialize(encoded);
+        spec_signature_verify_strict_internal(signature.bytes, public_key.bytes, message)
+    }
+
 }
diff --git a/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move b/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move
index 64c4217203b08..36f95b7506704 100644
--- a/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move
@@ -5,15 +5,18 @@ spec aptos_std::multi_ed25519 {
     // -----------------------
 
     spec new_unvalidated_public_key_from_bytes(bytes: vector): UnvalidatedPublicKey {
+        include NewUnvalidatedPublicKeyFromBytesAbortsIf;
+        ensures result == UnvalidatedPublicKey { bytes };
+    }
+    spec schema NewUnvalidatedPublicKeyFromBytesAbortsIf {
+        bytes: vector;
         let length = len(bytes);
         aborts_if length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
         aborts_if length % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES != THRESHOLD_SIZE_BYTES;
-        ensures result == UnvalidatedPublicKey { bytes };
     }
 
     spec new_validated_public_key_from_bytes(bytes: vector): Option {
-        aborts_if len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES
-            && len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
+        aborts_if false;
         let cond = len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES
             && spec_public_key_validate_internal(bytes);
         ensures cond ==> result == option::spec_some(ValidatedPublicKey{bytes});
@@ -21,17 +24,24 @@ spec aptos_std::multi_ed25519 {
     }
 
     spec new_signature_from_bytes(bytes: vector): Signature {
-        aborts_if len(bytes) % INDIVIDUAL_SIGNATURE_NUM_BYTES != BITMAP_NUM_OF_BYTES;
+        include NewSignatureFromBytesAbortsIf;
         ensures result == Signature { bytes };
     }
+    spec schema NewSignatureFromBytesAbortsIf {
+        bytes: vector;
+        aborts_if len(bytes) % INDIVIDUAL_SIGNATURE_NUM_BYTES != BITMAP_NUM_OF_BYTES;
+    }
 
+    spec public_key_bytes_to_authentication_key(pk_bytes: vector): vector {
+        pragma opaque;
+        aborts_if false;
+        ensures [abstract] result == spec_public_key_bytes_to_authentication_key(pk_bytes);
+    }
 
     // ----------------
     // Native functions
     // ----------------
 
-    spec fun spec_public_key_validate_internal(bytes: vector): bool;
-
     spec fun spec_signature_verify_strict_internal(
         multisignature: vector,
         public_key: vector,
@@ -40,7 +50,8 @@ spec aptos_std::multi_ed25519 {
 
     spec public_key_validate_internal(bytes: vector): bool {
         pragma opaque;
-        aborts_if len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;
+        aborts_if false;
+        ensures (len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS) ==> (result == false);
         ensures result == spec_public_key_validate_internal(bytes);
     }
 
@@ -53,4 +64,19 @@ spec aptos_std::multi_ed25519 {
         aborts_if false;
         ensures result == spec_signature_verify_strict_internal(multisignature, public_key, message);
     }
+
+
+    // ----------------
+    // Helper functions
+    // ----------------
+
+    spec fun spec_public_key_validate_internal(bytes: vector): bool;
+
+    spec fun spec_public_key_bytes_to_authentication_key(pk_bytes: vector): vector;
+
+    spec fun spec_signature_verify_strict_t(signature: Signature, public_key: UnvalidatedPublicKey, data: T): bool {
+        let encoded = ed25519::new_signed_message(data);
+        let message = bcs::serialize(encoded);
+        spec_signature_verify_strict_internal(signature.bytes, public_key.bytes, message)
+    }
 }
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 f73b3f11e2595..ad582864b0a09 100644
--- a/aptos-move/framework/aptos-stdlib/sources/type_info.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/type_info.spec.move
@@ -1,14 +1,27 @@
 spec aptos_std::type_info {
-    // Move Prover natively supports `type_of` and `type_name`.
 
     spec native fun spec_is_struct(): bool;
 
-    // The chain ID is modeled as an uninterpreted function.
-    spec fun spec_chain_id_internal(): u8;
+    spec type_of(): TypeInfo {
+        // Move Prover natively supports this function.
+        // This function will abort if `T` is not a struct type.
+    }
+
+    spec type_name(): string::String {
+        // Move Prover natively supports this function.
+    }
+
+    spec chain_id(): u8 {
+        // TODO: Requires the bit operation support to specify the aborts_if condition.
+        ensures result == spec_chain_id_internal();
+    }
 
     spec chain_id_internal(): u8 {
         pragma opaque;
         aborts_if false;
         ensures result == spec_chain_id_internal();
     }
+
+    // The chain ID is modeled as an uninterpreted function.
+    spec fun spec_chain_id_internal(): u8;
 }
diff --git a/aptos-move/framework/move-stdlib/doc/option.md b/aptos-move/framework/move-stdlib/doc/option.md
index 5f041a4f609fb..47e28cb42d931 100644
--- a/aptos-move/framework/move-stdlib/doc/option.md
+++ b/aptos-move/framework/move-stdlib/doc/option.md
@@ -898,6 +898,7 @@ because it's 0 for "none" or 1 for "some".
 
 
 
pragma opaque;
+aborts_if false;
 ensures result == old(t);
 ensures borrow(t) == e;
 

diff --git a/aptos-move/framework/move-stdlib/sources/option.move b/aptos-move/framework/move-stdlib/sources/option.move
index 435d7fba7d58b..055f9b02152f0 100644
--- a/aptos-move/framework/move-stdlib/sources/option.move
+++ b/aptos-move/framework/move-stdlib/sources/option.move
@@ -189,6 +189,7 @@ module std::option {
     }
     spec swap_or_fill {
         pragma opaque;
+        aborts_if false;
         ensures result == old(t);
         ensures borrow(t) == e;
     }