Merge remote-tracking branch 'origin/main' into nonnull-challenge

.github/TOOL_REQUEST_TEMPLATE.md

@@ -0,0 +1,31 @@
+_The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be **supported** if it is to be included._
+
+## Tool Name
+_Please enter your tool name here._
+
+## Description
+_Please enter a description for your tool and any information you deem relevant._
+
+## Tool Information
+
+* [ ] Does the tool perform Rust verification? 
+* [ ] Does the tool deal with *unsafe* Rust code? 
+* [ ] Does the tool run independently in CI? 
+* [ ] Is the tool open source?
+* [ ] Is the tool under development? 
+* [ ] Will you or your team be able to provide support for the tool?
+
+## Licenses
+_Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s)._
+
+## Steps to Use the Tool
+
+1. [First Step]
+2. [Second Step]
+3. [and so on...]
+
+## Artifacts
+_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._
+
+## CI & Versioning
+_Please describe how you version the tool and how it will be supported in CI pipelines._

.github/pull_requests.toml

@@ -9,5 +9,8 @@ members = [
     "remi-delmas-3000",
     "qinheping",
     "tautschnig",
-    "jaisnan"
+    "jaisnan",
+    "patricklam",
+    "ranjitjhala",
+    "carolynzech"
 ]

README.md

@@ -7,7 +7,8 @@
 This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official
-Rust releases.
+Rust releases. The repository is tool agnostic and welcomes the addition of 
+new tools.
 
 The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
 1. Contributing to the core mechanism of verifying the rust standard library
@@ -36,12 +37,14 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
 ## License
 
 ### Kani
-
 Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details.
 
 ## Rust
-
 Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
 
 See [the Rust repository](https://github.com/rust-lang/rust) for details.
+
+## Introducing a New Tool
+
+Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.

doc/src/SUMMARY.md

@@ -19,3 +19,5 @@
   - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
   - [Inductive data type](./challenges/0005-linked-list.md)
   - [Safety of NonNull](./challenges/0006-nonnull.md)
+  - [Contracts for SmallSort](./challenges/0008-smallsort.md)
+  - [Memory safety of String](./challenges/0010-string.md)

doc/src/challenges/0008-smallsort.md

@@ -0,0 +1,54 @@
+# Challenge 8: Contracts for SmallSort
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/56)
+- **Start date:** *2024-08-17*
+- **End date:** *2024-12-10*
+
+-------------------
+
+
+## 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.
+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.
+
+### Success Criteria
+
+Prove absence of undefined behavior of the following public functions.
+
+1. `<T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort`
+2. `<T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort`
+3. `<T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort`
+4. `slice::sort::shared::smallsort::swap_if_less`
+5. `slice::sort::shared::smallsort::insertion_sort_shift_left`
+6. `slice::sort::shared::smallsort::sort4_stable`
+7. `slice::sort::shared::smallsort::has_efficient_in_place_swap`
+
+Write contracts for the following public functions that show that they actually sort the slices.
+
+1. `<T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort`
+2. `<T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort`
+3. `<T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort`
+
+The memory safety and the contracts of the above listed functions must be verified
+for all possible slices with arbitrary valid length.
+
+Note that most of the functions listed above call functions that contain loops.
+Function contracts and loop contracts of those callee functions may be required.
+
+### List of UBs
+
+In addition to any properties called out as `SAFETY` comments in the source
+code,
+all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

doc/src/challenges/0010-string.md

@@ -0,0 +1,75 @@
+# Challenge 10: Memory safety of String
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61)
+- **Start date:** *2024-08-19*
+- **End date:** *2024-12-10*
+
+-------------------
+
+## Goal
+
+In this challenge, the goal is to verify the memory safety of `std::string::String`.
+Even though the majority of `String` methods are safe, many of them are safe abstractions over unsafe code.
+
+For instance, the `insert` method is implemented as follows in v1.80.1:
+```rust
+pub fn insert(&mut self, idx: usize, ch: char) {
+    assert!(self.is_char_boundary(idx));
+    let mut bits = [0; 4];
+    let bits = ch.encode_utf8(&mut bits).as_bytes();
+
+    unsafe {
+        self.insert_bytes(idx, bits);
+    }
+}
+```
+where `insert_bytes` has the following implementation:
+```rust
+unsafe fn insert_bytes(&mut self, idx: usize, bytes: &[u8]) {
+    let len = self.len();
+    let amt = bytes.len();
+    self.vec.reserve(amt);
+
+    unsafe {
+        ptr::copy(self.vec.as_ptr().add(idx), self.vec.as_mut_ptr().add(idx + amt), len - idx);
+        ptr::copy_nonoverlapping(bytes.as_ptr(), self.vec.as_mut_ptr().add(idx), amt);
+        self.vec.set_len(len + amt);
+    }
+}
+```
+The call to the unsafe `insert_bytes` method (which itself contains unsafe code) makes `insert` susceptible to undefined behavior.
+
+### Success Criteria
+
+Verify the memory safety of all public functions that are safe abstractions over unsafe code:
+
+1. `from_utf16le` (unbounded)
+1. `from_utf16le_lossy`(unbounded)
+1. `from_utf16be` (unbounded)
+1. `from_utf16be_lossy` (unbounded)
+1. `pop`
+1. `remove`
+1. `remove_matches` (unbounded)
+1. `retain` (unbounded)
+1. `insert`
+1. `insert_str` (unbounded)
+1. `split_off` (unbounded)
+1. `drain`
+1. `replace_range` (unbounded)
+1. `into_boxed_str`
+1. `leak`
+
+Ones marked as unbounded must be verified for any string/slice length.
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

