Skip to content
Aptos Docs

storage_gas - [mainnet]

Gas parameters for global storage.

General overview sections

Definitions

Function dependencies

Definitions

Utilization dimensions

Global storage gas fluctuates each epoch based on total utilization, which is defined across two dimensions:

  1. The number of “items” in global storage.
  2. The number of bytes in global storage.

“Items” include:

  1. Resources having the key attribute, which have been moved into global storage via a move_to() operation.
  2. Table entries.

Utilization ratios

initialize() sets an arbitrary “target” utilization for both item-wise and byte-wise storage, then each epoch, gas parameters are reconfigured based on the “utilization ratio” for each of the two utilization dimensions. The utilization ratio for a given dimension, either item-wise or byte-wise, is taken as the quotient of actual utilization and target utilization. For example, given a 500 GB target and 250 GB actual utilization, the byte-wise utilization ratio is 50%.

See base_8192_exponential_curve() for mathematical definitions.

Gas curve lookup

The utilization ratio in a given epoch is used as a lookup value in a Eulerian approximation to an exponential curve, known as a GasCurve, which is defined in base_8192_exponential_curve(), based on a minimum gas charge and a maximum gas charge.

The minimum gas charge and maximum gas charge at the endpoints of the curve are set in initialize(), and correspond to the following operations defined in StorageGas:

  1. Per-item read
  2. Per-item create
  3. Per-item write
  4. Per-byte read
  5. Per-byte create
  6. Per-byte write

For example, if the byte-wise utilization ratio is 50%, then per-byte reads will charge the minimum per-byte gas cost, plus 1.09% of the difference between the maximum and the minimum cost. See base_8192_exponential_curve() for a supporting calculation.

Item-wise operations

  1. Per-item read gas is assessed whenever an item is read from global storage via borrow_global<T>() or via a table entry read operation.
  2. Per-item create gas is assessed whenever an item is created in global storage via move_to<T>() or via a table entry creation operation.
  3. Per-item write gas is assessed whenever an item is overwritten in global storage via borrow_global_mut<T> or via a table entry mutation operation.

Byte-wise operations

Byte-wise operations are assessed in a manner similar to per-item operations, but account for the number of bytes affected by the given operation. Notably, this number denotes the total number of bytes in an entire item.

For example, if an operation mutates a u8 field in a resource that has 5 other u128 fields, the per-byte gas write cost will account for (5∗128)/8+1=81(5 * 128) / 8 + 1 = 81 bytes. Vectors are similarly treated as fields.

Constants

const MAX_U64: u64 = 18446744073709551615;
const BASIS_POINT_DENOMINATION: u64 = 10000;
const EINVALID_GAS_RANGE: u64 = 2;
const EINVALID_MONOTONICALLY_NON_DECREASING_CURVE: u64 = 5;
const EINVALID_POINT_RANGE: u64 = 6;
const ESTORAGE_GAS: u64 = 1;
const ESTORAGE_GAS_CONFIG: u64 = 0;
const ETARGET_USAGE_TOO_BIG: u64 = 4;
const EZERO_TARGET_USAGE: u64 = 3;

Structs

Point

A point in a Eulerian curve approximation, with each coordinate given in basis points:

Field valuePercentage
100.01 %
1000.10 %
10001.00 %
100010.00 %
struct Point has copy, drop, store
Fields
x: u64
x-coordinate basis points, corresponding to utilization ratio in base_8192_exponential_curve().
y: u64
y-coordinate basis points, corresponding to utilization multiplier in base_8192_exponential_curve().

UsageGasConfig

A gas configuration for either per-item or per-byte costs.

Contains a target usage amount, as well as a Eulerian approximation of an exponential curve for reads, creations, and overwrites. See StorageGasConfig.

struct UsageGasConfig has copy, drop, store
Fields
target_usage: u64
read_curve: storage_gas::GasCurve
create_curve: storage_gas::GasCurve
write_curve: storage_gas::GasCurve

