diff --git a/aptos-move/framework/aptos-framework/doc/auth_data.md b/aptos-move/framework/aptos-framework/doc/auth_data.md new file mode 100644 index 0000000000000..d24ad59f5cc25 --- /dev/null +++ b/aptos-move/framework/aptos-framework/doc/auth_data.md @@ -0,0 +1,111 @@ + + + +# Module `0x1::auth_data` + + + +- [Enum `AbstractionAuthData`](#0x1_auth_data_AbstractionAuthData) +- [Function `digest`](#0x1_auth_data_digest) +- [Function `authenticator`](#0x1_auth_data_authenticator) + + +
+ + + + + +## Enum `AbstractionAuthData` + + + +
enum AbstractionAuthData has copy, drop
+
+ + + +
+Variants + + +
+V1 + + +
+Fields + + +
+
+digest: vector<u8> +
+
+ +
+
+authenticator: vector<u8> +
+
+ +
+
+ + +
+ +
+ +
+ + + +## Function `digest` + + + +
public fun digest(signing_data: &auth_data::AbstractionAuthData): &vector<u8>
+
+ + + +
+Implementation + + +
public fun digest(signing_data: &AbstractionAuthData): &vector<u8> {
+    &signing_data.digest
+}
+
+ + + +
+ + + +## Function `authenticator` + + + +
public fun authenticator(signing_data: &auth_data::AbstractionAuthData): &vector<u8>
+
+ + + +
+Implementation + + +
public fun authenticator(signing_data: &AbstractionAuthData): &vector<u8> {
+    &signing_data.authenticator
+}
+
+ + + +
+ + +[move-book]: https://aptos.dev/move/book/SUMMARY diff --git a/aptos-move/framework/aptos-framework/doc/bcs_stream.md b/aptos-move/framework/aptos-framework/doc/bcs_stream.md index d1761a2e3abd8..0a48a8d096dd3 100644 --- a/aptos-move/framework/aptos-framework/doc/bcs_stream.md +++ b/aptos-move/framework/aptos-framework/doc/bcs_stream.md @@ -21,6 +21,7 @@ - [Function `deserialize_vector`](#0x1_bcs_stream_deserialize_vector) - [Function `deserialize_string`](#0x1_bcs_stream_deserialize_string) - [Function `deserialize_option`](#0x1_bcs_stream_deserialize_option) +- [Specification](#@Specification_1) 
use 0x1::error;
@@ -639,5 +640,14 @@ The elem_deserializer lambda expression is used to deserialize the
 
 
 
+
+
+## Specification
+
+
+
+
pragma verify = false;
+

+
 
 [move-book]: https://aptos.dev/move/book/SUMMARY
