Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

…hecked

library/core/src/num/mod.rs

@@ -1831,7 +1831,7 @@ mod verify {
         }
     }
 
-    // Part 3: Float to Integer Conversion function Harness Generation Macros
+    // Part 3: Float to Integer Conversion function Harness Generation Macro
     macro_rules! generate_to_int_unchecked_harness {
         ($floatType:ty, $($intType:ty, $harness_name:ident),+) => {
             $(
@@ -1845,7 +1845,7 @@ mod verify {
             )+
         }
     }
-/*
+
     // `unchecked_add` proofs
     //
     // Target types:
@@ -2141,8 +2141,51 @@ mod verify {
     generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32);
     generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
     generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
-    generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);*/
+    generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
 
+    // `f{16,32,64,128}::to_int_unchecked` proofs
+    //
+    // Target integer types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // 1. Float is not `NaN` and infinite
+    // 2. Float is representable in the return type `Int`, after truncating
+    //    off its fractional part
+    // [requires(self.is_finite() && kani::float::float_to_int_in_range::<Self, Int>(self))]
+    //
+    // Target function:
+    // pub unsafe fn to_int_unchecked<Int>(self) -> Int where Self: FloatToInt<Int>
+    generate_to_int_unchecked_harness!(f32,
+        i8, checked_f32_to_int_unchecked_i8,
+        i16, checked_f32_to_int_unchecked_i16,
+        i32, checked_f32_to_int_unchecked_i32,
+        i64, checked_f32_to_int_unchecked_i64,
+        i128, checked_f32_to_int_unchecked_i128,
+        isize, checked_f32_to_int_unchecked_isize,
+        u8, checked_f32_to_int_unchecked_u8,
+        u16, checked_f32_to_int_unchecked_u16,
+        u32, checked_f32_to_int_unchecked_u32,
+        u64, checked_f32_to_int_unchecked_u64,
+        u128, checked_f32_to_int_unchecked_u128,
+        usize, checked_f32_to_int_unchecked_usize
+    );
+
+    generate_to_int_unchecked_harness!(f64,
+        i8, checked_f64_to_int_unchecked_i8,
+        i16, checked_f64_to_int_unchecked_i16,
+        i32, checked_f64_to_int_unchecked_i32,
+        i64, checked_f64_to_int_unchecked_i64,
+        i128, checked_f64_to_int_unchecked_i128,
+        isize, checked_f64_to_int_unchecked_isize,
+        u8, checked_f64_to_int_unchecked_u8,
+        u16, checked_f64_to_int_unchecked_u16,
+        u32, checked_f64_to_int_unchecked_u32,
+        u64, checked_f64_to_int_unchecked_u64,
+        u128, checked_f64_to_int_unchecked_u128,
+        usize, checked_f64_to_int_unchecked_usize
+    );
+
     generate_to_int_unchecked_harness!(f16,
         i8, checked_f16_to_int_unchecked_i8,
         i16, checked_f16_to_int_unchecked_i16,
@@ -2157,7 +2200,7 @@ mod verify {
         u128, checked_f16_to_int_unchecked_u128,
         usize, checked_f16_to_int_unchecked_usize
     );
-
+  
     generate_to_int_unchecked_harness!(f128,
         i8, checked_f128_to_int_unchecked_i8,
         i16, checked_f128_to_int_unchecked_i16,