Skip to content

Latest commit

 

History

History
860 lines (431 loc) · 21.7 KB

U256.md

File metadata and controls

860 lines (431 loc) · 21.7 KB
Raw

Module 0x1::U256

Implementation u256.

use 0x1::Arith;
use 0x1::Errors;
use 0x1::Vector;

Struct U256

use vector to represent data. so that we can use buildin vector ops later to construct U256. vector should always has two elements.

struct U256 has copy, drop, store
Fields
bits: vector<u64>
little endian representation

Constants

const EQUAL: u8 = 0;


const GREATER_THAN: u8 = 2;


const LESS_THAN: u8 = 1;


const ERR_INVALID_LENGTH: u64 = 100;


const ERR_OVERFLOW: u64 = 200;


const WORD: u8 = 4;

Function zero

public fun zero(): U256::U256
Implementation 
public fun zero(): U256 {
    from_u128(0u128)
}

Function one

public fun one(): U256::U256
Implementation 
public fun one(): U256 {
    from_u128(1u128)
}

Function from_u64

public fun from_u64(v: u64): U256::U256
Implementation 
public fun from_u64(v: u64): U256 {
    from_u128((v as u128))
}

Function from_u128

public fun from_u128(v: u128): U256::U256
Implementation 
public fun from_u128(v: u128): U256 {
    let low = ((v & 0xffffffffffffffff) as u64);
    let high = ((v >> 64) as u64);
    let bits = Vector::singleton(low);
    Vector::push_back(&mut bits, high);
    Vector::push_back(&mut bits, 0u64);
    Vector::push_back(&mut bits, 0u64);
    U256 {
        bits
    }
}
Specification 
pragma opaque;
ensures value_of_U256(result) == v;

Function from_big_endian

public fun from_big_endian(data: vector<u8>): U256::U256
Implementation 
public fun from_big_endian(data: vector<u8>): U256 {
    // TODO: define error code.
    assert!(Vector::length(&data) <= 32, Errors::invalid_argument(ERR_INVALID_LENGTH));
    from_bytes(&data, true)
}

Function from_little_endian

public fun from_little_endian(data: vector<u8>): U256::U256
Implementation 
public fun from_little_endian(data: vector<u8>): U256 {
    // TODO: define error code.
    assert!(Vector::length(&data) <= 32, Errors::invalid_argument(ERR_INVALID_LENGTH));
    from_bytes(&data, false)
}

Function to_u128

public fun to_u128(v: &U256::U256): u128
Implementation 
public fun to_u128(v: &U256): u128 {
    assert!(*Vector::borrow(&v.bits, 3) == 0, Errors::invalid_state(ERR_OVERFLOW));
    assert!(*Vector::borrow(&v.bits, 2) == 0, Errors::invalid_state(ERR_OVERFLOW));
    ((*Vector::borrow(&v.bits, 1) as u128) << 64) | (*Vector::borrow(&v.bits, 0) as u128)
}
Specification 
pragma opaque;
aborts_if value_of_U256(v) >= (1 << 128);
ensures value_of_U256(v) == result;

Function compare

public fun compare(a: &U256::U256, b: &U256::U256): u8
Implementation 
public fun compare(a: &U256, b: &U256): u8 {
    let i = (WORD as u64);
    while (i > 0) {
        i = i - 1;
        let a_bits = *Vector::borrow(&a.bits, i);
        let b_bits = *Vector::borrow(&b.bits, i);
        if (a_bits != b_bits) {
            if (a_bits < b_bits) {
                return LESS_THAN
            } else {
                return GREATER_THAN
            }
        }
    };
    EQUAL
}

Function add

public fun add(a: U256::U256, b: U256::U256): U256::U256
Implementation 
public fun add(a: U256, b: U256): U256 {
    native_add(&mut a, &b);
    a
}
Specification 
pragma opaque;
aborts_if value_of_U256(a) + value_of_U256(b) >= (1 << 256);
ensures value_of_U256(result) == value_of_U256(a) + value_of_U256(b);

Function sub

