spec for set_originating_address

aptos-labs · Nov 5, 2024 · 5a591c2 · 5a591c2
1 parent 59b7f51
commit 5a591c2
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 0 deletions.
diff --git a/aptos-move/framework/aptos-framework/doc/account.md b/aptos-move/framework/aptos-framework/doc/account.md
@@ -74,6 +74,7 @@
     -  [Function `rotate_authentication_key`](#@Specification_1_rotate_authentication_key)
     -  [Function `rotate_authentication_key_with_rotation_capability`](#@Specification_1_rotate_authentication_key_with_rotation_capability)
     -  [Function `offer_rotation_capability`](#@Specification_1_offer_rotation_capability)
+    -  [Function `set_originating_address`](#@Specification_1_set_originating_address)
     -  [Function `is_rotation_capability_offered`](#@Specification_1_is_rotation_capability_offered)
     -  [Function `get_rotation_capability_offer_for`](#@Specification_1_get_rotation_capability_offer_for)
     -  [Function `revoke_rotation_capability`](#@Specification_1_revoke_rotation_capability)
@@ -2946,6 +2947,22 @@ The authentication scheme is ED25519_SCHEME and MULTI_ED25519_SCHEME
 
 
 
+<a id="@Specification_1_set_originating_address"></a>
+
+### Function `set_originating_address`
+
+
+<pre><code>entry <b>fun</b> <a href="account.md#0x1_account_set_originating_address">set_originating_address</a>(<a href="account.md#0x1_account">account</a>: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>)
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> verify=<b>false</b>;
+</code></pre>
+
+
+
 <a id="@Specification_1_is_rotation_capability_offered"></a>
 
 ### Function `is_rotation_capability_offered`

diff --git a/aptos-move/framework/aptos-framework/sources/account.spec.move b/aptos-move/framework/aptos-framework/sources/account.spec.move
@@ -661,6 +661,10 @@ spec aptos_framework::account {
         aborts_if account.sequence_number != 0;
     }
 
+    spec originating_address(auth_key: address): Option<address> {
+        pragma verify=false;
+    }
+
     spec update_auth_key_and_originating_address_table(
         originating_addr: address,
         account_resource: &mut Account,
@@ -681,6 +685,7 @@ spec aptos_framework::account {
         aborts_if table::spec_contains(address_map, curr_auth_key) &&
             table::spec_get(address_map, curr_auth_key) != originating_addr;
         aborts_if !from_bcs::deserializable<address>(new_auth_key_vector);
+        aborts_if curr_auth_key == new_auth_key;
         aborts_if curr_auth_key != new_auth_key && table::spec_contains(address_map, new_auth_key);
 
         ensures table::spec_contains(global<OriginatingAddress>(@aptos_framework).address_map, from_bcs::deserialize<address>(new_auth_key_vector));
@@ -729,4 +734,8 @@ spec aptos_framework::account {
 
         aborts_if account_scheme != ED25519_SCHEME && account_scheme != MULTI_ED25519_SCHEME;
     }
+
+    spec set_originating_address(account: &signer) {
+        pragma verify=false;
+    }
 }