GasCurve

Eulerian approximation of an exponential curve.

Assumes the following endpoints:

  • (x0,y0)=(0,0)(x_0, y_0) = (0, 0)
  • (xf,yf)=(10000,10000)(x_f, y_f) = (10000, 10000)

Intermediate points must satisfy:

  1. xi>xi−1x_i > x_{i - 1} ( xx is strictly increasing).
  2. 0≤xi≤100000 \leq x_i \leq 10000 ( xx is between 0 and 10000).
  3. yi≥yi−1y_i \geq y_{i - 1} ( yy is non-decreasing).
  4. 0≤yi≤100000 \leq y_i \leq 10000 ( yy is between 0 and 10000).

Lookup between two successive points is calculated via linear interpolation, e.g., as if there were a straight line between them.

See base_8192_exponential_curve().

struct GasCurve has copy, drop, store
Fields
min_gas: u64
max_gas: u64
points: vector<storage_gas::Point>

Resources

StorageGas

Storage parameters, reconfigured each epoch.

Parameters are updated during reconfiguration via on_reconfig(), based on storage utilization at the beginning of the epoch in which the reconfiguration transaction is executed. The gas schedule derived from these parameters will then be used to calculate gas for the entirety of the following epoch, such that the data is one epoch older than ideal. Notably, however, per this approach, the virtual machine does not need to reload gas parameters after the first transaction of an epoch.

struct StorageGas has key
Fields
per_item_read: u64
Cost to read an item from global storage.
per_item_create: u64
Cost to create an item in global storage.
per_item_write: u64
Cost to overwrite an item in global storage.
per_byte_read: u64
Cost to read a byte from global storage.
per_byte_create: u64
Cost to create a byte in global storage.
per_byte_write: u64
Cost to overwrite a byte in global storage.

StorageGasConfig

Gas configurations for per-item and per-byte prices.

struct StorageGasConfig has copy, drop, key
Fields
item_config: storage_gas::UsageGasConfig
Per-item gas configuration.
byte_config: storage_gas::UsageGasConfig
Per-byte gas configuration.

Functions

dependencies

The below dependency chart uses mermaid.js syntax, which can be automatically rendered into a diagram (depending on the browser) when viewing the documentation file generated from source code. If a browser renders the diagrams with coloring that makes it difficult to read, try a different browser.

Initialization

flowchart LR


initialize --> base_8192_exponential_curve
base_8192_exponential_curve --> new_gas_curve
base_8192_exponential_curve --> new_point
new_gas_curve --> validate_points

Reconfiguration

flowchart LR


calculate_gas --> Interpolate %% capitalized
calculate_read_gas --> calculate_gas
calculate_create_gas --> calculate_gas
calculate_write_gas --> calculate_gas
on_reconfig --> calculate_read_gas
on_reconfig --> calculate_create_gas
on_reconfig --> calculate_write_gas
reconfiguration::reconfigure --> on_reconfig

Here, the function interpolate() is spelled Interpolate because interpolate is a reserved word in mermaid.js.

Setting configurations

flowchart LR


gas_schedule::set_storage_gas_config --> set_config

base_8192_exponential_curve

Default exponential curve having base 8192.

Function definition

Gas price as a function of utilization ratio is defined as:

g(ur)=gmin+(bur−1)b−1Δgg(u_r) = g_{min} + \frac{(b^{u_r} - 1)}{b - 1} \Delta_g

g(ur)=gmin+umΔgg(u_r) = g_{min} + u_m \Delta_g

VariableDescription
gming_{min}min_gas
gmaxg_{max}max_gas
Δg=gmax−gmin\Delta_{g} = g_{max} - g_{min}Gas delta
uuUtilization
utu_tTarget utilization
ur=u/utu_r = u / u_tUtilization ratio
um=(bur−1)b−1u_m = \frac{(b^{u_r} - 1)}{b - 1}Utilization multiplier
b=8192b = 8192Exponent base

