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::state_storage 

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

Struct Usage 

struct Usage has copy, drop, store
Fields
items: u64
bytes: u64

Resource 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

Resource GasParameter 

struct GasParameter has store, key
Fields
usage: state_storage::Usage

Constants 

const ESTATE_STORAGE_USAGE: u64 = 0;

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

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

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

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

Function on_reconfig 

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

Specification

High-level Requirements

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

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

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

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

Function get_state_storage_usage_only_at_epoch_beginning 

fun get_state_storage_usage_only_at_epoch_beginning(): state_storage::Usage

pragma opaque;

Function on_reconfig 

public(friend) fun on_reconfig()

aborts_if true;