pub proof fn unsigned_int_max_values()Expand description
ensures
(usize::MAX as nat) == pow2(usize::BITS as nat) - 1,(usize::MAX as nat) == pow(256, size_of::<usize>()) - 1,(u8::MAX as nat) == pow2(u8::BITS as nat) - 1,(u8::MAX as nat) == pow(256, size_of::<u8>()) - 1,(u16::MAX as nat) == pow2(u16::BITS as nat) - 1,(u16::MAX as nat) == pow(256, size_of::<u16>()) - 1,(u32::MAX as nat) == pow2(u32::BITS as nat) - 1,(u32::MAX as nat) == pow(256, size_of::<u32>()) - 1,(u64::MAX as nat) == pow2(u64::BITS as nat) - 1,(u64::MAX as nat) == pow(256, size_of::<u64>()) - 1,(u128::MAX as nat) == pow2(u128::BITS as nat) - 1,(u128::MAX as nat) == pow(256, size_of::<u128>()) - 1,Relates the unsigned integer max values to their sizes and bits.