pub proof fn signed_int_min_max_values()Expand description
ensures
(isize::MAX as nat) == pow2((isize::BITS - 1) as nat) - 1,abs(isize::MIN as int) == pow2((isize::BITS - 1) as nat),(isize::MAX as nat) * 2 == pow(256, size_of::<isize>()) - 2,abs(isize::MIN as int) * 2 == pow(256, size_of::<isize>()),(i8::MAX as nat) == pow2((i8::BITS - 1) as nat) - 1,abs(i8::MIN as int) == pow2((i8::BITS - 1) as nat),(i8::MAX as nat) * 2 == pow(256, size_of::<i8>()) - 2,abs(i8::MIN as int) * 2 == pow(256, size_of::<i8>()),(i16::MAX as nat) == pow2((i16::BITS - 1) as nat) - 1,abs(i16::MIN as int) == pow2((i16::BITS - 1) as nat),(i16::MAX as nat) * 2 == pow(256, size_of::<i16>()) - 2,abs(i16::MIN as int) * 2 == pow(256, size_of::<i16>()),(i32::MAX as nat) == pow2((i32::BITS - 1) as nat) - 1,abs(i32::MIN as int) == pow2((i32::BITS - 1) as nat),(i32::MAX as nat) * 2 == pow(256, size_of::<i32>()) - 2,abs(i32::MIN as int) * 2 == pow(256, size_of::<i32>()),(i64::MAX as nat) == pow2((i64::BITS - 1) as nat) - 1,abs(i64::MIN as int) == pow2((i64::BITS - 1) as nat),(i64::MAX as nat) * 2 == pow(256, size_of::<i64>()) - 2,abs(i64::MIN as int) * 2 == pow(256, size_of::<i64>()),(i128::MAX as nat) == pow2((i128::BITS - 1) as nat) - 1,abs(i128::MIN as int) == pow2((i128::BITS - 1) as nat),(i128::MAX as nat) * 2 == pow(256, size_of::<i128>()) - 2,abs(i128::MIN as int) * 2 == pow(256, size_of::<i128>()),Relates the signed integer min and max values to their sizes and bits.