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

Simple module for tracking and calculating shares of a pool of coins. The shares are worth more as the total coins in the pool increases. New shareholder can buy more shares or redeem their existing shares.

Example flow:

  1. Pool start outs empty.
  2. Shareholder A buys in with 1000 coins. A will receive 1000 shares in the pool. Pool now has 1000 total coins and 1000 total shares.
  3. Pool appreciates in value from rewards and now has 2000 coins. A’s 1000 shares are now worth 2000 coins.
  4. Shareholder B now buys in with 1000 coins. Since before the buy in, each existing share is worth 2 coins, B will receive 500 shares in exchange for 1000 coins. Pool now has 1500 shares and 3000 coins.
  5. Pool appreciates in value from rewards and now has 6000 coins.
  6. A redeems 500 shares. Each share is worth 6000 / 1500 = 4. A receives 2000 coins. Pool has 4000 coins and 1000 shares left.
use 0x1::error;
use 0x1::table_with_length;

Struct Pool 

struct Pool has store
Fields
total_coins: u64
total_shares: u128
shares: table_with_length::TableWithLength<address, u128>
scaling_factor: u64

Constants 

const MAX_U64: u64 = 18446744073709551615;


const MAX_U128: u128 = 340282366920938463463374607431768211455;

Cannot redeem more shares than the shareholder has in the pool.

const EINSUFFICIENT_SHARES: u64 = 4;

Cannot destroy non-empty pool.

const EPOOL_IS_NOT_EMPTY: u64 = 3;

Pool’s total coins cannot exceed u64.max.

const EPOOL_TOTAL_COINS_OVERFLOW: u64 = 6;

Pool’s total shares cannot exceed u64.max.

const EPOOL_TOTAL_SHARES_OVERFLOW: u64 = 7;

Shareholder not present in pool.

const ESHAREHOLDER_NOT_FOUND: u64 = 1;

Shareholder cannot have more than u64.max shares.

const ESHAREHOLDER_SHARES_OVERFLOW: u64 = 5;

There are too many shareholders in the pool.

const ETOO_MANY_SHAREHOLDERS: u64 = 2;

Function new

Create a new pool.

public fun new(): pool_u64_unbound::Pool
Implementation 
public fun new(): Pool {
    // Default to a scaling factor of 1 (effectively no scaling).
    create_with_scaling_factor(1)
}

Function create

Deprecated. Use new instead. Create a new pool.

#[deprecated]
public fun create(): pool_u64_unbound::Pool
Implementation 
public fun create(): Pool {
    new()
}

Function create_with_scaling_factor

Create a new pool with custom scaling_factor.

public fun create_with_scaling_factor(scaling_factor: u64): pool_u64_unbound::Pool
Implementation 
public fun create_with_scaling_factor(scaling_factor: u64): Pool {
    Pool {
        total_coins: 0,
        total_shares: 0,
        shares: table::new<address, u128>(),
        scaling_factor,
    }
}

Function destroy_empty

Destroy an empty pool. This will fail if the pool has any balance of coins.

public fun destroy_empty(self: pool_u64_unbound::Pool)
Implementation 
public fun destroy_empty(self: Pool) {
    assert!(self.total_coins == 0, error::invalid_state(EPOOL_IS_NOT_EMPTY));
    let Pool {
        total_coins: _,
        total_shares: _,
        shares,
        scaling_factor: _,
    } = self;
    shares.destroy_empty<address, u128>();
}

Function total_coins

Return self’s total balance of coins.

public fun total_coins(self: &pool_u64_unbound::Pool): u64
Implementation 
public fun total_coins(self: &Pool): u64 {
    self.total_coins
}

Function total_shares

Return the total number of shares across all shareholders in self.

public fun total_shares(self: &pool_u64_unbound::Pool): u128
Implementation 
public fun total_shares(self: &Pool): u128 {
    self.total_shares
}

Function contains

Return true if shareholder is in self.

public fun contains(self: &pool_u64_unbound::Pool, shareholder: address): bool
Implementation 
public fun contains(self: &Pool, shareholder: address): bool {
    self.shares.contains(shareholder)
}

Function shares

Return the number of shares of stakeholder in self.

public fun shares(self: &pool_u64_unbound::Pool, shareholder: address): u128
Implementation 
public fun shares(self: &Pool, shareholder: address): u128 {
    if (self.contains(shareholder)) {
        *self.shares.borrow(shareholder)
    } else {
        0
    }
}

