0x1::U256
Implementation u256.
U256
zero
one
from_u64
from_u128
from_big_endian
from_little_endian
to_u128
compare
add
sub
mul
div
rem
pow
add_nocarry
sub_noborrow
from_bytes
native_add
native_sub
native_mul
native_div
native_rem
native_pow
use 0x1::Arith;
use 0x1::Errors;
use 0x1::Vector;
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
bits: vector<u64>
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;
zero
public fun zero(): U256::U256
one
public fun one(): U256::U256
from_u64
public fun from_u64(v: u64): U256::U256
from_u128
public fun from_u128(v: u128): U256::U256
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
}
}
pragma opaque;
ensures value_of_U256(result) == v;
from_big_endian
public fun from_big_endian(data: vector<u8>): U256::U256
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)
}
from_little_endian
public fun from_little_endian(data: vector<u8>): U256::U256
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)
}
to_u128
public fun to_u128(v: &U256::U256): u128
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)
}
pragma opaque;
aborts_if value_of_U256(v) >= (1 << 128);
ensures value_of_U256(v) == result;
compare
public fun compare(a: &U256::U256, b: &U256::U256): u8
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
}
add
public fun add(a: U256::U256, b: U256::U256): U256::U256
public fun add(a: U256, b: U256): U256 {
native_add(&mut a, &b);
a
}
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);
sub
public fun sub(a: U256::U256, b: U256::U256): U256::U256
public fun sub(a: U256, b: U256): U256 {
native_sub(&mut a, &b);
a
}
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);
mul
public fun mul(a: U256::U256, b: U256::U256): U256::U256
public fun mul(a: U256, b: U256): U256 {
native_mul(&mut a, &b);
a
}
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);
div
public fun div(a: U256::U256, b: U256::U256): U256::U256
public fun div(a: U256, b: U256): U256 {
native_div(&mut a, &b);
a
}
pragma opaque;
aborts_if value_of_U256(b) == 0;
ensures value_of_U256(result) == value_of_U256(a) / value_of_U256(b);
rem
public fun rem(a: U256::U256, b: U256::U256): U256::U256
public fun rem(a: U256, b: U256): U256 {
native_rem(&mut a, &b);
a
}
pragma opaque;
aborts_if value_of_U256(b) == 0;
ensures value_of_U256(result) == value_of_U256(a) % value_of_U256(b);
pow
public fun pow(a: U256::U256, b: U256::U256): U256::U256
public fun pow(a: U256, b: U256): U256 {
native_pow(&mut a, &b);
a
}
pragma opaque;
add_nocarry
move implementation of native_add.
fun add_nocarry(a: &mut U256::U256, b: &U256::U256)
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);
}
sub_noborrow
move implementation of native_sub.
fun sub_noborrow(a: &mut U256::U256, b: &U256::U256)
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);
}
from_bytes
fun from_bytes(data: &vector<u8>, be: bool): U256::U256
native fun from_bytes(data: &vector<u8>, be: bool): U256;
native_add
fun native_add(a: &mut U256::U256, b: &U256::U256)
native fun native_add(a: &mut U256, b: &U256);
native_sub
fun native_sub(a: &mut U256::U256, b: &U256::U256)
native fun native_sub(a: &mut U256, b: &U256);
native_mul
fun native_mul(a: &mut U256::U256, b: &U256::U256)
native fun native_mul(a: &mut U256, b: &U256);
native_div
fun native_div(a: &mut U256::U256, b: &U256::U256)
native fun native_div(a: &mut U256, b: &U256);
native_rem
fun native_rem(a: &mut U256::U256, b: &U256::U256)
native fun native_rem(a: &mut U256, b: &U256);
native_pow
fun native_pow(a: &mut U256::U256, b: &U256::U256)
native fun native_pow(a: &mut U256, b: &U256);
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
)
}