From 3590903ee1631eb00f4a7454b16719c220efbb04 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 17 Feb 2025 10:04:41 -0800 Subject: [PATCH 01/18] refine challenges --- doc/src/challenges/0006-nonnull.md | 2 +- doc/src/challenges/0008-smallsort.md | 3 +-- doc/src/challenges/0012-nonzero.md | 2 +- doc/src/challenges/0014-convert-num.md | 2 +- 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index 86cb8366a36a2..b37ac36deb556 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -1,6 +1,6 @@ # Challenge 6: Safety of NonNull -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53) - **Start date:** *2024/08/16* - **End date:** *2025/04/10* diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md index 1052031506517..ea4e90caa94dc 100644 --- a/doc/src/challenges/0008-smallsort.md +++ b/doc/src/challenges/0008-smallsort.md @@ -11,8 +11,7 @@ ## Goal -The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting -algorithms optimized for slices with small lengths. +The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting algorithms with optimized implementations for slices with small lengths. In this challenge, the goal is to, first prove the memory safety of the public functions in the `smallsort` module, and, second, write contracts for them to show that the sorting algorithms actually sort the slices. diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index d5252cd939da7..f7daea6210ab6 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -1,6 +1,6 @@ # Challenge 12: Safety of `NonZero` -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024/08/23* - **End date:** *2025/04/10* diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index e6dc78666718d..fd7bc245fc01d 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -1,6 +1,6 @@ # Challenge 14: Safety of Primitive Conversions -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220 - **Start date:** 2024/12/15 - **End date:** 2025/2/28 From 6c640a31436a539ac62688fb64e4667434d6bfe1 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Feb 2025 17:50:10 -0800 Subject: [PATCH 02/18] add missing haenesses for nonnull --- doc/src/challenges/0012-nonzero.md | 2 +- library/Cargo.lock | 88 +++++++++++++++ library/core/src/ptr/non_null.rs | 167 +++++++++++++++++++++++++++++ 3 files changed, 256 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index f7daea6210ab6..d5252cd939da7 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -1,6 +1,6 @@ # Challenge 12: Safety of `NonZero` -- **Status:** Resolved +- **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024/08/23* - **End date:** *2025/04/10* diff --git a/library/Cargo.lock b/library/Cargo.lock index 55851daaf2a80..fd350c067da07 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -32,6 +32,7 @@ dependencies = [ "core", "rand", "rand_xorshift", + "safety", ] [[package]] @@ -75,6 +76,7 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", + "safety", ] [[package]] @@ -222,6 +224,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.93" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "60946a68e5f9d28b0dc1c21bb8a97ee7d018a8b322fa57838ba31cc878e22d99" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -239,6 +274,15 @@ dependencies = [ "core", ] +[[package]] +name = "quote" +version = "1.0.38" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "4.5.0" @@ -315,6 +359,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.98", +] + [[package]] name = "shlex" version = "1.3.0" @@ -344,6 +398,7 @@ dependencies = [ "rand", "rand_xorshift", "rustc-demangle", + "safety", "std_detect", "unwind", "wasi", @@ -361,6 +416,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.98" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "36147f1a48ae0ec2b5b3bc5b537d267457555a10dc06f3dbc8cb11ba3006d3b1" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -381,6 +457,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a210d160f08b701c8721ba1c726c11662f877ea6b7094007e1ca9a1041945034" + [[package]] name = "unicode-width" version = "0.1.14" @@ -414,6 +496,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/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c9361e4d7b4bd..c3b7cec212a9b 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1155,6 +1155,11 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] + #[requires( + ub_checks::can_write(self.as_ptr()) && + self.as_ptr().is_aligned() + )] pub const unsafe fn write(self, val: T) where T: Sized, @@ -1174,6 +1179,17 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(self.as_ptr(), count)))] + #[requires( + count <= isize::MAX as usize && + (count as isize).checked_mul(core::mem::size_of::() as isize).is_some() && + (self.as_ptr() as isize).checked_add((count as isize).wrapping_mul(core::mem::size_of::() as isize)).is_some() && + //(count == 0 || ub_checks::same_allocation(self.as_ptr() as *const (), self.as_ptr().wrapping_offset(count as isize) as *const ())) && + ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count)) && + self.as_ptr().is_aligned() + )] + #[ensures(|_| + ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(self.as_ptr() as *const u8, count * size_of::())))] pub const unsafe fn write_bytes(self, val: u8, count: usize) where T: Sized, @@ -1217,6 +1233,8 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] + #[requires(ub_checks::can_write(self.as_ptr()))] pub const unsafe fn write_unaligned(self, val: T) where T: Sized, @@ -2463,6 +2481,98 @@ mod verify { } } + macro_rules! generate_write_harness { + ($type:ty, $byte_size:expr, $harness_name:ident) => { + #[kani::proof_for_contract(NonNull::write)] + pub fn $harness_name() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<$byte_size>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut $type = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: $type = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read(), new_value); + } + } + }; + } + + // Generate proof harnesses for multiple types with appropriate byte sizes + generate_write_harness!(i8, 1, non_null_check_write_i8); + generate_write_harness!(i16, 2, non_null_check_write_i16); + generate_write_harness!(i32, 4, non_null_check_write_i32); + generate_write_harness!(i64, 8, non_null_check_write_i64); + generate_write_harness!(i128, 16, non_null_check_write_i128); + generate_write_harness!(isize, { core::mem::size_of::() }, non_null_check_write_isize); + generate_write_harness!(u8, 1, non_null_check_write_u8); + generate_write_harness!(u16, 2, non_null_check_write_u16); + generate_write_harness!(u32, 4, non_null_check_write_u32); + generate_write_harness!(u64, 8, non_null_check_write_u64); + generate_write_harness!(u128, 16, non_null_check_write_u128); + generate_write_harness!(usize, { core::mem::size_of::() }, non_null_check_write_usize); + generate_write_harness!((), 1, non_null_check_write_unit); + + macro_rules! generate_write_unaligned_harness { + ($type:ty, $byte_size:expr, $harness_name:ident) => { + #[kani::proof_for_contract(NonNull::write_unaligned)] + pub fn $harness_name() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<$byte_size>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut $type = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: $type = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_unaligned(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read_unaligned(), new_value); + } + } + }; + } + + // Generate proof harnesses for multiple types with appropriate byte sizes + generate_write_unaligned_harness!(i8, 1, non_null_check_write_unaligned_i8); + generate_write_unaligned_harness!(i16, 2, non_null_check_write_unaligned_i16); + generate_write_unaligned_harness!(i32, 4, non_null_check_write_unaligned_i32); + generate_write_unaligned_harness!(i64, 8, non_null_check_write_unaligned_i64); + generate_write_unaligned_harness!(i128, 16, non_null_check_write_unaligned_i128); + generate_write_unaligned_harness!( + isize, + { core::mem::size_of::() }, + non_null_check_write_unaligned_isize + ); + generate_write_unaligned_harness!(u8, 1, non_null_check_write_unaligned_u8); + generate_write_unaligned_harness!(u16, 2, non_null_check_write_unaligned_u16); + generate_write_unaligned_harness!(u32, 4, non_null_check_write_unaligned_u32); + generate_write_unaligned_harness!(u64, 8, non_null_check_write_unaligned_u64); + generate_write_unaligned_harness!(u128, 16, non_null_check_write_unaligned_u128); + generate_write_unaligned_harness!( + usize, + { core::mem::size_of::() }, + non_null_check_write_unaligned_usize + ); + generate_write_unaligned_harness!((), 1, non_null_check_write_unaligned_unit); + macro_rules! generate_write_volatile_harness { ($type:ty, $byte_size:expr, $harness_name:ident) => { #[kani::proof_for_contract(NonNull::write_volatile)] @@ -2513,6 +2623,63 @@ mod verify { ); generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit); + macro_rules! generate_write_bytes_harness { + ($type:ty, $byte_size:expr, $harness_name:ident) => { + #[kani::proof_for_contract(NonNull::write_bytes)] + pub fn $harness_name() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<$byte_size>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut $type = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let val: u8 = kani::any(); + + // Create a non-deterministic count + let count: usize = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_bytes(val, count); + + // Create a non-deterministic count + //let i: usize = kani::any_where(|&x| x < count * $byte_size); + //let ptr_byte = ptr.as_ptr() as *const u8; + + // Read back the value and assert it's correct + //assert_eq!(*ptr_byte.add(i), val); + } + } + }; + } + + // Generate proof harnesses for multiple types with appropriate byte sizes + generate_write_bytes_harness!(i8, 1, non_null_check_write_bytes_i8); + generate_write_bytes_harness!(i16, 2, non_null_check_write_bytes_i16); + generate_write_bytes_harness!(i32, 4, non_null_check_write_bytes_i32); + generate_write_bytes_harness!(i64, 8, non_null_check_write_bytes_i64); + generate_write_bytes_harness!(i128, 16, non_null_check_write_bytes_i128); + generate_write_bytes_harness!( + isize, + { core::mem::size_of::() }, + non_null_check_write_bytes_isize + ); + generate_write_bytes_harness!(u8, 1, non_null_check_write_bytes_u8); + generate_write_bytes_harness!(u16, 2, non_null_check_write_bytes_u16); + generate_write_bytes_harness!(u32, 4, non_null_check_write_bytes_u32); + generate_write_bytes_harness!(u64, 8, non_null_check_write_bytes_u64); + generate_write_bytes_harness!(u128, 16, non_null_check_write_bytes_u128); + generate_write_bytes_harness!( + usize, + { core::mem::size_of::() }, + non_null_check_write_bytes_usize + ); + generate_write_bytes_harness!((), 1, non_null_check_write_bytes_unit); + #[kani::proof_for_contract(NonNull::byte_add)] pub fn non_null_byte_add_proof() { // Make size as 1000 to ensure the array is large enough to cover various senarios From d58fe2686be315b64b3c59f5931483007f3f91f8 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 08:26:44 -0800 Subject: [PATCH 03/18] add correctness check for write_bytes --- library/core/src/ptr/non_null.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c3b7cec212a9b..0757d35d7b2ae 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -2647,11 +2647,11 @@ mod verify { ptr.write_bytes(val, count); // Create a non-deterministic count - //let i: usize = kani::any_where(|&x| x < count * $byte_size); - //let ptr_byte = ptr.as_ptr() as *const u8; + let i: usize = kani::any_where(|&x| x < count * $byte_size); + let ptr_byte = ptr.as_ptr() as *const u8; // Read back the value and assert it's correct - //assert_eq!(*ptr_byte.add(i), val); + assert_eq!(*ptr_byte.add(i), val); } } }; From 1e662dc1f30a5bf68e5313af0ae15ee22b2e7d8a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 10:46:32 -0800 Subject: [PATCH 04/18] remove correctness for NonZero challenge --- doc/src/challenges/0012-nonzero.md | 1 - 1 file changed, 1 deletion(-) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index d5252cd939da7..7a42360bca183 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -73,7 +73,6 @@ Verify the safety of the following functions and methods (all located within `co | `from_mut` | | `from_mut_unchecked` | -You are not required to write correctness contracts for these methods (e.g., for `max`, ensuring that the `result` is indeed the maximum of the inputs), but it would be great to do so! ### List of UBs From 00ba598f75ff5662bfad3c2aad359e52c7a39f97 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 11:00:22 -0800 Subject: [PATCH 05/18] add contributors for NonNull --- doc/src/challenges/0006-nonnull.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index b37ac36deb556..aa41ce09d729f 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -5,7 +5,7 @@ - **Start date:** *2024/08/16* - **End date:** *2025/04/10* - **Reward:** *N/A* - +- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), Dhvani Kapadia(https://github.com/Dhvani-Kapadia) and JY(https://github.com/Jimmycreative) ------------------- From cedd00c581c58e9ca25cf783686cb3e1c8f41b65 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 11:12:30 -0800 Subject: [PATCH 06/18] add contributors for Primitive conversions --- doc/src/challenges/0014-convert-num.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index fd7bc245fc01d..fb15d0395bff2 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -5,7 +5,7 @@ - **Start date:** 2024/12/15 - **End date:** 2025/2/28 - **Prize:** *TBD* - +- **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla) ------------------- ## Goal From 69031dcc9474e890c4ba6a64febaafac611ad19e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 13:25:51 -0800 Subject: [PATCH 07/18] fix write_bytes contract for unit --- library/core/src/ptr/non_null.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 0757d35d7b2ae..deee2ef7d8a86 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1181,6 +1181,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(self.as_ptr(), count)))] #[requires( + (!T::IS_ZST || count == 0 ) && count <= isize::MAX as usize && (count as isize).checked_mul(core::mem::size_of::() as isize).is_some() && (self.as_ptr() as isize).checked_add((count as isize).wrapping_mul(core::mem::size_of::() as isize)).is_some() && From 972bcb2111f11c28cb8675dd88f5f012510d1621 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 3 Mar 2025 16:52:30 -0800 Subject: [PATCH 08/18] update contributor name --- doc/src/challenges/0006-nonnull.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index aa41ce09d729f..99af5146fcb39 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -5,7 +5,7 @@ - **Start date:** *2024/08/16* - **End date:** *2025/04/10* - **Reward:** *N/A* -- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), Dhvani Kapadia(https://github.com/Dhvani-Kapadia) and JY(https://github.com/Jimmycreative) +- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), Dhvani Kapadia(https://github.com/Dhvani-Kapadia) and Jiun Chi Yang(https://github.com/Jimmycreative) ------------------- From aa5dd3006fc73aff21811abd95bf443da7b9aa25 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 3 Mar 2025 16:53:17 -0800 Subject: [PATCH 09/18] update write functions contracts and harnesses --- library/core/src/ptr/non_null.rs | 254 +++++++++++++++++++------------ 1 file changed, 157 insertions(+), 97 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index d0741c6e850d0..776d0a510444e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1214,10 +1214,7 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] #[cfg_attr(kani, kani::modifies(self.as_ptr()))] - #[requires( - ub_checks::can_write(self.as_ptr()) && - self.as_ptr().is_aligned() - )] + #[requires(ub_checks::can_write(self.as_ptr()))] pub const unsafe fn write(self, val: T) where T: Sized, @@ -1239,13 +1236,8 @@ impl NonNull { #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(self.as_ptr(), count)))] #[requires( - (!T::IS_ZST || count == 0 ) && - count <= isize::MAX as usize && - (count as isize).checked_mul(core::mem::size_of::() as isize).is_some() && - (self.as_ptr() as isize).checked_add((count as isize).wrapping_mul(core::mem::size_of::() as isize)).is_some() && - //(count == 0 || ub_checks::same_allocation(self.as_ptr() as *const (), self.as_ptr().wrapping_offset(count as isize) as *const ())) && - ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count)) && - self.as_ptr().is_aligned() + count.checked_mul(core::mem::size_of::() as usize).is_some_and(|x| x.wrapping_add(self.as_ptr() as usize) <= isize::MAX as usize) && + ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count)) )] #[ensures(|_| ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(self.as_ptr() as *const u8, count * size_of::())))] @@ -1293,7 +1285,7 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] #[cfg_attr(kani, kani::modifies(self.as_ptr()))] - #[requires(ub_checks::can_write(self.as_ptr()))] + #[requires(ub_checks::can_write_unaligned(self.as_ptr()))] pub const unsafe fn write_unaligned(self, val: T) where T: Sized, @@ -2555,11 +2547,12 @@ mod verify { } macro_rules! generate_write_harness { - ($type:ty, $byte_size:expr, $harness_name:ident) => { + ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract(NonNull::write)] pub fn $harness_name() { // Create a pointer generator for the given type with appropriate byte size - let mut generator = kani::PointerGenerator::<$byte_size>::new(); + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); // Get a raw pointer from the generator let raw_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2581,27 +2574,50 @@ mod verify { }; } + #[kani::proof_for_contract(NonNull::write)] + pub fn non_null_check_write_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: () = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read(), new_value); + } + } + // Generate proof harnesses for multiple types with appropriate byte sizes - generate_write_harness!(i8, 1, non_null_check_write_i8); - generate_write_harness!(i16, 2, non_null_check_write_i16); - generate_write_harness!(i32, 4, non_null_check_write_i32); - generate_write_harness!(i64, 8, non_null_check_write_i64); - generate_write_harness!(i128, 16, non_null_check_write_i128); - generate_write_harness!(isize, { core::mem::size_of::() }, non_null_check_write_isize); - generate_write_harness!(u8, 1, non_null_check_write_u8); - generate_write_harness!(u16, 2, non_null_check_write_u16); - generate_write_harness!(u32, 4, non_null_check_write_u32); - generate_write_harness!(u64, 8, non_null_check_write_u64); - generate_write_harness!(u128, 16, non_null_check_write_u128); - generate_write_harness!(usize, { core::mem::size_of::() }, non_null_check_write_usize); - generate_write_harness!((), 1, non_null_check_write_unit); + generate_write_harness!(i8, non_null_check_write_i8); + generate_write_harness!(i16, non_null_check_write_i16); + generate_write_harness!(i32, non_null_check_write_i32); + generate_write_harness!(i64, non_null_check_write_i64); + generate_write_harness!(i128, non_null_check_write_i128); + generate_write_harness!(isize, non_null_check_write_isize); + generate_write_harness!(u8, non_null_check_write_u8); + generate_write_harness!(u16, non_null_check_write_u16); + generate_write_harness!(u32, non_null_check_write_u32); + generate_write_harness!(u64, non_null_check_write_u64); + generate_write_harness!(u128, non_null_check_write_u128); + generate_write_harness!(usize, non_null_check_write_usize); macro_rules! generate_write_unaligned_harness { - ($type:ty, $byte_size:expr, $harness_name:ident) => { + ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract(NonNull::write_unaligned)] pub fn $harness_name() { // Create a pointer generator for the given type with appropriate byte size - let mut generator = kani::PointerGenerator::<$byte_size>::new(); + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); // Get a raw pointer from the generator let raw_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2623,35 +2639,50 @@ mod verify { }; } + #[kani::proof_for_contract(NonNull::write_unaligned)] + pub fn non_null_check_write_unaligned_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: () = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_unaligned(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read_unaligned(), new_value); + } + } + // Generate proof harnesses for multiple types with appropriate byte sizes - generate_write_unaligned_harness!(i8, 1, non_null_check_write_unaligned_i8); - generate_write_unaligned_harness!(i16, 2, non_null_check_write_unaligned_i16); - generate_write_unaligned_harness!(i32, 4, non_null_check_write_unaligned_i32); - generate_write_unaligned_harness!(i64, 8, non_null_check_write_unaligned_i64); - generate_write_unaligned_harness!(i128, 16, non_null_check_write_unaligned_i128); - generate_write_unaligned_harness!( - isize, - { core::mem::size_of::() }, - non_null_check_write_unaligned_isize - ); - generate_write_unaligned_harness!(u8, 1, non_null_check_write_unaligned_u8); - generate_write_unaligned_harness!(u16, 2, non_null_check_write_unaligned_u16); - generate_write_unaligned_harness!(u32, 4, non_null_check_write_unaligned_u32); - generate_write_unaligned_harness!(u64, 8, non_null_check_write_unaligned_u64); - generate_write_unaligned_harness!(u128, 16, non_null_check_write_unaligned_u128); - generate_write_unaligned_harness!( - usize, - { core::mem::size_of::() }, - non_null_check_write_unaligned_usize - ); - generate_write_unaligned_harness!((), 1, non_null_check_write_unaligned_unit); + generate_write_unaligned_harness!(i8, non_null_check_write_unaligned_i8); + generate_write_unaligned_harness!(i16, non_null_check_write_unaligned_i16); + generate_write_unaligned_harness!(i32, non_null_check_write_unaligned_i32); + generate_write_unaligned_harness!(i64, non_null_check_write_unaligned_i64); + generate_write_unaligned_harness!(i128, non_null_check_write_unaligned_i128); + generate_write_unaligned_harness!(isize, non_null_check_write_unaligned_isize); + generate_write_unaligned_harness!(u8, non_null_check_write_unaligned_u8); + generate_write_unaligned_harness!(u16, non_null_check_write_unaligned_u16); + generate_write_unaligned_harness!(u32, non_null_check_write_unaligned_u32); + generate_write_unaligned_harness!(u64, non_null_check_write_unaligned_u64); + generate_write_unaligned_harness!(u128, non_null_check_write_unaligned_u128); + generate_write_unaligned_harness!(usize, non_null_check_write_unaligned_usize); macro_rules! generate_write_volatile_harness { - ($type:ty, $byte_size:expr, $harness_name:ident) => { + ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract(NonNull::write_volatile)] pub fn $harness_name() { // Create a pointer generator for the given type with appropriate byte size - let mut generator = kani::PointerGenerator::<$byte_size>::new(); + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); // Get a raw pointer from the generator let raw_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2673,35 +2704,50 @@ mod verify { }; } + #[kani::proof_for_contract(NonNull::write_volatile)] + pub fn non_null_check_write_volatile_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: () = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_volatile(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read_volatile(), new_value); + } + } + // Generate proof harnesses for multiple types with appropriate byte sizes - generate_write_volatile_harness!(i8, 1, non_null_check_write_volatile_i8); - generate_write_volatile_harness!(i16, 2, non_null_check_write_volatile_i16); - generate_write_volatile_harness!(i32, 4, non_null_check_write_volatile_i32); - generate_write_volatile_harness!(i64, 8, non_null_check_write_volatile_i64); - generate_write_volatile_harness!(i128, 16, non_null_check_write_volatile_i128); - generate_write_volatile_harness!( - isize, - { core::mem::size_of::() }, - non_null_check_write_volatile_isize - ); - generate_write_volatile_harness!(u8, 1, non_null_check_write_volatile_u8); - generate_write_volatile_harness!(u16, 2, non_null_check_write_volatile_u16); - generate_write_volatile_harness!(u32, 4, non_null_check_write_volatile_u32); - generate_write_volatile_harness!(u64, 8, non_null_check_write_volatile_u64); - generate_write_volatile_harness!(u128, 16, non_null_check_write_volatile_u128); - generate_write_volatile_harness!( - usize, - { core::mem::size_of::() }, - non_null_check_write_volatile_usize - ); - generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit); + generate_write_volatile_harness!(i8, non_null_check_write_volatile_i8); + generate_write_volatile_harness!(i16, non_null_check_write_volatile_i16); + generate_write_volatile_harness!(i32, non_null_check_write_volatile_i32); + generate_write_volatile_harness!(i64, non_null_check_write_volatile_i64); + generate_write_volatile_harness!(i128, non_null_check_write_volatile_i128); + generate_write_volatile_harness!(isize, non_null_check_write_volatile_isize); + generate_write_volatile_harness!(u8, non_null_check_write_volatile_u8); + generate_write_volatile_harness!(u16, non_null_check_write_volatile_u16); + generate_write_volatile_harness!(u32, non_null_check_write_volatile_u32); + generate_write_volatile_harness!(u64, non_null_check_write_volatile_u64); + generate_write_volatile_harness!(u128, non_null_check_write_volatile_u128); + generate_write_volatile_harness!(usize, non_null_check_write_volatile_usize); macro_rules! generate_write_bytes_harness { - ($type:ty, $byte_size:expr, $harness_name:ident) => { + ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract(NonNull::write_bytes)] pub fn $harness_name() { // Create a pointer generator for the given type with appropriate byte size - let mut generator = kani::PointerGenerator::<$byte_size>::new(); + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); // Get a raw pointer from the generator let raw_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2720,7 +2766,7 @@ mod verify { ptr.write_bytes(val, count); // Create a non-deterministic count - let i: usize = kani::any_where(|&x| x < count * $byte_size); + let i: usize = kani::any_where(|&x| x < count * mem::size_of::<$type>()); let ptr_byte = ptr.as_ptr() as *const u8; // Read back the value and assert it's correct @@ -2730,28 +2776,42 @@ mod verify { }; } + #[kani::proof_for_contract(NonNull::write_bytes)] + pub fn non_null_check_write_bytes_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let val: u8 = kani::any(); + + // Create a non-deterministic count + let count: usize = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_bytes(val, count); + } + } + // Generate proof harnesses for multiple types with appropriate byte sizes - generate_write_bytes_harness!(i8, 1, non_null_check_write_bytes_i8); - generate_write_bytes_harness!(i16, 2, non_null_check_write_bytes_i16); - generate_write_bytes_harness!(i32, 4, non_null_check_write_bytes_i32); - generate_write_bytes_harness!(i64, 8, non_null_check_write_bytes_i64); - generate_write_bytes_harness!(i128, 16, non_null_check_write_bytes_i128); - generate_write_bytes_harness!( - isize, - { core::mem::size_of::() }, - non_null_check_write_bytes_isize - ); - generate_write_bytes_harness!(u8, 1, non_null_check_write_bytes_u8); - generate_write_bytes_harness!(u16, 2, non_null_check_write_bytes_u16); - generate_write_bytes_harness!(u32, 4, non_null_check_write_bytes_u32); - generate_write_bytes_harness!(u64, 8, non_null_check_write_bytes_u64); - generate_write_bytes_harness!(u128, 16, non_null_check_write_bytes_u128); - generate_write_bytes_harness!( - usize, - { core::mem::size_of::() }, - non_null_check_write_bytes_usize - ); - generate_write_bytes_harness!((), 1, non_null_check_write_bytes_unit); + generate_write_bytes_harness!(i8, non_null_check_write_bytes_i8); + generate_write_bytes_harness!(i16, non_null_check_write_bytes_i16); + generate_write_bytes_harness!(i32, non_null_check_write_bytes_i32); + generate_write_bytes_harness!(i64, non_null_check_write_bytes_i64); + generate_write_bytes_harness!(i128, non_null_check_write_bytes_i128); + generate_write_bytes_harness!(isize, non_null_check_write_bytes_isize); + generate_write_bytes_harness!(u8, non_null_check_write_bytes_u8); + generate_write_bytes_harness!(u16, non_null_check_write_bytes_u16); + generate_write_bytes_harness!(u32, non_null_check_write_bytes_u32); + generate_write_bytes_harness!(u64, non_null_check_write_bytes_u64); + generate_write_bytes_harness!(u128, non_null_check_write_bytes_u128); + generate_write_bytes_harness!(usize, non_null_check_write_bytes_usize); #[kani::proof_for_contract(NonNull::byte_add)] pub fn non_null_byte_add_proof() { From ecef1bf6303084895e36b4d622b55d60ba813e4b Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 08:17:28 -0800 Subject: [PATCH 10/18] close linked-list challenge --- doc/src/challenges/0005-linked-list.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index 3bfcb87cc73a3..accdedf0f70af 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -1,10 +1,11 @@ # Challenge 5: Verify functions iterating over inductive data type: `linked_list` -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) - **Start date:** *2024/07/01* - **End date:** *2025/04/10* - **Reward:** *5,000 USD* +- **Contributors**: [Bart Jacobs](https://github.com/btj) ------------------- From bf328b263d7e1509b8e48e417801f325a75f1da9 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 14:00:02 -0800 Subject: [PATCH 11/18] fix some typos --- doc/src/challenges/0006-nonnull.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index 99af5146fcb39..4b1b73b75ccf5 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -5,7 +5,7 @@ - **Start date:** *2024/08/16* - **End date:** *2025/04/10* - **Reward:** *N/A* -- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), Dhvani Kapadia(https://github.com/Dhvani-Kapadia) and Jiun Chi Yang(https://github.com/Jimmycreative) +- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), [Dhvani Kapadia](https://github.com/Dhvani-Kapadia) and [Jiun Chi Yang](https://github.com/Jimmycreative) ------------------- From 31ea8520eb42ceb4faea7623c0839cf8f2b02305 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 14:00:27 -0800 Subject: [PATCH 12/18] close nonzero challenge --- doc/src/challenges/0012-nonzero.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index 7a42360bca183..bb43d579ac428 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -1,10 +1,11 @@ # Challenge 12: Safety of `NonZero` -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024/08/23* - **End date:** *2025/04/10* - **Reward:** *N/A* +- **Contributors**: [Aaron Lang](https://github.com/lang280), [Shivani Ghuge](https://github.com/SahithiMV) and [Alvaro Luna](https://github.com/aa-luna) ------------------- From 9c685f4d90199251afca7a7a7460d800c56c695e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 14:01:12 -0800 Subject: [PATCH 13/18] delete file --- library/Cargo.lock | 582 --------------------------------------------- 1 file changed, 582 deletions(-) delete mode 100644 library/Cargo.lock diff --git a/library/Cargo.lock b/library/Cargo.lock deleted file mode 100644 index 2eea43532f668..0000000000000 --- a/library/Cargo.lock +++ /dev/null @@ -1,582 +0,0 @@ -# This file is automatically @generated by Cargo. -# It is not intended for manual editing. -version = 4 - -[[package]] -name = "addr2line" -version = "0.24.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1" -dependencies = [ - "compiler_builtins", - "gimli", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "adler2" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", -] - -[[package]] -name = "alloc" -version = "0.0.0" -dependencies = [ - "compiler_builtins", - "core", - "rand", - "rand_xorshift", - "safety", -] - -[[package]] -name = "allocator-api2" -version = "0.2.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" - -[[package]] -name = "cc" -version = "1.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1aeb932158bd710538c73702db6945cb68a8fb08c519e6e12706b94263b36db8" -dependencies = [ - "shlex", -] - -[[package]] -name = "cfg-if" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", -] - -[[package]] -name = "compiler_builtins" -version = "0.1.145" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da0705f5abaaab7168ccc14f8f340ded61be2bd3ebea86b9834b6acbc8495de8" -dependencies = [ - "cc", - "rustc-std-workspace-core", -] - -[[package]] -name = "core" -version = "0.0.0" - -[[package]] -name = "coretests" -version = "0.0.0" -dependencies = [ - "rand", - "rand_xorshift", - "safety", -] - -[[package]] -name = "dlmalloc" -version = "0.2.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9b5e0d321d61de16390ed273b647ce51605b575916d3c25e6ddf27a1e140035" -dependencies = [ - "cfg-if", - "compiler_builtins", - "libc", - "rustc-std-workspace-core", - "windows-sys", -] - -[[package]] -name = "fortanix-sgx-abi" -version = "0.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57cafc2274c10fab234f176b25903ce17e690fca7597090d50880e047a0389c5" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", -] - -[[package]] -name = "getopts" -version = "0.2.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5" -dependencies = [ - "rustc-std-workspace-core", - "rustc-std-workspace-std", - "unicode-width", -] - -[[package]] -name = "gimli" -version = "0.31.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "hashbrown" -version = "0.15.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" -dependencies = [ - "allocator-api2", - "compiler_builtins", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "hermit-abi" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fbf6a919d6cf397374f7dfeeea91d974c7c0a7221d0d0f4f20d859d329e53fcc" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "libc" -version = "0.2.169" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a" -dependencies = [ - "rustc-std-workspace-core", -] - -[[package]] -name = "memchr" -version = "2.7.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", -] - -[[package]] -name = "miniz_oxide" -version = "0.8.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8402cab7aefae129c6977bb0ff1b8fd9a04eb5b51efc50a70bea51cda0c7924" -dependencies = [ - "adler2", - "compiler_builtins", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "object" -version = "0.36.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87" -dependencies = [ - "compiler_builtins", - "memchr", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "panic_abort" -version = "0.0.0" -dependencies = [ - "alloc", - "cfg-if", - "compiler_builtins", - "core", - "libc", -] - -[[package]] -name = "panic_unwind" -version = "0.0.0" -dependencies = [ - "alloc", - "cfg-if", - "compiler_builtins", - "core", - "libc", - "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.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60946a68e5f9d28b0dc1c21bb8a97ee7d018a8b322fa57838ba31cc878e22d99" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "proc_macro" -version = "0.0.0" -dependencies = [ - "core", - "std", -] - -[[package]] -name = "profiler_builtins" -version = "0.0.0" -dependencies = [ - "cc", -] - -[[package]] -name = "quote" -version = "1.0.38" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" -dependencies = [ - "proc-macro2", -] - -[[package]] -name = "r-efi" -version = "4.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e9e935efc5854715dfc0a4c9ef18dc69dee0ec3bf9cc3ab740db831c0fdd86a3" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", -] - -[[package]] -name = "r-efi-alloc" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "31d6f09fe2b6ad044bc3d2c34ce4979796581afd2f1ebc185837e02421e02fd7" -dependencies = [ - "compiler_builtins", - "r-efi", - "rustc-std-workspace-core", -] - -[[package]] -name = "rand" -version = "0.8.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" -dependencies = [ - "rand_core", -] - -[[package]] -name = "rand_core" -version = "0.6.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" - -[[package]] -name = "rand_xorshift" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f" -dependencies = [ - "rand_core", -] - -[[package]] -name = "rustc-demangle" -version = "0.1.24" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", -] - -[[package]] -name = "rustc-std-workspace-alloc" -version = "1.99.0" -dependencies = [ - "alloc", -] - -[[package]] -name = "rustc-std-workspace-core" -version = "1.99.0" -dependencies = [ - "core", -] - -[[package]] -name = "rustc-std-workspace-std" -version = "1.99.0" -dependencies = [ - "std", -] - -[[package]] -name = "safety" -version = "0.1.0" -dependencies = [ - "proc-macro-error", - "proc-macro2", - "quote", - "syn 2.0.98", -] - -[[package]] -name = "shlex" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" - -[[package]] -name = "std" -version = "0.0.0" -dependencies = [ - "addr2line", - "alloc", - "cfg-if", - "compiler_builtins", - "core", - "dlmalloc", - "fortanix-sgx-abi", - "hashbrown", - "hermit-abi", - "libc", - "miniz_oxide", - "object", - "panic_abort", - "panic_unwind", - "r-efi", - "r-efi-alloc", - "rand", - "rand_xorshift", - "rustc-demangle", - "safety", - "std_detect", - "unwind", - "wasi", - "windows-targets 0.0.0", -] - -[[package]] -name = "std_detect" -version = "0.1.5" -dependencies = [ - "cfg-if", - "compiler_builtins", - "libc", - "rustc-std-workspace-alloc", - "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.98" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36147f1a48ae0ec2b5b3bc5b537d267457555a10dc06f3dbc8cb11ba3006d3b1" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "sysroot" -version = "0.0.0" -dependencies = [ - "proc_macro", - "profiler_builtins", - "std", - "test", -] - -[[package]] -name = "test" -version = "0.0.0" -dependencies = [ - "core", - "getopts", - "libc", - "std", -] - -[[package]] -name = "unicode-ident" -version = "1.0.16" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a210d160f08b701c8721ba1c726c11662f877ea6b7094007e1ca9a1041945034" - -[[package]] -name = "unicode-width" -version = "0.1.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-core", - "rustc-std-workspace-std", -] - -[[package]] -name = "unwind" -version = "0.0.0" -dependencies = [ - "cfg-if", - "compiler_builtins", - "core", - "libc", - "unwinding", -] - -[[package]] -name = "unwinding" -version = "0.2.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "51f06a05848f650946acef3bf525fe96612226b61f74ae23ffa4e98bfbb8ab3c" -dependencies = [ - "compiler_builtins", - "gimli", - "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" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" -dependencies = [ - "compiler_builtins", - "rustc-std-workspace-alloc", - "rustc-std-workspace-core", -] - -[[package]] -name = "windows-sys" -version = "0.59.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets 0.52.6", -] - -[[package]] -name = "windows-targets" -version = "0.0.0" - -[[package]] -name = "windows-targets" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" -dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", -] - -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" - -[[package]] -name = "windows_aarch64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" - -[[package]] -name = "windows_i686_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" - -[[package]] -name = "windows_i686_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" - -[[package]] -name = "windows_i686_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" - -[[package]] -name = "windows_x86_64_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" - -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" - -[[package]] -name = "windows_x86_64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" From 0ca03a89aac80511de5f5a2ec2cd3018ed52f618 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 14:10:27 -0800 Subject: [PATCH 14/18] re-add file --- library/Cargo.lock | 494 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 494 insertions(+) create mode 100644 library/Cargo.lock diff --git a/library/Cargo.lock b/library/Cargo.lock new file mode 100644 index 0000000000000..8b78908e6d730 --- /dev/null +++ b/library/Cargo.lock @@ -0,0 +1,494 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "addr2line" +version = "0.24.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1" +dependencies = [ + "compiler_builtins", + "gimli", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "adler2" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", +] + +[[package]] +name = "alloc" +version = "0.0.0" +dependencies = [ + "compiler_builtins", + "core", + "rand", + "rand_xorshift", +] + +[[package]] +name = "allocator-api2" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" + +[[package]] +name = "cc" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1aeb932158bd710538c73702db6945cb68a8fb08c519e6e12706b94263b36db8" +dependencies = [ + "shlex", +] + +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", +] + +[[package]] +name = "compiler_builtins" +version = "0.1.145" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da0705f5abaaab7168ccc14f8f340ded61be2bd3ebea86b9834b6acbc8495de8" +dependencies = [ + "cc", + "rustc-std-workspace-core", +] + +[[package]] +name = "core" +version = "0.0.0" + +[[package]] +name = "coretests" +version = "0.0.0" +dependencies = [ + "rand", + "rand_xorshift", +] + +[[package]] +name = "dlmalloc" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b5e0d321d61de16390ed273b647ce51605b575916d3c25e6ddf27a1e140035" +dependencies = [ + "cfg-if", + "compiler_builtins", + "libc", + "rustc-std-workspace-core", + "windows-sys", +] + +[[package]] +name = "fortanix-sgx-abi" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57cafc2274c10fab234f176b25903ce17e690fca7597090d50880e047a0389c5" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", +] + +[[package]] +name = "getopts" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5" +dependencies = [ + "rustc-std-workspace-core", + "rustc-std-workspace-std", + "unicode-width", +] + +[[package]] +name = "gimli" +version = "0.31.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "hashbrown" +version = "0.15.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" +dependencies = [ + "allocator-api2", + "compiler_builtins", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "hermit-abi" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fbf6a919d6cf397374f7dfeeea91d974c7c0a7221d0d0f4f20d859d329e53fcc" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "libc" +version = "0.2.169" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a" +dependencies = [ + "rustc-std-workspace-core", +] + +[[package]] +name = "memchr" +version = "2.7.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", +] + +[[package]] +name = "miniz_oxide" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8402cab7aefae129c6977bb0ff1b8fd9a04eb5b51efc50a70bea51cda0c7924" +dependencies = [ + "adler2", + "compiler_builtins", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "object" +version = "0.36.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87" +dependencies = [ + "compiler_builtins", + "memchr", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "panic_abort" +version = "0.0.0" +dependencies = [ + "alloc", + "cfg-if", + "compiler_builtins", + "core", + "libc", +] + +[[package]] +name = "panic_unwind" +version = "0.0.0" +dependencies = [ + "alloc", + "cfg-if", + "compiler_builtins", + "core", + "libc", + "unwind", +] + +[[package]] +name = "proc_macro" +version = "0.0.0" +dependencies = [ + "core", + "std", +] + +[[package]] +name = "profiler_builtins" +version = "0.0.0" +dependencies = [ + "cc", +] + +[[package]] +name = "r-efi" +version = "4.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9e935efc5854715dfc0a4c9ef18dc69dee0ec3bf9cc3ab740db831c0fdd86a3" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", +] + +[[package]] +name = "r-efi-alloc" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "31d6f09fe2b6ad044bc3d2c34ce4979796581afd2f1ebc185837e02421e02fd7" +dependencies = [ + "compiler_builtins", + "r-efi", + "rustc-std-workspace-core", +] + +[[package]] +name = "rand" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +dependencies = [ + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" + +[[package]] +name = "rand_xorshift" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f" +dependencies = [ + "rand_core", +] + +[[package]] +name = "rustc-demangle" +version = "0.1.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", +] + +[[package]] +name = "rustc-std-workspace-alloc" +version = "1.99.0" +dependencies = [ + "alloc", +] + +[[package]] +name = "rustc-std-workspace-core" +version = "1.99.0" +dependencies = [ + "core", +] + +[[package]] +name = "rustc-std-workspace-std" +version = "1.99.0" +dependencies = [ + "std", +] + +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "std" +version = "0.0.0" +dependencies = [ + "addr2line", + "alloc", + "cfg-if", + "compiler_builtins", + "core", + "dlmalloc", + "fortanix-sgx-abi", + "hashbrown", + "hermit-abi", + "libc", + "miniz_oxide", + "object", + "panic_abort", + "panic_unwind", + "r-efi", + "r-efi-alloc", + "rand", + "rand_xorshift", + "rustc-demangle", + "std_detect", + "unwind", + "wasi", + "windows-targets 0.0.0", +] + +[[package]] +name = "std_detect" +version = "0.1.5" +dependencies = [ + "cfg-if", + "compiler_builtins", + "libc", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "sysroot" +version = "0.0.0" +dependencies = [ + "proc_macro", + "profiler_builtins", + "std", + "test", +] + +[[package]] +name = "test" +version = "0.0.0" +dependencies = [ + "core", + "getopts", + "libc", + "std", +] + +[[package]] +name = "unicode-width" +version = "0.1.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-core", + "rustc-std-workspace-std", +] + +[[package]] +name = "unwind" +version = "0.0.0" +dependencies = [ + "cfg-if", + "compiler_builtins", + "core", + "libc", + "unwinding", +] + +[[package]] +name = "unwinding" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "51f06a05848f650946acef3bf525fe96612226b61f74ae23ffa4e98bfbb8ab3c" +dependencies = [ + "compiler_builtins", + "gimli", + "rustc-std-workspace-core", +] + +[[package]] +name = "wasi" +version = "0.11.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" +dependencies = [ + "compiler_builtins", + "rustc-std-workspace-alloc", + "rustc-std-workspace-core", +] + +[[package]] +name = "windows-sys" +version = "0.59.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" +dependencies = [ + "windows-targets 0.52.6", +] + +[[package]] +name = "windows-targets" +version = "0.0.0" + +[[package]] +name = "windows-targets" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_gnullvm", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" From d21014ae6b6e81f961a1c378e2aafdf90e962b5b Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 15:31:32 -0800 Subject: [PATCH 15/18] reduce ARR_SIZE write_bytes harness --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 776d0a510444e..aa8b6f8e17535 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -2746,7 +2746,7 @@ mod verify { #[kani::proof_for_contract(NonNull::write_bytes)] pub fn $harness_name() { // Create a pointer generator for the given type with appropriate byte size - const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + const ARR_SIZE: usize = mem::size_of::<$type>() * 10; let mut generator = kani::PointerGenerator::::new(); // Get a raw pointer from the generator From 1af74838b91d5d1db3cd06301f1743a2d102c079 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 17 Mar 2025 11:01:31 -0700 Subject: [PATCH 16/18] Update library/core/src/ptr/non_null.rs Co-authored-by: Carolyn Zech --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index aa8b6f8e17535..625db457f5261 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1236,7 +1236,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(self.as_ptr(), count)))] #[requires( - count.checked_mul(core::mem::size_of::() as usize).is_some_and(|x| x.wrapping_add(self.as_ptr() as usize) <= isize::MAX as usize) && + count.checked_mul(core::mem::size_of::() as usize).is_some_and(|byte_count| byte_count.wrapping_add(self.as_ptr() as usize) <= isize::MAX as usize) && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count)) )] #[ensures(|_| From ae10478a509da199353ada709ed14aebf7086d13 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 17 Mar 2025 11:06:20 -0700 Subject: [PATCH 17/18] change NonZero back to Open --- doc/src/challenges/0012-nonzero.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index bb43d579ac428..7a42360bca183 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -1,11 +1,10 @@ # Challenge 12: Safety of `NonZero` -- **Status:** Resolved +- **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024/08/23* - **End date:** *2025/04/10* - **Reward:** *N/A* -- **Contributors**: [Aaron Lang](https://github.com/lang280), [Shivani Ghuge](https://github.com/SahithiMV) and [Alvaro Luna](https://github.com/aa-luna) ------------------- From c320681e03887394d63b02876d9f90d5bae43c55 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 20 Mar 2025 09:38:27 -0700 Subject: [PATCH 18/18] change the Status of Linklist back to open --- doc/src/challenges/0005-linked-list.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index accdedf0f70af..3bfcb87cc73a3 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -1,11 +1,10 @@ # Challenge 5: Verify functions iterating over inductive data type: `linked_list` -- **Status:** Resolved +- **Status:** Open - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) - **Start date:** *2024/07/01* - **End date:** *2025/04/10* - **Reward:** *5,000 USD* -- **Contributors**: [Bart Jacobs](https://github.com/btj) -------------------