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

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.

Struct 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

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;

Function limit

Returns limit exceeding which aggregator overflows.

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

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

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

Function read

Returns a value stored in this aggregator.

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

Function destroy

Destroys an aggregator and removes it from its AggregatorFactory.

public fun destroy(aggregator: aggregator::Aggregator)
Implementation 
public native fun destroy(aggregator: Aggregator);

Specification

Struct Aggregator 

struct Aggregator has store
handle: address
key: address
limit: u128

High-level Requirements

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

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

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

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

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

Function destroy 

public fun destroy(aggregator: aggregator::Aggregator)

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