pub open spec fn wrapping_sub(x: u64, y: u64) -> u64
{ if x - y < 0 { (x - y + 0x1_0000_0000_0000_0000) as u64 } else { (x - y) as u64 } }