Module `0x1::DiemSystem`

Maintains information about the set of validators used during consensus. Provides functions to add, remove, and update validators in the validator set.

Note: When trying to understand this code, it's important to know that "config" and "configuration" are used for several distinct concepts.

Struct ValidatorInfo
Resource CapabilityHolder
Struct DiemSystem
Constants
Function initialize_validator_set
Function set_diem_system_config
Function add_validator
Function remove_validator
Function update_config_and_reconfigure
Function get_diem_system_config
Function is_validator
Function get_validator_config
Function validator_set_size
Function get_ith_validator_address
Function get_validator_index_
Function update_ith_validator_info_
Function is_validator_
Module Specification

<pre><code>use <a href="CoreAddresses.md#0x1_CoreAddresses">0x1::CoreAddresses</a>; use <a href="DiemConfig.md#0x1_DiemConfig">0x1::DiemConfig</a>; 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/Option.md#0x1_Option">0x1::Option</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="ValidatorConfig.md#0x1_ValidatorConfig">0x1::ValidatorConfig</a>; use <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector">0x1::Vector</a>; </code></pre>

Struct `ValidatorInfo`

Information about a Validator Owner.

<pre><code>struct <a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>addr: address</code> </dt> <dd> The address (account) of the Validator Owner </dd> <dt> <code>consensus_voting_power: u64</code> </dt> <dd> The voting power of the Validator Owner (currently always 1). </dd> <dt> <code>config: <a href="ValidatorConfig.md#0x1_ValidatorConfig_Config">ValidatorConfig::Config</a></code> </dt> <dd> Configuration information about the Validator, such as the Validator Operator, human name, and info such as consensus key and network addresses. </dd> <dt> <code>last_config_update_time: u64</code> </dt> <dd> The time of last reconfiguration invoked by this validator in microseconds </dd> </dl> </details>

Resource `CapabilityHolder`

Enables a scheme that restricts the DiemSystem config in DiemConfig from being modified by any other module. Only code in this module can get a reference to the ModifyConfigCapability<DiemSystem>, which is required by <code><a href="DiemConfig.md#0x1_DiemConfig_set_with_capability_and_reconfigure">DiemConfig::set_with_capability_and_reconfigure</a></code> to modify the DiemSystem config. This is only needed by <code>update_config_and_reconfigure</code>. Only Diem root can add or remove a validator from the validator set, so the capability is not needed for access control in those functions.

<pre><code>resource struct <a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>cap: <a href="DiemConfig.md#0x1_DiemConfig_ModifyConfigCapability">DiemConfig::ModifyConfigCapability</a><<a href="DiemSystem.md#0x1_DiemSystem_DiemSystem">DiemSystem::DiemSystem</a>></code> </dt> <dd> Holds a capability returned by <code><a href="DiemConfig.md#0x1_DiemConfig_publish_new_config_and_get_capability">DiemConfig::publish_new_config_and_get_capability</a></code> which is called in <code>initialize_validator_set</code>. </dd> </dl> </details>

Struct `DiemSystem`

The DiemSystem struct stores the validator set and crypto scheme in DiemConfig. The DiemSystem struct is stored by DiemConfig, which publishes a DiemConfig<DiemSystem> resource.

<pre><code>struct <a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>scheme: u8</code> </dt> <dd> The current consensus crypto scheme. </dd> <dt> <code>validators: vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">DiemSystem::ValidatorInfo</a>></code> </dt> <dd> The current validator set. </dd> </dl> </details> <details> <summary>Specification</summary>

Members of <code>validators</code> vector (the validator set) have unique addresses.

<pre><code>invariant forall i in 0..len(validators), j in 0..len(validators): validators[i].addr == validators[j].addr ==> i == j; </code></pre> </details>

Constants

The validator operator is not the operator for the specified validator

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_EINVALID_TRANSACTION_SENDER">EINVALID_TRANSACTION_SENDER</a>: u64 = 4; </code></pre>

Tried to add a validator to the validator set that was already in it

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_EALREADY_A_VALIDATOR">EALREADY_A_VALIDATOR</a>: u64 = 2; </code></pre>

The <code><a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a></code> resource was not in the required state

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_ECAPABILITY_HOLDER">ECAPABILITY_HOLDER</a>: u64 = 0; </code></pre>

