helpers::math

Module 0xc0ded0c0::math

Safe maths helpers

Adapted from https://github.com/pentagonxyz/movemate/

---

• Safe maths helpers

• Constants

• Function mul_div

  • Assumes

• Function safe_mul_div

  • Abort conditions

• Function mul_div_with_init

• Function safe_sub

• Function safe_sub_u128

• Function add_possibly_negative

  • Abort conditions

• Function round_robin

  • Abort conditions

• Function max_u128

• Function safe_add_to_iterable_table_custom

• Function subtract_from_iterable_table_custom

• Function safe_get_from_iterable_table_custom

• Function calc_shares_to_value

use 0x1::error;
use 0xc0ded0c0::iterable_table_custom;

Constants

When an illegal operation is requested

const EARITHMETIC_ERROR: u64 = 0;

const FLOATING_POINT_SHIFT: u64 = 100;

These parameters may depend on staking_config and epoch length

const FLOATING_POINT_TOLERANCE: u64 = 1000;

Function mul_div

Returns a * b / c but converts to u128s for calculations to avoid overflow.

Assumes

• c > 0.

• a * b / c fits into u64.

public fun mul_div(a: u64, b: u64, c: u64): u64

Implementation

public fun mul_div(a: u64, b: u64, c: u64): u64 {
    ((a as u128) * (b as u128) / (c as u128) as u64)
}

Specification

aborts_if c == 0;
aborts_if a * b / c > MAX_U64;
ensures result <= MAX_U64;

Function safe_mul_div

Returns a * b / c without overflows but returns 0 when a = 0.

Abort conditions

Aborts with error_code if c = 0.

public fun safe_mul_div(a: u64, b: u64, c: u64, error_code: u64): u64

Implementation

public fun safe_mul_div(a: u64, b: u64, c: u64, error_code: u64): u64 {
    if (a == 0) {
        return 0
    };
    assert!(c > 0, error::invalid_state(error_code));
    mul_div(a, b, c)
}

Function mul_div_with_init

Returns a * b / c without overflows if a and c are not 0. Returns 0 if a = 0. Returns a * init_factor if c = 0.

public fun mul_div_with_init(a: u64, b: u64, c: u64, init_factor: u64): u64

Implementation

public fun mul_div_with_init(
    a: u64,
    b: u64,
    c: u64,
    init_factor: u64
): u64 {
    if (a == 0) {
        return 0
    };
    if (c == 0) {
        return a * init_factor
    };
    mul_div(a, b, c)
}

Function safe_sub

Returns a - b if a > b and 0 otherwise.

public fun safe_sub(a: u64, b: u64): u64

Implementation

public fun safe_sub(a: u64, b: u64): u64 {
    if (a >= b) {
        a - b
    } else {
        0
    }
}

Function safe_sub_u128

Returns a - b if a > b and 0 otherwise for u128.

public fun safe_sub_u128(a: u128, b: u128): u128

Implementation

public fun safe_sub_u128(a: u128, b: u128): u128 {
    if (a >= b) {
        a - b
    } else {
        0
    }
}

Specification

aborts_if false;

Function add_possibly_negative

Returns either a + pos_b or a - neg_b depending on which is non-zero.

Abort conditions

If both pos_b and neg_b are non-zero.

public fun add_possibly_negative(a: u64, pos_b: u64, neg_b: u64): u64

Implementation

public fun add_possibly_negative(a: u64, pos_b: u64, neg_b: u64): u64 {
    assert!(pos_b == 0 || neg_b == 0, 0);
    if (pos_b > 0) {
        a + pos_b
    } else {
        safe_sub(a, neg_b)
    }
}

Function round_robin

Returns the index of ath entry in an array of b entries. If a == b, returns 0, else returns a.

Abort conditions

If a > b or b == 0.

public fun round_robin(a: u64, b: u64): u64

Implementation

public fun round_robin(a: u64, b: u64): u64 {
    assert!(b > 0 && a <= b, error::invalid_argument(EARITHMETIC_ERROR));
    if (a < b) a else 0
}

Specification

aborts_if b == 0 || a > b;

Function max_u128

Returns the maximum between two u128 values.

public fun max_u128(a: u128, b: u128): u128

Implementation

public fun max_u128(a: u128, b: u128): u128 {
    if (a >= b) a else b
}

Function safe_add_to_iterable_table_custom

Adds an entry to the table with the given key address and value u64. If the entry already existed, then the passed value is added to the existing value. Otherwise, a new entry is created in the table for the given address.

public fun safe_add_to_iterable_table_custom(table: &mut iterable_table_custom::IterableTableCustom<address, u64>, key: address, amount: u64)

Implementation

public fun safe_add_to_iterable_table_custom(
    table: &mut IterableTableCustom<address, u64>,
    key: address,
    amount: u64
) {
    if (amount == 0) {
        return
    };

    if (iterable_table_custom::contains(table, key)) {
        let current = iterable_table_custom::borrow_mut(table, key);
        *current = *current + amount;
    }
    else {
        iterable_table_custom::add(table, key, amount);
    };
}

Function subtract_from_iterable_table_custom

Remove amount from iterable table from the key. Delete the key if its value goes to 0. Returns the actual amount removed from the value. It may be smaller than the amount passed if the existing value was smaller.

public fun subtract_from_iterable_table_custom(table: &mut iterable_table_custom::IterableTableCustom<address, u64>, key: address, amount: u64): u64

Implementation

public fun subtract_from_iterable_table_custom(
    table: &mut IterableTableCustom<address, u64>,
    key: address,
    amount: u64,
): u64 {
    let current = iterable_table_custom::borrow_mut(table, key);
    let current_val = *current;
    if (current_val > amount) {
        *current = *current - amount;
        amount
    } else {
        iterable_table_custom::remove(table, key);
        current_val
    }
}

Function safe_get_from_iterable_table_custom

Returns the value of the entry with the given key address in the table. If the entry does not exist, returns 0.

public fun safe_get_from_iterable_table_custom(table: &iterable_table_custom::IterableTableCustom<address, u64>, key: address): u64

Implementation

public fun safe_get_from_iterable_table_custom(
    table: &IterableTableCustom<address, u64>,
    key: address
): u64 {
    if (iterable_table_custom::contains(table, key)) {
        *iterable_table_custom::borrow(table, key)
    } else {
        0
    }
}

Function calc_shares_to_value

This function is used in tortuga::stake_router. We verify it here as prover doesn't seem to work well in tortuga::stake_router.

fun calc_shares_to_value(num_shares: u64, total_worth: u64, t_apt_supply: u64): u64

Implementation

fun calc_shares_to_value(
    num_shares: u64,
    total_worth: u64,
    t_apt_supply: u64
): u64 {
    assert!(
        t_apt_supply >= num_shares,
        error::invalid_state(0)
    );
    safe_mul_div(num_shares, total_worth, t_apt_supply, 0)
}

Specification

requires t_apt_supply != 0;
aborts_if t_apt_supply < num_shares;
ensures result <= MAX_U64;
ensures result == num_shares * total_worth / t_apt_supply;