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
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
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
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;
Remove amount from iterable 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.
Returns the value of the entry with the given key address in the . If the entry does not exist, returns 0.
