From dffe30baa86decbbb6e92aeb568e1baa917d4e68 Mon Sep 17 00:00:00 2001 From: aaluna Date: Fri, 20 Sep 2024 14:38:41 -0400 Subject: [PATCH 01/34] Initial proof/contract/harness for nonzero: Added contract and placeholder harness --- library/core/src/num/nonzero.rs | 35 +++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 8b888f12da0b1..517b3d86746c1 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -8,6 +8,9 @@ use crate::ops::{BitOr, BitOrAssign, Div, DivAssign, Neg, Rem, RemAssign}; use crate::panic::{RefUnwindSafe, UnwindSafe}; use crate::str::FromStr; use crate::{fmt, intrinsics, ptr, ub_checks}; +use safety::{ensures, requires}; +#[cfg(kani)] +use crate::kani; /// A marker trait for primitive types which can be zero. /// @@ -348,6 +351,7 @@ where #[rustc_const_stable(feature = "const_nonzero_int_methods", since = "1.47.0")] #[must_use] #[inline] + pub const fn new(n: T) -> Option { // SAFETY: Memory layout optimization guarantees that `Option>` has // the same layout and size as `T`, with `0` representing `None`. @@ -364,6 +368,8 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] + #[requires(n != T::zero())] + #[ensures(|result: Self| result.get() == n)] pub const unsafe fn new_unchecked(n: T) -> Self { match Self::new(n) { Some(n) => n, @@ -381,6 +387,10 @@ where } } + + + + /// Converts a reference to a non-zero mutable reference /// if the referenced value is not zero. #[unstable(feature = "nonzero_from_mut", issue = "106290")] @@ -442,6 +452,9 @@ where } } + + + macro_rules! nonzero_integer { ( #[$stability:meta] @@ -2171,3 +2184,25 @@ nonzero_integer! { swapped = "0x5634129078563412", reversed = "0x6a2c48091e6a2c48", } + +#[unstable(feature="kani", issue="none")] +#[cfg(kani)] + mod verify { + use core::num::NonZeroI32; // Use core::num instead of std::num + use super::*; + use NonZero; + + +// pub const unsafe fn newunchecked(n: T) -> Self +#[kani::proof_for_contract(NonZero::new_unchecked)] +fn nonzero_check_new_unchecked() { + let x: i32 = kani::any(); // Generates a symbolic value of type i32 + + // Only proceed if x is not zero, because passing zero would violate the precondition + kani::assume(x != 0); + + unsafe { + let _ = NonZeroI32::new_unchecked(x); // Calls NonZero::new_unchecked + } + } +} From daf157631b2bd5493fcb3b34901af92a43a722df Mon Sep 17 00:00:00 2001 From: SahithiMV Date: Sun, 6 Oct 2024 21:47:51 +0000 Subject: [PATCH 02/34] Bytewise comparision (new_unchecked contract) --- library/core/src/num/nonzero.rs | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 517b3d86746c1..2eff437b9e717 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -368,8 +368,23 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] - #[requires(n != T::zero())] - #[ensures(|result: Self| result.get() == n)] + #[rustc_allow_const_fn_unstable(const_refs_to_cell)] + #[requires({ + let size = core::mem::size_of::(); + let ptr = &n as *const T as *const u8; + let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; + !slice.iter().all(|&byte| byte == 0) + })] + #[ensures(|result: &Self|{ + let size = core::mem::size_of::(); + let n_ptr: *const T = &n; + let result_inner: T = result.get(); + let result_ptr: *const T = &result_inner; + let n_slice = unsafe { core::slice::from_raw_parts(n_ptr as *const u8, size) }; + let result_slice = unsafe { core::slice::from_raw_parts(result_ptr as *const u8, size) }; + + n_slice == result_slice + })] pub const unsafe fn new_unchecked(n: T) -> Self { match Self::new(n) { Some(n) => n, From 21ae29ed22a257b6038cc8b088cc874c49b38adc Mon Sep 17 00:00:00 2001 From: aaluna Date: Tue, 8 Oct 2024 19:40:26 -0400 Subject: [PATCH 03/34] Removed kani assumes removed from proof_for_contract --- library/core/src/num/nonzero.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 2eff437b9e717..9774d500c719a 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2213,9 +2213,6 @@ nonzero_integer! { fn nonzero_check_new_unchecked() { let x: i32 = kani::any(); // Generates a symbolic value of type i32 - // Only proceed if x is not zero, because passing zero would violate the precondition - kani::assume(x != 0); - unsafe { let _ = NonZeroI32::new_unchecked(x); // Calls NonZero::new_unchecked } From 4241687f9f7230f1afa3d813d87aecf939572f0c Mon Sep 17 00:00:00 2001 From: SahithiMV Date: Sun, 13 Oct 2024 20:23:50 +0000 Subject: [PATCH 04/34] Macros for data types --- library/Cargo.lock | 86 +++++++++++++++++++++++++++++++++ library/core/Cargo.toml | 1 + library/core/src/num/nonzero.rs | 40 +++++++++++---- 3 files changed, 117 insertions(+), 10 deletions(-) diff --git a/library/Cargo.lock b/library/Cargo.lock index 54ad052c52322..695e3c4bcb306 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -72,6 +72,7 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", + "safety", ] [[package]] @@ -219,6 +220,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -236,6 +270,15 @@ dependencies = [ "core", ] +[[package]] +name = "quote" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "4.5.0" @@ -312,6 +355,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.79", +] + [[package]] name = "std" version = "0.0.0" @@ -353,6 +406,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -372,6 +446,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" + [[package]] name = "unicode-width" version = "0.1.13" @@ -405,6 +485,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index 9121227bc2615..ca54c5ecc7b91 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -26,6 +26,7 @@ test = true [dependencies] safety = {path = "../contracts/safety" } +paste = "1.0" [dev-dependencies] rand = { version = "0.8.5", default-features = false } diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 9774d500c719a..cac0810b5c9d0 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -11,6 +11,7 @@ use crate::{fmt, intrinsics, ptr, ub_checks}; use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +use paste::paste; /// A marker trait for primitive types which can be zero. /// @@ -2207,14 +2208,33 @@ nonzero_integer! { use super::*; use NonZero; - -// pub const unsafe fn newunchecked(n: T) -> Self -#[kani::proof_for_contract(NonZero::new_unchecked)] -fn nonzero_check_new_unchecked() { - let x: i32 = kani::any(); // Generates a symbolic value of type i32 - - unsafe { - let _ = NonZeroI32::new_unchecked(x); // Calls NonZero::new_unchecked - } + macro_rules! nonzero_check { + ($t:ty, $nonzero_type:ty) => { + paste! { + #[kani::proof_for_contract(NonZero::new_unchecked)] + pub fn []() { + let x: $t = kani::any(); // Generates a symbolic value of the provided type + + // Only proceed if x is not zero, because passing zero would violate the precondition + kani::assume(x != 0); + + unsafe { + let _ = <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type + } + } + } + }; } -} + + // Use the macro to generate different versions of the function for multiple types + nonzero_check!(i8, core::num::NonZeroI8); + nonzero_check!(i16, core::num::NonZeroI16); + nonzero_check!(i64, core::num::NonZeroI64); + nonzero_check!(i128, core::num::NonZeroI128); + nonzero_check!(u8, core::num::NonZeroU8); + nonzero_check!(u16, core::num::NonZeroU16); + nonzero_check!(u32, core::num::NonZeroU32); + nonzero_check!(u64, core::num::NonZeroU64); + nonzero_check!(u128, core::num::NonZeroU128); + nonzero_check!(usize, core::num::NonZeroUsize); +} \ No newline at end of file From 801f9a49f42ebe4b3edbf0356f6f883838d24611 Mon Sep 17 00:00:00 2001 From: SahithiMV Date: Sun, 13 Oct 2024 20:37:29 +0000 Subject: [PATCH 05/34] Adding i32 and isize --- library/core/src/num/nonzero.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index cac0810b5c9d0..9a8770cb4f2c8 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2229,6 +2229,7 @@ nonzero_integer! { // Use the macro to generate different versions of the function for multiple types nonzero_check!(i8, core::num::NonZeroI8); nonzero_check!(i16, core::num::NonZeroI16); + nonzero_check!(i32, core::num::NonZeroI32); nonzero_check!(i64, core::num::NonZeroI64); nonzero_check!(i128, core::num::NonZeroI128); nonzero_check!(u8, core::num::NonZeroU8); @@ -2237,4 +2238,5 @@ nonzero_integer! { nonzero_check!(u64, core::num::NonZeroU64); nonzero_check!(u128, core::num::NonZeroU128); nonzero_check!(usize, core::num::NonZeroUsize); + nonzero_check!(isize, core::num::NonZeroIsize); } \ No newline at end of file From eafef0b2b3d41e3e6c97ff1871e3215f8f20d905 Mon Sep 17 00:00:00 2001 From: aaluna Date: Sun, 20 Oct 2024 16:12:09 -0400 Subject: [PATCH 06/34] Pull Request fixes Corrected issues from Pull Request --- library/core/src/num/nonzero.rs | 49 +++++++++++++-------------------- 1 file changed, 19 insertions(+), 30 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 9a8770cb4f2c8..f8df437ae3fcc 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -11,8 +11,6 @@ use crate::{fmt, intrinsics, ptr, ub_checks}; use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; -use paste::paste; - /// A marker trait for primitive types which can be zero. /// /// This is an implementation detail for [NonZero]\ which may disappear or be replaced at any time. @@ -403,10 +401,6 @@ where } } - - - - /// Converts a reference to a non-zero mutable reference /// if the referenced value is not zero. #[unstable(feature = "nonzero_from_mut", issue = "106290")] @@ -2209,34 +2203,29 @@ nonzero_integer! { use NonZero; macro_rules! nonzero_check { - ($t:ty, $nonzero_type:ty) => { - paste! { - #[kani::proof_for_contract(NonZero::new_unchecked)] - pub fn []() { - let x: $t = kani::any(); // Generates a symbolic value of the provided type - - // Only proceed if x is not zero, because passing zero would violate the precondition - kani::assume(x != 0); - - unsafe { - let _ = <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type - } + ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { + #[kani::proof_for_contract(NonZero::new_unchecked)] + pub fn $nonzero_check_new_unchecked_for() { + let x: $t = kani::any(); // Generates a symbolic value of the provided type + + unsafe { + <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type } } }; } // Use the macro to generate different versions of the function for multiple types - nonzero_check!(i8, core::num::NonZeroI8); - nonzero_check!(i16, core::num::NonZeroI16); - nonzero_check!(i32, core::num::NonZeroI32); - nonzero_check!(i64, core::num::NonZeroI64); - nonzero_check!(i128, core::num::NonZeroI128); - nonzero_check!(u8, core::num::NonZeroU8); - nonzero_check!(u16, core::num::NonZeroU16); - nonzero_check!(u32, core::num::NonZeroU32); - nonzero_check!(u64, core::num::NonZeroU64); - nonzero_check!(u128, core::num::NonZeroU128); - nonzero_check!(usize, core::num::NonZeroUsize); - nonzero_check!(isize, core::num::NonZeroIsize); + nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); + nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); + nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32); + nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); + nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128); + nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize); + nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8); + nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16); + nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32); + nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); + nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); + nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); } \ No newline at end of file From 3015febb3d8112a63d4eb672d0967737b63fa2ba Mon Sep 17 00:00:00 2001 From: aaluna Date: Mon, 21 Oct 2024 15:34:43 -0400 Subject: [PATCH 07/34] Pull Request fixes Restored previous cargo files --- library/Cargo.lock | 86 ----------------------------------------- library/core/Cargo.toml | 1 - 2 files changed, 87 deletions(-) diff --git a/library/Cargo.lock b/library/Cargo.lock index 695e3c4bcb306..54ad052c52322 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -72,7 +72,6 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", - "safety", ] [[package]] @@ -220,39 +219,6 @@ dependencies = [ "unwind", ] -[[package]] -name = "proc-macro-error" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" -dependencies = [ - "proc-macro-error-attr", - "proc-macro2", - "quote", - "syn 1.0.109", - "version_check", -] - -[[package]] -name = "proc-macro-error-attr" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" -dependencies = [ - "proc-macro2", - "quote", - "version_check", -] - -[[package]] -name = "proc-macro2" -version = "1.0.86" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" -dependencies = [ - "unicode-ident", -] - [[package]] name = "proc_macro" version = "0.0.0" @@ -270,15 +236,6 @@ dependencies = [ "core", ] -[[package]] -name = "quote" -version = "1.0.37" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" -dependencies = [ - "proc-macro2", -] - [[package]] name = "r-efi" version = "4.5.0" @@ -355,16 +312,6 @@ dependencies = [ "std", ] -[[package]] -name = "safety" -version = "0.1.0" -dependencies = [ - "proc-macro-error", - "proc-macro2", - "quote", - "syn 2.0.79", -] - [[package]] name = "std" version = "0.0.0" @@ -406,27 +353,6 @@ dependencies = [ "rustc-std-workspace-core", ] -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "unicode-ident", -] - -[[package]] -name = "syn" -version = "2.0.79" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - [[package]] name = "sysroot" version = "0.0.0" @@ -446,12 +372,6 @@ dependencies = [ "std", ] -[[package]] -name = "unicode-ident" -version = "1.0.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" - [[package]] name = "unicode-width" version = "0.1.13" @@ -485,12 +405,6 @@ dependencies = [ "rustc-std-workspace-core", ] -[[package]] -name = "version_check" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index ca54c5ecc7b91..9121227bc2615 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -26,7 +26,6 @@ test = true [dependencies] safety = {path = "../contracts/safety" } -paste = "1.0" [dev-dependencies] rand = { version = "0.8.5", default-features = false } From ce918f8c01a5ed5bb808f78fe312a1c727120003 Mon Sep 17 00:00:00 2001 From: aaluna <166172412+MooniniteErr@users.noreply.github.com> Date: Sun, 27 Oct 2024 14:07:39 -0400 Subject: [PATCH 08/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index f8df437ae3fcc..47ab5a4847ec7 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -350,7 +350,6 @@ where #[rustc_const_stable(feature = "const_nonzero_int_methods", since = "1.47.0")] #[must_use] #[inline] - pub const fn new(n: T) -> Option { // SAFETY: Memory layout optimization guarantees that `Option>` has // the same layout and size as `T`, with `0` representing `None`. From 2304fadd45688c77a556fcc9db52264e3f66a37b Mon Sep 17 00:00:00 2001 From: aaluna <166172412+MooniniteErr@users.noreply.github.com> Date: Sun, 27 Oct 2024 14:12:13 -0400 Subject: [PATCH 09/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 47ab5a4847ec7..77eb453489749 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -461,9 +461,6 @@ where } } - - - macro_rules! nonzero_integer { ( #[$stability:meta] From 14a50e2357878ea2ce1e45db06715b5bc2f5ee57 Mon Sep 17 00:00:00 2001 From: aa-luna Date: Sun, 27 Oct 2024 14:13:31 -0400 Subject: [PATCH 10/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 77eb453489749..eeaf8dc86ea39 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2194,9 +2194,7 @@ nonzero_integer! { #[unstable(feature="kani", issue="none")] #[cfg(kani)] mod verify { - use core::num::NonZeroI32; // Use core::num instead of std::num - use super::*; - use NonZero; + use super::*; macro_rules! nonzero_check { ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { From acef65adac0658bbe404f82f89003bea43211d7b Mon Sep 17 00:00:00 2001 From: aa-luna Date: Sun, 27 Oct 2024 14:13:39 -0400 Subject: [PATCH 11/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index eeaf8dc86ea39..a9facd0c62997 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2222,4 +2222,4 @@ nonzero_integer! { nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); -} \ No newline at end of file +} From 4d3efd16f6e03a3dbeeba497ebf6b6c843dc5168 Mon Sep 17 00:00:00 2001 From: aa-luna Date: Sun, 27 Oct 2024 14:15:07 -0400 Subject: [PATCH 12/34] Update library/core/src/num/nonzero.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index a9facd0c62997..28bc0e0752b72 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2193,7 +2193,7 @@ nonzero_integer! { #[unstable(feature="kani", issue="none")] #[cfg(kani)] - mod verify { +mod verify { use super::*; macro_rules! nonzero_check { From 7bc64eb68b36682d3e1e7dd4821a23a5a7a1ee50 Mon Sep 17 00:00:00 2001 From: aaluna Date: Sun, 3 Nov 2024 11:46:41 -0500 Subject: [PATCH 13/34] doc: add explanations for const function attribute --- library/core/src/num/nonzero.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 28bc0e0752b72..97964e8c86973 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -366,6 +366,10 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] + // #[rustc_allow_const_fn_unstable(const_refs_to_cell)] enables byte-level + // comparisons within const functions. This is needed here to validate the + // contents of `T` by converting a pointer to a `u8` slice for our `requires` + // and `ensures` checks. #[rustc_allow_const_fn_unstable(const_refs_to_cell)] #[requires({ let size = core::mem::size_of::(); From d67be7e4f2b52098c06e24e786b80eb76e4ebe68 Mon Sep 17 00:00:00 2001 From: Sahithi Maddula Date: Sun, 24 Nov 2024 22:48:24 +0000 Subject: [PATCH 14/34] Unchecked Add and Mul: Init --- library/core/src/num/nonzero.rs | 44 ++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 162c599b3468f..4371c3cc783ce 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -1009,6 +1009,15 @@ macro_rules! nonzero_integer { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[requires({ + let (result, overflow) = self.get().overflowing_mul(other.get()); + !overflow // Precondition to ensure no overflow occurs during multiplication + })] + #[ensures(|result: &Self| { + // Ensure the resulting value is the expected product + let (expected_result, _) = self.get().overflowing_mul(other.get()); + result.get() == expected_result + })] pub const unsafe fn unchecked_mul(self, other: Self) -> Self { // SAFETY: The caller ensures there is no overflow. unsafe { Self::new_unchecked(self.get().unchecked_mul(other.get())) } @@ -1371,6 +1380,15 @@ macro_rules! nonzero_integer_signedness_dependent_methods { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[requires({ + let (result, overflow) = self.get().overflowing_add(other); + !overflow // Precondition: no overflow can occur + })] + #[ensures(|result: &Self| { + // Postcondition: the result matches the expected addition + let (expected_result, _) = self.get().overflowing_add(other); + result.get() == expected_result + })] pub const unsafe fn unchecked_add(self, other: $Int) -> Self { // SAFETY: The caller ensures there is no overflow. unsafe { Self::new_unchecked(self.get().unchecked_add(other)) } @@ -2214,4 +2232,28 @@ mod verify { nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); -} + + #[kani::proof_for_contract(i8::unchecked_mul)] + fn nonzero_unchecked_mul() { + let x: NonZeroI8 = kani::any(); + let y: NonZeroI8 = kani::any(); + + // Check the precondition to assume no overflow + let (result, overflow) = x.get().overflowing_mul(y.get()); + kani::assume(!overflow); // Ensure the multiplication does not overflow + + unsafe { + let _ = x.unchecked_mul(y); + } + } + + #[kani::proof_for_contract(i8::unchecked_add)] + fn nonzero_unchecked_add() { + let x: i8 = kani::any(); + let y: i8 = kani::any(); + unsafe { + let _ = x.unchecked_add(y); // Call the unchecked function + } + } + +} \ No newline at end of file From 36e75beb300808305508d47210ff0c1178e4d2a7 Mon Sep 17 00:00:00 2001 From: Sahithi Maddula Date: Tue, 26 Nov 2024 20:10:35 +0000 Subject: [PATCH 15/34] Unchecked Mul and Add: Adding Macros & cleanup --- library/core/src/num/nonzero.rs | 85 +++++++++++++++++++++------------ 1 file changed, 55 insertions(+), 30 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 4371c3cc783ce..b74d10f5ab737 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -1010,13 +1010,10 @@ macro_rules! nonzero_integer { without modifying the original"] #[inline] #[requires({ - let (result, overflow) = self.get().overflowing_mul(other.get()); - !overflow // Precondition to ensure no overflow occurs during multiplication + !self.get().checked_mul(other.get()).is_some() })] #[ensures(|result: &Self| { - // Ensure the resulting value is the expected product - let (expected_result, _) = self.get().overflowing_mul(other.get()); - result.get() == expected_result + self.get().checked_mul(other.get()).unwrap() == result.get() })] pub const unsafe fn unchecked_mul(self, other: Self) -> Self { // SAFETY: The caller ensures there is no overflow. @@ -1381,13 +1378,11 @@ macro_rules! nonzero_integer_signedness_dependent_methods { without modifying the original"] #[inline] #[requires({ - let (result, overflow) = self.get().overflowing_add(other); - !overflow // Precondition: no overflow can occur + !self.get().checked_add(other).is_some() })] #[ensures(|result: &Self| { // Postcondition: the result matches the expected addition - let (expected_result, _) = self.get().overflowing_add(other); - result.get() == expected_result + self.get().checked_add(other).unwrap() == result.get() })] pub const unsafe fn unchecked_add(self, other: $Int) -> Self { // SAFETY: The caller ensures there is no overflow. @@ -2233,27 +2228,57 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); - #[kani::proof_for_contract(i8::unchecked_mul)] - fn nonzero_unchecked_mul() { - let x: NonZeroI8 = kani::any(); - let y: NonZeroI8 = kani::any(); - - // Check the precondition to assume no overflow - let (result, overflow) = x.get().overflowing_mul(y.get()); - kani::assume(!overflow); // Ensure the multiplication does not overflow - - unsafe { - let _ = x.unchecked_mul(y); - } + macro_rules! nonzero_check_mul { + ($t:ty, $nonzero_type:ty, $nonzero_unchecked_mul:ident) => { + #[kani::proof_for_contract(NonZero::unchecked_mul)] + pub fn $nonzero_unchecked_mul_for() { + let x: NonZeroI8 = kani::any(); + let y: NonZeroI8 = kani::any(); + unsafe { + let _ = x.unchecked_mul(y); + } + } + }; } - - #[kani::proof_for_contract(i8::unchecked_add)] - fn nonzero_unchecked_add() { - let x: i8 = kani::any(); - let y: i8 = kani::any(); - unsafe { - let _ = x.unchecked_add(y); // Call the unchecked function - } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check!(i8, core::num::NonZeroI8, nonzero_unchecked_mul_for_i8); + nonzero_check!(i16, core::num::NonZeroI16, nonzero_unchecked_mul_for_16); + nonzero_check!(i32, core::num::NonZeroI32, nonzero_unchecked_mul_for_32); + nonzero_check!(i64, core::num::NonZeroI64, nonzero_unchecked_mul_for_64); + nonzero_check!(i128, core::num::NonZeroI128, nonzero_unchecked_mul_for_128); + nonzero_check!(isize, core::num::NonZeroIsize, nonzero_unchecked_mul_for_isize); + nonzero_check!(u8, core::num::NonZeroU8, nonzero_unchecked_mul_for_u8); + nonzero_check!(u16, core::num::NonZeroU16, nonzero_unchecked_mul_for_u16); + nonzero_check!(u32, core::num::NonZeroU32, nonzero_unchecked_mul_for_u32); + nonzero_check!(u64, core::num::NonZeroU64, nonzero_unchecked_mul_for_u64); + nonzero_check!(u128, core::num::NonZeroU128, nonzero_unchecked_mul_for_u128); + nonzero_check!(usize, core::num::NonZeroUsize, nonzero_unchecked_mul_for_usize); + + macro_rules! nonzero_check_add { + ($t:ty, $nonzero_type:ty, $nonzero_unchecked_add:ident) => { + #[kani::proof_for_contract(NonZero::unchecked_add)] + pub fn $nonzero_unchecked_add_for() { + let x: i8 = kani::any(); + let y: i8 = kani::any(); + unsafe { + let _ = x.unchecked_add(y); // Call the unchecked function + } + } + }; } - + + // Use the macro to generate different versions of the function for multiple types + nonzero_check!(i8, core::num::NonZeroI8, nonzero_unchecked_add_for_i8); + nonzero_check!(i16, core::num::NonZeroI16, nonzero_unchecked_add_for_16); + nonzero_check!(i32, core::num::NonZeroI32, nonzero_unchecked_add_for_32); + nonzero_check!(i64, core::num::NonZeroI64, nonzero_unchecked_add_for_64); + nonzero_check!(i128, core::num::NonZeroI128, nonzero_unchecked_add_for_128); + nonzero_check!(isize, core::num::NonZeroIsize, nonzero_unchecked_add_for_isize); + nonzero_check!(u8, core::num::NonZeroU8, nonzero_unchecked_add_for_u8); + nonzero_check!(u16, core::num::NonZeroU16, nonzero_unchecked_add_for_u16); + nonzero_check!(u32, core::num::NonZeroU32, nonzero_unchecked_add_for_u32); + nonzero_check!(u64, core::num::NonZeroU64, nonzero_unchecked_add_for_u64); + nonzero_check!(u128, core::num::NonZeroU128, nonzero_unchecked_add_for_u128); + nonzero_check!(usize, core::num::NonZeroUsize, nonzero_unchecked_add_for_usize); } \ No newline at end of file From 4f945c8039470c7b5e955a40fe921430010dfdf4 Mon Sep 17 00:00:00 2001 From: Sahithi Maddula Date: Mon, 9 Dec 2024 15:30:14 +0000 Subject: [PATCH 16/34] Fixes --- library/core/src/num/nonzero.rs | 178 ++++++++++++++++++++++++-------- 1 file changed, 136 insertions(+), 42 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index b74d10f5ab737..b8f6224afc9ca 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -1010,7 +1010,7 @@ macro_rules! nonzero_integer { without modifying the original"] #[inline] #[requires({ - !self.get().checked_mul(other.get()).is_some() + self.get().checked_mul(other.get()).is_some() })] #[ensures(|result: &Self| { self.get().checked_mul(other.get()).unwrap() == result.get() @@ -1378,7 +1378,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods { without modifying the original"] #[inline] #[requires({ - !self.get().checked_add(other).is_some() + self.get().checked_add(other).is_some() })] #[ensures(|result: &Self| { // Postcondition: the result matches the expected addition @@ -2228,57 +2228,151 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); - macro_rules! nonzero_check_mul { - ($t:ty, $nonzero_type:ty, $nonzero_unchecked_mul:ident) => { - #[kani::proof_for_contract(NonZero::unchecked_mul)] - pub fn $nonzero_unchecked_mul_for() { - let x: NonZeroI8 = kani::any(); - let y: NonZeroI8 = kani::any(); + + macro_rules! nonzero_check_from_mut_unchecked { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let mut x: $t = kani::any(); + kani::assume(x != 0); unsafe { - let _ = x.unchecked_mul(y); + <$nonzero_type>::from_mut_unchecked(&mut x); } } }; } - // Use the macro to generate different versions of the function for multiple types - nonzero_check!(i8, core::num::NonZeroI8, nonzero_unchecked_mul_for_i8); - nonzero_check!(i16, core::num::NonZeroI16, nonzero_unchecked_mul_for_16); - nonzero_check!(i32, core::num::NonZeroI32, nonzero_unchecked_mul_for_32); - nonzero_check!(i64, core::num::NonZeroI64, nonzero_unchecked_mul_for_64); - nonzero_check!(i128, core::num::NonZeroI128, nonzero_unchecked_mul_for_128); - nonzero_check!(isize, core::num::NonZeroIsize, nonzero_unchecked_mul_for_isize); - nonzero_check!(u8, core::num::NonZeroU8, nonzero_unchecked_mul_for_u8); - nonzero_check!(u16, core::num::NonZeroU16, nonzero_unchecked_mul_for_u16); - nonzero_check!(u32, core::num::NonZeroU32, nonzero_unchecked_mul_for_u32); - nonzero_check!(u64, core::num::NonZeroU64, nonzero_unchecked_mul_for_u64); - nonzero_check!(u128, core::num::NonZeroU128, nonzero_unchecked_mul_for_u128); - nonzero_check!(usize, core::num::NonZeroUsize, nonzero_unchecked_mul_for_usize); + // Generate harnesses for multiple types + nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); + nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); + nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); + nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); + nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); + nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); + nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); + nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); + nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); + nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); + nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); + nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); + + + + macro_rules! check_mul_unchecked_small{ + ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident) => { + #[kani::proof_for_contract(<$t>::unchecked_mul)] + pub fn $nonzero_check_mul_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + + unsafe { + x.unchecked_mul(y); + } + } + }; + } + + macro_rules! check_mul_unchecked_intervals{ + ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { + #[kani::proof_for_contract(<$t>::unchecked_mul)] + pub fn $nonzero_check_mul_for() { + let x = kani::any::<$t>(); + let y = kani::any::<$t>(); + + kani::assume(x != 0 && x >= $min && x <= $max); + kani::assume(y != 0 && y >= $min && y <= $max); + + let x = <$nonzero_type>::new(x).unwrap(); + let y = <$nonzero_type>::new(y).unwrap(); + + unsafe { + x.unchecked_mul(y); + } + } + }; + } + + //Calls for i32 + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_small, NonZeroI32::new(-10i32).unwrap().into(), NonZeroI32::new(10i32).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_pos, NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_neg, NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_pos, NonZeroI32::new(i32::MAX / 2).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_neg, NonZeroI32::new(i32::MIN / 2).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); + + //Calls for i64 + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_small, NonZeroI64::new(-10i64).unwrap().into(), NonZeroI64::new(10i64).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_pos, NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_neg, NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_pos, NonZeroI64::new(i64::MAX / 2).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_neg, NonZeroI64::new(i64::MIN / 2).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); + + //calls for i128 + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_small, NonZeroI128::new(-10i128).unwrap().into(), NonZeroI128::new(10i128).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_pos, NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_neg, NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_pos, NonZeroI128::new(i128::MAX / 2).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_neg, NonZeroI128::new(i128::MIN / 2).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); + + //calls for isize + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_small, NonZeroIsize::new(-10isize).unwrap().into(), NonZeroIsize::new(10isize).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_pos, NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_neg, NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_pos, NonZeroIsize::new(isize::MAX / 2).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_neg, NonZeroIsize::new(isize::MIN / 2).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); + + //calls for u32 + check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_small, NonZeroU32::new(1u32).unwrap().into(), NonZeroU32::new(10u32).unwrap().into()); + check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_large, NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); + check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_edge, NonZeroU32::new(u32::MAX / 2).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); + + //calls for u64 + check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_small, NonZeroU64::new(1u64).unwrap().into(), NonZeroU64::new(10u64).unwrap().into()); + check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_large, NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); + check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_edge, NonZeroU64::new(u64::MAX / 2).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); + + //calls for u128 + check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_small, NonZeroU128::new(1u128).unwrap().into(), NonZeroU128::new(10u128).unwrap().into()); + check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_large, NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); + check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_edge, NonZeroU128::new(u128::MAX / 2).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); + + //calls for usize + check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_small, NonZeroUsize::new(1usize).unwrap().into(), NonZeroUsize::new(10usize).unwrap().into()); + check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_large, NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); + check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_edge, NonZeroUsize::new(usize::MAX / 2).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); + + //calls for i8, i16, u8, u16 + check_mul_unchecked_small!(i8, NonZeroI8, nonzero_check_mul_for_i8); + check_mul_unchecked_small!(i16, NonZeroI16, nonzero_check_mul_for_i16); + check_mul_unchecked_small!(u8, NonZeroU8, nonzero_check_mul_for_u8); + check_mul_unchecked_small!(u16, NonZeroU16, nonzero_check_mul_for_u16); + + //check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16); macro_rules! nonzero_check_add { - ($t:ty, $nonzero_type:ty, $nonzero_unchecked_add:ident) => { - #[kani::proof_for_contract(NonZero::unchecked_add)] - pub fn $nonzero_unchecked_add_for() { - let x: i8 = kani::any(); - let y: i8 = kani::any(); + ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { + #[kani::proof_for_contract(<$t>::unchecked_add)] + pub fn $nonzero_check_unchecked_add_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + unsafe { - let _ = x.unchecked_add(y); // Call the unchecked function + x.get().unchecked_add(y.get()); } } }; } - // Use the macro to generate different versions of the function for multiple types - nonzero_check!(i8, core::num::NonZeroI8, nonzero_unchecked_add_for_i8); - nonzero_check!(i16, core::num::NonZeroI16, nonzero_unchecked_add_for_16); - nonzero_check!(i32, core::num::NonZeroI32, nonzero_unchecked_add_for_32); - nonzero_check!(i64, core::num::NonZeroI64, nonzero_unchecked_add_for_64); - nonzero_check!(i128, core::num::NonZeroI128, nonzero_unchecked_add_for_128); - nonzero_check!(isize, core::num::NonZeroIsize, nonzero_unchecked_add_for_isize); - nonzero_check!(u8, core::num::NonZeroU8, nonzero_unchecked_add_for_u8); - nonzero_check!(u16, core::num::NonZeroU16, nonzero_unchecked_add_for_u16); - nonzero_check!(u32, core::num::NonZeroU32, nonzero_unchecked_add_for_u32); - nonzero_check!(u64, core::num::NonZeroU64, nonzero_unchecked_add_for_u64); - nonzero_check!(u128, core::num::NonZeroU128, nonzero_unchecked_add_for_u128); - nonzero_check!(usize, core::num::NonZeroUsize, nonzero_unchecked_add_for_usize); -} \ No newline at end of file + // Generate proofs for all NonZero types + nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); + nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); + nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); + nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); + nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); + nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); + nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); + nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); + nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); + nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); + nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); + nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); +} From 71e57fa61e3f2df19eb58790941959c8b2d7773d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 08:42:46 +0000 Subject: [PATCH 17/34] Apply suggestions --- library/core/src/num/nonzero.rs | 36 ++++++++++++++++----------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index bdcc40789908d..7269084242a08 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2561,18 +2561,32 @@ mod verify { macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(<$t>::unchecked_add)] + #[kani::proof_for_contract(<$nonzero_type>::unchecked_add)] pub fn $nonzero_check_unchecked_add_for() { let x: $nonzero_type = kani::any(); - let y: $nonzero_type = kani::any(); - + let y: $t = kani::any(); + unsafe { - x.get().unchecked_add(y.get()); + x.unchecked_add(y); } } }; } + // Generate proofs for all NonZero types + nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); + nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); + nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); + nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); + nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); + nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); + nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); + nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); + nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); + nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); + nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); + nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); + // Use the macro to generate different versions of the function for multiple types nonzero_check_cmp!(core::num::NonZeroI8, nonzero_check_cmp_for_i8); nonzero_check_cmp!(core::num::NonZeroI16, nonzero_check_cmp_for_i16); @@ -2602,20 +2616,6 @@ mod verify { } }; } - - // Generate proofs for all NonZero types - nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); - nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); - nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); - nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); - nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); - nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); - nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); - nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); - nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); - nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); - nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); - nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); nonzero_check_max!(core::num::NonZeroI8, nonzero_check_max_for_i8); nonzero_check_max!(core::num::NonZeroI16, nonzero_check_max_for_i16); From fcfd000acf165f7366ee2350967e85c8a8638da7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 08:45:45 +0000 Subject: [PATCH 18/34] Arrange lines --- library/core/src/num/nonzero.rs | 240 ++++++++++++++++---------------- 1 file changed, 119 insertions(+), 121 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 7269084242a08..81b73e14de657 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2435,7 +2435,7 @@ mod verify { } }; } - + // Generate harnesses for multiple types nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); @@ -2449,22 +2449,6 @@ mod verify { nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); - - - - macro_rules! check_mul_unchecked_small{ - ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident) => { - #[kani::proof_for_contract(<$t>::unchecked_mul)] - pub fn $nonzero_check_mul_for() { - let x: $nonzero_type = kani::any(); - let y: $nonzero_type = kani::any(); - - unsafe { - x.unchecked_mul(y); - } - } - }; - } macro_rules! nonzero_check_cmp { ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { @@ -2483,110 +2467,6 @@ mod verify { }; } - macro_rules! check_mul_unchecked_intervals{ - ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract(<$t>::unchecked_mul)] - pub fn $nonzero_check_mul_for() { - let x = kani::any::<$t>(); - let y = kani::any::<$t>(); - - kani::assume(x != 0 && x >= $min && x <= $max); - kani::assume(y != 0 && y >= $min && y <= $max); - - let x = <$nonzero_type>::new(x).unwrap(); - let y = <$nonzero_type>::new(y).unwrap(); - - unsafe { - x.unchecked_mul(y); - } - } - }; - } - - //Calls for i32 - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_small, NonZeroI32::new(-10i32).unwrap().into(), NonZeroI32::new(10i32).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_pos, NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_neg, NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_pos, NonZeroI32::new(i32::MAX / 2).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_neg, NonZeroI32::new(i32::MIN / 2).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); - - //Calls for i64 - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_small, NonZeroI64::new(-10i64).unwrap().into(), NonZeroI64::new(10i64).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_pos, NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_neg, NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_pos, NonZeroI64::new(i64::MAX / 2).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_neg, NonZeroI64::new(i64::MIN / 2).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); - - //calls for i128 - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_small, NonZeroI128::new(-10i128).unwrap().into(), NonZeroI128::new(10i128).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_pos, NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_neg, NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_pos, NonZeroI128::new(i128::MAX / 2).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_neg, NonZeroI128::new(i128::MIN / 2).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); - - //calls for isize - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_small, NonZeroIsize::new(-10isize).unwrap().into(), NonZeroIsize::new(10isize).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_pos, NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_neg, NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_pos, NonZeroIsize::new(isize::MAX / 2).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_neg, NonZeroIsize::new(isize::MIN / 2).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); - - //calls for u32 - check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_small, NonZeroU32::new(1u32).unwrap().into(), NonZeroU32::new(10u32).unwrap().into()); - check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_large, NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); - check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_edge, NonZeroU32::new(u32::MAX / 2).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); - - //calls for u64 - check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_small, NonZeroU64::new(1u64).unwrap().into(), NonZeroU64::new(10u64).unwrap().into()); - check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_large, NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); - check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_edge, NonZeroU64::new(u64::MAX / 2).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); - - //calls for u128 - check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_small, NonZeroU128::new(1u128).unwrap().into(), NonZeroU128::new(10u128).unwrap().into()); - check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_large, NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); - check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_edge, NonZeroU128::new(u128::MAX / 2).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); - - //calls for usize - check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_small, NonZeroUsize::new(1usize).unwrap().into(), NonZeroUsize::new(10usize).unwrap().into()); - check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_large, NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); - check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_edge, NonZeroUsize::new(usize::MAX / 2).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); - - //calls for i8, i16, u8, u16 - check_mul_unchecked_small!(i8, NonZeroI8, nonzero_check_mul_for_i8); - check_mul_unchecked_small!(i16, NonZeroI16, nonzero_check_mul_for_i16); - check_mul_unchecked_small!(u8, NonZeroU8, nonzero_check_mul_for_u8); - check_mul_unchecked_small!(u16, NonZeroU16, nonzero_check_mul_for_u16); - - //check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16); - - macro_rules! nonzero_check_add { - ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(<$nonzero_type>::unchecked_add)] - pub fn $nonzero_check_unchecked_add_for() { - let x: $nonzero_type = kani::any(); - let y: $t = kani::any(); - - unsafe { - x.unchecked_add(y); - } - } - }; - } - - // Generate proofs for all NonZero types - nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); - nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); - nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); - nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); - nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); - nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); - nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); - nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); - nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); - nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); - nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); - nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); - // Use the macro to generate different versions of the function for multiple types nonzero_check_cmp!(core::num::NonZeroI8, nonzero_check_cmp_for_i8); nonzero_check_cmp!(core::num::NonZeroI16, nonzero_check_cmp_for_i16); @@ -2783,4 +2663,122 @@ mod verify { nonzero_check_rotate_left_and_right!(core::num::NonZeroU64, nonzero_check_rotate_for_u64); nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128); nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize); + + macro_rules! check_mul_unchecked_small{ + ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident) => { + #[kani::proof_for_contract(<$t>::unchecked_mul)] + pub fn $nonzero_check_mul_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + + unsafe { + x.unchecked_mul(y); + } + } + }; + } + + macro_rules! check_mul_unchecked_intervals{ + ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { + #[kani::proof_for_contract(<$t>::unchecked_mul)] + pub fn $nonzero_check_mul_for() { + let x = kani::any::<$t>(); + let y = kani::any::<$t>(); + + kani::assume(x != 0 && x >= $min && x <= $max); + kani::assume(y != 0 && y >= $min && y <= $max); + + let x = <$nonzero_type>::new(x).unwrap(); + let y = <$nonzero_type>::new(y).unwrap(); + + unsafe { + x.unchecked_mul(y); + } + } + }; + } + + //Calls for i32 + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_small, NonZeroI32::new(-10i32).unwrap().into(), NonZeroI32::new(10i32).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_pos, NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_neg, NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_pos, NonZeroI32::new(i32::MAX / 2).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_neg, NonZeroI32::new(i32::MIN / 2).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); + + //Calls for i64 + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_small, NonZeroI64::new(-10i64).unwrap().into(), NonZeroI64::new(10i64).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_pos, NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_neg, NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_pos, NonZeroI64::new(i64::MAX / 2).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_neg, NonZeroI64::new(i64::MIN / 2).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); + + //calls for i128 + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_small, NonZeroI128::new(-10i128).unwrap().into(), NonZeroI128::new(10i128).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_pos, NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_neg, NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_pos, NonZeroI128::new(i128::MAX / 2).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); + check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_neg, NonZeroI128::new(i128::MIN / 2).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); + + //calls for isize + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_small, NonZeroIsize::new(-10isize).unwrap().into(), NonZeroIsize::new(10isize).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_pos, NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_neg, NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_pos, NonZeroIsize::new(isize::MAX / 2).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); + check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_neg, NonZeroIsize::new(isize::MIN / 2).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); + + //calls for u32 + check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_small, NonZeroU32::new(1u32).unwrap().into(), NonZeroU32::new(10u32).unwrap().into()); + check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_large, NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); + check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_edge, NonZeroU32::new(u32::MAX / 2).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); + + //calls for u64 + check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_small, NonZeroU64::new(1u64).unwrap().into(), NonZeroU64::new(10u64).unwrap().into()); + check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_large, NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); + check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_edge, NonZeroU64::new(u64::MAX / 2).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); + + //calls for u128 + check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_small, NonZeroU128::new(1u128).unwrap().into(), NonZeroU128::new(10u128).unwrap().into()); + check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_large, NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); + check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_edge, NonZeroU128::new(u128::MAX / 2).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); + + //calls for usize + check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_small, NonZeroUsize::new(1usize).unwrap().into(), NonZeroUsize::new(10usize).unwrap().into()); + check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_large, NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); + check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_edge, NonZeroUsize::new(usize::MAX / 2).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); + + //calls for i8, i16, u8, u16 + check_mul_unchecked_small!(i8, NonZeroI8, nonzero_check_mul_for_i8); + check_mul_unchecked_small!(i16, NonZeroI16, nonzero_check_mul_for_i16); + check_mul_unchecked_small!(u8, NonZeroU8, nonzero_check_mul_for_u8); + check_mul_unchecked_small!(u16, NonZeroU16, nonzero_check_mul_for_u16); + + //check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16); + + macro_rules! nonzero_check_add { + ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { + #[kani::proof_for_contract(<$nonzero_type>::unchecked_add)] + pub fn $nonzero_check_unchecked_add_for() { + let x: $nonzero_type = kani::any(); + let y: $t = kani::any(); + + unsafe { + x.unchecked_add(y); + } + } + }; + } + + // Generate proofs for all NonZero types + nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); + nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); + nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); + nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); + nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); + nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); + nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); + nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); + nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); + nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); + nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); + nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); } From 76039844276159b9e6cc08157e5ff70d2f22f2a6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 08:50:55 +0000 Subject: [PATCH 19/34] Add contract to from_mut_unchecked --- library/core/src/num/nonzero.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 81b73e14de657..26b45a7fa8c4c 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -452,6 +452,12 @@ where #[unstable(feature = "nonzero_from_mut", issue = "106290")] #[must_use] #[inline] + #[requires({ + let size = core::mem::size_of::(); + let ptr = &n as *const T as *const u8; + let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; + !slice.iter().all(|&byte| byte == 0) + })] pub unsafe fn from_mut_unchecked(n: &mut T) -> &mut Self { match Self::from_mut(n) { Some(n) => n, @@ -2425,10 +2431,9 @@ mod verify { macro_rules! nonzero_check_from_mut_unchecked { ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - #[kani::proof] + #[kani::proof_for_contract(NonZero::from_mut_unchecked)] pub fn $harness_name() { let mut x: $t = kani::any(); - kani::assume(x != 0); unsafe { <$nonzero_type>::from_mut_unchecked(&mut x); } From 6dab042b03dccc8f6b00aef529ec9c50078373e8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 11:24:58 +0000 Subject: [PATCH 20/34] Fix syntax error, naming --- library/core/src/num/nonzero.rs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 26b45a7fa8c4c..df61ebcb7a2da 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -454,7 +454,7 @@ where #[inline] #[requires({ let size = core::mem::size_of::(); - let ptr = &n as *const T as *const u8; + let ptr = n as *const T as *const u8; let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; !slice.iter().all(|&byte| byte == 0) })] @@ -2431,7 +2431,7 @@ mod verify { macro_rules! nonzero_check_from_mut_unchecked { ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - #[kani::proof_for_contract(NonZero::from_mut_unchecked)] + #[kani::proof_for_contract(NonZero<$t>::from_mut_unchecked)] pub fn $harness_name() { let mut x: $t = kani::any(); unsafe { @@ -2671,8 +2671,8 @@ mod verify { macro_rules! check_mul_unchecked_small{ ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident) => { - #[kani::proof_for_contract(<$t>::unchecked_mul)] - pub fn $nonzero_check_mul_for() { + #[kani::proof_for_contract(NonZero<$t>::unchecked_mul)] + pub fn $nonzero_check_unchecked_mul_for() { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); @@ -2685,16 +2685,16 @@ mod verify { macro_rules! check_mul_unchecked_intervals{ ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract(<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero<$t>::unchecked_mul)] pub fn $nonzero_check_mul_for() { let x = kani::any::<$t>(); - let y = kani::any::<$t>(); + let y = kani::any::<$t>(); - kani::assume(x != 0 && x >= $min && x <= $max); - kani::assume(y != 0 && y >= $min && y <= $max); + kani::assume(x != 0 && x >= $min && x <= $max); + kani::assume(y != 0 && y >= $min && y <= $max); - let x = <$nonzero_type>::new(x).unwrap(); - let y = <$nonzero_type>::new(y).unwrap(); + let x = <$nonzero_type>::new(x).unwrap(); + let y = <$nonzero_type>::new(y).unwrap(); unsafe { x.unchecked_mul(y); @@ -2761,7 +2761,7 @@ mod verify { macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(<$nonzero_type>::unchecked_add)] + #[kani::proof_for_contract(NonZero<$t>::unchecked_add)] pub fn $nonzero_check_unchecked_add_for() { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); From 06fad10d6497d4cffae62618afd67dcea26a4aec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 12:50:15 +0000 Subject: [PATCH 21/34] Disable what does not currently compile --- library/core/src/num/nonzero.rs | 77 +++++++++++++++++---------------- 1 file changed, 39 insertions(+), 38 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index df61ebcb7a2da..f1e3f15f72a6b 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -452,12 +452,13 @@ where #[unstable(feature = "nonzero_from_mut", issue = "106290")] #[must_use] #[inline] - #[requires({ - let size = core::mem::size_of::(); - let ptr = n as *const T as *const u8; - let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; - !slice.iter().all(|&byte| byte == 0) - })] + // TODO: not sure how to refer to a parameter that is a mutable reference + // #[requires({ + // let size = core::mem::size_of::(); + // let ptr = n as *const T as *const u8; + // let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; + // !slice.iter().all(|&byte| byte == 0) + // })] pub unsafe fn from_mut_unchecked(n: &mut T) -> &mut Self { match Self::from_mut(n) { Some(n) => n, @@ -2429,31 +2430,31 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); - macro_rules! nonzero_check_from_mut_unchecked { - ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - #[kani::proof_for_contract(NonZero<$t>::from_mut_unchecked)] - pub fn $harness_name() { - let mut x: $t = kani::any(); - unsafe { - <$nonzero_type>::from_mut_unchecked(&mut x); - } - } - }; - } - - // Generate harnesses for multiple types - nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); - nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); - nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); - nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); - nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); - nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); - nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); - nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); - nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); - nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); - nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); - nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); + // macro_rules! nonzero_check_from_mut_unchecked { + // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + // #[kani::proof_for_contract(NonZero<$t>::from_mut_unchecked)] + // pub fn $harness_name() { + // let mut x: $t = kani::any(); + // unsafe { + // <$nonzero_type>::from_mut_unchecked(&mut x); + // } + // } + // }; + // } + + // // Generate harnesses for multiple types + // nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); + // nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); + // nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); + // nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); + // nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); + // nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); + // nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); + // nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); + // nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); + // nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); + // nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); + // nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); macro_rules! nonzero_check_cmp { ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { @@ -2670,7 +2671,7 @@ mod verify { nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize); macro_rules! check_mul_unchecked_small{ - ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident) => { + ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { #[kani::proof_for_contract(NonZero<$t>::unchecked_mul)] pub fn $nonzero_check_unchecked_mul_for() { let x: $nonzero_type = kani::any(); @@ -2774,12 +2775,12 @@ mod verify { } // Generate proofs for all NonZero types - nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); - nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); - nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); - nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); - nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); - nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); + // nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); + // nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); + // nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); + // nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); + // nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); + // nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); From d8e39776a90ed7cee797cf79813c1d0d23e8aa55 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 13:03:48 +0000 Subject: [PATCH 22/34] Proof target names --- library/core/src/num/nonzero.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index f1e3f15f72a6b..2b212d58e201d 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2432,7 +2432,7 @@ mod verify { // macro_rules! nonzero_check_from_mut_unchecked { // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - // #[kani::proof_for_contract(NonZero<$t>::from_mut_unchecked)] + // #[kani::proof_for_contract(NonZero::<$t>::from_mut_unchecked)] // pub fn $harness_name() { // let mut x: $t = kani::any(); // unsafe { @@ -2672,7 +2672,7 @@ mod verify { macro_rules! check_mul_unchecked_small{ ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { - #[kani::proof_for_contract(NonZero<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)] pub fn $nonzero_check_unchecked_mul_for() { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); @@ -2686,7 +2686,7 @@ mod verify { macro_rules! check_mul_unchecked_intervals{ ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract(NonZero<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)] pub fn $nonzero_check_mul_for() { let x = kani::any::<$t>(); let y = kani::any::<$t>(); @@ -2762,7 +2762,7 @@ mod verify { macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(NonZero<$t>::unchecked_add)] + #[kani::proof_for_contract(NonZero::<$t>::unchecked_add)] pub fn $nonzero_check_unchecked_add_for() { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); From 014a44eb65ee560cb9fec511ae12d5fd6e563c67 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Apr 2025 13:12:39 +0000 Subject: [PATCH 23/34] Contracts lookup, again --- library/core/src/num/nonzero.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 2b212d58e201d..2b8ebe4aeb1d1 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2432,7 +2432,7 @@ mod verify { // macro_rules! nonzero_check_from_mut_unchecked { // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - // #[kani::proof_for_contract(NonZero::<$t>::from_mut_unchecked)] + // #[kani::proof_for_contract(NonZero::::from_mut_unchecked)] // pub fn $harness_name() { // let mut x: $t = kani::any(); // unsafe { @@ -2672,7 +2672,7 @@ mod verify { macro_rules! check_mul_unchecked_small{ ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { - #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero::::unchecked_mul)] pub fn $nonzero_check_unchecked_mul_for() { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); @@ -2686,7 +2686,7 @@ mod verify { macro_rules! check_mul_unchecked_intervals{ ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero::::unchecked_mul)] pub fn $nonzero_check_mul_for() { let x = kani::any::<$t>(); let y = kani::any::<$t>(); @@ -2762,7 +2762,7 @@ mod verify { macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(NonZero::<$t>::unchecked_add)] + #[kani::proof_for_contract(NonZero::::unchecked_add)] pub fn $nonzero_check_unchecked_add_for() { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); From 0a7a3c6020ac31064787d9c72dea9b4bc785511a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Apr 2025 09:27:42 +0000 Subject: [PATCH 24/34] Lookup, once more --- library/core/src/num/nonzero.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 2b8ebe4aeb1d1..b27dc1d43849f 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2432,7 +2432,7 @@ mod verify { // macro_rules! nonzero_check_from_mut_unchecked { // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - // #[kani::proof_for_contract(NonZero::::from_mut_unchecked)] + // #[kani::proof_for_contract(::from_mut_unchecked)] // pub fn $harness_name() { // let mut x: $t = kani::any(); // unsafe { @@ -2672,7 +2672,7 @@ mod verify { macro_rules! check_mul_unchecked_small{ ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { - #[kani::proof_for_contract(NonZero::::unchecked_mul)] + #[kani::proof_for_contract(<$t>::unchecked_mul)] pub fn $nonzero_check_unchecked_mul_for() { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); @@ -2686,7 +2686,7 @@ mod verify { macro_rules! check_mul_unchecked_intervals{ ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract(NonZero::::unchecked_mul)] + #[kani::proof_for_contract(<$t>::unchecked_mul)] pub fn $nonzero_check_mul_for() { let x = kani::any::<$t>(); let y = kani::any::<$t>(); @@ -2762,7 +2762,7 @@ mod verify { macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(NonZero::::unchecked_add)] + #[kani::proof_for_contract(<$t>::unchecked_add)] pub fn $nonzero_check_unchecked_add_for() { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); From fb8ad3eeeeff6b87f923440b5515bb9b9279f961 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Apr 2025 10:36:46 +0000 Subject: [PATCH 25/34] rustfmt --- library/core/src/num/nonzero.rs | 350 +++++++++++++++++++++++++++----- 1 file changed, 301 insertions(+), 49 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index b27dc1d43849f..240eb9a8c8a24 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2418,17 +2418,57 @@ mod verify { // Use the macro to generate different versions of the function for multiple types nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); - nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); - nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32); - nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); - nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128); - nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize); + nonzero_check!( + i16, + core::num::NonZeroI16, + nonzero_check_new_unchecked_for_16 + ); + nonzero_check!( + i32, + core::num::NonZeroI32, + nonzero_check_new_unchecked_for_32 + ); + nonzero_check!( + i64, + core::num::NonZeroI64, + nonzero_check_new_unchecked_for_64 + ); + nonzero_check!( + i128, + core::num::NonZeroI128, + nonzero_check_new_unchecked_for_128 + ); + nonzero_check!( + isize, + core::num::NonZeroIsize, + nonzero_check_new_unchecked_for_isize + ); nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8); - nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16); - nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32); - nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); - nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); - nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); + nonzero_check!( + u16, + core::num::NonZeroU16, + nonzero_check_new_unchecked_for_u16 + ); + nonzero_check!( + u32, + core::num::NonZeroU32, + nonzero_check_new_unchecked_for_u32 + ); + nonzero_check!( + u64, + core::num::NonZeroU64, + nonzero_check_new_unchecked_for_u64 + ); + nonzero_check!( + u128, + core::num::NonZeroU128, + nonzero_check_new_unchecked_for_u128 + ); + nonzero_check!( + usize, + core::num::NonZeroUsize, + nonzero_check_new_unchecked_for_usize + ); // macro_rules! nonzero_check_from_mut_unchecked { // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { @@ -2670,7 +2710,7 @@ mod verify { nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128); nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize); - macro_rules! check_mul_unchecked_small{ + macro_rules! check_mul_unchecked_small { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { #[kani::proof_for_contract(<$t>::unchecked_mul)] pub fn $nonzero_check_unchecked_mul_for() { @@ -2684,7 +2724,7 @@ mod verify { }; } - macro_rules! check_mul_unchecked_intervals{ + macro_rules! check_mul_unchecked_intervals { ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { #[kani::proof_for_contract(<$t>::unchecked_mul)] pub fn $nonzero_check_mul_for() { @@ -2705,52 +2745,244 @@ mod verify { } //Calls for i32 - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_small, NonZeroI32::new(-10i32).unwrap().into(), NonZeroI32::new(10i32).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_pos, NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_neg, NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_pos, NonZeroI32::new(i32::MAX / 2).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_neg, NonZeroI32::new(i32::MIN / 2).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!( + i32, + NonZeroI32, + check_mul_i32_small, + NonZeroI32::new(-10i32).unwrap().into(), + NonZeroI32::new(10i32).unwrap().into() + ); + check_mul_unchecked_intervals!( + i32, + NonZeroI32, + check_mul_i32_large_pos, + NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), + NonZeroI32::new(i32::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + i32, + NonZeroI32, + check_mul_i32_large_neg, + NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), + NonZeroI32::new(i32::MIN + 1).unwrap().into() + ); + check_mul_unchecked_intervals!( + i32, + NonZeroI32, + check_mul_i32_edge_pos, + NonZeroI32::new(i32::MAX / 2).unwrap().into(), + NonZeroI32::new(i32::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + i32, + NonZeroI32, + check_mul_i32_edge_neg, + NonZeroI32::new(i32::MIN / 2).unwrap().into(), + NonZeroI32::new(i32::MIN + 1).unwrap().into() + ); //Calls for i64 - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_small, NonZeroI64::new(-10i64).unwrap().into(), NonZeroI64::new(10i64).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_pos, NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_neg, NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_pos, NonZeroI64::new(i64::MAX / 2).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_neg, NonZeroI64::new(i64::MIN / 2).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!( + i64, + NonZeroI64, + check_mul_i64_small, + NonZeroI64::new(-10i64).unwrap().into(), + NonZeroI64::new(10i64).unwrap().into() + ); + check_mul_unchecked_intervals!( + i64, + NonZeroI64, + check_mul_i64_large_pos, + NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), + NonZeroI64::new(i64::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + i64, + NonZeroI64, + check_mul_i64_large_neg, + NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), + NonZeroI64::new(i64::MIN + 1).unwrap().into() + ); + check_mul_unchecked_intervals!( + i64, + NonZeroI64, + check_mul_i64_edge_pos, + NonZeroI64::new(i64::MAX / 2).unwrap().into(), + NonZeroI64::new(i64::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + i64, + NonZeroI64, + check_mul_i64_edge_neg, + NonZeroI64::new(i64::MIN / 2).unwrap().into(), + NonZeroI64::new(i64::MIN + 1).unwrap().into() + ); //calls for i128 - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_small, NonZeroI128::new(-10i128).unwrap().into(), NonZeroI128::new(10i128).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_pos, NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_neg, NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_pos, NonZeroI128::new(i128::MAX / 2).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into()); - check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_neg, NonZeroI128::new(i128::MIN / 2).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!( + i128, + NonZeroI128, + check_mul_i128_small, + NonZeroI128::new(-10i128).unwrap().into(), + NonZeroI128::new(10i128).unwrap().into() + ); + check_mul_unchecked_intervals!( + i128, + NonZeroI128, + check_mul_i128_large_pos, + NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), + NonZeroI128::new(i128::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + i128, + NonZeroI128, + check_mul_i128_large_neg, + NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), + NonZeroI128::new(i128::MIN + 1).unwrap().into() + ); + check_mul_unchecked_intervals!( + i128, + NonZeroI128, + check_mul_i128_edge_pos, + NonZeroI128::new(i128::MAX / 2).unwrap().into(), + NonZeroI128::new(i128::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + i128, + NonZeroI128, + check_mul_i128_edge_neg, + NonZeroI128::new(i128::MIN / 2).unwrap().into(), + NonZeroI128::new(i128::MIN + 1).unwrap().into() + ); //calls for isize - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_small, NonZeroIsize::new(-10isize).unwrap().into(), NonZeroIsize::new(10isize).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_pos, NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_neg, NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_pos, NonZeroIsize::new(isize::MAX / 2).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into()); - check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_neg, NonZeroIsize::new(isize::MIN / 2).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into()); + check_mul_unchecked_intervals!( + isize, + NonZeroIsize, + check_mul_isize_small, + NonZeroIsize::new(-10isize).unwrap().into(), + NonZeroIsize::new(10isize).unwrap().into() + ); + check_mul_unchecked_intervals!( + isize, + NonZeroIsize, + check_mul_isize_large_pos, + NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), + NonZeroIsize::new(isize::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + isize, + NonZeroIsize, + check_mul_isize_large_neg, + NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), + NonZeroIsize::new(isize::MIN + 1).unwrap().into() + ); + check_mul_unchecked_intervals!( + isize, + NonZeroIsize, + check_mul_isize_edge_pos, + NonZeroIsize::new(isize::MAX / 2).unwrap().into(), + NonZeroIsize::new(isize::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + isize, + NonZeroIsize, + check_mul_isize_edge_neg, + NonZeroIsize::new(isize::MIN / 2).unwrap().into(), + NonZeroIsize::new(isize::MIN + 1).unwrap().into() + ); //calls for u32 - check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_small, NonZeroU32::new(1u32).unwrap().into(), NonZeroU32::new(10u32).unwrap().into()); - check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_large, NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); - check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_edge, NonZeroU32::new(u32::MAX / 2).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into()); + check_mul_unchecked_intervals!( + u32, + NonZeroU32, + check_mul_u32_small, + NonZeroU32::new(1u32).unwrap().into(), + NonZeroU32::new(10u32).unwrap().into() + ); + check_mul_unchecked_intervals!( + u32, + NonZeroU32, + check_mul_u32_large, + NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), + NonZeroU32::new(u32::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + u32, + NonZeroU32, + check_mul_u32_edge, + NonZeroU32::new(u32::MAX / 2).unwrap().into(), + NonZeroU32::new(u32::MAX).unwrap().into() + ); //calls for u64 - check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_small, NonZeroU64::new(1u64).unwrap().into(), NonZeroU64::new(10u64).unwrap().into()); - check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_large, NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); - check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_edge, NonZeroU64::new(u64::MAX / 2).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into()); + check_mul_unchecked_intervals!( + u64, + NonZeroU64, + check_mul_u64_small, + NonZeroU64::new(1u64).unwrap().into(), + NonZeroU64::new(10u64).unwrap().into() + ); + check_mul_unchecked_intervals!( + u64, + NonZeroU64, + check_mul_u64_large, + NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), + NonZeroU64::new(u64::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + u64, + NonZeroU64, + check_mul_u64_edge, + NonZeroU64::new(u64::MAX / 2).unwrap().into(), + NonZeroU64::new(u64::MAX).unwrap().into() + ); //calls for u128 - check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_small, NonZeroU128::new(1u128).unwrap().into(), NonZeroU128::new(10u128).unwrap().into()); - check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_large, NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); - check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_edge, NonZeroU128::new(u128::MAX / 2).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into()); + check_mul_unchecked_intervals!( + u128, + NonZeroU128, + check_mul_u128_small, + NonZeroU128::new(1u128).unwrap().into(), + NonZeroU128::new(10u128).unwrap().into() + ); + check_mul_unchecked_intervals!( + u128, + NonZeroU128, + check_mul_u128_large, + NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), + NonZeroU128::new(u128::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + u128, + NonZeroU128, + check_mul_u128_edge, + NonZeroU128::new(u128::MAX / 2).unwrap().into(), + NonZeroU128::new(u128::MAX).unwrap().into() + ); //calls for usize - check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_small, NonZeroUsize::new(1usize).unwrap().into(), NonZeroUsize::new(10usize).unwrap().into()); - check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_large, NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); - check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_edge, NonZeroUsize::new(usize::MAX / 2).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into()); + check_mul_unchecked_intervals!( + usize, + NonZeroUsize, + check_mul_usize_small, + NonZeroUsize::new(1usize).unwrap().into(), + NonZeroUsize::new(10usize).unwrap().into() + ); + check_mul_unchecked_intervals!( + usize, + NonZeroUsize, + check_mul_usize_large, + NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), + NonZeroUsize::new(usize::MAX).unwrap().into() + ); + check_mul_unchecked_intervals!( + usize, + NonZeroUsize, + check_mul_usize_edge, + NonZeroUsize::new(usize::MAX / 2).unwrap().into(), + NonZeroUsize::new(usize::MAX).unwrap().into() + ); //calls for i8, i16, u8, u16 check_mul_unchecked_small!(i8, NonZeroI8, nonzero_check_mul_for_i8); @@ -2782,9 +3014,29 @@ mod verify { // nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); // nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); - nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); - nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); - nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); - nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); - nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); + nonzero_check_add!( + u16, + core::num::NonZeroU16, + nonzero_check_unchecked_add_for_u16 + ); + nonzero_check_add!( + u32, + core::num::NonZeroU32, + nonzero_check_unchecked_add_for_u32 + ); + nonzero_check_add!( + u64, + core::num::NonZeroU64, + nonzero_check_unchecked_add_for_u64 + ); + nonzero_check_add!( + u128, + core::num::NonZeroU128, + nonzero_check_unchecked_add_for_u128 + ); + nonzero_check_add!( + usize, + core::num::NonZeroUsize, + nonzero_check_unchecked_add_for_usize + ); } From 3b69e2101ace4759546041ac5ecc8c41a86e9500 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Apr 2025 11:15:57 +0000 Subject: [PATCH 26/34] rustfmt 2 --- library/core/src/num/nonzero.rs | 90 ++++++--------------------------- 1 file changed, 15 insertions(+), 75 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 240eb9a8c8a24..86bf42355004f 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2418,57 +2418,17 @@ mod verify { // Use the macro to generate different versions of the function for multiple types nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); - nonzero_check!( - i16, - core::num::NonZeroI16, - nonzero_check_new_unchecked_for_16 - ); - nonzero_check!( - i32, - core::num::NonZeroI32, - nonzero_check_new_unchecked_for_32 - ); - nonzero_check!( - i64, - core::num::NonZeroI64, - nonzero_check_new_unchecked_for_64 - ); - nonzero_check!( - i128, - core::num::NonZeroI128, - nonzero_check_new_unchecked_for_128 - ); - nonzero_check!( - isize, - core::num::NonZeroIsize, - nonzero_check_new_unchecked_for_isize - ); + nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); + nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32); + nonzero_check!( i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); + nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128); + nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize); nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8); - nonzero_check!( - u16, - core::num::NonZeroU16, - nonzero_check_new_unchecked_for_u16 - ); - nonzero_check!( - u32, - core::num::NonZeroU32, - nonzero_check_new_unchecked_for_u32 - ); - nonzero_check!( - u64, - core::num::NonZeroU64, - nonzero_check_new_unchecked_for_u64 - ); - nonzero_check!( - u128, - core::num::NonZeroU128, - nonzero_check_new_unchecked_for_u128 - ); - nonzero_check!( - usize, - core::num::NonZeroUsize, - nonzero_check_new_unchecked_for_usize - ); + nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16); + nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32); + nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); + nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); + nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); // macro_rules! nonzero_check_from_mut_unchecked { // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { @@ -3014,29 +2974,9 @@ mod verify { // nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); // nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); - nonzero_check_add!( - u16, - core::num::NonZeroU16, - nonzero_check_unchecked_add_for_u16 - ); - nonzero_check_add!( - u32, - core::num::NonZeroU32, - nonzero_check_unchecked_add_for_u32 - ); - nonzero_check_add!( - u64, - core::num::NonZeroU64, - nonzero_check_unchecked_add_for_u64 - ); - nonzero_check_add!( - u128, - core::num::NonZeroU128, - nonzero_check_unchecked_add_for_u128 - ); - nonzero_check_add!( - usize, - core::num::NonZeroUsize, - nonzero_check_unchecked_add_for_usize - ); + nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); + nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); + nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); + nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); + nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); } From 8bd1151573ca7ee40c31c59bf18758e1287bd9b8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Apr 2025 11:50:12 +0000 Subject: [PATCH 27/34] Remove stray space --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 86bf42355004f..8f9bb54634ce9 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2420,7 +2420,7 @@ mod verify { nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32); - nonzero_check!( i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); + nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128); nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize); nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8); From 233c41c2059fbc751b23955d13899b1b3376300a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 17:18:54 +0200 Subject: [PATCH 28/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 8f9bb54634ce9..98880b30fcd8d 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -1121,7 +1121,7 @@ macro_rules! nonzero_integer { self.get().checked_mul(other.get()).is_some() })] #[ensures(|result: &Self| { - self.get().checked_mul(other.get()).unwrap() == result.get() + self.get().checked_mul(other.get()).is_some_and(|product| product == result.get()) })] pub const unsafe fn unchecked_mul(self, other: Self) -> Self { // SAFETY: The caller ensures there is no overflow. From d21fdf25cc81306ba39bcfb961faead6b2c78327 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 17:19:04 +0200 Subject: [PATCH 29/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 98880b30fcd8d..dde7e6bf79b95 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -1530,7 +1530,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods { })] #[ensures(|result: &Self| { // Postcondition: the result matches the expected addition - self.get().checked_add(other).unwrap() == result.get() + self.get().checked_add(other).is_some_and(|sum| sum == result.get()) })] pub const unsafe fn unchecked_add(self, other: $Int) -> Self { // SAFETY: The caller ensures there is no overflow. From 5f13ef4939198d1a111b1bf2a32c5a23339cd40a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 17:21:30 +0200 Subject: [PATCH 30/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 7 ------- 1 file changed, 7 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index dde7e6bf79b95..cbe99b8e54815 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2966,13 +2966,6 @@ mod verify { }; } - // Generate proofs for all NonZero types - // nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8); - // nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16); - // nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32); - // nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64); - // nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128); - // nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize); nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8); nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16); nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32); From 36030a8b01b8d5745b482308f94f51aef88581f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 17:23:03 +0200 Subject: [PATCH 31/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index cbe99b8e54815..6879f767a6699 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2950,8 +2950,6 @@ mod verify { check_mul_unchecked_small!(u8, NonZeroU8, nonzero_check_mul_for_u8); check_mul_unchecked_small!(u16, NonZeroU16, nonzero_check_mul_for_u16); - //check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16); - macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { #[kani::proof_for_contract(<$t>::unchecked_add)] From 1c5b394d1b550c22ee71d9c87331c25b7029acd0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 17:23:38 +0200 Subject: [PATCH 32/34] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 26 -------------------------- 1 file changed, 26 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 6879f767a6699..f0850f6e74f99 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2430,32 +2430,6 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); - // macro_rules! nonzero_check_from_mut_unchecked { - // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - // #[kani::proof_for_contract(::from_mut_unchecked)] - // pub fn $harness_name() { - // let mut x: $t = kani::any(); - // unsafe { - // <$nonzero_type>::from_mut_unchecked(&mut x); - // } - // } - // }; - // } - - // // Generate harnesses for multiple types - // nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); - // nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); - // nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); - // nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); - // nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); - // nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); - // nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); - // nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); - // nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); - // nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); - // nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); - // nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); - macro_rules! nonzero_check_cmp { ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { #[kani::proof] From ebfd87673c955f268bad1db0c7fbc9aa2a77feed Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Apr 2025 20:50:48 +0000 Subject: [PATCH 33/34] Remove from_mut_unchecked contract/harnesses (commented out) --- library/core/src/num/nonzero.rs | 33 --------------------------------- 1 file changed, 33 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index baa651ef19e0a..84715dcfc13ad 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -452,13 +452,6 @@ where #[unstable(feature = "nonzero_from_mut", issue = "106290")] #[must_use] #[inline] - // TODO: not sure how to refer to a parameter that is a mutable reference - // #[requires({ - // let size = core::mem::size_of::(); - // let ptr = n as *const T as *const u8; - // let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; - // !slice.iter().all(|&byte| byte == 0) - // })] pub unsafe fn from_mut_unchecked(n: &mut T) -> &mut Self { match Self::from_mut(n) { Some(n) => n, @@ -2435,32 +2428,6 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); - // macro_rules! nonzero_check_from_mut_unchecked { - // ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - // #[kani::proof_for_contract(::from_mut_unchecked)] - // pub fn $harness_name() { - // let mut x: $t = kani::any(); - // unsafe { - // <$nonzero_type>::from_mut_unchecked(&mut x); - // } - // } - // }; - // } - - // // Generate harnesses for multiple types - // nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); - // nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); - // nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); - // nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); - // nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); - // nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); - // nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); - // nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); - // nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); - // nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); - // nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); - // nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); - macro_rules! nonzero_check_cmp { ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { #[kani::proof] From 2e6ccae3cfa090c01e1a9ff9b89cc4fec0b34f83 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 17:32:01 +0000 Subject: [PATCH 34/34] Adjust target lookup --- library/core/src/num/nonzero.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index ffa6d0d77630c..df6f5bb1da77f 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2592,7 +2592,7 @@ mod verify { macro_rules! check_mul_unchecked_small { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { - #[kani::proof_for_contract(<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)] pub fn $nonzero_check_unchecked_mul_for() { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); @@ -2606,7 +2606,7 @@ mod verify { macro_rules! check_mul_unchecked_intervals { ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract(<$t>::unchecked_mul)] + #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)] pub fn $nonzero_check_mul_for() { let x = kani::any::<$t>(); let y = kani::any::<$t>(); @@ -2872,7 +2872,7 @@ mod verify { macro_rules! nonzero_check_add { ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { - #[kani::proof_for_contract(<$t>::unchecked_add)] + #[kani::proof_for_contract(NonZero::<$t>::unchecked_add)] pub fn $nonzero_check_unchecked_add_for() { let x: $nonzero_type = kani::any(); let y: $t = kani::any();