Module 0x1::fixed_point64

Defines a fixed-point numeric type with a 64-bit integer part and a 64-bit fractional part.

• Struct FixedPoint64
• Constants
• Function sub
• Function add
• Function multiply_u128
• Function divide_u128
• Function create_from_rational
• Function create_from_raw_value
• Function get_raw_value
• Function is_zero
• Function min
• Function max
• Function less_or_equal
• Function less
• Function greater_or_equal
• Function greater
• Function equal
• Function almost_equal
• Function create_from_u128
• Function floor
• Function ceil
• Function round
• Specification
  • Function sub
  • Function add
  • Function multiply_u128
  • Function divide_u128
  • Function create_from_rational
  • Function create_from_raw_value
  • Function min
  • Function max
  • Function less_or_equal
  • Function less
  • Function greater_or_equal
  • Function greater
  • Function equal
  • Function almost_equal
  • Function create_from_u128
  • Function floor
  • Function ceil
  • Function round

Struct FixedPoint64

Define a fixed-point numeric type with 64 fractional bits. This is just a u128 integer but it is wrapped in a struct to make a unique type. This is a binary representation, so decimal values may not be exactly representable, but it provides more than 9 decimal digits of precision both before and after the decimal point (18 digits total). For comparison, double precision floating-point has less than 16 decimal digits of precision, so be careful about using floating-point to convert these values to decimal.

struct FixedPoint64 has copy, drop, store

Constants

const MAX_U128: u256 = 340282366920938463463374607431768211455;

The denominator provided was zero

const EDENOMINATOR: u64 = 65537;

The quotient value would be too large to be held in a u128

const EDIVISION: u64 = 131074;

A division by zero was encountered

const EDIVISION_BY_ZERO: u64 = 65540;

The multiplied value would be too large to be held in a u128

const EMULTIPLICATION: u64 = 131075;

The computed ratio when converting to a FixedPoint64 would be unrepresentable

const ERATIO_OUT_OF_RANGE: u64 = 131077;

Abort code on calculation result is negative.

const ENEGATIVE_RESULT: u64 = 65542;

Function sub

Returns self - y. self must be not less than y.

