chain_status - [mainnet]

This module code to assert that it is running in genesis (Self::assert_genesis) or after genesis (Self::assert_operating). These are essentially distinct states of the system. Specifically, if Self::assert_operating succeeds, assumptions about invariants over the global state can be made which reflect that the system has been successfully initialized.

use 0x1::error;
use 0x1::system_addresses;

Constants

The blockchain is not in the genesis status.

const ENOT_GENESIS: u64 = 2;

The blockchain is not in the operating status.

const ENOT_OPERATING: u64 = 1;

Resources

`GenesisEndMarker`

Marker to publish at the end of genesis.

struct GenesisEndMarker has key

Fields

dummy_field: bool

Functions

`set_genesis_end`

Marks that genesis has finished.

public(friend) fun set_genesis_end(aptos_framework: &signer)

Implementation

public(friend) fun set_genesis_end(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);
    move_to(aptos_framework, GenesisEndMarker {});
}

`is_genesis`

Helper function to determine if Aptos is in genesis state.

#[view]
public fun is_genesis(): bool

Implementation

public fun is_genesis(): bool {
    !exists<GenesisEndMarker>(@aptos_framework)
}

`is_operating`

Helper function to determine if Aptos is operating. This is the same as !is_genesis() and is provided for convenience. Testing is_operating() is more frequent than is_genesis().

#[view]
public fun is_operating(): bool

Implementation

public fun is_operating(): bool {
    exists<GenesisEndMarker>(@aptos_framework)
}

`assert_operating`

Helper function to assert operating (not genesis) state.

public fun assert_operating()

Implementation

public fun assert_operating() {
    assert!(is_operating(), error::invalid_state(ENOT_OPERATING));
}

`assert_genesis`

Helper function to assert genesis state.

public fun assert_genesis()

Implementation

public fun assert_genesis() {
    assert!(is_genesis(), error::invalid_state(ENOT_OPERATING));
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	The end of genesis mark should persist throughout the entire life of the chain.	Medium	The Aptos framework account should never drop the GenesisEndMarker resource.	Audited that GenesisEndMarker is published at the end of genesis and never removed. Formally verified via set_genesis_end that GenesisEndMarker is published.
2	The status of the chain should never be genesis and operating at the same time.	Low	The status of the chain is determined by the GenesisEndMarker resource.	Formally verified via global invariant.
3	The status of the chain should only be changed once, from genesis to operating.	Low	Attempting to assign a resource type more than once will abort.	Formally verified via set_genesis_end.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_strict;
// This enforces high-level requirement 2:
invariant is_genesis() == !is_operating();

`set_genesis_end`

public(friend) fun set_genesis_end(aptos_framework: &signer)

pragma verify = true;
pragma delegate_invariants_to_caller;
let addr = signer::address_of(aptos_framework);
aborts_if addr != @aptos_framework;
// This enforces high-level requirement 3:
aborts_if exists<GenesisEndMarker>(@aptos_framework);
// This enforces high-level requirement 1:
ensures global<GenesisEndMarker>(@aptos_framework) == GenesisEndMarker {};

schema RequiresIsOperating {
    requires is_operating();
}

`assert_operating`

public fun assert_operating()

aborts_if !is_operating();

`assert_genesis`

public fun assert_genesis()

aborts_if !is_genesis();