0x1::U256Implementation u256.
U256zeroonefrom_u64from_u128from_big_endianfrom_little_endianto_u128compareaddsubmuldivrempowadd_nocarrysub_noborrowfrom_bytesnative_addnative_subnative_mulnative_divnative_remnative_powuse 0x1::Arith;
use 0x1::Errors;
use 0x1::Vector;
U256use 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;
zeropublic fun zero(): U256::U256
onepublic fun one(): U256::U256
from_u64public fun from_u64(v: u64): U256::U256
from_u128public 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_endianpublic 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_endianpublic 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_u128public 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;
comparepublic 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
}
addpublic 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);
subpublic 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);
mulpublic 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);
divpublic 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);
rempublic 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);
powpublic 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_nocarrymove 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_noborrowmove 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_bytesfun from_bytes(data: &vector<u8>, be: bool): U256::U256
native fun from_bytes(data: &vector<u8>, be: bool): U256;
native_addfun native_add(a: &mut U256::U256, b: &U256::U256)
native fun native_add(a: &mut U256, b: &U256);
native_subfun native_sub(a: &mut U256::U256, b: &U256::U256)
native fun native_sub(a: &mut U256, b: &U256);
native_mulfun native_mul(a: &mut U256::U256, b: &U256::U256)
native fun native_mul(a: &mut U256, b: &U256);
native_divfun native_div(a: &mut U256::U256, b: &U256::U256)
native fun native_div(a: &mut U256, b: &U256);
native_remfun native_rem(a: &mut U256::U256, b: &U256::U256)
native fun native_rem(a: &mut U256, b: &U256);
native_powfun 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
)
}