Function balance

Return the balance in coins of shareholder in self.

public fun balance(self: &pool_u64_unbound::Pool, shareholder: address): u64
Implementation 
public fun balance(self: &Pool, shareholder: address): u64 {
    let num_shares = self.shares(shareholder);
    self.shares_to_amount(num_shares)
}

Function shareholders_count

Return the number of shareholders in self.

public fun shareholders_count(self: &pool_u64_unbound::Pool): u64
Implementation 
public fun shareholders_count(self: &Pool): u64 {
    self.shares.length()
}

Function update_total_coins

Update self’s total balance of coins.

public fun update_total_coins(self: &mut pool_u64_unbound::Pool, new_total_coins: u64)
Implementation 
public fun update_total_coins(self: &mut Pool, new_total_coins: u64) {
    self.total_coins = new_total_coins;
}

Function buy_in

Allow an existing or new shareholder to add their coins to the pool in exchange for new shares.

public fun buy_in(self: &mut pool_u64_unbound::Pool, shareholder: address, coins_amount: u64): u128
Implementation 
public fun buy_in(self: &mut Pool, shareholder: address, coins_amount: u64): u128 {
    if (coins_amount == 0) return 0;

    let new_shares = self.amount_to_shares(coins_amount);
    assert!(MAX_U64 - self.total_coins >= coins_amount, error::invalid_argument(EPOOL_TOTAL_COINS_OVERFLOW));
    assert!(MAX_U128 - self.total_shares >= new_shares, error::invalid_argument(EPOOL_TOTAL_SHARES_OVERFLOW));

    self.total_coins += coins_amount;
    self.total_shares += new_shares;
    self.add_shares(shareholder, new_shares);
    new_shares
}

Function add_shares

Add the number of shares directly for shareholder in self. This would dilute other shareholders if the pool’s balance of coins didn’t change.

fun add_shares(self: &mut pool_u64_unbound::Pool, shareholder: address, new_shares: u128): u128
Implementation 
fun add_shares(self: &mut Pool, shareholder: address, new_shares: u128): u128 {
    if (self.contains(shareholder)) {
        let existing_shares = self.shares.borrow_mut(shareholder);
        let current_shares = *existing_shares;
        assert!(MAX_U128 - current_shares >= new_shares, error::invalid_argument(ESHAREHOLDER_SHARES_OVERFLOW));

        *existing_shares = current_shares + new_shares;
        *existing_shares
    } else if (new_shares > 0) {
        self.shares.add(shareholder, new_shares);
        new_shares
    } else {
        new_shares
    }
}

Function redeem_shares

Allow shareholder to redeem their shares in self for coins.

public fun redeem_shares(self: &mut pool_u64_unbound::Pool, shareholder: address, shares_to_redeem: u128): u64
Implementation 
public fun redeem_shares(self: &mut Pool, shareholder: address, shares_to_redeem: u128): u64 {
    assert!(self.contains(shareholder), error::invalid_argument(ESHAREHOLDER_NOT_FOUND));
    assert!(self.shares(shareholder) >= shares_to_redeem, error::invalid_argument(EINSUFFICIENT_SHARES));

    if (shares_to_redeem == 0) return 0;

    let redeemed_coins = self.shares_to_amount(shares_to_redeem);
    self.total_coins -= redeemed_coins;
    self.total_shares -= shares_to_redeem;
    self.deduct_shares(shareholder, shares_to_redeem);

    redeemed_coins
}

Function transfer_shares

Transfer shares from shareholder_1 to shareholder_2.

public fun transfer_shares(self: &mut pool_u64_unbound::Pool, shareholder_1: address, shareholder_2: address, shares_to_transfer: u128)
Implementation 
public fun transfer_shares(
    self: &mut Pool,
    shareholder_1: address,
    shareholder_2: address,
    shares_to_transfer: u128,
) {
    assert!(self.contains(shareholder_1), error::invalid_argument(ESHAREHOLDER_NOT_FOUND));
    assert!(self.shares(shareholder_1) >= shares_to_transfer, error::invalid_argument(EINSUFFICIENT_SHARES));
    if (shares_to_transfer == 0) return;

    self.deduct_shares(shareholder_1, shares_to_transfer);
    self.add_shares(shareholder_2, shares_to_transfer);
}

Function deduct_shares