Rate limited when trying to update config

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_ECONFIG_UPDATE_RATE_LIMITED">ECONFIG_UPDATE_RATE_LIMITED</a>: u64 = 6; </code></pre>

Tried to add a validator with an invalid state to the validator set

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_EINVALID_PROSPECTIVE_VALIDATOR">EINVALID_PROSPECTIVE_VALIDATOR</a>: u64 = 1; </code></pre>

Validator set already at maximum allowed size

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_EMAX_VALIDATORS">EMAX_VALIDATORS</a>: u64 = 7; </code></pre>

An operation was attempted on an address not in the vaidator set

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_ENOT_AN_ACTIVE_VALIDATOR">ENOT_AN_ACTIVE_VALIDATOR</a>: u64 = 3; </code></pre>

An out of bounds index for the validator set was encountered

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_EVALIDATOR_INDEX">EVALIDATOR_INDEX</a>: u64 = 5; </code></pre>

Number of microseconds in 5 minutes

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_FIVE_MINUTES">FIVE_MINUTES</a>: u64 = 300000000; </code></pre>

The maximum number of allowed validators in the validator set

<pre><code>const <a href="DiemSystem.md#0x1_DiemSystem_MAX_VALIDATORS">MAX_VALIDATORS</a>: u64 = 256; </code></pre>

Function `initialize_validator_set`

Publishes the DiemConfig for the DiemSystem struct, which contains the current validator set. Also publishes the <code><a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a></code> with the ModifyConfigCapability<DiemSystem> returned by the publish function, which allows code in this module to change DiemSystem config (including the validator set). Must be invoked by the Diem root a single time in Genesis.

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_initialize_validator_set">initialize_validator_set</a>(dr_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_initialize_validator_set">initialize_validator_set</a>( dr_account: &signer, ) { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); let cap = <a href="DiemConfig.md#0x1_DiemConfig_publish_new_config_and_get_capability">DiemConfig::publish_new_config_and_get_capability</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>( dr_account, <a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a> { scheme: 0, validators: <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_empty">Vector::empty</a>(), }, ); assert( !exists<<a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="DiemSystem.md#0x1_DiemSystem_ECAPABILITY_HOLDER">ECAPABILITY_HOLDER</a>) ); move_to(dr_account, <a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a> { cap }) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>modifies global<<a href="DiemConfig.md#0x1_DiemConfig_DiemConfig">DiemConfig::DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; <a name="0x1_DiemSystem_dr_addr$20"></a> let dr_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(dr_account); aborts_if <a href="DiemConfig.md#0x1_DiemConfig_spec_is_published">DiemConfig::spec_is_published</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; aborts_if exists<<a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a>>(dr_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; ensures exists<<a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a>>(dr_addr); ensures <a href="DiemConfig.md#0x1_DiemConfig_spec_is_published">DiemConfig::spec_is_published</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>(); ensures len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()) == 0; </code></pre> </details>

Function `set_diem_system_config`

Copies a DiemSystem struct into the DiemConfig<DiemSystem> resource Called by the add, remove, and update functions.

<pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_set_diem_system_config">set_diem_system_config</a>(value: <a href="DiemSystem.md#0x1_DiemSystem_DiemSystem">DiemSystem::DiemSystem</a>) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_set_diem_system_config">set_diem_system_config</a>(value: <a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>) acquires <a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); assert( exists<<a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemSystem.md#0x1_DiemSystem_ECAPABILITY_HOLDER">ECAPABILITY_HOLDER</a>) ); // Updates the <a href="DiemConfig.md#0x1_DiemConfig">DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>> and emits a reconfigure event. <a href="DiemConfig.md#0x1_DiemConfig_set_with_capability_and_reconfigure">DiemConfig::set_with_capability_and_reconfigure</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>( &borrow_global<<a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()).cap, value ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; modifies global<<a href="DiemConfig.md#0x1_DiemConfig_DiemConfig">DiemConfig::DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); modifies global<<a href="DiemConfig.md#0x1_DiemConfig_Configuration">DiemConfig::Configuration</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; include <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureAbortsIf">DiemConfig::ReconfigureAbortsIf</a>; </code></pre>

<code>payload</code> is the only field of DiemConfig, so next completely specifies it.

<pre><code>ensures global<<a href="DiemConfig.md#0x1_DiemConfig_DiemConfig">DiemConfig::DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()).payload == value; include <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureEmits">DiemConfig::ReconfigureEmits</a>; </code></pre> </details>

Function `add_validator`

Adds a new validator to the validator set.

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_add_validator">add_validator</a>(dr_account: &signer, validator_addr: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_add_validator">add_validator</a>( dr_account: &signer, validator_addr: address ) acquires <a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); // A prospective validator must have a validator config resource assert(<a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validator_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_EINVALID_PROSPECTIVE_VALIDATOR">EINVALID_PROSPECTIVE_VALIDATOR</a>)); // Bound the validator set size assert( <a href="DiemSystem.md#0x1_DiemSystem_validator_set_size">validator_set_size</a>() < <a href="DiemSystem.md#0x1_DiemSystem_MAX_VALIDATORS">MAX_VALIDATORS</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="DiemSystem.md#0x1_DiemSystem_EMAX_VALIDATORS">EMAX_VALIDATORS</a>) ); let diem_system_config = <a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>(); // Ensure that this address is not already a validator assert( !<a href="DiemSystem.md#0x1_DiemSystem_is_validator_">is_validator_</a>(validator_addr, &diem_system_config.validators), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_EALREADY_A_VALIDATOR">EALREADY_A_VALIDATOR</a>) ); // it is guaranteed that the config is non-empty let config = <a href="ValidatorConfig.md#0x1_ValidatorConfig_get_config">ValidatorConfig::get_config</a>(validator_addr); <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_push_back">Vector::push_back</a>(&mut diem_system_config.validators, <a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a> { addr: validator_addr, config, // copy the config over to ValidatorSet consensus_voting_power: 1, last_config_update_time: <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_microseconds">DiemTimestamp::now_microseconds</a>(), }); <a href="DiemSystem.md#0x1_DiemSystem_set_diem_system_config">set_diem_system_config</a>(diem_system_config); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>modifies global<<a href="DiemConfig.md#0x1_DiemConfig_DiemConfig">DiemConfig::DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); include <a href="DiemSystem.md#0x1_DiemSystem_AddValidatorAbortsIf">AddValidatorAbortsIf</a>; include <a href="DiemSystem.md#0x1_DiemSystem_AddValidatorEnsures">AddValidatorEnsures</a>; include <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureEmits">DiemConfig::ReconfigureEmits</a>; </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_AddValidatorAbortsIf">AddValidatorAbortsIf</a> { dr_account: signer; validator_addr: address; aborts_if <a href="DiemSystem.md#0x1_DiemSystem_validator_set_size">validator_set_size</a>() >= <a href="DiemSystem.md#0x1_DiemSystem_MAX_VALIDATORS">MAX_VALIDATORS</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; include <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureAbortsIf">DiemConfig::ReconfigureAbortsIf</a>; aborts_if !<a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validator_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if <a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(validator_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_AddValidatorEnsures">AddValidatorEnsures</a> { validator_addr: address; } </code></pre>