diff --git a/aptos-move/framework/aptos-framework/doc/lite_account.md b/aptos-move/framework/aptos-framework/doc/lite_account.md
index fe595f286e68b..98793b596ef70 100644
--- a/aptos-move/framework/aptos-framework/doc/lite_account.md
+++ b/aptos-move/framework/aptos-framework/doc/lite_account.md
@@ -23,14 +23,14 @@
     -  [Function `dispatchable_authenticate`](#@Specification_1_dispatchable_authenticate)
 
 
-
use 0x1::create_signer;
+
use 0x1::auth_data;
+use 0x1::create_signer;
 use 0x1::error;
 use 0x1::event;
 use 0x1::function_info;
 use 0x1::object;
 use 0x1::option;
 use 0x1::signer;
-use 0x1::signing_data;
 use 0x1::simple_map;
 use 0x1::string;
 

@@ -466,7 +466,7 @@ Return the current dispatchable authenticator move function info. Nonefun authenticate(account: signer, func_info: function_info::FunctionInfo, signing_data: signing_data::SigningData): signer
+
fun authenticate(account: signer, func_info: function_info::FunctionInfo, signing_data: auth_data::AbstractionAuthData): signer
 

 
 
@@ -478,12 +478,12 @@ Return the current dispatchable authenticator move function info. Nonefun authenticate(
     account: signer,
     func_info: FunctionInfo,
-    signing_data: SigningData,
+    signing_data: AbstractionAuthData,
 ): signer acquires DispatchableAuthenticator {
     let func_infos = dispatchable_authenticator_internal(signer::address_of(&account));
     assert!(simple_map::contains_key(func_infos, &func_info), error::not_found(EFUNCTION_INFO_EXISTENCE));
     function_info::load_module_from_function(&func_info);
-    dispatchable_authenticate(account, signing_data, &func_info)
+    dispatchable_authenticate(account, signing_data, &func_info)
 }
 

 
@@ -498,7 +498,7 @@ Return the current dispatchable authenticator move function info. Nonefun dispatchable_authenticate(account: signer, signing_data: signing_data::SigningData, function: &function_info::FunctionInfo): signer
+
fun dispatchable_authenticate(account: signer, signing_data: auth_data::AbstractionAuthData, function: &function_info::FunctionInfo): signer
 

 
 
@@ -509,7 +509,7 @@ The native function to dispatch customized move authentication function.
 
 
native fun dispatchable_authenticate(
     account: signer,
-    signing_data: SigningData,
+    signing_data: AbstractionAuthData,
     function: &FunctionInfo
 ): signer;
 

@@ -529,18 +529,32 @@ The native function to dispatch customized move authentication function.
 
 
 
+
+
+
+
+
fun spec_dispatchable_authenticate(
+   account: signer,
+   signing_data: AbstractionAuthData,
+   function: &FunctionInfo
+): signer;
+

+
+
+
 
 
 ### Function `dispatchable_authenticate`
 
 
-
fun dispatchable_authenticate(account: signer, signing_data: signing_data::SigningData, function: &function_info::FunctionInfo): signer
+
fun dispatchable_authenticate(account: signer, signing_data: auth_data::AbstractionAuthData, function: &function_info::FunctionInfo): signer
 

 
 
 
 
 
pragma opaque;
+ensures [abstract] result == spec_dispatchable_authenticate(account, signing_data, function);
 

 
 
diff --git a/aptos-move/framework/aptos-framework/doc/overview.md b/aptos-move/framework/aptos-framework/doc/overview.md
index dabef52fb55df..f79041d921116 100644
--- a/aptos-move/framework/aptos-framework/doc/overview.md
+++ b/aptos-move/framework/aptos-framework/doc/overview.md
@@ -19,6 +19,7 @@ This is the reference documentation of the Aptos framework.
 -  [`0x1::aptos_account`](aptos_account.md#0x1_aptos_account)
 -  [`0x1::aptos_coin`](aptos_coin.md#0x1_aptos_coin)
 -  [`0x1::aptos_governance`](aptos_governance.md#0x1_aptos_governance)
+-  [`0x1::auth_data`](auth_data.md#0x1_auth_data)
 -  [`0x1::bcs_stream`](bcs_stream.md#0x1_bcs_stream)
 -  [`0x1::block`](block.md#0x1_block)
 -  [`0x1::chain_id`](chain_id.md#0x1_chain_id)
@@ -57,7 +58,6 @@ This is the reference documentation of the Aptos framework.
 -  [`0x1::reconfiguration_state`](reconfiguration_state.md#0x1_reconfiguration_state)
 -  [`0x1::reconfiguration_with_dkg`](reconfiguration_with_dkg.md#0x1_reconfiguration_with_dkg)
 -  [`0x1::resource_account`](resource_account.md#0x1_resource_account)
--  [`0x1::signing_data`](signing_data.md#0x1_signing_data)
 -  [`0x1::stake`](stake.md#0x1_stake)
 -  [`0x1::staking_config`](staking_config.md#0x1_staking_config)
 -  [`0x1::staking_contract`](staking_contract.md#0x1_staking_contract)
diff --git a/aptos-move/framework/aptos-framework/sources/account_abstraction/auth_data.move b/aptos-move/framework/aptos-framework/sources/account_abstraction/auth_data.move
new file mode 100644
index 0000000000000..57b7290e5c241
--- /dev/null
+++ b/aptos-move/framework/aptos-framework/sources/account_abstraction/auth_data.move
@@ -0,0 +1,18 @@
+module aptos_framework::auth_data {
+    enum AbstractionAuthData has copy, drop {
+        V1 { digest: vector, authenticator: vector },
+    }
+
+    #[test_only]
+    public fun create_auth_data(digest: vector): AbstractionAuthData {
+        AbstractionAuthData::V1 { digest }
+    }
+
+    public fun digest(signing_data: &AbstractionAuthData): &vector {
+        &signing_data.digest
+    }
+
+    public fun authenticator(signing_data: &AbstractionAuthData): &vector {
+        &signing_data.authenticator
+    }
+}
diff --git a/aptos-move/framework/aptos-framework/sources/account_abstraction/bcs_stream.spec.move b/aptos-move/framework/aptos-framework/sources/account_abstraction/bcs_stream.spec.move
new file mode 100644
index 0000000000000..d8ea888f9f269
--- /dev/null
+++ b/aptos-move/framework/aptos-framework/sources/account_abstraction/bcs_stream.spec.move
@@ -0,0 +1,5 @@
+spec aptos_framework::bcs_stream {
+    spec module {
+        pragma verify = false;
+    }
+}
diff --git a/aptos-move/framework/aptos-framework/sources/account_abstraction/signing_data.move b/aptos-move/framework/aptos-framework/sources/account_abstraction/signing_data.move
deleted file mode 100644
index 4c51dcfbcb4ad..0000000000000
--- a/aptos-move/framework/aptos-framework/sources/account_abstraction/signing_data.move
+++ /dev/null
@@ -1,18 +0,0 @@
-module aptos_framework::signing_data {
-    enum SigningData has copy, drop {
-        V1 { digest: vector, authenticator: vector },
-    }
-
-    #[test_only]
-    public fun create_signing_data(digest: vector): SigningData {
-        SigningData::V1 { digest }
-    }
-
-    public fun digest(signing_data: &SigningData): &vector {
-        &signing_data.digest
-    }
-
-    public fun authenticator(signing_data: &SigningData): &vector {
-        &signing_data.authenticator
-    }
-}
diff --git a/aptos-move/framework/aptos-framework/sources/lite_account.move b/aptos-move/framework/aptos-framework/sources/lite_account.move
index 6926d85fbcd48..d7debaab3fd41 100644
--- a/aptos-move/framework/aptos-framework/sources/lite_account.move
+++ b/aptos-move/framework/aptos-framework/sources/lite_account.move
@@ -10,7 +10,7 @@ module aptos_framework::lite_account {
     use aptos_framework::event;
     use aptos_framework::function_info::{Self, FunctionInfo};
     use aptos_framework::object;
-    use aptos_framework::signing_data::SigningData;
+    use aptos_framework::auth_data::AbstractionAuthData;
     #[test_only]
     use aptos_framework::account::create_account_for_test;
 
@@ -162,7 +162,7 @@ module aptos_framework::lite_account {
     fun authenticate(
         account: signer,
         func_info: FunctionInfo,
-        signing_data: SigningData,
+        signing_data: AbstractionAuthData,
     ): signer acquires DispatchableAuthenticator {
         let func_infos = dispatchable_authenticator_internal(signer::address_of(&account));
         assert!(simple_map::contains_key(func_infos, &func_info), error::not_found(EFUNCTION_INFO_EXISTENCE));
@@ -173,7 +173,7 @@ module aptos_framework::lite_account {
     /// The native function to dispatch customized move authentication function.
     native fun dispatchable_authenticate(
         account: signer,
-        signing_data: SigningData,
+        signing_data: AbstractionAuthData,
         function: &FunctionInfo
     ): signer;
 
diff --git a/aptos-move/framework/aptos-framework/sources/lite_account.spec.move b/aptos-move/framework/aptos-framework/sources/lite_account.spec.move
index d5c0deec34884..c099ea9f26404 100644
--- a/aptos-move/framework/aptos-framework/sources/lite_account.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/lite_account.spec.move
@@ -3,7 +3,15 @@ spec aptos_framework::lite_account {
         pragma verify = false;
     }
 
-    spec dispatchable_authenticate {
+
+    spec fun spec_dispatchable_authenticate(
+        account: signer,
+        signing_data: AbstractionAuthData,
+        function: &FunctionInfo
+    ): signer;
+
+    spec dispatchable_authenticate(account: signer, signing_data: AbstractionAuthData, function: &FunctionInfo): signer {
         pragma opaque;
+        ensures [abstract] result == spec_dispatchable_authenticate(account, signing_data, function);
     }
 }
diff --git a/aptos-move/move-examples/account_abstraction/bls12381_single_key/sources/single_key.move b/aptos-move/move-examples/account_abstraction/bls12381_single_key/sources/single_key.move
index 73b3f5b62033f..25e1e37c0ffa7 100644
--- a/aptos-move/move-examples/account_abstraction/bls12381_single_key/sources/single_key.move
+++ b/aptos-move/move-examples/account_abstraction/bls12381_single_key/sources/single_key.move
@@ -2,7 +2,7 @@ module aa::single_key {
     use std::option;
     use std::signer;
     use aptos_std::bls12381::{Self, PublicKey};
-    use aptos_framework::signing_data::{Self, SigningData};
+    use aptos_framework::auth_data::{Self, AbstractionAuthData};
 
     /// Only fungible asset metadata owner can make changes.
     const EINVALID_PUBLIC_KEY: u64 = 1;
@@ -32,16 +32,16 @@ module aa::single_key {
     /// Authorization function for account abstraction.
     public fun authenticate(
         account: signer,
-        signing_data: SigningData,
+        signing_data: AbstractionAuthData,
     ): signer acquires BLSPublicKey {
         let addr = signer::address_of(&account);
         assert!(exists(addr), EPUBLIC_KEY_NOT_FOUND);
         let pubkey = &borrow_global(addr).key;
         assert!(
             bls12381::verify_normal_signature(
-                &bls12381::signature_from_bytes(*signing_data::authenticator(&signing_data)),
+                &bls12381::signature_from_bytes(*auth_data::authenticator(&signing_data)),
                 pubkey,
-                *signing_data::digest(&signing_data)
+                *auth_data::digest(&signing_data)
             ),
             EINVALID_SIGNATURE
         );