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

Standard math utilities missing in the Move Language.

use 0x1::error;
use 0x1::fixed_point32;
use 0x1::math128;

Constants

Abort code on overflow

const EOVERFLOW_EXP: u64 = 1;

Natural log 2 in 32 bit fixed point

const LN2: u128 = 2977044472;


const LN2_X_32: u64 = 95265423104;

Function sqrt

Square root of fixed point number

public fun sqrt(x: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32
Implementation 
public fun sqrt(x: FixedPoint32): FixedPoint32 {
    let y = (x.get_raw_value() as u128);
    fixed_point32::create_from_raw_value((math128::sqrt(y << 32) as u64))
}

Function exp

Exponent function with a precission of 9 digits.

public fun exp(x: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32
Implementation 
public fun exp(x: FixedPoint32): FixedPoint32 {
    let raw_value = (x.get_raw_value() as u128);
    fixed_point32::create_from_raw_value((exp_raw(raw_value) as u64))
}

Function log2_plus_32

Because log2 is negative for values < 1 we instead return log2(x) + 32 which is positive for all values of x.

public fun log2_plus_32(x: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32
Implementation 
public fun log2_plus_32(x: FixedPoint32): FixedPoint32 {
    let raw_value = (x.get_raw_value() as u128);
    math128::log2(raw_value)
}

Function ln_plus_32ln2 

public fun ln_plus_32ln2(x: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32
Implementation 
public fun ln_plus_32ln2(x: FixedPoint32): FixedPoint32 {
    let raw_value = (x.get_raw_value() as u128);
    let x = (math128::log2(raw_value).get_raw_value() as u128);
    fixed_point32::create_from_raw_value((x * LN2 >> 32 as u64))
}

Function pow

Integer power of a fixed point number

public fun pow(x: fixed_point32::FixedPoint32, n: u64): fixed_point32::FixedPoint32
Implementation 
public fun pow(x: FixedPoint32, n: u64): FixedPoint32 {
    let raw_value = (x.get_raw_value() as u128);
    fixed_point32::create_from_raw_value((pow_raw(raw_value, (n as u128)) as u64))
}

Function mul_div

Specialized function for x * y / z that omits intermediate shifting

public fun mul_div(x: fixed_point32::FixedPoint32, y: fixed_point32::FixedPoint32, z: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32
Implementation 
public fun mul_div(x: FixedPoint32, y: FixedPoint32, z: FixedPoint32): FixedPoint32 {
    let a = x.get_raw_value();
    let b = y.get_raw_value();
    let c = z.get_raw_value();
    fixed_point32::create_from_raw_value (math64::mul_div(a, b, c))
}

Function exp_raw 

fun exp_raw(x: u128): u128
Implementation 
fun exp_raw(x: u128): u128 {
    // exp(x / 2^32) = 2^(x / (2^32 * ln(2))) = 2^(floor(x / (2^32 * ln(2))) + frac(x / (2^32 * ln(2))))
    let shift_long = x / LN2;
    assert!(shift_long <= 31, std::error::invalid_state(EOVERFLOW_EXP));
    let shift = (shift_long as u8);
    let remainder = x % LN2;
    // At this point we want to calculate 2^(remainder / ln2) << shift
    // ln2 = 595528 * 4999 which means
    let bigfactor = 595528;
    let exponent = remainder / bigfactor;
    let x = remainder % bigfactor;
    // 2^(remainder / ln2) = (2^(1/4999))^exponent * exp(x / 2^32)
    let roottwo = 4295562865;  // fixed point representation of 2^(1/4999)
    // This has an error of 5000 / 4 10^9 roughly 6 digits of precission
    let power = pow_raw(roottwo, exponent);
    let eps_correction = 1241009291;
    power += ((power * eps_correction * exponent) >> 64);
    // x is fixed point number smaller than 595528/2^32 < 0.00014 so we need only 2 tayler steps
    // to get the 6 digits of precission
    let taylor1 = (power * x) >> (32 - shift);
    let taylor2 = (taylor1 * x) >> 32;
    let taylor3 = (taylor2 * x) >> 32;
    (power << shift) + taylor1 + taylor2 / 2 + taylor3 / 6
}

Function pow_raw 

fun pow_raw(x: u128, n: u128): u128
Implementation 
fun pow_raw(x: u128, n: u128): u128 {
    let res: u256 = 1 << 64;
    x <<= 32;
    while (n != 0) {
        if (n & 1 != 0) {
            res = (res * (x as u256)) >> 64;
        };
        n >>= 1;
        x = ((((x as u256) * (x as u256)) >> 64) as u128);
    };
    ((res >> 32) as u128)
}

Specification

Function sqrt 

public fun sqrt(x: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32

sqrt never aborts: math128::sqrt(0)==0 so the Newton step is skipped; for y>0 result fits in u64. No loop in the body, so callers can inline without havocing.

aborts_if false;

Function mul_div 

public fun mul_div(x: fixed_point32::FixedPoint32, y: fixed_point32::FixedPoint32, z: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32

mul_div aborts when z is zero or when x * y / z overflows u64. The result equals the exact arithmetic quotient.

aborts_if z.get_raw_value() == 0;
aborts_if (x.get_raw_value() as u128) * (y.get_raw_value() as u128) / (z.get_raw_value() as u128) > MAX_U64;
ensures (result.get_raw_value() as u128) ==
        (x.get_raw_value() as u128) * (y.get_raw_value() as u128) / (z.get_raw_value() as u128);