DIP-6 property: validator has validator role. The code does not check this explicitly, but it is implied by the <code>assert <a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a></code>, since there is an invariant (in ValidatorConfig) that a an address with a published ValidatorConfig has a ValidatorRole

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_AddValidatorEnsures">AddValidatorEnsures</a> { ensures <a href="Roles.md#0x1_Roles_spec_has_validator_role_addr">Roles::spec_has_validator_role_addr</a>(validator_addr); ensures <a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validator_addr); ensures <a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(validator_addr); <a name="0x1_DiemSystem_vs$15"></a> let vs = <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(); ensures <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_eq_push_back">Vector::eq_push_back</a>(vs, old(vs), <a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a> { addr: validator_addr, config: <a href="ValidatorConfig.md#0x1_ValidatorConfig_spec_get_config">ValidatorConfig::spec_get_config</a>(validator_addr), consensus_voting_power: 1, last_config_update_time: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_microseconds">DiemTimestamp::spec_now_microseconds</a>(), } ); } </code></pre> </details>

Function `remove_validator`

Removes a validator, aborts unless called by diem root account

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_remove_validator">remove_validator</a>(dr_account: &signer, validator_addr: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_remove_validator">remove_validator</a>( dr_account: &signer, validator_addr: address ) acquires <a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); let diem_system_config = <a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>(); // Ensure that this address is an active validator let to_remove_index_vec = <a href="DiemSystem.md#0x1_DiemSystem_get_validator_index_">get_validator_index_</a>(&diem_system_config.validators, validator_addr); assert(<a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(&to_remove_index_vec), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_ENOT_AN_ACTIVE_VALIDATOR">ENOT_AN_ACTIVE_VALIDATOR</a>)); let to_remove_index = *<a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(&to_remove_index_vec); // Remove corresponding <a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a> from the validator set _ = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_swap_remove">Vector::swap_remove</a>(&mut diem_system_config.validators, to_remove_index); <a href="DiemSystem.md#0x1_DiemSystem_set_diem_system_config">set_diem_system_config</a>(diem_system_config); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>modifies global<<a href="DiemConfig.md#0x1_DiemConfig_DiemConfig">DiemConfig::DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); include <a href="DiemSystem.md#0x1_DiemSystem_RemoveValidatorAbortsIf">RemoveValidatorAbortsIf</a>; include <a href="DiemSystem.md#0x1_DiemSystem_RemoveValidatorEnsures">RemoveValidatorEnsures</a>; include <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureEmits">DiemConfig::ReconfigureEmits</a>; </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_RemoveValidatorAbortsIf">RemoveValidatorAbortsIf</a> { dr_account: signer; validator_addr: address; include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; include <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureAbortsIf">DiemConfig::ReconfigureAbortsIf</a>; aborts_if !<a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(validator_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_RemoveValidatorEnsures">RemoveValidatorEnsures</a> { validator_addr: address; <a name="0x1_DiemSystem_vs$16"></a> let vs = <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(); ensures forall vi in vs where vi.addr != validator_addr: exists ovi in old(vs): vi == ovi; } </code></pre>