library/core/src/ptr/alignment.rs

@@ -1,4 +1,4 @@
-use safety::requires;
+use safety::{ensures, requires};
 use crate::num::NonZero;
 #[cfg(debug_assertions)]
 use crate::ub_checks::assert_unsafe_precondition;
@@ -48,6 +48,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(mem::align_of::<T>().is_power_of_two())]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const fn of<T>() -> Self {
         // SAFETY: rustc ensures that type alignment is always a power of two.
         unsafe { Alignment::new_unchecked(mem::align_of::<T>()) }
@@ -60,6 +62,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| align.is_power_of_two() == result.is_some())]
+    #[ensures(|result| result.is_none() || result.unwrap().as_usize() == align)]
     pub const fn new(align: usize) -> Option<Self> {
         if align.is_power_of_two() {
             // SAFETY: Just checked it only has one bit set
@@ -80,8 +84,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
-    #[requires(align > 0)]
-    #[requires((align & (align - 1)) == 0)]
+    #[requires(align > 0 && (align & (align - 1)) == 0)]
+    #[ensures(|result| result.as_usize() == align)]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(
@@ -99,6 +104,7 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| result.is_power_of_two())]
     pub const fn as_usize(self) -> usize {
         self.0 as usize
     }
@@ -107,6 +113,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| result.get().is_power_of_two())]
+    #[ensures(|result| result.get() == self.as_usize())]
     pub const fn as_nonzero(self) -> NonZero<usize> {
         // SAFETY: All the discriminants are non-zero.
         unsafe { NonZero::new_unchecked(self.as_usize()) }
@@ -128,6 +136,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(self.as_usize().is_power_of_two())]
+    #[ensures(|result| (*result as usize) < mem::size_of::<usize>() * 8)]
+    #[ensures(|result| 1usize << *result == self.as_usize())]
     pub const fn log2(self) -> u32 {
         self.as_nonzero().trailing_zeros()
     }
@@ -158,6 +169,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| *result > 0)]
+    #[ensures(|result| *result == !(self.as_usize() -1))]
+    #[ensures(|result| self.as_usize() & *result == self.as_usize())]
     pub const fn mask(self) -> usize {
         // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
         !(unsafe { self.as_usize().unchecked_sub(1) })
@@ -370,3 +384,68 @@ enum AlignmentEnum {
     _Align1Shl62 = 1 << 62,
     _Align1Shl63 = 1 << 63,
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    impl kani::Arbitrary for Alignment {
+        fn any() -> Self {
+            let align = kani::any_where(|a: &usize| a.is_power_of_two());
+            unsafe { mem::transmute::<usize, Alignment>(align) }
+        }
+    }
+
+    // pub const fn of<T>() -> Self
+    #[kani::proof_for_contract(Alignment::of)]
+    pub fn check_of_i32() {
+        let _ = Alignment::of::<i32>();
+    }
+
+    // pub const fn new(align: usize) -> Option<Self>
+    #[kani::proof_for_contract(Alignment::new)]
+    pub fn check_new() {
+        let a = kani::any::<usize>();
+        let _ = Alignment::new(a);
+    }
+
+    // pub const unsafe fn new_unchecked(align: usize) -> Self
+    #[kani::proof_for_contract(Alignment::new_unchecked)]
+    pub fn check_new_unchecked() {
+        let a = kani::any::<usize>();
+        unsafe {
+            let _ = Alignment::new_unchecked(a);
+        }
+    }
+
+    // pub const fn as_usize(self) -> usize
+    #[kani::proof_for_contract(Alignment::as_usize)]
+    pub fn check_as_usize() {
+        let a = kani::any::<usize>();
+        if let Some(alignment) = Alignment::new(a) {
+            assert_eq!(alignment.as_usize(), a);
+        }
+    }
+
+    // pub const fn as_nonzero(self) -> NonZero<usize>
+    #[kani::proof_for_contract(Alignment::as_nonzero)]
+    pub fn check_as_nonzero() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.as_nonzero();
+    }
+
+    // pub const fn log2(self) -> u32
+    #[kani::proof_for_contract(Alignment::log2)]
+    pub fn check_log2() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.log2();
+    }
+
+    // pub const fn mask(self) -> usize
+    #[kani::proof_for_contract(Alignment::mask)]
+    pub fn check_mask() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.mask();
+    }
+}