Module `0x1::NetworkIdentity`

Module managing Diemnet NetworkIdentity

Resource NetworkIdentity
Resource NetworkIdentityEventHandle
Struct NetworkIdentityChangeNotification
Constants
Function initialize_network_identity_event_handle
Function tc_network_identity_event_handle_exists
Function initialize_network_identity
Function get
Function add_identities
Function remove_identities
Function add_members_internal
Function remove_members_internal

<pre><code>use <a href="DiemTimestamp.md#0x1_DiemTimestamp">0x1::DiemTimestamp</a>; use <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors">0x1::Errors</a>; use <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event">0x1::Event</a>; use <a href="Roles.md#0x1_Roles">0x1::Roles</a>; use <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer">0x1::Signer</a>; use <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector">0x1::Vector</a>; </code></pre>

Resource `NetworkIdentity`

Holder for all <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a></code> in an account

<pre><code>struct <a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>identities: vector<vector<u8>></code> </dt> <dd> </dd> </dl> </details> <details> <summary>Specification</summary> <pre><code>include <a href="NetworkIdentity.md#0x1_NetworkIdentity_UniqueMembers">UniqueMembers</a><vector<u8>> {members: identities}; </code></pre> </details>

Resource `NetworkIdentityEventHandle`

<pre><code>struct <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>identity_change_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentity::NetworkIdentityChangeNotification</a>></code> </dt> <dd> Event handle for <code>identities</code> rotation events </dd> </dl> </details>

Struct `NetworkIdentityChangeNotification`

Message sent when there are updates to the <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a></code>.

<pre><code>struct <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>account: address</code> </dt> <dd> The address of the account that changed identities </dd> <dt> <code>identities: vector<vector<u8>></code> </dt> <dd> The new identities </dd> <dt> <code>time_rotated_seconds: u64</code> </dt> <dd> The time at which the <code>identities</code> was rotated </dd> </dl> </details>

Constants

Network ID doesn't exist when trying to get it

<pre><code>const <a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>: u64 = 0; </code></pre>

Network identity event handle invalid

<pre><code>const <a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_EVENT_HANDLE_INVALID">ENETWORK_ID_EVENT_HANDLE_INVALID</a>: u64 = 3; </code></pre>

Limit exceeded on number of identities for an address

<pre><code>const <a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_LIMIT_EXCEEDED">ENETWORK_ID_LIMIT_EXCEEDED</a>: u64 = 1; </code></pre>

No identities provided for changes

<pre><code>const <a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_NO_INPUT">ENETWORK_ID_NO_INPUT</a>: u64 = 2; </code></pre>

<pre><code>const <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a>: u64 = 100; </code></pre>

Function `initialize_network_identity_event_handle`

<pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_initialize_network_identity_event_handle">initialize_network_identity_event_handle</a>(tc_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_initialize_network_identity_event_handle">initialize_network_identity_event_handle</a>(tc_account: &signer) { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); assert( !exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(tc_account)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_EVENT_HANDLE_INVALID">ENETWORK_ID_EVENT_HANDLE_INVALID</a>) ); let event_handle = <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a> { identity_change_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a>>(tc_account), }; move_to( tc_account, event_handle, ); } </code></pre> </details>

Function `tc_network_identity_event_handle_exists`

<pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_tc_network_identity_event_handle_exists">tc_network_identity_event_handle_exists</a>(): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_tc_network_identity_event_handle_exists">tc_network_identity_event_handle_exists</a>(): bool { exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a>>(@TreasuryCompliance) } </code></pre> </details>

Function `initialize_network_identity`

Initialize <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a></code> with an empty list

<pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_initialize_network_identity">initialize_network_identity</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_initialize_network_identity">initialize_network_identity</a>(account: &signer) { let identities = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_empty">Vector::empty</a><vector<u8>>(); move_to(account, <a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a> { identities }); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); modifies global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr); </code></pre> </details>

Function `get`

Return the underlying <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a></code> bytes

<pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_get">get</a>(account_addr: address): vector<vector<u8>> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_get">get</a>(account_addr: address): vector<vector<u8>> acquires <a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a> { assert( exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>) ); *&borrow_global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>aborts_if !exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; ensures result == global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities; </code></pre> </details>

Function `add_identities`

Update and create if not exist <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a></code>

<pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_add_identities">add_identities</a>(account: &signer, to_add: vector<vector<u8>>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_add_identities">add_identities</a>(account: &signer, to_add: vector<vector<u8>>) acquires <a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>, <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a> { assert(<a href="NetworkIdentity.md#0x1_NetworkIdentity_tc_network_identity_event_handle_exists">tc_network_identity_event_handle_exists</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_EVENT_HANDLE_INVALID">ENETWORK_ID_EVENT_HANDLE_INVALID</a>)); let num_to_add = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&to_add); assert(num_to_add > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_NO_INPUT">ENETWORK_ID_NO_INPUT</a>)); if (!exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account))) { <a href="NetworkIdentity.md#0x1_NetworkIdentity_initialize_network_identity">initialize_network_identity</a>(account); }; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); let identity = borrow_global_mut<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr); let identities = &mut identity.identities; assert( <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(identities) + num_to_add <= <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_LIMIT_EXCEEDED">ENETWORK_ID_LIMIT_EXCEEDED</a>) ); let has_change = <a href="NetworkIdentity.md#0x1_NetworkIdentity_add_members_internal">add_members_internal</a>(identities, &to_add); if (has_change) { <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut borrow_global_mut<<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a>>(@TreasuryCompliance).identity_change_events, <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> { account: account_addr, identities: *&identity.identities, time_rotated_seconds: <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_seconds">DiemTimestamp::now_seconds</a>(), } ); } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma verify=false; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); let prior_identities = if (exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr)) { global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities } else { vec() }; let has_change = (exists e in to_add: !contains(prior_identities, e)); let post handle = global<<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a>>(@TreasuryCompliance).identity_change_events; let post msg = <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> { account: account_addr, identities: global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities, time_rotated_seconds: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_seconds">DiemTimestamp::spec_now_seconds</a>(), }; aborts_if !<a href="NetworkIdentity.md#0x1_NetworkIdentity_tc_network_identity_event_handle_exists">tc_network_identity_event_handle_exists</a>() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if len(to_add) == 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if len(prior_identities) + len(to_add) > MAX_U64; aborts_if len(prior_identities) + len(to_add) > <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; include has_change ==> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; include <a href="NetworkIdentity.md#0x1_NetworkIdentity_AddMembersInternalEnsures">AddMembersInternalEnsures</a><vector<u8>> { old_members: prior_identities, new_members: global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities, }; modifies global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr); emits msg to handle if has_change; </code></pre> </details>

Function `remove_identities`

Remove <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a></code>, skipping if it doesn't exist

<pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_remove_identities">remove_identities</a>(account: &signer, to_remove: vector<vector<u8>>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_remove_identities">remove_identities</a>(account: &signer, to_remove: vector<vector<u8>>) acquires <a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>, <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a> { assert(<a href="NetworkIdentity.md#0x1_NetworkIdentity_tc_network_identity_event_handle_exists">tc_network_identity_event_handle_exists</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_EVENT_HANDLE_INVALID">ENETWORK_ID_EVENT_HANDLE_INVALID</a>)); let num_to_remove = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&to_remove); assert(num_to_remove > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_NO_INPUT">ENETWORK_ID_NO_INPUT</a>)); assert( num_to_remove <= <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_LIMIT_EXCEEDED">ENETWORK_ID_LIMIT_EXCEEDED</a>) ); let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert( exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>) ); let identity = borrow_global_mut<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr); let identities = &mut identity.identities; let has_change = <a href="NetworkIdentity.md#0x1_NetworkIdentity_remove_members_internal">remove_members_internal</a>(identities, &to_remove); if (has_change) { <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut borrow_global_mut<<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a>>(@TreasuryCompliance).identity_change_events, <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> { account: account_addr, identities: *&identity.identities, time_rotated_seconds: <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_seconds">DiemTimestamp::now_seconds</a>(), } ); }; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); let prior_identities = global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities; let has_change = (exists e in to_remove: contains(prior_identities, e)); let post handle = global<<a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityEventHandle">NetworkIdentityEventHandle</a>>(@TreasuryCompliance).identity_change_events; let post msg = <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> { account: account_addr, identities: global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities, time_rotated_seconds: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_seconds">DiemTimestamp::spec_now_seconds</a>(), }; aborts_if !<a href="NetworkIdentity.md#0x1_NetworkIdentity_tc_network_identity_event_handle_exists">tc_network_identity_event_handle_exists</a>() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if len(to_remove) == 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if len(to_remove) > <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; aborts_if !exists<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; include has_change ==> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; include <a href="NetworkIdentity.md#0x1_NetworkIdentity_RemoveMembersInternalEnsures">RemoveMembersInternalEnsures</a><vector<u8>> { old_members: prior_identities, new_members: global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr).identities, }; modifies global<<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>>(account_addr); emits msg to handle if has_change; </code></pre> </details>

Function `add_members_internal`

Add all elements that appear in <code>to_add</code> into <code>members</code>.

The <code>members</code> argument is essentially a set simulated by a vector, hence the uniqueness of its elements are guaranteed, before and after the bulk insertion. The <code>to_add</code> argument, on the other hand, does not guarantee to be a set and hence can have duplicated elements.

<pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_add_members_internal">add_members_internal</a><T: copy>(members: &mut vector<T>, to_add: &vector<T>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_add_members_internal">add_members_internal</a><T: copy>( members: &mut vector<T>, to_add: &vector<T>, ): bool { let num_to_add = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(to_add); let num_existing = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(members); let i = 0; while ({ spec { invariant i <= num_to_add; // the set can never reduce in size invariant len(members) >= len(old(members)); // the current set maintains the uniqueness of the elements invariant forall j in 0..len(members), k in 0..len(members): members[j] == members[k] ==> j == k; // the left-split of the current set is exactly the same as the original set invariant forall j in 0..len(old(members)): members[j] == old(members)[j]; // all elements in the the right-split of the current set is from the `to_add` vector invariant forall j in len(old(members))..len(members): contains(to_add[0..i], members[j]); // the current set includes everything in `to_add` we have seen so far invariant forall j in 0..i: contains(members, to_add[j]); // having no new members means that all elements in the `to_add` vector we have seen so far are already // in the existing set, and vice versa. invariant len(members) == len(old(members)) <==> (forall j in 0..i: contains(old(members), to_add[j])); }; (i < num_to_add) }) { let entry = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(to_add, i); if (!<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_contains">Vector::contains</a>(members, entry)) { <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_push_back">Vector::push_back</a>(members, *entry); }; i = i + 1; }; <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(members) > num_existing } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; ensures [concrete] true; aborts_if false; include <a href="NetworkIdentity.md#0x1_NetworkIdentity_AddMembersInternalEnsures">AddMembersInternalEnsures</a><T> { old_members: old(members), new_members: members, }; include <a href="NetworkIdentity.md#0x1_NetworkIdentity_UniqueMembers">UniqueMembers</a><T>; ensures result == (exists e in to_add: !contains(old(members), e)); </code></pre>

<pre><code>schema <a href="NetworkIdentity.md#0x1_NetworkIdentity_AddMembersInternalEnsures">AddMembersInternalEnsures</a><T> { old_members: vector<T>; new_members: vector<T>; to_add: vector<T>; ensures forall e in to_add: contains(new_members, e); ensures forall e in old_members: contains(new_members, e); ensures forall e in new_members: (contains(old_members, e) || contains(to_add, e)); } </code></pre> </details>

Function `remove_members_internal`

Remove all elements that appear in <code>to_remove</code> from <code>members</code>.

The <code>members</code> argument is essentially a set simulated by a vector, hence the uniqueness of its elements are guaranteed, before and after the bulk removal. The <code>to_remove</code> argument, on the other hand, does not guarantee to be a set and hence can have duplicated elements.

<pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_remove_members_internal">remove_members_internal</a><T: drop>(members: &mut vector<T>, to_remove: &vector<T>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="NetworkIdentity.md#0x1_NetworkIdentity_remove_members_internal">remove_members_internal</a><T: drop>( members: &mut vector<T>, to_remove: &vector<T>, ): bool { let num_existing = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(members); let num_to_remove = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(to_remove); let i = 0; while ({ spec { invariant i <= num_to_remove; // the set can never grow in size invariant len(members) <= len(old(members)); // the current set maintains the uniqueness of the elements invariant forall j in 0..len(members), k in 0..len(members): members[j] == members[k] ==> j == k; // all elements in the the current set come from the original set invariant forall j in 0..len(members): contains(old(members), members[j]); // the current set never contains anything from the `to_remove` vector invariant forall j in 0..i: !contains(members, to_remove[j]); // the current set should never remove an element from the original set which is not in `to_remove` invariant forall j in 0..len(old(members)): (contains(to_remove[0..i], old(members)[j]) || contains(members, old(members)[j])); // having the same member means that all elements in the `to_remove` vector we have seen so far are not // in the existing set, and vice versa. invariant len(members) == len(old(members)) <==> (forall j in 0..i: !contains(old(members), to_remove[j])); }; (i < num_to_remove) }) { let entry = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(to_remove, i); let (exist, index) = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_index_of">Vector::index_of</a>(members, entry); if (exist) { <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_swap_remove">Vector::swap_remove</a>(members, index); }; i = i + 1; }; <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(members) < num_existing } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma verify = false; pragma opaque; ensures [concrete] true; aborts_if false; include <a href="NetworkIdentity.md#0x1_NetworkIdentity_RemoveMembersInternalEnsures">RemoveMembersInternalEnsures</a><T> { old_members: old(members), new_members: members, }; include <a href="NetworkIdentity.md#0x1_NetworkIdentity_UniqueMembers">UniqueMembers</a><T>; ensures result == (exists e in to_remove: contains(old(members), e)); </code></pre>

<pre><code>schema <a href="NetworkIdentity.md#0x1_NetworkIdentity_RemoveMembersInternalEnsures">RemoveMembersInternalEnsures</a><T> { old_members: vector<T>; new_members: vector<T>; to_remove: vector<T>; ensures forall e in to_remove: !contains(new_members, e); ensures forall e in new_members: contains(old_members, e); ensures forall e in old_members: (contains(to_remove, e) || contains(new_members, e)); } </code></pre>

<pre><code>schema <a href="NetworkIdentity.md#0x1_NetworkIdentity_UniqueMembers">UniqueMembers</a><T> { members: vector<T>; invariant forall i in 0..len(members), j in 0..len(members): members[i] == members[j] ==> i == j; } </code></pre> </details>

Module `0x1::NetworkIdentity`

Module 0x1::NetworkIdentity

Resource NetworkIdentity

Resource NetworkIdentityEventHandle

Struct NetworkIdentityChangeNotification

Constants

Function initialize_network_identity_event_handle

Function tc_network_identity_event_handle_exists

Function initialize_network_identity

Function get

Function add_identities

Function remove_identities

Function add_members_internal

Function remove_members_internal

Module `0x1::NetworkIdentity`

Resource `NetworkIdentity`

Resource `NetworkIdentityEventHandle`

Struct `NetworkIdentityChangeNotification`

Function `initialize_network_identity_event_handle`

Function `tc_network_identity_event_handle_exists`

Function `initialize_network_identity`

Function `get`

Function `add_identities`

Function `remove_identities`

Function `add_members_internal`

Function `remove_members_internal`