Removed validator is no longer a validator. Depends on no other entries for same address in validator_set

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_RemoveValidatorEnsures">RemoveValidatorEnsures</a> { ensures !<a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(validator_addr); } </code></pre> </details>

Function `update_config_and_reconfigure`

Copy the information from ValidatorConfig into the validator set. This function makes no changes to the size or the members of the set. If the config in the ValidatorSet changes, it stores the new DiemSystem and emits a reconfigurationevent.

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_update_config_and_reconfigure">update_config_and_reconfigure</a>(validator_operator_account: &signer, validator_addr: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_update_config_and_reconfigure">update_config_and_reconfigure</a>( validator_operator_account: &signer, validator_addr: address, ) acquires <a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="Roles.md#0x1_Roles_assert_validator_operator">Roles::assert_validator_operator</a>(validator_operator_account); assert( <a href="ValidatorConfig.md#0x1_ValidatorConfig_get_operator">ValidatorConfig::get_operator</a>(validator_addr) == <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(validator_operator_account), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_EINVALID_TRANSACTION_SENDER">EINVALID_TRANSACTION_SENDER</a>) ); let diem_system_config = <a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>(); let to_update_index_vec = <a href="DiemSystem.md#0x1_DiemSystem_get_validator_index_">get_validator_index_</a>(&diem_system_config.validators, validator_addr); assert(<a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(&to_update_index_vec), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_ENOT_AN_ACTIVE_VALIDATOR">ENOT_AN_ACTIVE_VALIDATOR</a>)); let to_update_index = *<a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(&to_update_index_vec); let is_validator_info_updated = <a href="DiemSystem.md#0x1_DiemSystem_update_ith_validator_info_">update_ith_validator_info_</a>(&mut diem_system_config.validators, to_update_index); if (is_validator_info_updated) { let validator_info = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&mut diem_system_config.validators, to_update_index); assert(<a href="DiemTimestamp.md#0x1_DiemTimestamp_now_microseconds">DiemTimestamp::now_microseconds</a>() > validator_info.last_config_update_time + <a href="DiemSystem.md#0x1_DiemSystem_FIVE_MINUTES">FIVE_MINUTES</a>, <a href="DiemSystem.md#0x1_DiemSystem_ECONFIG_UPDATE_RATE_LIMITED">ECONFIG_UPDATE_RATE_LIMITED</a>); validator_info.last_config_update_time = <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_microseconds">DiemTimestamp::now_microseconds</a>(); <a href="DiemSystem.md#0x1_DiemSystem_set_diem_system_config">set_diem_system_config</a>(diem_system_config); } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; pragma verify = false; modifies global<<a href="DiemConfig.md#0x1_DiemConfig_Configuration">DiemConfig::Configuration</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); modifies global<<a href="DiemConfig.md#0x1_DiemConfig_DiemConfig">DiemConfig::DiemConfig</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); include <a href="ValidatorConfig.md#0x1_ValidatorConfig_AbortsIfGetOperator">ValidatorConfig::AbortsIfGetOperator</a>{addr: validator_addr}; include <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureAbortsIf">UpdateConfigAndReconfigureAbortsIf</a>; include <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureEnsures">UpdateConfigAndReconfigureEnsures</a>; <a name="0x1_DiemSystem_is_validator_info_updated$21"></a> let is_validator_info_updated = <a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validator_addr) && (exists v_info in <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(): v_info.addr == validator_addr && v_info.config != <a href="ValidatorConfig.md#0x1_ValidatorConfig_spec_get_config">ValidatorConfig::spec_get_config</a>(validator_addr)); include is_validator_info_updated ==> <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureAbortsIf">DiemConfig::ReconfigureAbortsIf</a>; include <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureEmits">UpdateConfigAndReconfigureEmits</a>; </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureAbortsIf">UpdateConfigAndReconfigureAbortsIf</a> { validator_addr: address; validator_operator_account: signer; <a name="0x1_DiemSystem_validator_operator_addr$17"></a> let validator_operator_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(validator_operator_account); include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; } </code></pre>

Must abort if the signer does not have the ValidatorOperator role [H15].

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureAbortsIf">UpdateConfigAndReconfigureAbortsIf</a> { include <a href="Roles.md#0x1_Roles_AbortsIfNotValidatorOperator">Roles::AbortsIfNotValidatorOperator</a>{validator_operator_addr: validator_operator_addr}; include <a href="ValidatorConfig.md#0x1_ValidatorConfig_AbortsIfNoValidatorConfig">ValidatorConfig::AbortsIfNoValidatorConfig</a>{addr: validator_addr}; aborts_if <a href="ValidatorConfig.md#0x1_ValidatorConfig_get_operator">ValidatorConfig::get_operator</a>(validator_addr) != validator_operator_addr with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if !<a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(validator_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

Does not change the length of the validator set, only changes ValidatorInfo for validator_addr, and doesn't change any addresses.

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureEnsures">UpdateConfigAndReconfigureEnsures</a> { validator_addr: address; <a name="0x1_DiemSystem_vs$18"></a> let vs = <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(); ensures len(vs) == len(old(vs)); } </code></pre>

No addresses change in the validator set

If the <code><a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a></code> address is not the one we're changing, the info does not change.

It updates the correct entry in the correct way

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureEnsures">UpdateConfigAndReconfigureEnsures</a> { ensures forall i in 0..len(vs): vs[i].config == old(vs[i].config) || (old(vs)[i].addr == validator_addr && vs[i].config == <a href="ValidatorConfig.md#0x1_ValidatorConfig_get_config">ValidatorConfig::get_config</a>(validator_addr)); } </code></pre>

DIP-6 property

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureEnsures">UpdateConfigAndReconfigureEnsures</a> { ensures <a href="Roles.md#0x1_Roles_spec_has_validator_role_addr">Roles::spec_has_validator_role_addr</a>(validator_addr); } </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_UpdateConfigAndReconfigureEmits">UpdateConfigAndReconfigureEmits</a> { validator_addr: address; <a name="0x1_DiemSystem_is_validator_info_updated$19"></a> let is_validator_info_updated = <a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validator_addr) && (exists v_info in <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(): v_info.addr == validator_addr && v_info.config != <a href="ValidatorConfig.md#0x1_ValidatorConfig_spec_get_config">ValidatorConfig::spec_get_config</a>(validator_addr)); include is_validator_info_updated ==> <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureEmits">DiemConfig::ReconfigureEmits</a>; } </code></pre> </details>

Function `get_diem_system_config`

Get the DiemSystem configuration from DiemConfig

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>(): <a href="DiemSystem.md#0x1_DiemSystem_DiemSystem">DiemSystem::DiemSystem</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>(): <a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a> { <a href="DiemConfig.md#0x1_DiemConfig_get">DiemConfig::get</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>() } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="DiemConfig.md#0x1_DiemConfig_AbortsIfNotPublished">DiemConfig::AbortsIfNotPublished</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>; ensures result == <a href="DiemConfig.md#0x1_DiemConfig_get">DiemConfig::get</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>(); </code></pre> </details>

Function `is_validator`

Return true if <code>addr</code> is in the current validator set

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_is_validator">is_validator</a>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_is_validator">is_validator</a>(addr: address): bool { <a href="DiemSystem.md#0x1_DiemSystem_is_validator_">is_validator_</a>(addr, &<a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>().validators) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="DiemConfig.md#0x1_DiemConfig_AbortsIfNotPublished">DiemConfig::AbortsIfNotPublished</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>; ensures result == <a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(addr); </code></pre>

<pre><code>define <a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(addr: address): bool { exists v in <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(): v.addr == addr } </code></pre> </details>

Function `get_validator_config`

Returns validator config. Aborts if <code>addr</code> is not in the validator set.

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_get_validator_config">get_validator_config</a>(addr: address): <a href="ValidatorConfig.md#0x1_ValidatorConfig_Config">ValidatorConfig::Config</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_get_validator_config">get_validator_config</a>(addr: address): <a href="ValidatorConfig.md#0x1_ValidatorConfig_Config">ValidatorConfig::Config</a> { let diem_system_config = <a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>(); let validator_index_vec = <a href="DiemSystem.md#0x1_DiemSystem_get_validator_index_">get_validator_index_</a>(&diem_system_config.validators, addr); assert(<a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(&validator_index_vec), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_ENOT_AN_ACTIVE_VALIDATOR">ENOT_AN_ACTIVE_VALIDATOR</a>)); *&(<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&diem_system_config.validators, *<a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(&validator_index_vec))).config } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="DiemConfig.md#0x1_DiemConfig_AbortsIfNotPublished">DiemConfig::AbortsIfNotPublished</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>; aborts_if !<a href="DiemSystem.md#0x1_DiemSystem_spec_is_validator">spec_is_validator</a>(addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; ensures exists info in <a href="DiemConfig.md#0x1_DiemConfig_get">DiemConfig::get</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>().validators where info.addr == addr: result == info.config; </code></pre> </details>

Function `validator_set_size`

Return the size of the current validator set

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_validator_set_size">validator_set_size</a>(): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_validator_set_size">validator_set_size</a>(): u64 { <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&<a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>().validators) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="DiemConfig.md#0x1_DiemConfig_AbortsIfNotPublished">DiemConfig::AbortsIfNotPublished</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>; ensures result == len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()); </code></pre> </details>

Function `get_ith_validator_address`

Get the <code>i</code>'th validator address in the validator set.

<pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_get_ith_validator_address">get_ith_validator_address</a>(i: u64): address </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="DiemSystem.md#0x1_DiemSystem_get_ith_validator_address">get_ith_validator_address</a>(i: u64): address { assert(i < <a href="DiemSystem.md#0x1_DiemSystem_validator_set_size">validator_set_size</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemSystem.md#0x1_DiemSystem_EVALIDATOR_INDEX">EVALIDATOR_INDEX</a>)); <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&<a href="DiemSystem.md#0x1_DiemSystem_get_diem_system_config">get_diem_system_config</a>().validators, i).addr } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="DiemConfig.md#0x1_DiemConfig_AbortsIfNotPublished">DiemConfig::AbortsIfNotPublished</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>; aborts_if i >= len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; ensures result == <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()[i].addr; </code></pre> </details>

Function `get_validator_index_`

Get the index of the validator by address in the <code>validators</code> vector It has a loop, so there are spec blocks in the code to assert loop invariants.

<pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_get_validator_index_">get_validator_index_</a>(validators: &vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">DiemSystem::ValidatorInfo</a>>, addr: address): <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_Option">Option::Option</a><u64> </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_get_validator_index_">get_validator_index_</a>(validators: &vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a>>, addr: address): <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option">Option</a><u64> { let size = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(validators); let i = 0; while ({ spec { assert i <= size; assert forall j in 0..i: validators[j].addr != addr; }; (i < size) }) { let validator_info_ref = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(validators, i); if (validator_info_ref.addr == addr) { spec { assert validators[i].addr == addr; }; return <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_some">Option::some</a>(i) }; i = i + 1; }; spec { assert i == size; assert forall j in 0..size: validators[j].addr != addr; }; return <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_none">Option::none</a>() } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; <a name="0x1_DiemSystem_size$22"></a> let size = len(validators); </code></pre>