public fun sub(a: U256::U256, b: U256::U256): U256::U256
Implementation 
public fun sub(a: U256, b: U256): U256 {
    native_sub(&mut a, &b);
    a
}
Specification 
pragma opaque;
aborts_if value_of_U256(a) > value_of_U256(b);
ensures value_of_U256(result) == value_of_U256(a) - value_of_U256(b);

Function mul

public fun mul(a: U256::U256, b: U256::U256): U256::U256
Implementation 
public fun mul(a: U256, b: U256): U256 {
    native_mul(&mut a, &b);
    a
}
Specification 
pragma opaque;
aborts_if value_of_U256(a) * value_of_U256(b) >= (1 << 256);
ensures value_of_U256(result) == value_of_U256(a) * value_of_U256(b);

Function div

public fun div(a: U256::U256, b: U256::U256): U256::U256
Implementation 
public fun div(a: U256, b: U256): U256 {
    native_div(&mut a, &b);
    a
}
Specification 
pragma opaque;
aborts_if value_of_U256(b) == 0;
ensures value_of_U256(result) == value_of_U256(a) / value_of_U256(b);

Function rem

public fun rem(a: U256::U256, b: U256::U256): U256::U256
Implementation 
public fun rem(a: U256, b: U256): U256 {
    native_rem(&mut a, &b);
    a
}
Specification 
pragma opaque;
aborts_if value_of_U256(b) == 0;
ensures value_of_U256(result) == value_of_U256(a) % value_of_U256(b);

Function pow

public fun pow(a: U256::U256, b: U256::U256): U256::U256
Implementation 
public fun pow(a: U256, b: U256): U256 {
    native_pow(&mut a, &b);
    a
}
Specification 
pragma opaque;

Function add_nocarry

move implementation of native_add.

fun add_nocarry(a: &mut U256::U256, b: &U256::U256)
Implementation 
fun add_nocarry(a: &mut U256, b: &U256) {
    let carry = 0;
    let idx = 0;
    let len = (WORD as u64);
    while (idx < len) {
        let a_bit = Vector::borrow_mut(&mut a.bits, idx);
        let b_bit = Vector::borrow(&b.bits, idx);
        *a_bit = StarcoinFramework::Arith::adc(*a_bit, *b_bit, &mut carry);
        idx = idx + 1;
    };

    // check overflow
    assert!(carry == 0, 100);
}

Function sub_noborrow

move implementation of native_sub.

fun sub_noborrow(a: &mut U256::U256, b: &U256::U256)
Implementation 
fun sub_noborrow(a: &mut U256, b: &U256) {
    let borrow = 0;
    let idx = 0;
    let len =(WORD as u64);
    while (idx < len) {
        let a_bit = Vector::borrow_mut(&mut a.bits, idx);
        let b_bit = Vector::borrow(&b.bits, idx);
        *a_bit = StarcoinFramework::Arith::sbb(*a_bit, *b_bit, &mut borrow);
        idx = idx + 1;
    };

    // check overflow
    assert!(borrow == 0, 100);

}

Function from_bytes

fun from_bytes(data: &vector<u8>, be: bool): U256::U256
Implementation 
native fun from_bytes(data: &vector<u8>, be: bool): U256;

Function native_add

fun native_add(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_add(a: &mut U256, b: &U256);

Function native_sub

fun native_sub(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_sub(a: &mut U256, b: &U256);

Function native_mul

fun native_mul(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_mul(a: &mut U256, b: &U256);

Function native_div

fun native_div(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_div(a: &mut U256, b: &U256);

Function native_rem

fun native_rem(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_rem(a: &mut U256, b: &U256);

Function native_pow

fun native_pow(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_pow(a: &mut U256, b: &U256);

Module Specification

pragma verify = false;


fun value_of_U256(a: U256): num {
   ( a.bits[0]             // 0 * 64
     + a.bits[1] << 64     // 1 * 64
     + a.bits[2] << 128    // 2 * 64
     + a.bits[3] << 192    // 3 * 64
   )
}