Module `0x1::FixedPoint32`

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

Struct FixedPoint32
Constants
Function multiply_u64
- Abstract Semantics
Function divide_u64
- Abstract Semantics
Function create_from_rational
- Abstract Semantics
Function create_from_raw_value
Function get_raw_value
Function is_zero
Module Specification

<pre><code>use <a href="Errors.md#0x1_Errors">0x1::Errors</a>; </code></pre>

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.

<pre><code>struct <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> has copy, drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>value: u64</code> </dt> <dd> </dd> </dl> </details>

Constants

TODO: This is a basic constant and should be provided somewhere centrally in the framework.

<pre><code>const <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a>: u128 = 18446744073709551615; </code></pre>

The denominator provided was zero

<pre><code>const <a href="FixedPoint32.md#0x1_FixedPoint32_EDENOMINATOR">EDENOMINATOR</a>: u64 = 0; </code></pre>

The quotient value would be too large to be held in a <code>u64</code>

<pre><code>const <a href="FixedPoint32.md#0x1_FixedPoint32_EDIVISION">EDIVISION</a>: u64 = 1; </code></pre>

A division by zero was encountered

<pre><code>const <a href="FixedPoint32.md#0x1_FixedPoint32_EDIVISION_BY_ZERO">EDIVISION_BY_ZERO</a>: u64 = 3; </code></pre>

The multiplied value would be too large to be held in a <code>u64</code>

<pre><code>const <a href="FixedPoint32.md#0x1_FixedPoint32_EMULTIPLICATION">EMULTIPLICATION</a>: u64 = 2; </code></pre>

The computed ratio when converting to a <code><a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a></code> would be unrepresentable

<pre><code>const <a href="FixedPoint32.md#0x1_FixedPoint32_ERATIO_OUT_OF_RANGE">ERATIO_OUT_OF_RANGE</a>: u64 = 4; </code></pre>

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.

<pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_multiply_u64">multiply_u64</a>(val: u64, multiplier: <a href="FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_multiply_u64">multiply_u64</a>(val: u64, multiplier: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): 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 <= <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a>, <a href="Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="FixedPoint32.md#0x1_FixedPoint32_EMULTIPLICATION">EMULTIPLICATION</a>)); (product as u64) } </code></pre> </details> <details> <summary>Specification</summary>

Because none of our SMT solvers supports non-linear arithmetic with reliable efficiency, we specify the concrete semantics of the implementation but use an abstracted, simplified semantics for verification of callers. For the verification outcome of callers, the actual result of this function is not relevant, as long as the abstraction behaves homomorphic. This does not guarantee that arithmetic functions using this code is correct.

<pre><code>pragma opaque; include [concrete] <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteMultiplyAbortsIf">ConcreteMultiplyAbortsIf</a>; ensures [concrete] result == <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_multiply_u64">spec_concrete_multiply_u64</a>(val, multiplier); include [abstract] <a href="FixedPoint32.md#0x1_FixedPoint32_MultiplyAbortsIf">MultiplyAbortsIf</a>; ensures [abstract] result == <a href="FixedPoint32.md#0x1_FixedPoint32_spec_multiply_u64">spec_multiply_u64</a>(val, multiplier); </code></pre>

<pre><code>schema <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteMultiplyAbortsIf">ConcreteMultiplyAbortsIf</a> { val: num; multiplier: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>; aborts_if <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_multiply_u64">spec_concrete_multiply_u64</a>(val, multiplier) > <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> with <a href="Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>fun <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_multiply_u64">spec_concrete_multiply_u64</a>(val: num, multiplier: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): num { (val * multiplier.value) >> 32 } </code></pre>

Abstract Semantics