If <code>addr</code> is not in validator set, returns none.

<pre><code>ensures (forall i in 0..size: validators[i].addr != addr) ==> <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_none">Option::is_none</a>(result); </code></pre>

If <code>addr</code> is in validator set, return the least index of an entry with that address. The data invariant associated with the DiemSystem.validators that implies that there is exactly one such address.

<pre><code>ensures (exists i in 0..size: validators[i].addr == addr) ==> <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(result) && { let at = <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(result); 0 <= at && at < size && validators[at].addr == addr }; </code></pre> </details>

Function `update_ith_validator_info_`

Updates ith validator info, if nothing changed, return false. This function never aborts.

<pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_update_ith_validator_info_">update_ith_validator_info_</a>(validators: &mut vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">DiemSystem::ValidatorInfo</a>>, i: u64): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_update_ith_validator_info_">update_ith_validator_info_</a>(validators: &mut vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a>>, i: u64): bool { let size = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(validators); // This provably cannot happen, but left it here for safety. if (i >= size) { return false }; let validator_info = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(validators, i); // "is_valid" below should always hold based on a global invariant later // in the file (which proves if we comment out some other specifications), // but it is left here for safety. if (!<a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validator_info.addr)) { return false }; let new_validator_config = <a href="ValidatorConfig.md#0x1_ValidatorConfig_get_config">ValidatorConfig::get_config</a>(validator_info.addr); // check if information is the same let config_ref = &mut validator_info.config; if (config_ref == &new_validator_config) { return false }; *config_ref = new_validator_config; true } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; <a name="0x1_DiemSystem_new_validator_config$23"></a> let new_validator_config = <a href="ValidatorConfig.md#0x1_ValidatorConfig_spec_get_config">ValidatorConfig::spec_get_config</a>(validators[i].addr); </code></pre>

