0x1::FixedPoint32The module provide operations for FixedPoint32.
FixedPoint32multiply_u64divide_u64create_from_rationalcreate_from_raw_valueget_raw_valueuse 0x1::Errors;
FixedPoint32Define 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.
struct FixedPoint32 has copy, drop, store
value: u64
const MAX_U64: u128 = 18446744073709551615;
The denominator provided was zero
const EDENOMINATOR: u64 = 101;
The quotient value would be too large to be held in a u64
const EDIVISION: u64 = 102;
A division by zero was encountered
const EDIVISION_BY_ZERO: u64 = 104;
The multiplied value would be too large to be held in a u64
const EMULTIPLICATION: u64 = 103;
The computed ratio when converting to a FixedPoint32 would be unrepresentable
const ERATIO_OUT_OF_RANGE: u64 = 105;
multiply_u64Multiply 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: FixedPoint32::FixedPoint32): u64
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, Errors::limit_exceeded(EMULTIPLICATION));
(product as u64)
}
FixedPoint32 is used for) is not relevant for the rest of the contract
control flow, so we can assume some arbitrary (but fixed) behavior here.
pragma opaque = true;
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 Errors::LIMIT_EXCEEDED;
}
fun spec_multiply_u64(val: num, multiplier: FixedPoint32): num {
(val * multiplier.value) >> 32
}
divide_u64Divide 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: FixedPoint32::FixedPoint32): u64
public fun divide_u64(val: u64, divisor: FixedPoint32): u64 {
// Check for division by zero.
assert!(divisor.value != 0, Errors::invalid_argument(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, Errors::limit_exceeded(EDIVISION));
// the value may be too large, which will cause the cast to fail
// with an arithmetic error.
(quotient as u64)
}
Self::multiply_64.
pragma opaque = true;
include DivideAbortsIf;
ensures result == spec_divide_u64(val, divisor);
schema DivideAbortsIf {
val: num;
divisor: FixedPoint32;
aborts_if divisor.value == 0 with Errors::INVALID_ARGUMENT;
aborts_if spec_divide_u64(val, divisor) > MAX_U64 with Errors::LIMIT_EXCEEDED;
}
fun spec_divide_u64(val: num, divisor: FixedPoint32): num {
(val << 32) / divisor.value
}
create_from_rationalCreate a fixed-point value from a rational number specified by its numerator and denominator. This function is for convenience; it is also perfectly fine to create a fixed-point value by directly specifying the raw value. This will abort if the denominator is zero or if the ratio is not in the range 2^-32 .. 2^32-1.
public fun create_from_rational(numerator: u64, denominator: u64): FixedPoint32::FixedPoint32
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, Errors::invalid_argument(EDENOMINATOR));
let quotient = scaled_numerator / scaled_denominator;
assert!(quotient != 0 || numerator == 0, Errors::invalid_argument(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, Errors::limit_exceeded(ERATIO_OUT_OF_RANGE));
FixedPoint32 { value: (quotient as u64) }
}
Self::multiply_64.
pragma verify = false;
pragma opaque = true;
include CreateFromRationalAbortsIf;
ensures result == spec_create_from_rational(numerator, denominator);
schema CreateFromRationalAbortsIf {
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 Errors::INVALID_ARGUMENT;
aborts_if quotient == 0 && scaled_numerator != 0 with Errors::INVALID_ARGUMENT;
aborts_if quotient > MAX_U64 with Errors::LIMIT_EXCEEDED;
}
fun spec_create_from_rational(numerator: num, denominator: num): FixedPoint32 {
FixedPoint32{value: (numerator << 64) / (denominator << 32)}
}
create_from_raw_valuecreate a fixedpoint 32 from u64.
public fun create_from_raw_value(value: u64): FixedPoint32::FixedPoint32
public fun create_from_raw_value(value: u64): FixedPoint32 {
FixedPoint32 { value }
}
pragma opaque;
aborts_if false;
ensures result.value == value;
get_raw_valueAccessor 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(num: FixedPoint32::FixedPoint32): u64
public fun get_raw_value(num: FixedPoint32): u64 {
num.value
}
pragma verify;
pragma aborts_if_is_strict;