optional_aggregator - [mainnet]

This module provides an interface to aggregate integers either via aggregator (parallelizable) or via normal integers.

use 0x1::aggregator;
use 0x1::aggregator_factory;
use 0x1::error;
use 0x1::option;

Constants

const MAX_U128: u128 = 340282366920938463463374607431768211455;

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

const EAGGREGATOR_OVERFLOW: u64 = 1;

Aggregator feature is not supported. Raised by native code.

const EAGGREGATOR_UNDERFLOW: u64 = 2;

OptionalAggregator (Agg V1) switch not supported any more.

const ESWITCH_DEPRECATED: u64 = 3;

Structs

`Integer`

Wrapper around integer with a custom overflow limit. Supports add, subtract and read just like Aggregator.

struct Integer has store

Fields

value: u128
limit: u128

`OptionalAggregator`

Contains either an aggregator or a normal integer, both overflowing on limit.

struct OptionalAggregator has store

Fields

aggregator: option::Option<aggregator::Aggregator>
integer: option::Option<optional_aggregator::Integer>

Functions

`new_integer`

Creates a new integer which overflows on exceeding a limit.

fun new_integer(limit: u128): optional_aggregator::Integer

Implementation

fun new_integer(limit: u128): Integer {
    Integer {
        value: 0,
        limit,
    }
}

`add_integer`

Adds value to integer. Aborts on overflowing the limit.

fun add_integer(integer: &mut optional_aggregator::Integer, value: u128)

Implementation

fun add_integer(integer: &mut Integer, value: u128) {
    assert!(
        value <= (integer.limit - integer.value),
        error::out_of_range(EAGGREGATOR_OVERFLOW)
    );
    integer.value = integer.value + value;
}

`sub_integer`

Subtracts value from integer. Aborts on going below zero.

fun sub_integer(integer: &mut optional_aggregator::Integer, value: u128)

Implementation

fun sub_integer(integer: &mut Integer, value: u128) {
    assert!(value <= integer.value, error::out_of_range(EAGGREGATOR_UNDERFLOW));
    integer.value = integer.value - value;
}

`limit`

Returns an overflow limit of integer.

fun limit(integer: &optional_aggregator::Integer): u128

Implementation

fun limit(integer: &Integer): u128 {
    integer.limit
}

`read_integer`

Returns a value stored in this integer.

fun read_integer(integer: &optional_aggregator::Integer): u128

Implementation

fun read_integer(integer: &Integer): u128 {
    integer.value
}

`destroy_integer`

Destroys an integer.

fun destroy_integer(integer: optional_aggregator::Integer)

Implementation

fun destroy_integer(integer: Integer) {
    let Integer { value: _, limit: _ } = integer;
}

`new`

Creates a new optional aggregator.

public(friend) fun new(parallelizable: bool): optional_aggregator::OptionalAggregator

Implementation

public(friend) fun new(parallelizable: bool): OptionalAggregator {
    if (parallelizable) {
        OptionalAggregator {
            aggregator: option::some(aggregator_factory::create_aggregator_internal()),
            integer: option::none(),
        }
    } else {
        OptionalAggregator {
            aggregator: option::none(),
            integer: option::some(new_integer(MAX_U128)),
        }
    }
}

`switch`

Switches between parallelizable and non-parallelizable implementations.

public fun switch(_optional_aggregator: &mut optional_aggregator::OptionalAggregator)

Implementation

public fun switch(_optional_aggregator: &mut OptionalAggregator) {
    abort error::invalid_state(ESWITCH_DEPRECATED)
}

`destroy`

Destroys optional aggregator.

public fun destroy(optional_aggregator: optional_aggregator::OptionalAggregator)

Implementation

public fun destroy(optional_aggregator: OptionalAggregator) {
    if (is_parallelizable(&optional_aggregator)) {
        destroy_optional_aggregator(optional_aggregator);
    } else {
        destroy_optional_integer(optional_aggregator);
    }
}

`destroy_optional_aggregator`

Destroys parallelizable optional aggregator and returns its limit.

fun destroy_optional_aggregator(optional_aggregator: optional_aggregator::OptionalAggregator): u128

Implementation

fun destroy_optional_aggregator(optional_aggregator: OptionalAggregator): u128 {
    let OptionalAggregator { aggregator, integer } = optional_aggregator;
    let limit = aggregator::limit(option::borrow(&aggregator));
    aggregator::destroy(option::destroy_some(aggregator));
    option::destroy_none(integer);
    limit
}

`destroy_optional_integer`

Destroys non-parallelizable optional aggregator and returns its limit.

fun destroy_optional_integer(optional_aggregator: optional_aggregator::OptionalAggregator): u128