Prover is able to prove this because get_validator_index_ ensures it in calling context.

<pre><code>requires 0 <= i && i < len(validators); </code></pre>

Somewhat simplified from the code because of properties guaranteed by the calling context.

<pre><code>ensures result == (<a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(validators[i].addr) && new_validator_config != old(validators[i].config)); </code></pre>

It only updates validators at index <code>i</code>, and updates the <code>config</code> field to <code>new_validator_config</code>.

<pre><code>ensures result ==> validators == update_vector( old(validators), i, update_field(old(validators[i]), config, new_validator_config) ); </code></pre>

Does not change validators if result is false

<pre><code>ensures !result ==> validators == old(validators); </code></pre>

Updates the ith validator entry (and nothing else), as appropriate.

<pre><code>ensures validators == update_vector(old(validators), i, validators[i]); </code></pre>

Needed these assertions to make "consensus voting power is always 1" invariant prove (not sure why).

<pre><code>requires forall i1 in 0..len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()): <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()[i1].consensus_voting_power == 1; ensures forall i1 in 0..len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()): <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()[i1].consensus_voting_power == 1; </code></pre> </details>

Function `is_validator_`

Private function checks for membership of <code>addr</code> in validator set.

<pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_is_validator_">is_validator_</a>(addr: address, validators_vec_ref: &vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">DiemSystem::ValidatorInfo</a>>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="DiemSystem.md#0x1_DiemSystem_is_validator_">is_validator_</a>(addr: address, validators_vec_ref: &vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a>>): bool { <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(&<a href="DiemSystem.md#0x1_DiemSystem_get_validator_index_">get_validator_index_</a>(validators_vec_ref, addr)) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == (exists v in validators_vec_ref: v.addr == addr); </code></pre> </details>

Module Specification

Initialization

After genesis, the <code><a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a></code> configuration is published, as well as the capability which grants the right to modify it to certain functions in this module.

<pre><code>invariant [global] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <a href="DiemConfig.md#0x1_DiemConfig_spec_is_published">DiemConfig::spec_is_published</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>() && exists<<a href="DiemSystem.md#0x1_DiemSystem_CapabilityHolder">CapabilityHolder</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); </code></pre>

