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

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

Struct FixedPoint32

Define a fixed-point numeric type with 32 fractional bits. This is just a u64 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 FixedPoint32 has copy, drop, store
Fields
value: u64

Constants 

const MAX_U64: u128 = 18446744073709551615;

The denominator provided was zero

const EDENOMINATOR: u64 = 65537;

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

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 u64

const EMULTIPLICATION: u64 = 131075;

The computed ratio when converting to a FixedPoint32 would be unrepresentable

const ERATIO_OUT_OF_RANGE: u64 = 131077;

Function multiply_u64

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

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

Function divide_u64

Divide a u64 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_u64(val: u64, divisor: fixed_point32::FixedPoint32): u64
Implementation 
public fun divide_u64(val: u64, divisor: FixedPoint32): u64 {
    // Check for division by zero.
    assert!(divisor.value != 0, EDIVISION_BY_ZERO);
    // First convert to 128 bits and then shift left to
    // add 32 fractional zero bits to the dividend.
    let scaled_value = (val as u128) << 32;
    let quotient = scaled_value / (divisor.value as u128);
    // Check whether the value is too large.
    assert!(quotient <= MAX_U64, EDIVISION);
    // the value may be too large, which will cause the cast to fail
    // with an arithmetic error.
    (quotient as u64)
}

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^-32 .. 2^32-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: u64, denominator: u64): fixed_point32::FixedPoint32
Implementation 
public fun create_from_rational(numerator: u64, denominator: u64): FixedPoint32 {
    // If the denominator is zero, this will abort.
    // Scale the numerator to have 64 fractional bits and the denominator
    // to have 32 fractional bits, so that the quotient will have 32
    // fractional bits.
    let scaled_numerator = (numerator as u128) << 64;
    let scaled_denominator = (denominator as u128) << 32;
    assert!(scaled_denominator != 0, EDENOMINATOR);
    let quotient = scaled_numerator / scaled_denominator;
    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_U64, ERATIO_OUT_OF_RANGE);
    FixedPoint32 { value: (quotient as u64) }
}

Function create_from_raw_value

Create a fixedpoint value from a raw value.

public fun create_from_raw_value(value: u64): fixed_point32::FixedPoint32
Implementation 
public fun create_from_raw_value(value: u64): FixedPoint32 {
    FixedPoint32 { value }
}

Function get_raw_value

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

public fun get_raw_value(self: fixed_point32::FixedPoint32): u64
Implementation 
public fun get_raw_value(self: FixedPoint32): u64 {
    self.value
}

Function is_zero

Returns true if the ratio is zero.

public fun is_zero(self: fixed_point32::FixedPoint32): bool
Implementation 
public fun is_zero(self: FixedPoint32): bool {
    self.value == 0
}

Function min

Returns the smaller of the two FixedPoint32 numbers.

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

Function max

Returns the larger of the two FixedPoint32 numbers.

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

Function create_from_u64

Create a fixedpoint value from a u64 value.

public fun create_from_u64(val: u64): fixed_point32::FixedPoint32
Implementation 
public fun create_from_u64(val: u64): FixedPoint32 {
    let value = (val as u128) << 32;
    assert!(value <= MAX_U64, ERATIO_OUT_OF_RANGE);
    FixedPoint32 {value: (value as u64)}
}

Function floor

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

public fun floor(self: fixed_point32::FixedPoint32): u64
Implementation 
public fun floor(self: FixedPoint32): u64 {
    self.value >> 32
}

Function ceil

Rounds up the given FixedPoint32 to the next largest integer.

public fun ceil(self: fixed_point32::FixedPoint32): u64
Implementation 
public fun ceil(self: FixedPoint32): u64 {
    let floored_num = self.floor() << 32;
    if (self.value == floored_num) {
        return floored_num >> 32
    };
    let val = ((floored_num as u128) + (1 << 32));
    (val >> 32 as u64)
}

Function round

Returns the value of a FixedPoint32 to the nearest integer.

