Merge branch 'main' into strIterchallenges

Author: thanhnguyen-aws

.github/workflows/update-subtree.yml

@@ -117,6 +117,10 @@ jobs:
         git remote add rust-filtered ../rust-tmp/
         git fetch rust-filtered
         git checkout -b subtree/library rust-filtered/subtree/library
+        # The checkout still leaves behind the library folder with submodules.
+        # We need to remove this as we'd otherwise have the create-pull-request
+        # action create an extra commit.
+        rm -rf library
         SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
         UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
         UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)

doc/mdbook-metrics/src/main.rs

@@ -44,6 +44,25 @@ fn run_kani_metrics_script() -> Result<(), Error> {
     Command::new("python")
         .args(&[
             "kani_std_analysis.py",
+            "--crate",
+            "core",
+            "--metrics-file",
+            "metrics-data-core.json",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--crate",
+            "std",
+            "--metrics-file",
+            "metrics-data-std.json",
             "--plot-only",
             "--plot-dir",
             &tools_path.to_string_lossy(),
@@ -83,12 +102,19 @@ fn add_graphs(chapter: &mut Chapter) {
 
 Note that these metrics are for x86-64 architectures.
 
-## `core`
+### `core`
 ![Unsafe Metrics](core_unsafe_metrics.png)
 
 ![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
 
 ![Safe Metrics](core_safe_metrics.png)
+
+### `std`
+![Unsafe Metrics](std_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](std_safe_abstractions_metrics.png)
+
+![Safe Metrics](std_safe_metrics.png)
 "#;
 
     chapter.content.push_str(new_content);

doc/src/challenges/0006-nonnull.md

@@ -1,11 +1,11 @@
 # 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*
 - **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)
 -------------------
 
 

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.
 

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
 

doc/src/challenges/0014-convert-num.md

@@ -1,11 +1,11 @@
 # Challenge 14: Safety of Primitive Conversions
 
-- **Status:** Open
-- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220
+- **Status:** Resolved
+- **Tracking Issue:** [#220](https://github.com/model-checking/verify-rust-std/issues/220)
 - **Start date:** 2024/12/15
 - **End date:** 2025/2/28
 - **Prize:** *TBD*
-
+- **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
 -------------------
 
 ## Goal

doc/src/challenges/0015-intrinsics-simd.md

@@ -3,7 +3,7 @@
 - **Status:** Open
 - **Reward:** 
 - **Solution:** 
-- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/173
+- **Tracking Issue:** [#173](https://github.com/model-checking/verify-rust-std/issues/173)
 - **Start date:** 2025/02/01
 - **End date:** 2025/08/01
 

library/Cargo.lock

@@ -4,6 +4,7 @@ members = [
   "std",
   "sysroot",
   "coretests",
+  "alloctests",
 ]
 
 exclude = [

library/Cargo.toml

@@ -1,3 +1,5 @@
+cargo-features = ["public-dependency"]
+
 [package]
 name = "alloc"
 version = "0.0.0"
@@ -6,35 +8,17 @@ repository = "https://github.com/rust-lang/rust.git"
 description = "The Rust core allocation and collections library"
 autotests = false
 autobenches = false
-edition = "2021"
+edition = "2024"
+
+[lib]
+test = false
+bench = false
 
 [dependencies]
-core = { path = "../core" }
-compiler_builtins = { version = "=0.1.145", features = ['rustc-dep-of-std'] }
+core = { path = "../core", public = true }
+compiler_builtins = { version = "=0.1.151", features = ['rustc-dep-of-std'] }
 safety = { path = "../contracts/safety" }
 
-[dev-dependencies]
-rand = { version = "0.8.5", default-features = false, features = ["alloc"] }
-rand_xorshift = "0.3.0"
-
-[[test]]
-name = "alloctests"
-path = "tests/lib.rs"
-
-[[test]]
-name = "vec_deque_alloc_error"
-path = "tests/vec_deque_alloc_error.rs"
-
-[[bench]]
-name = "allocbenches"
-path = "benches/lib.rs"
-test = true
-
-[[bench]]
-name = "vec_deque_append_bench"
-path = "benches/vec_deque_append.rs"
-harness = false
-
 [features]
 compiler-builtins-mem = ['compiler_builtins/mem']
 compiler-builtins-c = ["compiler_builtins/c"]