Access Control

Access control requirements for validator set are a bit more complicated than many parts of the framework because of <code>update_config_and_reconfigure</code>. That function updates the validator info (e.g., the network address) for a particular Validator Owner, but only if the signer is the Operator for that owner. Therefore, we must ensure that the information for other validators in the validator set are not changed, which is specified locally for <code>update_config_and_reconfigure</code>.

The permission "{Add, Remove} Validator" is granted to DiemRoot [H14].

<pre><code>apply <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account} to add_validator, remove_validator; </code></pre>

<pre><code>schema <a href="DiemSystem.md#0x1_DiemSystem_ValidatorSetConfigRemainsSame">ValidatorSetConfigRemainsSame</a> { ensures <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>() == old(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()); } </code></pre>

Only {add, remove} validator [H14] and update_config_and_reconfigure [H15] may change the set of validators in the configuration. <code>set_diem_system_config</code> is a private function which is only called by other functions in the "except" list. <code>initialize_validator_set</code> is only called in Genesis.

<pre><code>apply <a href="DiemSystem.md#0x1_DiemSystem_ValidatorSetConfigRemainsSame">ValidatorSetConfigRemainsSame</a> to *, *<T> except add_validator, remove_validator, update_config_and_reconfigure, initialize_validator_set, set_diem_system_config; </code></pre>