Directly deduct shareholder’s number of shares in self and return the number of remaining shares.

fun deduct_shares(self: &mut pool_u64_unbound::Pool, shareholder: address, num_shares: u128): u128
Implementation 
fun deduct_shares(self: &mut Pool, shareholder: address, num_shares: u128): u128 {
    assert!(self.contains(shareholder), error::invalid_argument(ESHAREHOLDER_NOT_FOUND));
    assert!(self.shares(shareholder) >= num_shares, error::invalid_argument(EINSUFFICIENT_SHARES));

    let existing_shares = self.shares.borrow_mut(shareholder);
    *existing_shares -= num_shares;

    // Remove the shareholder completely if they have no shares left.
    let remaining_shares = *existing_shares;
    if (remaining_shares == 0) {
        self.shares.remove(shareholder);
    };

    remaining_shares
}

Function amount_to_shares

Return the number of new shares coins_amount can buy in self. amount needs to big enough to avoid rounding number.

public fun amount_to_shares(self: &pool_u64_unbound::Pool, coins_amount: u64): u128
Implementation 
public fun amount_to_shares(self: &Pool, coins_amount: u64): u128 {
    self.amount_to_shares_with_total_coins(coins_amount, self.total_coins)
}

Function amount_to_shares_with_total_coins

Return the number of new shares coins_amount can buy in self with a custom total coins number. amount needs to big enough to avoid rounding number.

public fun amount_to_shares_with_total_coins(self: &pool_u64_unbound::Pool, coins_amount: u64, total_coins: u64): u128
Implementation 
public fun amount_to_shares_with_total_coins(self: &Pool, coins_amount: u64, total_coins: u64): u128 {
    // No shares yet so amount is worth the same number of shares.
    if (self.total_coins == 0 || self.total_shares == 0) {
        // Multiply by scaling factor to minimize rounding errors during internal calculations for buy ins/redeems.
        // This can overflow but scaling factor is expected to be chosen carefully so this would not overflow.
        (coins_amount as u128) * (self.scaling_factor as u128)
    } else {
        // Shares price = total_coins / total existing shares.
        // New number of shares = new_amount / shares_price = new_amount * existing_shares / total_amount.
        // We rearrange the calc and do multiplication first to avoid rounding errors.
        self.multiply_then_divide(coins_amount as u128, self.total_shares, total_coins as u128)
    }
}

Function shares_to_amount

Return the number of coins shares are worth in self. shares needs to big enough to avoid rounding number.

public fun shares_to_amount(self: &pool_u64_unbound::Pool, shares: u128): u64
Implementation 
public fun shares_to_amount(self: &Pool, shares: u128): u64 {
    self.shares_to_amount_with_total_coins(shares, self.total_coins)
}

Function shares_to_amount_with_total_coins

Return the number of coins shares are worth in self with a custom total coins number. shares needs to big enough to avoid rounding number.

public fun shares_to_amount_with_total_coins(self: &pool_u64_unbound::Pool, shares: u128, total_coins: u64): u64
Implementation 
public fun shares_to_amount_with_total_coins(self: &Pool, shares: u128, total_coins: u64): u64 {
    // No shares or coins yet so shares are worthless.
    if (self.total_coins == 0 || self.total_shares == 0) {
        0
    } else {
        // Shares price = total_coins / total existing shares.
        // Shares worth = shares * shares price = shares * total_coins / total existing shares.
        // We rearrange the calc and do multiplication first to avoid rounding errors.
        (self.multiply_then_divide(shares, total_coins as u128, self.total_shares) as u64)
    }
}

Function shares_to_amount_with_total_stats

Return the number of coins shares are worth in pool with custom total coins and shares numbers.

public fun shares_to_amount_with_total_stats(self: &pool_u64_unbound::Pool, shares: u128, total_coins: u64, total_shares: u128): u64
Implementation 
public fun shares_to_amount_with_total_stats(
    self: &Pool,
    shares: u128,
    total_coins: u64,
    total_shares: u128,
): u64 {
    if (self.total_coins == 0 || total_shares == 0) {
        0
    } else {
        (self.multiply_then_divide(shares, total_coins as u128, total_shares) as u64)
    }
}

Function multiply_then_divide 

public fun multiply_then_divide(self: &pool_u64_unbound::Pool, x: u128, y: u128, z: u128): u128
Implementation 
public fun multiply_then_divide(self: &Pool, x: u128, y: u128, z: u128): u128 {
    math128::mul_div(x, y, z)
}