public fun sub(self: fixed_point64::FixedPoint64, y: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

public fun sub(self: FixedPoint64, y: FixedPoint64): FixedPoint64 {
    let x_raw = self.get_raw_value();
    let y_raw = y.get_raw_value();
    assert!(x_raw >= y_raw, ENEGATIVE_RESULT);
    create_from_raw_value(x_raw - y_raw)
}

Function add

Returns self + y. The result cannot be greater than MAX_U128.

public fun add(self: fixed_point64::FixedPoint64, y: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

public fun add(self: FixedPoint64, y: FixedPoint64): FixedPoint64 {
    let x_raw = self.get_raw_value();
    let y_raw = y.get_raw_value();
    let result = (x_raw as u256) + (y_raw as u256);
    assert!(result <= MAX_U128, ERATIO_OUT_OF_RANGE);
    create_from_raw_value((result as u128))
}

Function multiply_u128

Multiply a u128 integer by a fixed-point number, truncating any fractional part of the product. This will abort if the product overflows.

public fun multiply_u128(val: u128, multiplier: fixed_point64::FixedPoint64): u128

public fun multiply_u128(val: u128, multiplier: FixedPoint64): u128 {
    // The product of two 128 bit values has 256 bits, so perform the
    // multiplication with u256 types and keep the full 256 bit product
    // to avoid losing accuracy.
    let unscaled_product = (val as u256) * (multiplier.value as u256);
    // The unscaled product has 64 fractional bits (from the multiplier)
    // so rescale it by shifting away the low bits.
    let product = unscaled_product >> 64;
    // Check whether the value is too large.
    assert!(product <= MAX_U128, EMULTIPLICATION);
    (product as u128)
}

Function divide_u128

Divide a u128 integer by a fixed-point number, truncating any fractional part of the quotient. This will abort if the divisor is zero or if the quotient overflows.

public fun divide_u128(val: u128, divisor: fixed_point64::FixedPoint64): u128

public fun divide_u128(val: u128, divisor: FixedPoint64): u128 {
    // Check for division by zero.
    assert!(divisor.value != 0, EDIVISION_BY_ZERO);
    // First convert to 256 bits and then shift left to
    // add 64 fractional zero bits to the dividend.
    let scaled_value = (val as u256) << 64;
    let quotient = scaled_value / (divisor.value as u256);
    // Check whether the value is too large.
    assert!(quotient <= MAX_U128, EDIVISION);
    // the value may be too large, which will cause the cast to fail
    // with an arithmetic error.
    (quotient as u128)
}

Function create_from_rational

Create a fixed-point value from a rational number specified by its numerator and denominator. Calling this function should be preferred for using Self::create_from_raw_value which is also available. This will abort if the denominator is zero. It will also abort if the numerator is nonzero and the ratio is not in the range 2^-64 .. 2^64-1. When specifying decimal fractions, be careful about rounding errors: if you round to display N digits after the decimal point, you can use a denominator of 10^N to avoid numbers where the very small imprecision in the binary representation could change the rounding, e.g., 0.0125 will round down to 0.012 instead of up to 0.013.

public fun create_from_rational(numerator: u128, denominator: u128): fixed_point64::FixedPoint64

public fun create_from_rational(numerator: u128, denominator: u128): FixedPoint64 {
    // If the denominator is zero, this will abort.
    // Scale the numerator to have 64 fractional bits, so that the quotient will have 64
    // fractional bits.
    let scaled_numerator = (numerator as u256) << 64;
    assert!(denominator != 0, EDENOMINATOR);
    let quotient = scaled_numerator / (denominator as u256);
    assert!(quotient != 0 || numerator == 0, ERATIO_OUT_OF_RANGE);
    // Return the quotient as a fixed-point number. We first need to check whether the cast
    // can succeed.
    assert!(quotient <= MAX_U128, ERATIO_OUT_OF_RANGE);
    FixedPoint64 { value: (quotient as u128) }
}

Function create_from_raw_value

Create a fixedpoint value from a raw value.

public fun create_from_raw_value(value: u128): fixed_point64::FixedPoint64

public fun create_from_raw_value(value: u128): FixedPoint64 {
    FixedPoint64 { value }
}

Function get_raw_value

Accessor for the raw u128 value. Other less common operations, such as adding or subtracting FixedPoint64 values, can be done using the raw values directly.

public fun get_raw_value(self: fixed_point64::FixedPoint64): u128

public fun get_raw_value(self: FixedPoint64): u128 {
    self.value
}

Function is_zero

Returns true if the ratio is zero.

public fun is_zero(self: fixed_point64::FixedPoint64): bool

public fun is_zero(self: FixedPoint64): bool {
    self.value == 0
}

Function min

Returns the smaller of the two FixedPoint64 numbers.

public fun min(num1: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

public fun min(num1: FixedPoint64, num2: FixedPoint64): FixedPoint64 {
    if (num1.value < num2.value) {
        num1
    } else {
        num2
    }
}

Function max

Returns the larger of the two FixedPoint64 numbers.

public fun max(num1: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

public fun max(num1: FixedPoint64, num2: FixedPoint64): FixedPoint64 {
    if (num1.value > num2.value) {
        num1
    } else {
        num2
    }
}

Function less_or_equal

Returns true if self <= num2

public fun less_or_equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

public fun less_or_equal(self: FixedPoint64, num2: FixedPoint64): bool {
    self.value <= num2.value
}

Function less

Returns true if self < num2

public fun less(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

public fun less(self: FixedPoint64, num2: FixedPoint64): bool {
    self.value < num2.value
}

Function greater_or_equal

Returns true if self >= num2

public fun greater_or_equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

public fun greater_or_equal(self: FixedPoint64, num2: FixedPoint64): bool {
    self.value >= num2.value
}

Function greater

Returns true if self > num2

public fun greater(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

public fun greater(self: FixedPoint64, num2: FixedPoint64): bool {
    self.value > num2.value
}

Function equal

Returns true if self = num2

public fun equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

public fun equal(self: FixedPoint64, num2: FixedPoint64): bool {
    self.value == num2.value
}

Function almost_equal

Returns true if self almost equals to num2, which means abs(num1-num2) <= precision

public fun almost_equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64, precision: fixed_point64::FixedPoint64): bool

public fun almost_equal(self: FixedPoint64, num2: FixedPoint64, precision: FixedPoint64): bool {
    if (self.value > num2.value) {
        (self.value - num2.value <= precision.value)
    } else {
        (num2.value - self.value <= precision.value)
    }
}

Function create_from_u128

Create a fixedpoint value from a u128 value.

public fun create_from_u128(val: u128): fixed_point64::FixedPoint64

public fun create_from_u128(val: u128): FixedPoint64 {
    let value = (val as u256) << 64;
    assert!(value <= MAX_U128, ERATIO_OUT_OF_RANGE);
    FixedPoint64 {value: (value as u128)}
}

Function floor

Returns the largest integer less than or equal to a given number.

public fun floor(self: fixed_point64::FixedPoint64): u128

public fun floor(self: FixedPoint64): u128 {
    self.value >> 64
}

Function ceil

Rounds up the given FixedPoint64 to the next largest integer.

public fun ceil(self: fixed_point64::FixedPoint64): u128

public fun ceil(self: FixedPoint64): u128 {
    let floored_num = self.floor() << 64;
    if (self.value == floored_num) {
        return floored_num >> 64
    };
    let val = ((floored_num as u256) + (1 << 64));
    (val >> 64 as u128)
}

Function round

Returns the value of a FixedPoint64 to the nearest integer.

public fun round(self: fixed_point64::FixedPoint64): u128

public fun round(self: FixedPoint64): u128 {
    let floored_num = self.floor() << 64;
    let boundary = floored_num + ((1 << 64) / 2);
    if (self.value < boundary) {
        floored_num >> 64
    } else {
        self.ceil()
    }
}

Specification

pragma aborts_if_is_strict;

Function sub

public fun sub(self: fixed_point64::FixedPoint64, y: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

pragma opaque;
aborts_if self.value < y.value with ENEGATIVE_RESULT;
ensures result.value == self.value - y.value;

Function add

public fun add(self: fixed_point64::FixedPoint64, y: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

pragma opaque;
aborts_if (self.value as u256) + (y.value as u256) > MAX_U128 with ERATIO_OUT_OF_RANGE;
ensures result.value == self.value + y.value;

Function multiply_u128

public fun multiply_u128(val: u128, multiplier: fixed_point64::FixedPoint64): u128

pragma opaque;
include MultiplyAbortsIf;
ensures result == spec_multiply_u128(val, multiplier);

schema MultiplyAbortsIf {
    val: num;
    multiplier: FixedPoint64;
    aborts_if spec_multiply_u128(val, multiplier) > MAX_U128 with EMULTIPLICATION;
}

fun spec_multiply_u128(val: num, multiplier: FixedPoint64): num {
   (val * multiplier.value) >> 64
}

Function divide_u128

public fun divide_u128(val: u128, divisor: fixed_point64::FixedPoint64): u128

pragma opaque;
include DivideAbortsIf;
ensures result == spec_divide_u128(val, divisor);

schema DivideAbortsIf {
    val: num;
    divisor: FixedPoint64;
    aborts_if divisor.value == 0 with EDIVISION_BY_ZERO;
    aborts_if spec_divide_u128(val, divisor) > MAX_U128 with EDIVISION;
}

fun spec_divide_u128(val: num, divisor: FixedPoint64): num {
   (val << 64) / divisor.value
}

Function create_from_rational

public fun create_from_rational(numerator: u128, denominator: u128): fixed_point64::FixedPoint64

pragma opaque;
include CreateFromRationalAbortsIf;
ensures result == spec_create_from_rational(numerator, denominator);

schema CreateFromRationalAbortsIf {
    numerator: u128;
    denominator: u128;
    let scaled_numerator = (numerator as u256)<< 64;
    let scaled_denominator = (denominator as u256);
    let quotient = scaled_numerator / scaled_denominator;
    aborts_if scaled_denominator == 0 with EDENOMINATOR;
    aborts_if quotient == 0 && scaled_numerator != 0 with ERATIO_OUT_OF_RANGE;
    aborts_if quotient > MAX_U128 with ERATIO_OUT_OF_RANGE;
}

fun spec_create_from_rational(numerator: num, denominator: num): FixedPoint64 {
   // Directly mirrors the body: (numerator as u256) << 64 / (denominator as u256).
   FixedPoint64{value: (numerator << 64) / denominator}
}

Function create_from_raw_value

public fun create_from_raw_value(value: u128): fixed_point64::FixedPoint64

pragma opaque;
aborts_if false;
ensures result.value == value;

Function min

public fun min(num1: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

pragma opaque;
aborts_if false;
ensures result == spec_min(num1, num2);

fun spec_min(num1: FixedPoint64, num2: FixedPoint64): FixedPoint64 {
   if (num1.value < num2.value) {
       num1
   } else {
       num2
   }
}

Function max

public fun max(num1: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): fixed_point64::FixedPoint64

pragma opaque;
aborts_if false;
ensures result == spec_max(num1, num2);

fun spec_max(num1: FixedPoint64, num2: FixedPoint64): FixedPoint64 {
   if (num1.value > num2.value) {
       num1
   } else {
       num2
   }
}

Function less_or_equal

public fun less_or_equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

pragma opaque;
aborts_if false;
ensures result == spec_less_or_equal(self, num2);

fun spec_less_or_equal(self: FixedPoint64, num2: FixedPoint64): bool {
   self.value <= num2.value
}

Function less

public fun less(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

pragma opaque;
aborts_if false;
ensures result == spec_less(self, num2);

fun spec_less(self: FixedPoint64, num2: FixedPoint64): bool {
   self.value < num2.value
}

Function greater_or_equal

public fun greater_or_equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

pragma opaque;
aborts_if false;
ensures result == spec_greater_or_equal(self, num2);

fun spec_greater_or_equal(self: FixedPoint64, num2: FixedPoint64): bool {
   self.value >= num2.value
}

Function greater

public fun greater(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

pragma opaque;
aborts_if false;
ensures result == spec_greater(self, num2);

fun spec_greater(self: FixedPoint64, num2: FixedPoint64): bool {
   self.value > num2.value
}

Function equal

public fun equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64): bool

pragma opaque;
aborts_if false;
ensures result == spec_equal(self, num2);

fun spec_equal(self: FixedPoint64, num2: FixedPoint64): bool {
   self.value == num2.value
}

Function almost_equal

public fun almost_equal(self: fixed_point64::FixedPoint64, num2: fixed_point64::FixedPoint64, precision: fixed_point64::FixedPoint64): bool

pragma opaque;
aborts_if false;
ensures result == spec_almost_equal(self, num2, precision);

fun spec_almost_equal(self: FixedPoint64, num2: FixedPoint64, precision: FixedPoint64): bool {
   if (self.value > num2.value) {
       (self.value - num2.value <= precision.value)
   } else {
       (num2.value - self.value <= precision.value)
   }
}

Function create_from_u128

public fun create_from_u128(val: u128): fixed_point64::FixedPoint64

pragma opaque;
include CreateFromU64AbortsIf;
ensures result == spec_create_from_u128(val);

schema CreateFromU64AbortsIf {
    val: num;
    let scaled_value = (val as u256) << 64;
    aborts_if scaled_value > MAX_U128;
}

fun spec_create_from_u128(val: num): FixedPoint64 {
   FixedPoint64 {value: val << 64}
}

Function floor

public fun floor(self: fixed_point64::FixedPoint64): u128

pragma opaque;
aborts_if false;
ensures result == spec_floor(self);

fun spec_floor(self: FixedPoint64): u128 {
   self.value >> 64
}

Function ceil

public fun ceil(self: fixed_point64::FixedPoint64): u128

pragma opaque;
aborts_if false;
ensures result == spec_ceil(self);

fun spec_ceil(self: FixedPoint64): u128 {
   if (self.value % (1 << 64) == 0) { self.value >> 64 }
   else { (self.value >> 64) + 1 }
}

Function round

public fun round(self: fixed_point64::FixedPoint64): u128

pragma opaque;
aborts_if false;
ensures result == spec_round(self);

fun spec_round(self: FixedPoint64): u128 {
   if (self.value % (1 << 64) < (1 << 64) / 2) { self.value >> 64 }
   else { (self.value >> 64) + 1 }
}