aggregator - [mainnet]

This module provides an interface for aggregators. Aggregators are similar to unsigned integers and support addition and subtraction (aborting on underflow or on overflowing a custom upper limit). The difference from integers is that aggregators allow to perform both additions and subtractions in parallel across multiple transactions, enabling parallel execution. For example, if the first transaction is doing add(X, 1) for aggregator resource X, and the second is doing sub(X,3), they can be executed in parallel avoiding a read-modify-write dependency. However, reading the aggregator value (i.e. calling read(X)) is an expensive operation and should be avoided as much as possible because it reduces the parallelism. Moreover, aggregators can only be created by Aptos Framework (0x1) at the moment.

Constants

The value of aggregator overflows. Raised by native code.

const EAGGREGATOR_OVERFLOW: u64 = 1;

The value of aggregator underflows (goes below zero). Raised by native code.

const EAGGREGATOR_UNDERFLOW: u64 = 2;

Aggregator feature is not supported. Raised by native code.

const ENOT_SUPPORTED: u64 = 3;

Structs

`Aggregator`

Represents an integer which supports parallel additions and subtractions across multiple transactions. See the module description for more details.

struct Aggregator has store

Fields

handle: address
key: address
limit: u128

Functions

`limit`

Returns limit exceeding which aggregator overflows.

public fun limit(aggregator: &aggregator::Aggregator): u128

Implementation

public fun limit(aggregator: &Aggregator): u128 {
    aggregator.limit
}

`add`

Adds value to aggregator. Aborts on overflowing the limit.

public fun add(aggregator: &mut aggregator::Aggregator, value: u128)

Implementation

public native fun add(aggregator: &mut Aggregator, value: u128);

`sub`

Subtracts value from aggregator. Aborts on going below zero.

public fun sub(aggregator: &mut aggregator::Aggregator, value: u128)

Implementation

public native fun sub(aggregator: &mut Aggregator, value: u128);

`read`

Returns a value stored in this aggregator.

public fun read(aggregator: &aggregator::Aggregator): u128

Implementation

public native fun read(aggregator: &Aggregator): u128;

`destroy`

Destroys an aggregator and removes it from its AggregatorFactory.

public fun destroy(aggregator: aggregator::Aggregator)

Implementation

public native fun destroy(aggregator: Aggregator);

Specification

`Aggregator`

struct Aggregator has store

handle: address
key: address
limit: u128

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	For a given aggregator, it should always be possible to: Return the limit value of the aggregator. Return the current value stored in the aggregator. Destroy an aggregator, removing it from its AggregatorFactory.	Low	The following functions should not abort if EventHandle exists: limit(), read(), destroy().	Formally verified via read, destroy, and limit.
2	If the value during addition exceeds the limit, an overflow occurs.	High	The native add() function checks the value of the addition to ensure it does not pass the defined limit and results in aggregator overflow.	Formally verified via add.
3	Operations over aggregators should be correct.	High	The implementation of the add, sub, read and destroy functions is correct.	The native implementation of the add, sub, read and destroy functions have been manually audited.

Module-level Specification

pragma intrinsic;

`limit`

public fun limit(aggregator: &aggregator::Aggregator): u128

pragma intrinsic;
// This enforces high-level requirement 1:
aborts_if [abstract] false;

native fun spec_read(aggregator: Aggregator): u128;

native fun spec_get_limit(a: Aggregator): u128;

native fun spec_get_handle(a: Aggregator): u128;

native fun spec_get_key(a: Aggregator): u128;

native fun spec_aggregator_set_val(a: Aggregator, v: u128): Aggregator;

native fun spec_aggregator_get_val(a: Aggregator): u128;

`add`

public fun add(aggregator: &mut aggregator::Aggregator, value: u128)

pragma opaque;
aborts_if spec_aggregator_get_val(aggregator) + value > spec_get_limit(aggregator);
// This enforces high-level requirement 2:
aborts_if spec_aggregator_get_val(aggregator) + value > MAX_U128;
ensures spec_get_limit(aggregator) == spec_get_limit(old(aggregator));
ensures aggregator == spec_aggregator_set_val(old(aggregator),
    spec_aggregator_get_val(old(aggregator)) + value);

`sub`

public fun sub(aggregator: &mut aggregator::Aggregator, value: u128)

pragma opaque;
aborts_if spec_aggregator_get_val(aggregator) < value;
ensures spec_get_limit(aggregator) == spec_get_limit(old(aggregator));
ensures aggregator == spec_aggregator_set_val(old(aggregator),
    spec_aggregator_get_val(old(aggregator)) - value);

`read`

public fun read(aggregator: &aggregator::Aggregator): u128

pragma opaque;
// This enforces high-level requirement 1:
aborts_if false;
ensures result == spec_read(aggregator);
ensures result <= spec_get_limit(aggregator);

`destroy`

public fun destroy(aggregator: aggregator::Aggregator)

pragma opaque;
// This enforces high-level requirement 1:
aborts_if false;