Helper Functions

Fetches the currently published validator set from the published DiemConfig<DiemSystem> resource.

<pre><code>define <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>(): vector<<a href="DiemSystem.md#0x1_DiemSystem_ValidatorInfo">ValidatorInfo</a>> { <a href="DiemConfig.md#0x1_DiemConfig_get">DiemConfig::get</a><<a href="DiemSystem.md#0x1_DiemSystem">DiemSystem</a>>().validators } </code></pre>

Every validator has a published ValidatorConfig whose config option is "some" (meaning of ValidatorConfig::is_valid).

Unfortunately, this times out for unknown reasons (it doesn't seem to be hard), so it is deactivated. The Prover can prove it if the uniqueness invariant for the DiemSystem resource is commented out, along with aborts for update_config_and_reconfigure and everything else that breaks (e.g., there is an ensures in remove_validator that has to be commented out)

<pre><code>invariant [deactivated, global] forall i1 in 0..len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()): <a href="ValidatorConfig.md#0x1_ValidatorConfig_is_valid">ValidatorConfig::is_valid</a>(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()[i1].addr); </code></pre>

Every validator in the validator set has a validator role.

Note: Verification of DiemSystem seems to be very sensitive, and will often time out after small changes. Disabling this property (with [deactivate, global]) is sometimes a quick temporary fix.

<pre><code>invariant [global] forall i1 in 0..len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()): <a href="Roles.md#0x1_Roles_spec_has_validator_role_addr">Roles::spec_has_validator_role_addr</a>(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()[i1].addr); </code></pre>

<code>Consensus_voting_power</code> is always 1. In future implementations, this field may have different values in which case this property will have to change. It's here currently because and accidental or illicit change to the voting power of a validator could defeat the Byzantine fault tolerance of DiemBFT.

<pre><code>invariant [global] forall i1 in 0..len(<a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()): <a href="DiemSystem.md#0x1_DiemSystem_spec_get_validators">spec_get_validators</a>()[i1].consensus_voting_power == 1; </code></pre>

Module `0x1::DiemSystem`

Module 0x1::DiemSystem

Struct ValidatorInfo

Resource CapabilityHolder

Struct DiemSystem

Constants

Function initialize_validator_set

Function set_diem_system_config

Function add_validator

Function remove_validator

Function update_config_and_reconfigure

Function get_diem_system_config

Function is_validator

Function get_validator_config

Function validator_set_size

Function get_ith_validator_address

Function get_validator_index_

Function update_ith_validator_info_

Function is_validator_

Module Specification

Initialization

Access Control

Helper Functions

Module `0x1::DiemSystem`

Struct `ValidatorInfo`

Resource `CapabilityHolder`

Struct `DiemSystem`

Function `initialize_validator_set`

Function `set_diem_system_config`

Function `add_validator`

Function `remove_validator`

Function `update_config_and_reconfigure`

Function `get_diem_system_config`

Function `is_validator`

Function `get_validator_config`

Function `validator_set_size`

Function `get_ith_validator_address`

Function `get_validator_index_`

Function `update_ith_validator_info_`

Function `is_validator_`