value: 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, EMULTIPLICATION);
    (product as 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
}

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)
}

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
}

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) }
}

pragma opaque;
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 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)}
}

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

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

public fun get_raw_value(num: FixedPoint32): u64 {
    num.value
}

public fun is_zero(num: FixedPoint32): bool {
    num.value == 0
}