Specification

Struct Pool 

struct Pool has store
total_coins: u64
total_shares: u128
shares: table_with_length::TableWithLength<address, u128>
scaling_factor: u64 
invariant forall addr: address:
    table::spec_contains(shares, addr) ==> (table::spec_get(shares, addr) > 0);


fun spec_contains(pool: Pool, shareholder: address): bool {
   table::spec_contains(pool.shares, shareholder)
}

Function contains 

public fun contains(self: &pool_u64_unbound::Pool, shareholder: address): bool

aborts_if false;
ensures result == spec_contains(self, shareholder);


fun spec_shares(pool: Pool, shareholder: address): u64 {
   if (spec_contains(pool, shareholder)) {
       table::spec_get(pool.shares, shareholder)
   }
   else {
       0
   }
}

Function shares 

public fun shares(self: &pool_u64_unbound::Pool, shareholder: address): u128

aborts_if false;
ensures result == spec_shares(self, shareholder);

Function balance 

public fun balance(self: &pool_u64_unbound::Pool, shareholder: address): u64

let shares = spec_shares(self, shareholder);
let total_coins = self.total_coins;
aborts_if self.total_coins > 0 && self.total_shares > 0 && (shares * total_coins) / self.total_shares > MAX_U64;
ensures result == spec_shares_to_amount_with_total_coins(self, shares, total_coins);

Function buy_in 

public fun buy_in(self: &mut pool_u64_unbound::Pool, shareholder: address, coins_amount: u64): u128

let new_shares = spec_amount_to_shares_with_total_coins(self, coins_amount, self.total_coins);
aborts_if self.total_coins + coins_amount > MAX_U64;
aborts_if self.total_shares + new_shares > MAX_U128;
include coins_amount > 0 ==> AddSharesAbortsIf { new_shares };
include coins_amount > 0 ==> AddSharesEnsures { new_shares };
ensures self.total_coins == old(self.total_coins) + coins_amount;
ensures self.total_shares == old(self.total_shares) + new_shares;
ensures result == new_shares;

Function add_shares 

fun add_shares(self: &mut pool_u64_unbound::Pool, shareholder: address, new_shares: u128): u128

include AddSharesAbortsIf;
include AddSharesEnsures;
let key_exists = table::spec_contains(self.shares, shareholder);
ensures result == if (key_exists) { table::spec_get(self.shares, shareholder) }
else { new_shares };


schema AddSharesAbortsIf {
    self: Pool;
    shareholder: address;
    new_shares: u64;
    let key_exists = table::spec_contains(self.shares, shareholder);
    let current_shares = table::spec_get(self.shares, shareholder);
    aborts_if key_exists && current_shares + new_shares > MAX_U128;
}


schema AddSharesEnsures {
    self: Pool;
    shareholder: address;
    new_shares: u64;
    let key_exists = table::spec_contains(self.shares, shareholder);
    let current_shares = table::spec_get(self.shares, shareholder);
    ensures key_exists ==>
        self.shares == table::spec_set(old(self.shares), shareholder, current_shares + new_shares);
    ensures (!key_exists && new_shares > 0) ==>
        self.shares == table::spec_set(old(self.shares), shareholder, new_shares);
}


fun spec_amount_to_shares_with_total_coins(pool: Pool, coins_amount: u64, total_coins: u64): u128 {
   if (pool.total_coins == 0 || pool.total_shares == 0) {
       coins_amount * pool.scaling_factor
   }
   else {
       (coins_amount * pool.total_shares) / total_coins
   }
}

Function redeem_shares 

public fun redeem_shares(self: &mut pool_u64_unbound::Pool, shareholder: address, shares_to_redeem: u128): u64

let redeemed_coins = spec_shares_to_amount_with_total_coins(self, shares_to_redeem, self.total_coins);
aborts_if !spec_contains(self, shareholder);
aborts_if spec_shares(self, shareholder) < shares_to_redeem;
aborts_if self.total_coins < redeemed_coins;
aborts_if self.total_shares < shares_to_redeem;
ensures self.total_coins == old(self.total_coins) - redeemed_coins;
ensures self.total_shares == old(self.total_shares) - shares_to_redeem;
include shares_to_redeem > 0 ==> DeductSharesEnsures {
    num_shares: shares_to_redeem
};
ensures result == redeemed_coins;