public fun round(self: fixed_point32::FixedPoint32): u64
Implementation 
public fun round(self: FixedPoint32): u64 {
    let floored_num = self.floor() << 32;
    let boundary = floored_num + ((1 << 32) / 2);
    if (self.value < boundary) {
        floored_num >> 32
    } else {
        self.ceil()
    }
}

Specification 

pragma aborts_if_is_strict;

Function multiply_u64 

public fun multiply_u64(val: u64, multiplier: fixed_point32::FixedPoint32): u64

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


schema MultiplyAbortsIf {
    val: num;
    multiplier: FixedPoint32;
    aborts_if spec_multiply_u64(val, multiplier) > MAX_U64 with EMULTIPLICATION;
}


fun spec_multiply_u64(val: num, multiplier: FixedPoint32): num {
   (val * multiplier.value) >> 32
}

Function divide_u64 

public fun divide_u64(val: u64, divisor: fixed_point32::FixedPoint32): u64

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


schema DivideAbortsIf {
    val: num;
    divisor: FixedPoint32;
    aborts_if divisor.value == 0 with EDIVISION_BY_ZERO;
    aborts_if spec_divide_u64(val, divisor) > MAX_U64 with EDIVISION;
}


fun spec_divide_u64(val: num, divisor: FixedPoint32): num {
   (val << 32) / divisor.value
}

Function create_from_rational 

public fun create_from_rational(numerator: u64, denominator: u64): fixed_point32::FixedPoint32

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


schema CreateFromRationalAbortsIf {
    numerator: u64;
    denominator: u64;
    let scaled_numerator = (numerator as u128)<< 64;
    let scaled_denominator = (denominator as u128) << 32;
    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_U64 with ERATIO_OUT_OF_RANGE;
}


fun spec_create_from_rational(numerator: num, denominator: num): FixedPoint32 {
   FixedPoint32{value: (numerator << 64) / (denominator << 32)}
}

Function create_from_raw_value 

public fun create_from_raw_value(value: u64): fixed_point32::FixedPoint32

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

Function min 

public fun min(num1: fixed_point32::FixedPoint32, num2: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32

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


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

Function max 

public fun max(num1: fixed_point32::FixedPoint32, num2: fixed_point32::FixedPoint32): fixed_point32::FixedPoint32

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


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

Function create_from_u64 

public fun create_from_u64(val: u64): fixed_point32::FixedPoint32

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


schema CreateFromU64AbortsIf {
    val: num;
    let scaled_value = (val as u128) << 32;
    aborts_if scaled_value > MAX_U64;
}


fun spec_create_from_u64(val: num): FixedPoint32 {
   FixedPoint32 {value: val << 32}
}

Function floor 

public fun floor(self: fixed_point32::FixedPoint32): u64

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


fun spec_floor(self: FixedPoint32): u64 {
   // Right-shifting discards the lower 32 bits unconditionally;
   // the original conditional was redundant since both branches equal self.value >> 32.
   self.value >> 32
}

Function ceil 

public fun ceil(self: fixed_point32::FixedPoint32): u64

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


fun spec_ceil(self: FixedPoint32): u64 {
   // Expressed in terms of floor_val to avoid modulo: the else branch
   // (self.value - fractional + 2^32) >> 32 = floor_val + 1, and
   // fractional == 0 iff self.value == floor_val << 32.
   let floor_val = self.value >> 32;
   if (self.value == floor_val << 32) {
       floor_val
   } else {
       floor_val + 1
   }
}

Function round 

public fun round(self: fixed_point32::FixedPoint32): u64

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


fun spec_round(self: FixedPoint32): u64 {
   // Expressed in terms of floor_val to avoid modulo: both result branches
   // equal floor_val or floor_val + 1, and the boundary condition
   // fractional < 2^31 is equivalent to self.value < floor_val<<32 + 2^31.
   let floor_val = self.value >> 32;
   if (self.value < (floor_val << 32) + (1 << 31)) {
       floor_val
   } else {
       floor_val + 1
   }
}