Example

Hence for a utilization ratio of 50% ( ur=0.5u_r = 0.5 ):

g(0.5)=gmin+81920.5−18192−1Δgg(0.5) = g_{min} + \frac{8192^{0.5} - 1}{8192 - 1} \Delta_g

g(0.5)≈gmin+0.0109Δgg(0.5) \approx g_{min} + 0.0109 \Delta_g

Which means that the price above min_gas is approximately 1.09% of the difference between max_gas and min_gas.

Utilization multipliers

uru_rumu_m (approximate)
10%0.02%
20%0.06%
30%0.17%
40%0.44%
50%1.09%
60%2.71%
70%6.69%
80%16.48%
90%40.61%
95%63.72%
99%91.38%
public fun base_8192_exponential_curve(min_gas: u64, max_gas: u64): storage_gas::GasCurve
Implementation 
public fun base_8192_exponential_curve(min_gas: u64, max_gas: u64): GasCurve {
    new_gas_curve(min_gas, max_gas,
        vector[
            new_point(1000, 2),
            new_point(2000, 6),
            new_point(3000, 17),
            new_point(4000, 44),
            new_point(5000, 109),
            new_point(6000, 271),
            new_point(7000, 669),
            new_point(8000, 1648),
            new_point(9000, 4061),
            new_point(9500, 6372),
            new_point(9900, 9138),
        ]
    )
}

new_point

public fun new_point(x: u64, y: u64): storage_gas::Point
Implementation 
public fun new_point(x: u64, y: u64): Point {
    assert!(
        x <= BASIS_POINT_DENOMINATION && y <= BASIS_POINT_DENOMINATION,
        error::invalid_argument(EINVALID_POINT_RANGE)
    );
    Point { x, y }
}

new_gas_curve

public fun new_gas_curve(min_gas: u64, max_gas: u64, points: vector<storage_gas::Point>): storage_gas::GasCurve
Implementation 
public fun new_gas_curve(min_gas: u64, max_gas: u64, points: vector<Point>): GasCurve {
    assert!(max_gas >= min_gas, error::invalid_argument(EINVALID_GAS_RANGE));
    assert!(max_gas <= MAX_U64 / BASIS_POINT_DENOMINATION, error::invalid_argument(EINVALID_GAS_RANGE));
    validate_points(&points);
    GasCurve {
        min_gas,
        max_gas,
        points
    }
}

new_usage_gas_config

public fun new_usage_gas_config(target_usage: u64, read_curve: storage_gas::GasCurve, create_curve: storage_gas::GasCurve, write_curve: storage_gas::GasCurve): storage_gas::UsageGasConfig
Implementation 
public fun new_usage_gas_config(target_usage: u64, read_curve: GasCurve, create_curve: GasCurve, write_curve: GasCurve): UsageGasConfig {
    assert!(target_usage > 0, error::invalid_argument(EZERO_TARGET_USAGE));
    assert!(target_usage <= MAX_U64 / BASIS_POINT_DENOMINATION, error::invalid_argument(ETARGET_USAGE_TOO_BIG));
    UsageGasConfig {
        target_usage,
        read_curve,
        create_curve,
        write_curve,
    }
}

new_storage_gas_config

public fun new_storage_gas_config(item_config: storage_gas::UsageGasConfig, byte_config: storage_gas::UsageGasConfig): storage_gas::StorageGasConfig
Implementation 
public fun new_storage_gas_config(item_config: UsageGasConfig, byte_config: UsageGasConfig): StorageGasConfig {
    StorageGasConfig {
        item_config,
        byte_config
    }
}

set_config

public(friend) fun set_config(aptos_framework: &signer, config: storage_gas::StorageGasConfig)
Implementation 
public(friend) fun set_config(aptos_framework: &signer, config: StorageGasConfig) acquires StorageGasConfig {
    system_addresses::assert_aptos_framework(aptos_framework);
    *borrow_global_mut<StorageGasConfig>(@aptos_framework) = config;
}

