From 4bf222374a46f9a7d102550cd12bb93c00a08690 Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Thu, 27 Aug 2026 17:00:15 -0700 Subject: [PATCH 1/2] Add proof harnesses for unchecked_disjoint_bitor on unsigned integer types --- library/core/src/num/mod.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 3e47debf38f8f..e3bf830e4cfb1 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2191,4 +2191,12 @@ mod verify { usize, checked_f128_to_int_unchecked_usize ); + + // `unchecked_disjoint_bitor` proofs + generate_unchecked_math_harness!(u8, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u8); + generate_unchecked_math_harness!(u16, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u16); + generate_unchecked_math_harness!(u32, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u32); + generate_unchecked_math_harness!(u64, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u64); + generate_unchecked_math_harness!(u128, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u128); + generate_unchecked_math_harness!(usize, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_usize); } From fdd4bb53f87c1c6c939b5954881c84e4f30c7324 Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Thu, 27 Aug 2026 17:00:15 -0700 Subject: [PATCH 2/2] Fix formatting per check_rustc.sh --- library/core/src/num/mod.rs | 36 ++++++++++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 6 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index e3bf830e4cfb1..a5ce315a94506 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2193,10 +2193,34 @@ mod verify { ); // `unchecked_disjoint_bitor` proofs - generate_unchecked_math_harness!(u8, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u8); - generate_unchecked_math_harness!(u16, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u16); - generate_unchecked_math_harness!(u32, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u32); - generate_unchecked_math_harness!(u64, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u64); - generate_unchecked_math_harness!(u128, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_u128); - generate_unchecked_math_harness!(usize, unchecked_disjoint_bitor, checked_unchecked_disjoint_bitor_usize); + generate_unchecked_math_harness!( + u8, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u8 + ); + generate_unchecked_math_harness!( + u16, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u16 + ); + generate_unchecked_math_harness!( + u32, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u32 + ); + generate_unchecked_math_harness!( + u64, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u64 + ); + generate_unchecked_math_harness!( + u128, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u128 + ); + generate_unchecked_math_harness!( + usize, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_usize + ); }