Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::chain_status

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;

Resource GenesisEndMarker

Marker to publish at the end of genesis.

struct GenesisEndMarker has key
Fields
dummy_field: bool

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;

Function 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 {});
}

Function 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)
}

Function 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)
}

Function 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));
}

Function 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.RequirementCriticalityImplementationEnforcement
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();

Function 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();
}

Function assert_operating 

public fun assert_operating()

aborts_if !is_operating();

Function assert_genesis 

public fun assert_genesis()

aborts_if !is_genesis();