initialize

Initialize per-item and per-byte gas prices.

Target utilization is set to 2 billion items and 1 TB.

GasCurve endpoints are initialized as follows:

Data styleOperationMinimum gasMaximum gas
Per itemRead300K300K * 100
Per itemCreate300k300k * 100
Per itemWrite300K300K * 100
Per byteRead300300 * 100
Per byteCreate5K5K * 100
Per byteWrite5K5K * 100

StorageGas values are additionally initialized, but per on_reconfig(), they will be reconfigured for each subsequent epoch after initialization.

See base_8192_exponential_curve() fore more information on target utilization.

public fun initialize(aptos_framework: &signer)
Implementation 
public fun initialize(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);
    assert!(
        !exists<StorageGasConfig>(@aptos_framework),
        error::already_exists(ESTORAGE_GAS_CONFIG)
    );


    let k: u64 = 1000;
    let m: u64 = 1000 * 1000;


    let item_config = UsageGasConfig {
        target_usage: 2 * k * m, // 2 billion
        read_curve: base_8192_exponential_curve(300 * k, 300 * k * 100),
        create_curve: base_8192_exponential_curve(300 * k, 300 * k * 100),
        write_curve: base_8192_exponential_curve(300 * k, 300 * k * 100),
    };
    let byte_config = UsageGasConfig {
        target_usage: 1 * m * m, // 1TB
        read_curve: base_8192_exponential_curve(300, 300 * 100),
        create_curve: base_8192_exponential_curve(5 * k,  5 * k * 100),
        write_curve: base_8192_exponential_curve(5 * k,  5 * k * 100),
    };
    move_to(aptos_framework, StorageGasConfig {
        item_config,
        byte_config,
    });


    assert!(
        !exists<StorageGas>(@aptos_framework),
        error::already_exists(ESTORAGE_GAS)
    );
    move_to(aptos_framework, StorageGas {
        per_item_read: 300 * k,
        per_item_create: 5 * m,
        per_item_write: 300 * k,
        per_byte_read: 300,
        per_byte_create: 5 * k,
        per_byte_write: 5 * k,
    });
}

validate_points

fun validate_points(points: &vector<storage_gas::Point>)
Implementation 
fun validate_points(points: &vector<Point>) {
    let len = vector::length(points);
    spec {
        assume len < MAX_U64;
    };
    let i = 0;
    while ({
        spec {
            invariant forall j in 0..i: {
                let cur = if (j == 0) { Point { x: 0, y: 0 } } else { points[j - 1] };
                let next = if (j == len) { Point { x: BASIS_POINT_DENOMINATION, y: BASIS_POINT_DENOMINATION } } else { points[j] };
                cur.x < next.x && cur.y <= next.y
            };
        };
        i <= len
    }) {
        let cur = if (i == 0) { &Point { x: 0, y: 0 } } else { vector::borrow(points, i - 1) };
        let next = if (i == len) { &Point { x: BASIS_POINT_DENOMINATION, y: BASIS_POINT_DENOMINATION } } else { vector::borrow(points, i) };
        assert!(cur.x < next.x && cur.y <= next.y, error::invalid_argument(EINVALID_MONOTONICALLY_NON_DECREASING_CURVE));
        i = i + 1;
    }
}

calculate_gas

