Tortuga Finance Docs
Website
Search
⌃K
Links
Comment on page

helpers::math

Module 0xc0ded0c0::math

Safe maths helpers

Adapted from https://github.com/pentagonxyz/movemate/
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;
Previous
helpers::circular_buffer
Next
helpers::pool
Last modified 1yr ago