pub fn U128_from_U64(x: U64) -> U128