pub open spec fn wrapping_add(x: u128, y: u128) -> u128
{ if x + y > <u128>::MAX { (x + y - 0x1_0000_0000_0000_0000_0000_0000_0000_0000) as u128 } else { (x + y) as u128 } }