aggregator_factory - [mainnet]

This module provides foundations to create aggregators. Currently only Aptos Framework (0x1) can create them, so this module helps to wrap the constructor of Aggregator struct so that only a system account can initialize one. In the future, this might change and aggregators can be enabled for the public.

use 0x1::aggregator;
use 0x1::error;
use 0x1::system_addresses;
use 0x1::table;

Constants

const MAX_U128: u128 = 340282366920938463463374607431768211455;

Aggregator factory is not published yet.

const EAGGREGATOR_FACTORY_NOT_FOUND: u64 = 1;

Aggregator V1 only supports limit == MAX_U128.

const EAGG_V1_LIMIT_DEPRECATED: u64 = 2;

Resources

`AggregatorFactory`

Creates new aggregators. Used to control the numbers of aggregators in the system and who can create them. At the moment, only Aptos Framework (0x1) account can.

struct AggregatorFactory has key

Fields

phantom_table: table::Table<address, u128>

Functions

`initialize_aggregator_factory`

Creates a new factory for aggregators. Can only be called during genesis.

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

Implementation

public(friend) fun initialize_aggregator_factory(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);
    let aggregator_factory = AggregatorFactory {
        phantom_table: table::new()
    };
    move_to(aptos_framework, aggregator_factory);
}

`create_aggregator_internal`

Creates a new aggregator instance which overflows on exceeding a limit.

public(friend) fun create_aggregator_internal(): aggregator::Aggregator

Implementation

public(friend) fun create_aggregator_internal(): Aggregator acquires AggregatorFactory {
    assert!(
        exists<AggregatorFactory>(@aptos_framework),
        error::not_found(EAGGREGATOR_FACTORY_NOT_FOUND)
    );

    let aggregator_factory = borrow_global_mut<AggregatorFactory>(@aptos_framework);
    new_aggregator(aggregator_factory, MAX_U128)
}

`create_aggregator`

This is currently a function closed for public. This can be updated in the future by on-chain governance to allow any signer to call.

#[deprecated]
public fun create_aggregator(account: &signer, limit: u128): aggregator::Aggregator

Implementation

public fun create_aggregator(account: &signer, limit: u128): Aggregator acquires AggregatorFactory {
    // deprecated. Currently used only in aptos-move/e2e-move-tests/src/tests/aggregator.data/pack/sources/aggregator_test.move

    // Only Aptos Framework (0x1) account can call this for now.
    system_addresses::assert_aptos_framework(account);
    assert!(
        limit == MAX_U128,
        error::invalid_argument(EAGG_V1_LIMIT_DEPRECATED)
    );
    create_aggregator_internal()
}

`new_aggregator`

Returns a new aggregator.

fun new_aggregator(aggregator_factory: &mut aggregator_factory::AggregatorFactory, limit: u128): aggregator::Aggregator

Implementation

native fun new_aggregator(aggregator_factory: &mut AggregatorFactory, limit: u128): Aggregator;

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	During the module's initialization, it guarantees that the Aptos framework is the caller and that the AggregatorFactory resource will move under the Aptos framework account.	High	The initialize function is responsible for establishing the initial state of the module by creating the AggregatorFactory resource, indicating its presence within the module's context. Subsequently, the resource transfers to the Aptos framework account.	Formally verified via initialize_aggregator_factory.
2	To create a new aggregator instance, the aggregator factory must already be initialized and exist under the Aptos account.	High	The create_aggregator_internal function asserts that AggregatorFactory exists for the Aptos account.	Formally verified via CreateAggregatorInternalAbortsIf.
3	Only the Aptos framework address may create an aggregator instance currently.	Low	The create_aggregator function ensures that the address calling it is the Aptos framework address.	Formally verified via create_aggregator.
4	The creation of new aggregators should be done correctly.	High	The native new_aggregator function correctly creates a new aggregator.	The new_aggregator native function has been manually audited.

Module-level Specification

pragma aborts_if_is_strict;

`initialize_aggregator_factory`

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

Make sure the caller is @aptos_framework. AggregatorFactory is not under the caller before creating the resource.

let addr = signer::address_of(aptos_framework);
aborts_if addr != @aptos_framework;
aborts_if exists<AggregatorFactory>(addr);
// This enforces high-level requirement 1:
ensures exists<AggregatorFactory>(addr);

`create_aggregator_internal`

public(friend) fun create_aggregator_internal(): aggregator::Aggregator

// This enforces high-level requirement 2:
include CreateAggregatorInternalAbortsIf;
ensures aggregator::spec_get_limit(result) == MAX_U128;
ensures aggregator::spec_aggregator_get_val(result) == 0;

schema CreateAggregatorInternalAbortsIf {
    aborts_if !exists<AggregatorFactory>(@aptos_framework);
}

`create_aggregator`

#[deprecated]
public fun create_aggregator(account: &signer, limit: u128): aggregator::Aggregator

Make sure the caller is @aptos_framework. AggregatorFactory existed under the @aptos_framework when Creating a new aggregator.

let addr = signer::address_of(account);
// This enforces high-level requirement 3:
aborts_if addr != @aptos_framework;
aborts_if limit != MAX_U128;
aborts_if !exists<AggregatorFactory>(@aptos_framework);

native fun spec_new_aggregator(limit: u128): Aggregator;

`new_aggregator`

fun new_aggregator(aggregator_factory: &mut aggregator_factory::AggregatorFactory, limit: u128): aggregator::Aggregator

pragma opaque;
aborts_if false;
ensures result == spec_new_aggregator(limit);
ensures aggregator::spec_get_limit(result) == limit;