From dffe30baa86decbbb6e92aeb568e1baa917d4e68 Mon Sep 17 00:00:00 2001 From: aaluna Date: Fri, 20 Sep 2024 14:38:41 -0400 Subject: [PATCH 01/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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); +}