fun calculate_gas(max_usage: u64, current_usage: u64, curve: &storage_gas::GasCurve): u64
Implementation 
fun calculate_gas(max_usage: u64, current_usage: u64, curve: &GasCurve): u64 {
    let capped_current_usage = if (current_usage > max_usage) max_usage else current_usage;
    let points = &curve.points;
    let num_points = vector::length(points);
    let current_usage_bps = capped_current_usage * BASIS_POINT_DENOMINATION / max_usage;


    // Check the corner case that current_usage_bps drops before the first point.
    let (left, right) = if (num_points == 0) {
        (&Point { x: 0, y: 0 }, &Point { x: BASIS_POINT_DENOMINATION, y: BASIS_POINT_DENOMINATION })
    } else if (current_usage_bps < vector::borrow(points, 0).x) {
        (&Point { x: 0, y: 0 }, vector::borrow(points, 0))
    } else if (vector::borrow(points, num_points - 1).x <= current_usage_bps) {
        (vector::borrow(points, num_points - 1), &Point { x: BASIS_POINT_DENOMINATION, y: BASIS_POINT_DENOMINATION })
    } else {
        let (i, j) = (0, num_points - 2);
        while ({
            spec {
                invariant i <= j;
                invariant j < num_points - 1;
                invariant points[i].x <= current_usage_bps;
                invariant current_usage_bps < points[j + 1].x;
            };
            i < j
        }) {
            let mid = j - (j - i) / 2;
            if (current_usage_bps < vector::borrow(points, mid).x) {
                spec {
                    // j is strictly decreasing.
                    assert mid - 1 < j;
                };
                j = mid - 1;
            } else {
                spec {
                    // i is strictly increasing.
                    assert i < mid;
                };
                i = mid;
            };
        };
        (vector::borrow(points, i), vector::borrow(points, i + 1))
    };
    let y_interpolated = interpolate(left.x, right.x, left.y, right.y, current_usage_bps);
    interpolate(0, BASIS_POINT_DENOMINATION, curve.min_gas, curve.max_gas, y_interpolated)
}

interpolate

fun interpolate(x0: u64, x1: u64, y0: u64, y1: u64, x: u64): u64
Implementation 
fun interpolate(x0: u64, x1: u64, y0: u64, y1: u64, x: u64): u64 {
    y0 + (x - x0) * (y1 - y0) / (x1 - x0)
}

calculate_read_gas

fun calculate_read_gas(config: &storage_gas::UsageGasConfig, usage: u64): u64
Implementation 
fun calculate_read_gas(config: &UsageGasConfig, usage: u64): u64 {
    calculate_gas(config.target_usage, usage, &config.read_curve)
}

calculate_create_gas

fun calculate_create_gas(config: &storage_gas::UsageGasConfig, usage: u64): u64
Implementation 
fun calculate_create_gas(config: &UsageGasConfig, usage: u64): u64 {
    calculate_gas(config.target_usage, usage, &config.create_curve)
}

calculate_write_gas

fun calculate_write_gas(config: &storage_gas::UsageGasConfig, usage: u64): u64
Implementation 
fun calculate_write_gas(config: &UsageGasConfig, usage: u64): u64 {
    calculate_gas(config.target_usage, usage, &config.write_curve)
}

on_reconfig

public(friend) fun on_reconfig()
Implementation 
public(friend) fun on_reconfig() acquires StorageGas, StorageGasConfig {
    assert!(
        exists<StorageGasConfig>(@aptos_framework),
        error::not_found(ESTORAGE_GAS_CONFIG)
    );
    assert!(
        exists<StorageGas>(@aptos_framework),
        error::not_found(ESTORAGE_GAS)
    );
    let (items, bytes) = state_storage::current_items_and_bytes();
    let gas_config = borrow_global<StorageGasConfig>(@aptos_framework);
    let gas = borrow_global_mut<StorageGas>(@aptos_framework);
    gas.per_item_read = calculate_read_gas(&gas_config.item_config, items);
    gas.per_item_create = calculate_create_gas(&gas_config.item_config, items);
    gas.per_item_write = calculate_write_gas(&gas_config.item_config, items);
    gas.per_byte_read = calculate_read_gas(&gas_config.byte_config, bytes);
    gas.per_byte_create = calculate_create_gas(&gas_config.byte_config, bytes);
    gas.per_byte_write = calculate_write_gas(&gas_config.byte_config, bytes);
}

