Skip to content

Latest commit

 

History

History
946 lines (465 loc) · 25 KB

U256.md

File metadata and controls

946 lines (465 loc) · 25 KB

Module 0x1::U256

Implementation u256.

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
Specification 
invariant len(bits) == 4;


fun value_of_U256(a: U256): num {
   a.bits[0] +
   a.bits[1] * P64 +
   a.bits[2] * P64 * P64 +
   a.bits[3] * P64 * P64 * P64
}

Constants

const P32: u64 = 4294967296;


const P64: u128 = 18446744073709551616;


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 verify = false;
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)
}
Specification 
pragma verify = false;

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)
}
Specification 
pragma verify = 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 verify = false;
pragma opaque;
aborts_if value_of_U256(v) >= P64 * P64;
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
            }
        }
    };
    return 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 
aborts_if value_of_U256(a) + value_of_U256(b) >= P64 * P64 * P64 * P64;
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 
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 verify = false;
pragma timeout = 200;
aborts_if value_of_U256(a) * value_of_U256(b) >= P64 * P64 * P64 * P64;
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 verify = false;
pragma timeout = 160;
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 verify = false;
pragma timeout = 160;
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 verify = false;
pragma opaque;
pragma timeout = 600;
let p = pow_spec(value_of_U256(a), value_of_U256(b));
aborts_if p >= P64 * P64 * P64 * P64;
ensures value_of_U256(result) == p;

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);
Specification 
pragma opaque;
aborts_if value_of_U256(a) + value_of_U256(b) >= P64 * P64 * P64 * P64;
ensures value_of_U256(a) == value_of_U256(old(a)) + value_of_U256(b);

Function native_sub

fun native_sub(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_sub(a: &mut U256, b: &U256);
Specification 
pragma opaque;
aborts_if value_of_U256(a) - value_of_U256(b) < 0;
ensures value_of_U256(a) == value_of_U256(old(a)) - value_of_U256(b);

Function native_mul

fun native_mul(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_mul(a: &mut U256, b: &U256);
Specification 
pragma opaque;
aborts_if value_of_U256(a) * value_of_U256(b) >= P64 * P64 * P64 * P64;
ensures value_of_U256(a) == value_of_U256(old(a)) * value_of_U256(b);

Function native_div

fun native_div(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_div(a: &mut U256, b: &U256);
Specification 
pragma opaque;
aborts_if value_of_U256(b) == 0;
ensures value_of_U256(a) == value_of_U256(old(a)) / value_of_U256(b);

Function native_rem

fun native_rem(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_rem(a: &mut U256, b: &U256);
Specification 
pragma opaque;
aborts_if value_of_U256(b) == 0;
ensures value_of_U256(a) == value_of_U256(old(a)) % value_of_U256(b);

Function native_pow

fun native_pow(a: &mut U256::U256, b: &U256::U256)
Implementation 
native fun native_pow(a: &mut U256, b: &U256);
Specification 
pragma opaque;
aborts_if pow_spec(value_of_U256(a), value_of_U256(b)) >= P64 * P64 * P64 * P64;
ensures value_of_U256(a) == pow_spec(value_of_U256(old(a)), value_of_U256(b));


fun pow_spec(base: num, expon: num): num {
   // This actually doesn't follow a strict definition as 0^0 is undefined
   // mathematically. But the U256::pow of Rust is defined to be like this:
   // Link: https://docs.rs/uint/0.9.3/src/uint/uint.rs.html#1000-1003
   if (expon > 0) {
       let x = pow_spec(base, expon / 2);
       if (expon % 2 == 0) { x * x } else { x * x * base }
   } else {
       1
   }
}

Module Specification

pragma verify = true;