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

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;

Struct 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

Struct 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>

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;

Function 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,
    }
}

Function 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 += value;
}

Function 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 -= value;
}

Function limit

Returns an overflow limit of integer.

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

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

Function destroy_integer

Destroys an integer.

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

Function 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)),
        }
    }
}

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

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

Function 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(aggregator.borrow());
    aggregator::destroy(aggregator.destroy_some());
    integer.destroy_none();
    limit
}

Function 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(integer.borrow());
    destroy_integer(integer.destroy_some());
    aggregator.destroy_none();
    limit
}

Function 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 (optional_aggregator.aggregator.is_some()) {
        let aggregator = optional_aggregator.aggregator.borrow_mut();
        aggregator::add(aggregator, value);
    } else {
        let integer = optional_aggregator.integer.borrow_mut();
        add_integer(integer, value);
    }
}

Function 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 (optional_aggregator.aggregator.is_some()) {
        let aggregator = optional_aggregator.aggregator.borrow_mut();
        aggregator::sub(aggregator, value);
    } else {
        let integer = optional_aggregator.integer.borrow_mut();
        sub_integer(integer, value);
    }
}

Function 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 (optional_aggregator.aggregator.is_some()) {
        let aggregator = optional_aggregator.aggregator.borrow();
        aggregator::read(aggregator)
    } else {
        let integer = optional_aggregator.integer.borrow();
        read_integer(integer)
    }
}

Function 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 {
    optional_aggregator.aggregator.is_some()
}

Specification

High-level Requirements

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

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

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

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

Function sub_integer 

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

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

Function limit 

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

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

Function read_integer 

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

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

Function destroy_integer 

fun destroy_integer(integer: optional_aggregator::Integer)

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

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

Function switch 

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

aborts_if true;

Function destroy 

public fun destroy(optional_aggregator: optional_aggregator::OptionalAggregator)

aborts_if is_parallelizable(optional_aggregator) && option::is_some(optional_aggregator.integer);
aborts_if !is_parallelizable(optional_aggregator) && option::is_none(optional_aggregator.integer);

Function 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 option::is_none(optional_aggregator.aggregator);
aborts_if option::is_some(optional_aggregator.integer);
ensures result == aggregator::spec_get_limit(option::borrow(optional_aggregator.aggregator));

Function 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 option::is_none(optional_aggregator.integer);
aborts_if option::is_some(optional_aggregator.aggregator);
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
   }
}

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

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

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