Specification

fun spec_calculate_gas(max_usage: u64, current_usage: u64, curve: GasCurve): u64;
schema NewGasCurveAbortsIf {
    min_gas: u64;
    max_gas: u64;
    aborts_if max_gas < min_gas;
    aborts_if max_gas > MAX_U64 / BASIS_POINT_DENOMINATION;
}

A non decreasing curve must ensure that next is greater than cur.

schema ValidatePointsAbortsIf {
    points: vector<Point>;
    // This enforces high-level requirement 2:
    aborts_if exists i in 0..len(points) - 1: (
        points[i].x >= points[i + 1].x || points[i].y > points[i + 1].y
    );
    aborts_if len(points) > 0 && points[0].x == 0;
    aborts_if len(points) > 0 && points[len(points) - 1].x == BASIS_POINT_DENOMINATION;
}

Point

struct Point has copy, drop, store
x: u64
x-coordinate basis points, corresponding to utilization ratio in base_8192_exponential_curve().
y: u64
y-coordinate basis points, corresponding to utilization multiplier in base_8192_exponential_curve(). 
invariant x <= BASIS_POINT_DENOMINATION;
invariant y <= BASIS_POINT_DENOMINATION;

UsageGasConfig

struct UsageGasConfig has copy, drop, store
target_usage: u64
read_curve: storage_gas::GasCurve
create_curve: storage_gas::GasCurve
write_curve: storage_gas::GasCurve 
invariant target_usage > 0;
invariant target_usage <= MAX_U64 / BASIS_POINT_DENOMINATION;

High-level Requirements

No.RequirementCriticalityImplementationEnforcement
1 The module's initialization guarantees the creation of the StorageGasConfig resource with a precise configuration, including accurate gas curves for per-item and per-byte operations. Medium The initialize function is responsible for setting up the initial state of the module, ensuring the fulfillment of the following conditions: (1) the creation of the StorageGasConfig resource, indicating its existence witqhin the module's context, and (2) the configuration of the StorageGasConfig resource includes the precise gas curves that define the behavior of per-item and per-byte operations. Formally verified via initialize. Moreover, the native gas logic has been manually audited.
2 The gas curve approximates an exponential curve based on a minimum and maximum gas charge. High The validate_points function ensures that the provided vector of points represents a monotonically non-decreasing curve. Formally verified via validate_points. Moreover, the configuration logic has been manually audited.
3 The initialized gas curve structure has values set according to the provided parameters. Low The new_gas_curve function initializes the GasCurve structure with values provided as parameters. Formally verified via new_gas_curve.
4 The initialized usage gas configuration structure has values set according to the provided parameters. Low The new_usage_gas_config function initializes the UsageGasConfig structure with values provided as parameters. Formally verified via new_usage_gas_config.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_strict;
invariant [suspendable] chain_status::is_operating() ==> exists<StorageGasConfig>(@aptos_framework);
invariant [suspendable] chain_status::is_operating() ==> exists<StorageGas>(@aptos_framework);

GasCurve

struct GasCurve has copy, drop, store
min_gas: u64
max_gas: u64
points: vector<storage_gas::Point>

Invariant 1: The minimum gas charge does not exceed the maximum gas charge.

invariant min_gas <= max_gas;

Invariant 2: The maximum gas charge is capped by MAX_U64 scaled down by the basis point denomination.

invariant max_gas <= MAX_U64 / BASIS_POINT_DENOMINATION;

Invariant 3: The x-coordinate increases monotonically and the y-coordinate increasing strictly monotonically, that is, the gas-curve is a monotonically increasing function.

invariant (len(points) > 0 ==> points[0].x > 0)
    && (len(points) > 0 ==> points[len(points) - 1].x < BASIS_POINT_DENOMINATION)
    && (forall i in 0..len(points) - 1: (points[i].x < points[i + 1].x && points[i].y <= points[i + 1].y));

