From 6c09ba2531887cf511afb142049b3a687f4174e2 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Dec 2024 14:06:36 -0500 Subject: [PATCH 1/3] reduce carrying_mul to use intervals --- library/core/src/num/mod.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index cea05a55a7cda..7d8a7ed83776e 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2048,9 +2048,10 @@ mod verify { ); // ====================== u16 Harnesses ====================== - /// Kani proof harness for `carrying_mul` on `u16` type with full range of values. generate_carrying_mul_intervals!(u16, u32, - carrying_mul_u16_full_range, 0u16, u16::MAX + carrying_mul_u16_small, 0u16, 10u16, + carrying_mul_u16_large, u16::MAX - 10u16, u16::MAX, + carrying_mul_u16_mid_edge, (u16::MAX / 2) - 10u16, (u16::MAX / 2) + 10u16 ); // ====================== u32 Harnesses ====================== From b9ed73136056fa43b2b74daa5f405b989e1db8e7 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Dec 2024 12:25:59 -0500 Subject: [PATCH 2/3] change solver to kissat instead --- library/core/src/num/mod.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 7d8a7ed83776e..f9f290c51a58a 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1759,6 +1759,7 @@ mod verify { ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { $( #[kani::proof] + #[kani::solver(kissat)] pub fn $harness_name() { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); @@ -2049,9 +2050,7 @@ mod verify { // ====================== u16 Harnesses ====================== generate_carrying_mul_intervals!(u16, u32, - carrying_mul_u16_small, 0u16, 10u16, - carrying_mul_u16_large, u16::MAX - 10u16, u16::MAX, - carrying_mul_u16_mid_edge, (u16::MAX / 2) - 10u16, (u16::MAX / 2) + 10u16 + carrying_mul_u16_full_range, 0u16, u16::MAX ); // ====================== u32 Harnesses ====================== From 9958c7e5fd964a0a29593f913d81c1decffb8305 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Dec 2024 12:26:45 -0500 Subject: [PATCH 3/3] put comment back --- library/core/src/num/mod.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index f9f290c51a58a..a561eb3f9375b 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2049,6 +2049,7 @@ mod verify { ); // ====================== u16 Harnesses ====================== + /// Kani proof harness for `carrying_mul` on `u16` type with full range of values. generate_carrying_mul_intervals!(u16, u32, carrying_mul_u16_full_range, 0u16, u16::MAX );