<pre><code>schema <a href="FixedPoint32.md#0x1_FixedPoint32_MultiplyAbortsIf">MultiplyAbortsIf</a> { val: num; multiplier: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>; aborts_if <a href="FixedPoint32.md#0x1_FixedPoint32_spec_multiply_u64">spec_multiply_u64</a>(val, multiplier) > <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> with <a href="Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>fun <a href="FixedPoint32.md#0x1_FixedPoint32_spec_multiply_u64">spec_multiply_u64</a>(val: num, multiplier: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): num { if (multiplier.value == 0) // Zero value 0 else if (multiplier.value == 1) // 1.0 val else if (multiplier.value == 2) // 0.5 val / 2 else // overflow <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> + 1 } </code></pre> </details>

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.

<pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_divide_u64">divide_u64</a>(val: u64, divisor: <a href="FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_divide_u64">divide_u64</a>(val: u64, divisor: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): u64 { // Check for division by zero. assert(divisor.value != 0, <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="FixedPoint32.md#0x1_FixedPoint32_EDIVISION_BY_ZERO">EDIVISION_BY_ZERO</a>)); // 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 <= <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a>, <a href="Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="FixedPoint32.md#0x1_FixedPoint32_EDIVISION">EDIVISION</a>)); // the value may be too large, which will cause the cast to fail // with an arithmetic error. (quotient as u64) } </code></pre> </details> <details> <summary>Specification</summary>

We specify the concrete semantics of the implementation but use an abstracted, simplified semantics for verification of callers.

<pre><code>pragma opaque; include [concrete] <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteDivideAbortsIf">ConcreteDivideAbortsIf</a>; ensures [concrete] result == <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_divide_u64">spec_concrete_divide_u64</a>(val, divisor); include [abstract] <a href="FixedPoint32.md#0x1_FixedPoint32_DivideAbortsIf">DivideAbortsIf</a>; ensures [abstract] result == <a href="FixedPoint32.md#0x1_FixedPoint32_spec_divide_u64">spec_divide_u64</a>(val, divisor); </code></pre>

<pre><code>schema <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteDivideAbortsIf">ConcreteDivideAbortsIf</a> { val: num; divisor: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>; aborts_if divisor.value == 0 with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_divide_u64">spec_concrete_divide_u64</a>(val, divisor) > <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> with <a href="Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>fun <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_divide_u64">spec_concrete_divide_u64</a>(val: num, divisor: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): num { (val << 32) / divisor.value } </code></pre>

Abstract Semantics

<pre><code>schema <a href="FixedPoint32.md#0x1_FixedPoint32_DivideAbortsIf">DivideAbortsIf</a> { val: num; divisor: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>; aborts_if divisor.value == 0 with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if <a href="FixedPoint32.md#0x1_FixedPoint32_spec_divide_u64">spec_divide_u64</a>(val, divisor) > <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> with <a href="Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>fun <a href="FixedPoint32.md#0x1_FixedPoint32_spec_divide_u64">spec_divide_u64</a>(val: num, divisor: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): num { if (divisor.value == 1) // 1.0 val else if (divisor.value == 2) // 0.5 val * 2 else <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> + 1 } </code></pre> </details>

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 <code><a href="FixedPoint32.md#0x1_FixedPoint32_create_from_raw_value">Self::create_from_raw_value</a></code> 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.

<pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_rational">create_from_rational</a>(numerator: u64, denominator: u64): <a href="FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_rational">create_from_rational</a>(numerator: u64, denominator: u64): <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { // 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, <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="FixedPoint32.md#0x1_FixedPoint32_EDENOMINATOR">EDENOMINATOR</a>)); let quotient = scaled_numerator / scaled_denominator; assert(quotient != 0 || numerator == 0, <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="FixedPoint32.md#0x1_FixedPoint32_ERATIO_OUT_OF_RANGE">ERATIO_OUT_OF_RANGE</a>)); // Return the quotient as a fixed-point number. We first need to check whether the cast // can succeed. assert(quotient <= <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a>, <a href="Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="FixedPoint32.md#0x1_FixedPoint32_ERATIO_OUT_OF_RANGE">ERATIO_OUT_OF_RANGE</a>)); <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { value: (quotient as u64) } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include [concrete] <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteCreateFromRationalAbortsIf">ConcreteCreateFromRationalAbortsIf</a>; ensures [concrete] result == <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_create_from_rational">spec_concrete_create_from_rational</a>(numerator, denominator); include [abstract] <a href="FixedPoint32.md#0x1_FixedPoint32_CreateFromRationalAbortsIf">CreateFromRationalAbortsIf</a>; ensures [abstract] result == <a href="FixedPoint32.md#0x1_FixedPoint32_spec_create_from_rational">spec_create_from_rational</a>(numerator, denominator); </code></pre>

<pre><code>schema <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteCreateFromRationalAbortsIf">ConcreteCreateFromRationalAbortsIf</a> { numerator: u64; denominator: u64; let scaled_numerator = numerator << 64; let scaled_denominator = denominator << 32; let quotient = scaled_numerator / scaled_denominator; aborts_if scaled_denominator == 0 with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if quotient == 0 && scaled_numerator != 0 with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if quotient > <a href="FixedPoint32.md#0x1_FixedPoint32_MAX_U64">MAX_U64</a> with <a href="Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>fun <a href="FixedPoint32.md#0x1_FixedPoint32_spec_concrete_create_from_rational">spec_concrete_create_from_rational</a>(numerator: num, denominator: num): <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>{value: (numerator << 64) / (denominator << 32)} } </code></pre>

Abstract Semantics

This is currently identical to the concrete semantics.

<pre><code>schema <a href="FixedPoint32.md#0x1_FixedPoint32_CreateFromRationalAbortsIf">CreateFromRationalAbortsIf</a> { include <a href="FixedPoint32.md#0x1_FixedPoint32_ConcreteCreateFromRationalAbortsIf">ConcreteCreateFromRationalAbortsIf</a>; } </code></pre>

Abstract to either 0.5 or 1. This assumes validation of numerator and denominator has succeeded.

<pre><code>fun <a href="FixedPoint32.md#0x1_FixedPoint32_spec_create_from_rational">spec_create_from_rational</a>(numerator: num, denominator: num): <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { if (numerator == denominator) // 1.0 <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>{value: 1} else // 0.5 <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>{value: 2} } </code></pre> </details>

Function `create_from_raw_value`

Create a fixedpoint value from a raw value.

<pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_raw_value">create_from_raw_value</a>(value: u64): <a href="FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_raw_value">create_from_raw_value</a>(value: u64): <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { value } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures [concrete] result.value == value; ensures [abstract] result.value == 2; </code></pre> </details>

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.

<pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_get_raw_value">get_raw_value</a>(num: <a href="FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_get_raw_value">get_raw_value</a>(num: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): u64 { num.value } </code></pre> </details>

Function `is_zero`

Returns true if the ratio is zero.

<pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_is_zero">is_zero</a>(num: <a href="FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="FixedPoint32.md#0x1_FixedPoint32_is_zero">is_zero</a>(num: <a href="FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>): bool { num.value == 0 } </code></pre> </details>

Module Specification

<pre><code>pragma aborts_if_is_strict; </code></pre>

Module `0x1::FixedPoint32`

Module 0x1::FixedPoint32

Struct FixedPoint32

Constants

Function multiply_u64

Abstract Semantics

Function divide_u64

Abstract Semantics

Function create_from_rational

Abstract Semantics

Function create_from_raw_value

Function get_raw_value

Function is_zero

Module Specification

Module `0x1::FixedPoint32`

Struct `FixedPoint32`

Function `multiply_u64`

Function `divide_u64`

Function `create_from_rational`

Function `create_from_raw_value`

Function `get_raw_value`

Function `is_zero`