base_8192_exponential_curve

public fun base_8192_exponential_curve(min_gas: u64, max_gas: u64): storage_gas::GasCurve
include NewGasCurveAbortsIf;

new_point

public fun new_point(x: u64, y: u64): storage_gas::Point
aborts_if x > BASIS_POINT_DENOMINATION || y > BASIS_POINT_DENOMINATION;
ensures result.x == x;
ensures result.y == y;

new_gas_curve

public fun new_gas_curve(min_gas: u64, max_gas: u64, points: vector<storage_gas::Point>): storage_gas::GasCurve

A non decreasing curve must ensure that next is greater than cur.

pragma verify_duration_estimate = 120;
include NewGasCurveAbortsIf;
include ValidatePointsAbortsIf;
// This enforces high-level requirement 3:
ensures result == GasCurve {
    min_gas,
    max_gas,
    points
};

new_usage_gas_config

public fun new_usage_gas_config(target_usage: u64, read_curve: storage_gas::GasCurve, create_curve: storage_gas::GasCurve, write_curve: storage_gas::GasCurve): storage_gas::UsageGasConfig
aborts_if target_usage == 0;
aborts_if target_usage > MAX_U64 / BASIS_POINT_DENOMINATION;
// This enforces high-level requirement 4:
ensures result == UsageGasConfig {
    target_usage,
    read_curve,
    create_curve,
    write_curve,
};

new_storage_gas_config

public fun new_storage_gas_config(item_config: storage_gas::UsageGasConfig, byte_config: storage_gas::UsageGasConfig): storage_gas::StorageGasConfig
aborts_if false;
ensures result.item_config == item_config;
ensures result.byte_config == byte_config;

set_config

public(friend) fun set_config(aptos_framework: &signer, config: storage_gas::StorageGasConfig)

Signer address must be @aptos_framework and StorageGasConfig exists.

include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
aborts_if !exists<StorageGasConfig>(@aptos_framework);

initialize

public fun initialize(aptos_framework: &signer)

Signer address must be @aptos_framework. Address @aptos_framework does not exist StorageGasConfig and StorageGas before the function call is restricted and exists after the function is executed.

include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
pragma verify_duration_estimate = 120;
aborts_if exists<StorageGasConfig>(@aptos_framework);
aborts_if exists<StorageGas>(@aptos_framework);
// This enforces high-level requirement 1:
ensures exists<StorageGasConfig>(@aptos_framework);
ensures exists<StorageGas>(@aptos_framework);

validate_points

fun validate_points(points: &vector<storage_gas::Point>)

A non decreasing curve must ensure that next is greater than cur.

pragma aborts_if_is_strict = false;
pragma verify = false;
pragma opaque;
include ValidatePointsAbortsIf;

calculate_gas

fun calculate_gas(max_usage: u64, current_usage: u64, curve: &storage_gas::GasCurve): u64
pragma opaque;
pragma verify_duration_estimate = 120;
requires max_usage > 0;
requires max_usage <= MAX_U64 / BASIS_POINT_DENOMINATION;
aborts_if false;
ensures [abstract] result == spec_calculate_gas(max_usage, current_usage, curve);

interpolate

fun interpolate(x0: u64, x1: u64, y0: u64, y1: u64, x: u64): u64
pragma opaque;
pragma intrinsic;
aborts_if false;

on_reconfig

public(friend) fun on_reconfig()

Address @aptos_framework must exist StorageGasConfig and StorageGas and StateStorageUsage.

requires chain_status::is_operating();
aborts_if !exists<StorageGasConfig>(@aptos_framework);
aborts_if !exists<StorageGas>(@aptos_framework);
aborts_if !exists<state_storage::StateStorageUsage>(@aptos_framework);

Complete docgen index

The below index is automatically generated from source code:

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