pub open spec fn wrapping_mul(x: u128, y: u128) -> u128
{ ((x as nat * y as nat) % 0x1_0000_0000_0000_0000_0000_0000_0000_0000 as nat) as u128 }