fn hi_lo_to_u128(lo: u64, hi: u64) -> u128