Module `0x1::RecoveryAddress`

This module defines an account recovery mechanism that can be used by VASPs.

Resource RecoveryAddress
Constants
Function publish
Function rotate_authentication_key
Function add_rotation_capability
Module Specification

<pre><code>use <a href="DiemAccount.md#0x1_DiemAccount">0x1::DiemAccount</a>; use <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors">0x1::Errors</a>; use <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer">0x1::Signer</a>; use <a href="VASP.md#0x1_VASP">0x1::VASP</a>; use <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector">0x1::Vector</a>; </code></pre>

Resource `RecoveryAddress`

A resource that holds the <code>KeyRotationCapability</code>s for several accounts belonging to the same VASP. A VASP account that delegates its <code>KeyRotationCapability</code> to but also allows the account that stores the <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource to rotate its authentication key. This is useful as an account recovery mechanism: VASP accounts can all delegate their rotation capabilities to a single <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource stored under address A. The authentication key for A can be "buried in the mountain" and dug up only if the need to recover one of accounts in <code>rotation_caps</code> arises.

<pre><code>struct <a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>rotation_caps: vector<<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>></code> </dt> <dd> </dd> </dl> </details>

Constants

Only VASPs can create a recovery address

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_ENOT_A_VASP">ENOT_A_VASP</a>: u64 = 0; </code></pre>

The account address couldn't be found in the account recovery resource

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_EACCOUNT_NOT_RECOVERABLE">EACCOUNT_NOT_RECOVERABLE</a>: u64 = 4; </code></pre>

The signer doesn't have the appropriate privileges to rotate the account's key

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_ECANNOT_ROTATE_KEY">ECANNOT_ROTATE_KEY</a>: u64 = 2; </code></pre>

Only accounts belonging to the same VASP can delegate their key rotation capability

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_EINVALID_KEY_ROTATION_DELEGATION">EINVALID_KEY_ROTATION_DELEGATION</a>: u64 = 3; </code></pre>

A cycle would have been created would be created

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_EKEY_ROTATION_DEPENDENCY_CYCLE">EKEY_ROTATION_DEPENDENCY_CYCLE</a>: u64 = 1; </code></pre>

The maximum allowed number of keys have been registered with this recovery address.

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_EMAX_KEYS_REGISTERED">EMAX_KEYS_REGISTERED</a>: u64 = 6; </code></pre>

A <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource was in an unexpected state

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_ERECOVERY_ADDRESS">ERECOVERY_ADDRESS</a>: u64 = 5; </code></pre>

The maximum number of keys that can be registered with a single recovery address.

<pre><code>const <a href="RecoveryAddress.md#0x1_RecoveryAddress_MAX_REGISTERED_KEYS">MAX_REGISTERED_KEYS</a>: u64 = 256; </code></pre>

Function `publish`

Extract the <code>KeyRotationCapability</code> for <code>recovery_account</code> and publish it in a <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource under <code>recovery_account</code>. Aborts if <code>recovery_account</code> has delegated its <code>KeyRotationCapability</code>, already has a <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource, or is not a VASP.