Implementation

fun destroy_optional_integer(optional_aggregator: OptionalAggregator): u128 {
    let OptionalAggregator { aggregator, integer } = optional_aggregator;
    let limit = limit(option::borrow(&integer));
    destroy_integer(option::destroy_some(integer));
    option::destroy_none(aggregator);
    limit
}

`add`

Adds value to optional aggregator, aborting on exceeding the limit.

public fun add(optional_aggregator: &mut optional_aggregator::OptionalAggregator, value: u128)

Implementation

public fun add(optional_aggregator: &mut OptionalAggregator, value: u128) {
    if (option::is_some(&optional_aggregator.aggregator)) {
        let aggregator = option::borrow_mut(&mut optional_aggregator.aggregator);
        aggregator::add(aggregator, value);
    } else {
        let integer = option::borrow_mut(&mut optional_aggregator.integer);
        add_integer(integer, value);
    }
}

`sub`

Subtracts value from optional aggregator, aborting on going below zero.

public fun sub(optional_aggregator: &mut optional_aggregator::OptionalAggregator, value: u128)

Implementation

public fun sub(optional_aggregator: &mut OptionalAggregator, value: u128) {
    if (option::is_some(&optional_aggregator.aggregator)) {
        let aggregator = option::borrow_mut(&mut optional_aggregator.aggregator);
        aggregator::sub(aggregator, value);
    } else {
        let integer = option::borrow_mut(&mut optional_aggregator.integer);
        sub_integer(integer, value);
    }
}

`read`

Returns the value stored in optional aggregator.

public fun read(optional_aggregator: &optional_aggregator::OptionalAggregator): u128

Implementation

public fun read(optional_aggregator: &OptionalAggregator): u128 {
    if (option::is_some(&optional_aggregator.aggregator)) {
        let aggregator = option::borrow(&optional_aggregator.aggregator);
        aggregator::read(aggregator)
    } else {
        let integer = option::borrow(&optional_aggregator.integer);
        read_integer(integer)
    }
}

`is_parallelizable`

Returns true if optional aggregator uses parallelizable implementation.

public fun is_parallelizable(optional_aggregator: &optional_aggregator::OptionalAggregator): bool

Implementation

