Module `0x1::Genesis`

The <code><a href="Genesis.md#0x1_Genesis">Genesis</a></code> module defines the Move initialization entry point of the Diem framework when executing from a fresh state.

TODO: Currently there are a few additional functions called from Rust during genesis. Document which these are and in which order they are called.

Function initialize

<pre><code>use <a href="AccountFreezing.md#0x1_AccountFreezing">0x1::AccountFreezing</a>; use <a href="ChainId.md#0x1_ChainId">0x1::ChainId</a>; use <a href="Diem.md#0x1_Diem">0x1::Diem</a>; use <a href="DiemAccount.md#0x1_DiemAccount">0x1::DiemAccount</a>; use <a href="DiemBlock.md#0x1_DiemBlock">0x1::DiemBlock</a>; use <a href="DiemConfig.md#0x1_DiemConfig">0x1::DiemConfig</a>; use <a href="DiemSystem.md#0x1_DiemSystem">0x1::DiemSystem</a>; use <a href="DiemTimestamp.md#0x1_DiemTimestamp">0x1::DiemTimestamp</a>; use <a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption">0x1::DiemTransactionPublishingOption</a>; use <a href="DiemVMConfig.md#0x1_DiemVMConfig">0x1::DiemVMConfig</a>; use <a href="DiemVersion.md#0x1_DiemVersion">0x1::DiemVersion</a>; use <a href="DualAttestation.md#0x1_DualAttestation">0x1::DualAttestation</a>; use <a href="TransactionFee.md#0x1_TransactionFee">0x1::TransactionFee</a>; use <a href="XDX.md#0x1_XDX">0x1::XDX</a>; use <a href="XUS.md#0x1_XUS">0x1::XUS</a>; </code></pre>

Function `initialize`

Initializes the Diem framework.

<pre><code>fun <a href="Genesis.md#0x1_Genesis_initialize">initialize</a>(dr_account: signer, tc_account: signer, dr_auth_key: vector<u8>, tc_auth_key: vector<u8>, initial_script_allow_list: vector<vector<u8>>, is_open_module: bool, instruction_schedule: vector<u8>, native_schedule: vector<u8>, chain_id: u8) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Genesis.md#0x1_Genesis_initialize">initialize</a>( dr_account: signer, tc_account: signer, dr_auth_key: vector<u8>, tc_auth_key: vector<u8>, initial_script_allow_list: vector<vector<u8>>, is_open_module: bool, instruction_schedule: vector<u8>, native_schedule: vector<u8>, chain_id: u8, ) { let dr_account = &dr_account; let tc_account = &tc_account; <a href="DiemAccount.md#0x1_DiemAccount_initialize">DiemAccount::initialize</a>(dr_account, x"00000000000000000000000000000000"); <a href="ChainId.md#0x1_ChainId_initialize">ChainId::initialize</a>(dr_account, chain_id); // On-chain config setup <a href="DiemConfig.md#0x1_DiemConfig_initialize">DiemConfig::initialize</a>(dr_account); // Currency setup <a href="Diem.md#0x1_Diem_initialize">Diem::initialize</a>(dr_account); // Currency setup <a href="XUS.md#0x1_XUS_initialize">XUS::initialize</a>(dr_account, tc_account); <a href="XDX.md#0x1_XDX_initialize">XDX::initialize</a>( dr_account, tc_account, ); <a href="AccountFreezing.md#0x1_AccountFreezing_initialize">AccountFreezing::initialize</a>(dr_account); <a href="TransactionFee.md#0x1_TransactionFee_initialize">TransactionFee::initialize</a>(tc_account); <a href="DiemSystem.md#0x1_DiemSystem_initialize_validator_set">DiemSystem::initialize_validator_set</a>( dr_account, ); <a href="DiemVersion.md#0x1_DiemVersion_initialize">DiemVersion::initialize</a>( dr_account, ); <a href="DualAttestation.md#0x1_DualAttestation_initialize">DualAttestation::initialize</a>( dr_account, ); <a href="DiemBlock.md#0x1_DiemBlock_initialize_block_metadata">DiemBlock::initialize_block_metadata</a>(dr_account); let dr_rotate_key_cap = <a href="DiemAccount.md#0x1_DiemAccount_extract_key_rotation_capability">DiemAccount::extract_key_rotation_capability</a>(dr_account); <a href="DiemAccount.md#0x1_DiemAccount_rotate_authentication_key">DiemAccount::rotate_authentication_key</a>(&dr_rotate_key_cap, dr_auth_key); <a href="DiemAccount.md#0x1_DiemAccount_restore_key_rotation_capability">DiemAccount::restore_key_rotation_capability</a>(dr_rotate_key_cap); <a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_initialize">DiemTransactionPublishingOption::initialize</a>( dr_account, initial_script_allow_list, is_open_module, ); <a href="DiemVMConfig.md#0x1_DiemVMConfig_initialize">DiemVMConfig::initialize</a>( dr_account, instruction_schedule, native_schedule, ); let tc_rotate_key_cap = <a href="DiemAccount.md#0x1_DiemAccount_extract_key_rotation_capability">DiemAccount::extract_key_rotation_capability</a>(tc_account); <a href="DiemAccount.md#0x1_DiemAccount_rotate_authentication_key">DiemAccount::rotate_authentication_key</a>(&tc_rotate_key_cap, tc_auth_key); <a href="DiemAccount.md#0x1_DiemAccount_restore_key_rotation_capability">DiemAccount::restore_key_rotation_capability</a>(tc_rotate_key_cap); // After we have called this function, all invariants which are guarded by // `<a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> ...` will become active and a verification condition. // See also discussion at function specification. <a href="DiemTimestamp.md#0x1_DiemTimestamp_set_time_has_started">DiemTimestamp::set_time_has_started</a>(dr_account); } </code></pre> </details> <details> <summary>Specification</summary>

For verification of genesis, the goal is to prove that all the invariants which become active after the end of this function hold. This cannot be achieved with modular verification as we do in regular continuous testing. Rather, this module must be verified together with the module(s) which provides the invariant.

TODO: currently verifying this module together with modules providing invariants (see above) times out. This can likely be solved by making more of the initialize functions called by this function opaque, and prove the according invariants locally to each module.

Assume that this is called in genesis state (no timestamp).

<pre><code>requires <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_genesis">DiemTimestamp::is_genesis</a>(); </code></pre> </details>

Module `0x1::Genesis`

Module 0x1::Genesis

Function initialize

Module `0x1::Genesis`

Function `initialize`