Function transfer_shares 

public fun transfer_shares(self: &mut pool_u64_unbound::Pool, shareholder_1: address, shareholder_2: address, shares_to_transfer: u128)

aborts_if (shareholder_1 != shareholder_2) && shares_to_transfer > 0 && spec_contains(self, shareholder_2) &&
    (spec_shares(self, shareholder_2) + shares_to_transfer > MAX_U128);
aborts_if !spec_contains(self, shareholder_1);
aborts_if spec_shares(self, shareholder_1) < shares_to_transfer;
ensures shareholder_1 == shareholder_2 ==> spec_shares(old(self), shareholder_1) == spec_shares(
    self, shareholder_1);
ensures ((shareholder_1 != shareholder_2) && (spec_shares(old(self), shareholder_1) == shares_to_transfer)) ==>
    !spec_contains(self, shareholder_1);
ensures (shareholder_1 != shareholder_2 && shares_to_transfer > 0) ==>
    (spec_contains(self, shareholder_2));
ensures (shareholder_1 != shareholder_2 && shares_to_transfer > 0 && !spec_contains(old(self), shareholder_2)) ==>
    (spec_contains(self, shareholder_2) && spec_shares(self, shareholder_2) == shares_to_transfer);
ensures (shareholder_1 != shareholder_2 && shares_to_transfer > 0 && spec_contains(old(self), shareholder_2)) ==>
    (spec_contains(self, shareholder_2) && spec_shares(self, shareholder_2) == spec_shares(old(self), shareholder_2) + shares_to_transfer);
ensures ((shareholder_1 != shareholder_2) && (spec_shares(old(self), shareholder_1) > shares_to_transfer)) ==>
    (spec_contains(self, shareholder_1) && (spec_shares(self, shareholder_1) == spec_shares(old(self), shareholder_1) - shares_to_transfer));

Function deduct_shares 

fun deduct_shares(self: &mut pool_u64_unbound::Pool, shareholder: address, num_shares: u128): u128

aborts_if !spec_contains(self, shareholder);
aborts_if spec_shares(self, shareholder) < num_shares;
include DeductSharesEnsures;
let remaining_shares = table::spec_get(self.shares, shareholder) - num_shares;
ensures remaining_shares > 0 ==> result == table::spec_get(self.shares, shareholder);
ensures remaining_shares == 0 ==> result == 0;


schema DeductSharesEnsures {
    self: Pool;
    shareholder: address;
    num_shares: u64;
    let remaining_shares = table::spec_get(self.shares, shareholder) - num_shares;
    ensures remaining_shares > 0 ==> table::spec_get(self.shares, shareholder) == remaining_shares;
    ensures remaining_shares == 0 ==> !table::spec_contains(self.shares, shareholder);
}

Function amount_to_shares_with_total_coins 

public fun amount_to_shares_with_total_coins(self: &pool_u64_unbound::Pool, coins_amount: u64, total_coins: u64): u128

aborts_if self.total_coins > 0 && self.total_shares > 0
    && (coins_amount * self.total_shares) / total_coins > MAX_U128;
aborts_if (self.total_coins == 0 || self.total_shares == 0)
    && coins_amount * self.scaling_factor > MAX_U128;
aborts_if self.total_coins > 0 && self.total_shares > 0 && total_coins == 0;
ensures result == spec_amount_to_shares_with_total_coins(self, coins_amount, total_coins);

Function shares_to_amount_with_total_coins 

public fun shares_to_amount_with_total_coins(self: &pool_u64_unbound::Pool, shares: u128, total_coins: u64): u64

aborts_if self.total_coins > 0 && self.total_shares > 0
    && (shares * total_coins) / self.total_shares > MAX_U64;
ensures result == spec_shares_to_amount_with_total_coins(self, shares, total_coins);


fun spec_shares_to_amount_with_total_coins(pool: Pool, shares: u128, total_coins: u64): u64 {
   if (pool.total_coins == 0 || pool.total_shares == 0) {
       0
   }
   else {
       (shares * total_coins) / pool.total_shares
   }
}

Function multiply_then_divide 

public fun multiply_then_divide(self: &pool_u64_unbound::Pool, x: u128, y: u128, z: u128): u128

aborts_if z == 0;
aborts_if (x * y) / z > MAX_U128;
ensures result == (x * y) / z;