state_storage - [mainnet]

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

Constants

const ESTATE_STORAGE_USAGE: u64 = 0;

Structs

`Usage`

struct Usage has copy, drop, store

Fields

items: u64
bytes: u64

Resources

`StateStorageUsage`

This is updated at the beginning of each epoch, reflecting the storage usage after the last txn of the previous epoch is committed.

struct StateStorageUsage has store, key

Fields

epoch: u64
usage: state_storage::Usage

`GasParameter`

struct GasParameter has store, key

Fields

usage: state_storage::Usage

Functions

`initialize`

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

Implementation

public(friend) fun initialize(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);
    assert!(
        !exists<StateStorageUsage>(@aptos_framework),
        error::already_exists(ESTATE_STORAGE_USAGE)
    );
    move_to(aptos_framework, StateStorageUsage {
        epoch: 0,
        usage: Usage {
            items: 0,
            bytes: 0,
        }
    });
}

`on_new_block`

public(friend) fun on_new_block(epoch: u64)

Implementation

public(friend) fun on_new_block(epoch: u64) acquires StateStorageUsage {
    assert!(
        exists<StateStorageUsage>(@aptos_framework),
        error::not_found(ESTATE_STORAGE_USAGE)
    );
    let usage = borrow_global_mut<StateStorageUsage>(@aptos_framework);
    if (epoch != usage.epoch) {
        usage.epoch = epoch;
        usage.usage = get_state_storage_usage_only_at_epoch_beginning();
    }
}

`current_items_and_bytes`

public(friend) fun current_items_and_bytes(): (u64, u64)

Implementation

public(friend) fun current_items_and_bytes(): (u64, u64) acquires StateStorageUsage {
    assert!(
        exists<StateStorageUsage>(@aptos_framework),
        error::not_found(ESTATE_STORAGE_USAGE)
    );
    let usage = borrow_global<StateStorageUsage>(@aptos_framework);
    (usage.usage.items, usage.usage.bytes)
}

`get_state_storage_usage_only_at_epoch_beginning`

Warning: the result returned is based on the base state view held by the VM for the entire block or chunk of transactions, it’s only deterministic if called from the first transaction of the block because the execution layer guarantees a fresh state view then.

fun get_state_storage_usage_only_at_epoch_beginning(): state_storage::Usage

Implementation

native fun get_state_storage_usage_only_at_epoch_beginning(): Usage;

`on_reconfig`

public(friend) fun on_reconfig()

Implementation

public(friend) fun on_reconfig() {
    abort 0
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	Given the blockchain is in an operating state, the resources for tracking state storage usage and gas parameters must exist for the Aptos framework address.	Critical	The initialize function ensures only the Aptos framework address can call it.	Formally verified via module.
2	During the initialization of the module, it is guaranteed that the resource for tracking state storage usage will be moved under the Aptos framework account with default initial values.	Medium	The resource for tracking state storage usage may only be initialized with specific values and published under the aptos_framework account.	Formally verified via initialize.
3	The initialization function is only called once, during genesis.	Medium	The initialize function ensures StateStorageUsage does not already exist.	Formally verified via initialize.
4	During the initialization of the module, it is guaranteed that the resource for tracking state storage usage will be moved under the Aptos framework account with default initial values.	Medium	The resource for tracking state storage usage may only be initialized with specific values and published under the aptos_framework account.	Formally verified via initialize.
5	The structure for tracking state storage usage should exist for it to be updated at the beginning of each new block and for retrieving the values of structure members.	Medium	The functions on_new_block and current_items_and_bytes verify that the StateStorageUsage structure exists before performing any further operations.	Formally Verified via current_items_and_bytes, on_new_block, and the global invariant.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_strict;
// This enforces high-level requirement 1 and high-level requirement 5:
invariant [suspendable] chain_status::is_operating() ==> exists<StateStorageUsage>(@aptos_framework);
invariant [suspendable] chain_status::is_operating() ==> exists<GasParameter>(@aptos_framework);

`initialize`

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

ensure caller is admin. aborts if StateStorageUsage already exists.

let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 4:
aborts_if !system_addresses::is_aptos_framework_address(addr);
// This enforces high-level requirement 3:
aborts_if exists<StateStorageUsage>(@aptos_framework);
ensures exists<StateStorageUsage>(@aptos_framework);
let post state_usage = global<StateStorageUsage>(@aptos_framework);
// This enforces high-level requirement 2:
ensures state_usage.epoch == 0 && state_usage.usage.bytes == 0 && state_usage.usage.items == 0;

`on_new_block`

public(friend) fun on_new_block(epoch: u64)

// This enforces high-level requirement 5:
requires chain_status::is_operating();
aborts_if false;
ensures epoch == global<StateStorageUsage>(@aptos_framework).epoch;

`current_items_and_bytes`

public(friend) fun current_items_and_bytes(): (u64, u64)

// This enforces high-level requirement 5:
aborts_if !exists<StateStorageUsage>(@aptos_framework);

`get_state_storage_usage_only_at_epoch_beginning`

fun get_state_storage_usage_only_at_epoch_beginning(): state_storage::Usage

pragma opaque;

`on_reconfig`

public(friend) fun on_reconfig()

aborts_if true;