<pre><code>public fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_publish">publish</a>(recovery_account: &signer, rotation_cap: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_publish">publish</a>(recovery_account: &signer, rotation_cap: KeyRotationCapability) { let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(recovery_account); // Only VASPs can create a recovery address assert(<a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_ENOT_A_VASP">ENOT_A_VASP</a>)); // put the rotation capability for the recovery account itself in `rotation_caps`. This // ensures two things: // (1) It's not possible to get into a "recovery cycle" where A is the recovery account for // B and B is the recovery account for A // (2) rotation_caps is always nonempty assert( *<a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">DiemAccount::key_rotation_capability_address</a>(&rotation_cap) == addr, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_EKEY_ROTATION_DEPENDENCY_CYCLE">EKEY_ROTATION_DEPENDENCY_CYCLE</a>) ); assert(!exists<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_ERECOVERY_ADDRESS">ERECOVERY_ADDRESS</a>)); move_to( recovery_account, <a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a> { rotation_caps: <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_singleton">Vector::singleton</a>(rotation_cap) } ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="RecoveryAddress.md#0x1_RecoveryAddress_PublishAbortsIf">PublishAbortsIf</a>; include <a href="RecoveryAddress.md#0x1_RecoveryAddress_PublishEnsures">PublishEnsures</a>; </code></pre>

<pre><code>schema <a href="RecoveryAddress.md#0x1_RecoveryAddress_PublishAbortsIf">PublishAbortsIf</a> { recovery_account: signer; rotation_cap: KeyRotationCapability; let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(recovery_account); aborts_if !<a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; aborts_if <a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">DiemAccount::key_rotation_capability_address</a>(rotation_cap) != addr with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

<pre><code>schema <a href="RecoveryAddress.md#0x1_RecoveryAddress_PublishEnsures">PublishEnsures</a> { recovery_account: signer; rotation_cap: KeyRotationCapability; let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(recovery_account); ensures <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(addr); ensures len(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(addr)) == 1; ensures <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(addr)[0] == rotation_cap; } </code></pre> </details>

Function `rotate_authentication_key`

Rotate the authentication key of <code>to_recover</code> to <code>new_key</code>. Can be invoked by either <code>recovery_address</code> or <code>to_recover</code>. Aborts if <code>recovery_address</code> does not have the <code>KeyRotationCapability</code> for <code>to_recover</code>.

<pre><code>public fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_rotate_authentication_key">rotate_authentication_key</a>(account: &signer, recovery_address: address, to_recover: address, new_key: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_rotate_authentication_key">rotate_authentication_key</a>( account: &signer, recovery_address: address, to_recover: address, new_key: vector<u8> ) acquires <a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a> { // Check that `recovery_address` has a `<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>` resource assert(exists<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(recovery_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_ERECOVERY_ADDRESS">ERECOVERY_ADDRESS</a>)); let sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert( // The original owner of a key rotation capability can rotate its own key sender == to_recover || // The owner of the `<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>` resource can rotate any key sender == recovery_address, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_ECANNOT_ROTATE_KEY">ECANNOT_ROTATE_KEY</a>) ); let caps = &borrow_global<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(recovery_address).rotation_caps; let i = 0; let len = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(caps); while ({ spec { assert i <= len; assert forall j in 0..i: caps[j].account_address != to_recover; }; (i < len) }) { let cap = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(caps, i); if (<a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">DiemAccount::key_rotation_capability_address</a>(cap) == &to_recover) { <a href="DiemAccount.md#0x1_DiemAccount_rotate_authentication_key">DiemAccount::rotate_authentication_key</a>(cap, new_key); return }; i = i + 1 }; spec { assert i == len; assert forall j in 0..len: caps[j].account_address != to_recover; }; // Couldn't find `to_recover` in the account recovery resource; abort abort <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_EACCOUNT_NOT_RECOVERABLE">EACCOUNT_NOT_RECOVERABLE</a>) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="RecoveryAddress.md#0x1_RecoveryAddress_RotateAuthenticationKeyAbortsIf">RotateAuthenticationKeyAbortsIf</a>; include <a href="RecoveryAddress.md#0x1_RecoveryAddress_RotateAuthenticationKeyEnsures">RotateAuthenticationKeyEnsures</a>; </code></pre>

<pre><code>schema <a href="RecoveryAddress.md#0x1_RecoveryAddress_RotateAuthenticationKeyAbortsIf">RotateAuthenticationKeyAbortsIf</a> { account: signer; recovery_address: address; to_recover: address; new_key: vector<u8>; aborts_if !<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(recovery_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">DiemAccount::exists_at</a>(to_recover) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if len(new_key) != 32 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if !<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_holds_key_rotation_cap_for">spec_holds_key_rotation_cap_for</a>(recovery_address, to_recover) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if !(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account) == recovery_address || <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account) == to_recover) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

<pre><code>schema <a href="RecoveryAddress.md#0x1_RecoveryAddress_RotateAuthenticationKeyEnsures">RotateAuthenticationKeyEnsures</a> { to_recover: address; new_key: vector<u8>; ensures <a href="DiemAccount.md#0x1_DiemAccount_authentication_key">DiemAccount::authentication_key</a>(to_recover) == new_key; } </code></pre> </details>

Function `add_rotation_capability`

Add <code>to_recover</code> to the <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource under <code>recovery_address</code>. Aborts if <code>to_recover.address</code> and <code>recovery_address</code> belong to different VASPs, or if <code>recovery_address</code> does not have a <code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> resource.

<pre><code>public fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_add_rotation_capability">add_rotation_capability</a>(to_recover: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>, recovery_address: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_add_rotation_capability">add_rotation_capability</a>(to_recover: KeyRotationCapability, recovery_address: address) acquires <a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a> { // Check that `recovery_address` has a `<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>` resource assert(exists<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(recovery_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_ERECOVERY_ADDRESS">ERECOVERY_ADDRESS</a>)); // Only accept the rotation capability if both accounts belong to the same <a href="VASP.md#0x1_VASP">VASP</a> let to_recover_address = *<a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">DiemAccount::key_rotation_capability_address</a>(&to_recover); assert( <a href="VASP.md#0x1_VASP_is_same_vasp">VASP::is_same_vasp</a>(recovery_address, to_recover_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_EINVALID_KEY_ROTATION_DELEGATION">EINVALID_KEY_ROTATION_DELEGATION</a>) ); let recovery_caps = &mut borrow_global_mut<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(recovery_address).rotation_caps; assert( <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(recovery_caps) < <a href="RecoveryAddress.md#0x1_RecoveryAddress_MAX_REGISTERED_KEYS">MAX_REGISTERED_KEYS</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="RecoveryAddress.md#0x1_RecoveryAddress_EMAX_KEYS_REGISTERED">EMAX_KEYS_REGISTERED</a>) ); <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_push_back">Vector::push_back</a>(recovery_caps, to_recover); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="RecoveryAddress.md#0x1_RecoveryAddress_AddRotationCapabilityAbortsIf">AddRotationCapabilityAbortsIf</a>; include <a href="RecoveryAddress.md#0x1_RecoveryAddress_AddRotationCapabilityEnsures">AddRotationCapabilityEnsures</a>; </code></pre>

<pre><code>schema <a href="RecoveryAddress.md#0x1_RecoveryAddress_AddRotationCapabilityAbortsIf">AddRotationCapabilityAbortsIf</a> { to_recover: KeyRotationCapability; recovery_address: address; aborts_if !<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(recovery_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if len(global<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(recovery_address).rotation_caps) >= <a href="RecoveryAddress.md#0x1_RecoveryAddress_MAX_REGISTERED_KEYS">MAX_REGISTERED_KEYS</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; let to_recover_address = <a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">DiemAccount::key_rotation_capability_address</a>(to_recover); aborts_if !<a href="VASP.md#0x1_VASP_spec_is_same_vasp">VASP::spec_is_same_vasp</a>(recovery_address, to_recover_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

<pre><code>schema <a href="RecoveryAddress.md#0x1_RecoveryAddress_AddRotationCapabilityEnsures">AddRotationCapabilityEnsures</a> { to_recover: KeyRotationCapability; recovery_address: address; let post num_rotation_caps = len(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(recovery_address)); ensures <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(recovery_address)[num_rotation_caps - 1] == to_recover; } </code></pre> </details>

Module Specification

Initialization

A RecoveryAddress has its own <code>KeyRotationCapability</code>.

<pre><code>invariant [global, isolated] forall addr1: address where <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(addr1): len(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(addr1)) > 0 && <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(addr1)[0].account_address == addr1; </code></pre>

Persistence of Resource

<pre><code>invariant update forall addr: address: old(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(addr)) ==> <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(addr); </code></pre>

Persistence of KeyRotationCapability

<code><a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a></code> persists

<pre><code>invariant update forall addr: address where old(exists<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(addr)): exists<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(addr); </code></pre>

If <code>recovery_addr</code> holds the <code>KeyRotationCapability</code> of <code>to_recovery_addr</code> in the previous state, then it continues to hold the capability after the update.

<pre><code>invariant update forall recovery_addr: address, to_recovery_addr: address where old(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(recovery_addr)): old(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_holds_key_rotation_cap_for">spec_holds_key_rotation_cap_for</a>(recovery_addr, to_recovery_addr)) ==> <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_holds_key_rotation_cap_for">spec_holds_key_rotation_cap_for</a>(recovery_addr, to_recovery_addr); </code></pre>

Consistency Between Resources and Roles

Only VASPs can hold <code>RecoverAddress</code> resources.

<pre><code>invariant [global, isolated] forall recovery_addr: address where <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(recovery_addr): <a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(recovery_addr); </code></pre>

Helper Functions

Returns true if <code>addr</code> is a recovery address.

<pre><code>fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_is_recovery_address">spec_is_recovery_address</a>(addr: address): bool { exists<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(addr) } </code></pre>

Returns all the <code>KeyRotationCapability</code>s held at <code>recovery_address</code>.

<pre><code>fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(recovery_address: address): vector<<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>> { global<<a href="RecoveryAddress.md#0x1_RecoveryAddress">RecoveryAddress</a>>(recovery_address).rotation_caps } </code></pre>

Returns true if <code>recovery_address</code> holds the <code>KeyRotationCapability</code> for <code>addr</code>.

<pre><code>fun <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_holds_key_rotation_cap_for">spec_holds_key_rotation_cap_for</a>( recovery_address: address, addr: address): bool { exists i: u64 where 0 <= i && i < len(<a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(recovery_address)): <a href="RecoveryAddress.md#0x1_RecoveryAddress_spec_get_rotation_caps">spec_get_rotation_caps</a>(recovery_address)[i].account_address == addr } </code></pre>

Module `0x1::RecoveryAddress`

Module 0x1::RecoveryAddress

Resource RecoveryAddress

Constants

Function publish

Function rotate_authentication_key

Function add_rotation_capability

Module Specification

Initialization

Persistence of Resource

Persistence of KeyRotationCapability

Consistency Between Resources and Roles

Helper Functions

Module `0x1::RecoveryAddress`

Resource `RecoveryAddress`

Function `publish`

Function `rotate_authentication_key`

Function `add_rotation_capability`