starcoin-framework

Module 0x1::SignedInteger64

Implementation of i64.

• Struct SignedInteger64
• Function multiply_u64
• Function divide_u64
• Function sub_u64
• Function add_u64
• Function create_from_raw_value
• Function get_value
• Function is_negative
• Module Specification

Struct SignedInteger64

Define a signed integer type with two 32 bits.

struct SignedInteger64 has copy, drop, store

Fields

value: u64

is_negative: bool

Function multiply_u64

Multiply a u64 integer by a signed integer number.

public fun multiply_u64(num: u64, multiplier: SignedInteger64::SignedInteger64): SignedInteger64::SignedInteger64

Implementation

public fun multiply_u64(num: u64, multiplier: SignedInteger64): SignedInteger64 {
    let product = multiplier.value * num;
    SignedInteger64 { value: (product as u64), is_negative: multiplier.is_negative }
}

Specification

aborts_if multiplier.value * num > max_u64();

Function divide_u64

Divide a u64 integer by a signed integer number.

public fun divide_u64(num: u64, divisor: SignedInteger64::SignedInteger64): SignedInteger64::SignedInteger64

Implementation

public fun divide_u64(num: u64, divisor: SignedInteger64): SignedInteger64 {
    let quotient = num / divisor.value;
    SignedInteger64 { value: (quotient as u64), is_negative: divisor.is_negative }
}

Specification

aborts_if divisor.value == 0;

Function sub_u64

Sub: num - minus

public fun sub_u64(num: u64, minus: SignedInteger64::SignedInteger64): SignedInteger64::SignedInteger64

Implementation

public fun sub_u64(num: u64, minus: SignedInteger64): SignedInteger64 {
    if (minus.is_negative) {
        let result = num + minus.value;
        SignedInteger64 { value: (result as u64), is_negative: false }
    } else {
        if (num > minus.value)  {
            let result = num - minus.value;
            SignedInteger64 { value: (result as u64), is_negative: false }
        }else {
            let result = minus.value - num;
            SignedInteger64 { value: (result as u64), is_negative: true }
        }
    }
}

Specification

aborts_if minus.is_negative && num + minus.value > max_u64();

Function add_u64

Add: num + addend

public fun add_u64(num: u64, addend: SignedInteger64::SignedInteger64): SignedInteger64::SignedInteger64

Implementation

public fun add_u64(num: u64, addend: SignedInteger64): SignedInteger64 {
    if (addend.is_negative) {
       if (num > addend.value)  {
           let result = num - addend.value;
           SignedInteger64 { value: (result as u64), is_negative: false }
       }else {
           let result = addend.value - num;
           SignedInteger64 { value: (result as u64), is_negative: true }
       }
    } else {
         let result = num + addend.value;
         SignedInteger64 { value: (result as u64), is_negative: false }
    }
}

Specification

aborts_if !addend.is_negative && num + addend.value > max_u64();

Function create_from_raw_value

Create a signed integer value from a unsigned integer

public fun create_from_raw_value(value: u64, is_negative: bool): SignedInteger64::SignedInteger64

Implementation

public fun create_from_raw_value(value: u64, is_negative: bool): SignedInteger64 {
    SignedInteger64 { value, is_negative }
}

Specification

aborts_if false;
ensures result == SignedInteger64 { value, is_negative };

Function get_value

Get value part of i64 ignore sign part.

public fun get_value(num: SignedInteger64::SignedInteger64): u64

Implementation

public fun get_value(num: SignedInteger64): u64 {
    num.value
}

Specification

aborts_if false;
ensures result == num.value;

Function is_negative

Check if the given num is negative.

public fun is_negative(num: SignedInteger64::SignedInteger64): bool

Implementation

public fun is_negative(num: SignedInteger64): bool {
    num.is_negative
}

Specification

aborts_if false;
ensures result == num.is_negative;

Module Specification

pragma verify;
pragma aborts_if_is_strict;

This site is open source. Improve this page.