public fun is_parallelizable(optional_aggregator: &OptionalAggregator): bool {
    option::is_some(&optional_aggregator.aggregator)
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	When creating a new integer instance, it guarantees that the limit assigned is a value passed into the function as an argument, and the value field becomes zero.	High	The new_integer function sets the limit field to the argument passed in, and the value field is set to zero.	Formally verified via new_integer.
2	For a given integer instance it should always be possible to: (1) return the limit value of the integer resource, (2) return the current value stored in that particular instance, and (3) destroy the integer instance.	Low	The following functions should not abort if the Integer instance exists: limit(), read_integer(), destroy_integer().	Formally verified via: read_integer, limit, and destroy_integer.
3	Every successful switch must end with the aggregator type changed from non-parallelizable to parallelizable or vice versa.	High	The switch function run, if successful, should always change the aggregator type.	Formally verified via switch_and_zero_out.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_strict;

`OptionalAggregator`

struct OptionalAggregator has store

aggregator: option::Option<aggregator::Aggregator>
integer: option::Option<optional_aggregator::Integer>

invariant option::is_some(aggregator) <==> option::is_none(integer);
invariant option::is_some(integer) <==> option::is_none(aggregator);
invariant option::is_some(integer) ==> option::borrow(integer).value <= option::borrow(integer).limit;
invariant option::is_some(aggregator) ==> aggregator::spec_aggregator_get_val(option::borrow(aggregator)) <=
    aggregator::spec_get_limit(option::borrow(aggregator));

`new_integer`

fun new_integer(limit: u128): optional_aggregator::Integer

aborts_if false;
ensures result.limit == limit;
// This enforces high-level requirement 1:
ensures result.value == 0;

`add_integer`

fun add_integer(integer: &mut optional_aggregator::Integer, value: u128)

Check for overflow.

aborts_if value > (integer.limit - integer.value);
aborts_if integer.value + value > MAX_U128;
ensures integer.value <= integer.limit;
ensures integer.value == old(integer.value) + value;

`sub_integer`

fun sub_integer(integer: &mut optional_aggregator::Integer, value: u128)

aborts_if value > integer.value;
ensures integer.value == old(integer.value) - value;

`limit`

fun limit(integer: &optional_aggregator::Integer): u128

// This enforces high-level requirement 2:
aborts_if false;

`read_integer`

fun read_integer(integer: &optional_aggregator::Integer): u128

// This enforces high-level requirement 2:
aborts_if false;

`destroy_integer`

fun destroy_integer(integer: optional_aggregator::Integer)

// This enforces high-level requirement 2:
aborts_if false;

`new`

public(friend) fun new(parallelizable: bool): optional_aggregator::OptionalAggregator

aborts_if parallelizable && !exists<aggregator_factory::AggregatorFactory>(@aptos_framework);
ensures parallelizable ==> is_parallelizable(result);
ensures !parallelizable ==> !is_parallelizable(result);
ensures optional_aggregator_value(result) == 0;
ensures optional_aggregator_value(result) <= optional_aggregator_limit(result);

`switch`

public fun switch(_optional_aggregator: &mut optional_aggregator::OptionalAggregator)

aborts_if true;

`destroy`

public fun destroy(optional_aggregator: optional_aggregator::OptionalAggregator)

aborts_if is_parallelizable(optional_aggregator) && len(optional_aggregator.integer.vec) != 0;
aborts_if !is_parallelizable(optional_aggregator) && len(optional_aggregator.integer.vec) == 0;

`destroy_optional_aggregator`

fun destroy_optional_aggregator(optional_aggregator: optional_aggregator::OptionalAggregator): u128

The aggregator exists and the integer does not exist when destroy the aggregator.

aborts_if len(optional_aggregator.aggregator.vec) == 0;
aborts_if len(optional_aggregator.integer.vec) != 0;
ensures result == aggregator::spec_get_limit(option::borrow(optional_aggregator.aggregator));

`destroy_optional_integer`

fun destroy_optional_integer(optional_aggregator: optional_aggregator::OptionalAggregator): u128

The integer exists and the aggregator does not exist when destroy the integer.

aborts_if len(optional_aggregator.integer.vec) == 0;
aborts_if len(optional_aggregator.aggregator.vec) != 0;
ensures result == option::borrow(optional_aggregator.integer).limit;

fun optional_aggregator_value(optional_aggregator: OptionalAggregator): u128 {
   if (is_parallelizable(optional_aggregator)) {
       aggregator::spec_aggregator_get_val(option::borrow(optional_aggregator.aggregator))
   } else {
       option::borrow(optional_aggregator.integer).value
   }
}

fun optional_aggregator_limit(optional_aggregator: OptionalAggregator): u128 {
   if (is_parallelizable(optional_aggregator)) {
       aggregator::spec_get_limit(option::borrow(optional_aggregator.aggregator))
   } else {
       option::borrow(optional_aggregator.integer).limit
   }
}

`add`

public fun add(optional_aggregator: &mut optional_aggregator::OptionalAggregator, value: u128)

include AddAbortsIf;
ensures ((optional_aggregator_value(optional_aggregator) == optional_aggregator_value(old(optional_aggregator)) + value));

schema AddAbortsIf {
    optional_aggregator: OptionalAggregator;
    value: u128;
    aborts_if is_parallelizable(optional_aggregator) && (aggregator::spec_aggregator_get_val(option::borrow(optional_aggregator.aggregator))
        + value > aggregator::spec_get_limit(option::borrow(optional_aggregator.aggregator)));
    aborts_if is_parallelizable(optional_aggregator) && (aggregator::spec_aggregator_get_val(option::borrow(optional_aggregator.aggregator))
        + value > MAX_U128);
    aborts_if !is_parallelizable(optional_aggregator) &&
        (option::borrow(optional_aggregator.integer).value + value > MAX_U128);
    aborts_if !is_parallelizable(optional_aggregator) &&
        (value > (option::borrow(optional_aggregator.integer).limit - option::borrow(optional_aggregator.integer).value));
}

`sub`

public fun sub(optional_aggregator: &mut optional_aggregator::OptionalAggregator, value: u128)

include SubAbortsIf;
ensures ((optional_aggregator_value(optional_aggregator) == optional_aggregator_value(old(optional_aggregator)) - value));

schema SubAbortsIf {
    optional_aggregator: OptionalAggregator;
    value: u128;
    aborts_if is_parallelizable(optional_aggregator) && (aggregator::spec_aggregator_get_val(option::borrow(optional_aggregator.aggregator))
        < value);
    aborts_if !is_parallelizable(optional_aggregator) &&
        (option::borrow(optional_aggregator.integer).value < value);
}

`read`

public fun read(optional_aggregator: &optional_aggregator::OptionalAggregator): u128

ensures !is_parallelizable(optional_aggregator) ==> result == option::borrow(optional_aggregator.integer).value;
ensures is_parallelizable(optional_aggregator) ==>
    result == aggregator::spec_read(option::borrow(optional_aggregator.aggregator));