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