Merge branch 'main' into main

Author: karthikbhargavan

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "ebafb8d0ca32d8c0fcd2a0cfef6b1b4bd4dc4a6f"
+  FLUX_VERSION: "a17246965a8752e3d3d4e3559865311048bb61f7"
 
 jobs:
   check-flux-on-core:

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*
+- **End date:** *2025/08/12*
 - **Reward:** *5,000 USD*
+- **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------
 

doc/src/challenges/0019-rawvec.md

@@ -1,10 +1,11 @@
-# Challenge 25: Verify the safety of `RawVec` functions
+# Challenge 19: Verify the safety of `RawVec` functions
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
+- **End date:** *2025-08-12*
 - **Reward:** *10000 USD*
+- **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------
 

library/Cargo.lock

@@ -1672,7 +1672,7 @@ unsafe impl<#[may_dangle] T: ?Sized, A: Allocator> Drop for Box<T, A> {
 #[cfg(not(no_global_oom_handling))]
 #[stable(feature = "rust1", since = "1.0.0")]
 impl<T: Default> Default for Box<T> {
-    /// Creates a `Box<T>`, with the `Default` value for T.
+    /// Creates a `Box<T>`, with the `Default` value for `T`.
     #[inline]
     fn default() -> Self {
         let mut x: Box<mem::MaybeUninit<T>> = Box::new_uninit();
@@ -1695,6 +1695,7 @@ impl<T: Default> Default for Box<T> {
 #[cfg(not(no_global_oom_handling))]
 #[stable(feature = "rust1", since = "1.0.0")]
 impl<T> Default for Box<[T]> {
+    /// Creates an empty `[T]` inside a `Box`.
     #[inline]
     fn default() -> Self {
         let ptr: Unique<[T]> = Unique::<[T; 0]>::dangling();
@@ -1716,6 +1717,19 @@ impl Default for Box<str> {
     }
 }
 
+#[cfg(not(no_global_oom_handling))]
+#[stable(feature = "pin_default_impls", since = "CURRENT_RUSTC_VERSION")]
+impl<T> Default for Pin<Box<T>>
+where
+    T: ?Sized,
+    Box<T>: Default,
+{
+    #[inline]
+    fn default() -> Self {
+        Box::into_pin(Box::<T>::default())
+    }
+}
+
 #[cfg(not(no_global_oom_handling))]
 #[stable(feature = "rust1", since = "1.0.0")]
 impl<T: Clone, A: Allocator + Clone> Clone for Box<T, A> {

library/alloc/src/boxed.rs

@@ -135,6 +135,8 @@ pub(super) const MIN_LEN: usize = node::MIN_LEN_AFTER_SPLIT;
 /// ]);
 /// ```
 ///
+/// ## `Entry` API
+///
 /// `BTreeMap` implements an [`Entry API`], which allows for complex
 /// methods of getting, setting, updating and removing keys and their values:
 ///

library/alloc/src/collections/btree/map.rs

@@ -1099,7 +1099,7 @@ impl From<&CStr> for CString {
     }
 }
 
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<CStr> for CString {
     #[inline]
     fn eq(&self, other: &CStr) -> bool {
@@ -1112,7 +1112,7 @@ impl PartialEq<CStr> for CString {
     }
 }
 
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<&CStr> for CString {
     #[inline]
     fn eq(&self, other: &&CStr) -> bool {
@@ -1126,7 +1126,7 @@ impl PartialEq<&CStr> for CString {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<Cow<'_, CStr>> for CString {
     #[inline]
     fn eq(&self, other: &Cow<'_, CStr>) -> bool {
@@ -1221,7 +1221,7 @@ impl CStr {
     }
 }
 
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<CString> for CStr {
     #[inline]
     fn eq(&self, other: &CString) -> bool {
@@ -1235,7 +1235,7 @@ impl PartialEq<CString> for CStr {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<Cow<'_, Self>> for CStr {
     #[inline]
     fn eq(&self, other: &Cow<'_, Self>) -> bool {
@@ -1249,7 +1249,7 @@ impl PartialEq<Cow<'_, Self>> for CStr {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<CStr> for Cow<'_, CStr> {
     #[inline]
     fn eq(&self, other: &CStr) -> bool {
@@ -1263,7 +1263,7 @@ impl PartialEq<CStr> for Cow<'_, CStr> {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<&CStr> for Cow<'_, CStr> {
     #[inline]
     fn eq(&self, other: &&CStr) -> bool {
@@ -1277,7 +1277,7 @@ impl PartialEq<&CStr> for Cow<'_, CStr> {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
 impl PartialEq<CString> for Cow<'_, CStr> {
     #[inline]
     fn eq(&self, other: &CString) -> bool {

library/alloc/src/ffi/c_str.rs

@@ -103,6 +103,7 @@
 #![feature(async_iterator)]
 #![feature(bstr)]
 #![feature(bstr_internals)]
+#![feature(cast_maybe_uninit)]
 #![feature(char_internals)]
 #![feature(char_max_len)]
 #![feature(clone_to_uninit)]

library/alloc/src/lib.rs

@@ -2357,7 +2357,7 @@ impl<T: Default> Default for Rc<T> {
     /// assert_eq!(*x, 0);
     /// ```
     #[inline]
-    fn default() -> Rc<T> {
+    fn default() -> Self {
         unsafe {
             Self::from_inner(
                 Box::leak(Box::write(
@@ -2373,7 +2373,7 @@ impl<T: Default> Default for Rc<T> {
 #[cfg(not(no_global_oom_handling))]
 #[stable(feature = "more_rc_default_impls", since = "1.80.0")]
 impl Default for Rc<str> {
-    /// Creates an empty str inside an Rc
+    /// Creates an empty `str` inside an `Rc`.
     ///
     /// This may or may not share an allocation with other Rcs on the same thread.
     #[inline]
@@ -2387,7 +2387,7 @@ impl Default for Rc<str> {
 #[cfg(not(no_global_oom_handling))]
 #[stable(feature = "more_rc_default_impls", since = "1.80.0")]
 impl<T> Default for Rc<[T]> {
-    /// Creates an empty `[T]` inside an Rc
+    /// Creates an empty `[T]` inside an `Rc`.
     ///
     /// This may or may not share an allocation with other Rcs on the same thread.
     #[inline]
@@ -2397,6 +2397,19 @@ impl<T> Default for Rc<[T]> {
     }
 }
 
+#[cfg(not(no_global_oom_handling))]
+#[stable(feature = "pin_default_impls", since = "CURRENT_RUSTC_VERSION")]
+impl<T> Default for Pin<Rc<T>>
+where
+    T: ?Sized,
+    Rc<T>: Default,
+{
+    #[inline]
+    fn default() -> Self {
+        unsafe { Pin::new_unchecked(Rc::<T>::default()) }
+    }
+}
+
 #[stable(feature = "rust1", since = "1.0.0")]
 trait RcEqIdent<T: ?Sized + PartialEq, A: Allocator> {
     fn eq(&self, other: &Rc<T, A>) -> bool;

library/alloc/src/rc.rs

@@ -3654,6 +3654,19 @@ impl<T> Default for Arc<[T]> {
     }
 }
 
+#[cfg(not(no_global_oom_handling))]
+#[stable(feature = "pin_default_impls", since = "CURRENT_RUSTC_VERSION")]
+impl<T> Default for Pin<Arc<T>>
+where
+    T: ?Sized,
+    Arc<T>: Default,
+{
+    #[inline]
+    fn default() -> Self {
+        unsafe { Pin::new_unchecked(Arc::<T>::default()) }
+    }
+}
+
 #[stable(feature = "rust1", since = "1.0.0")]
 impl<T: ?Sized + Hash, A: Allocator> Hash for Arc<T, A> {
     fn hash<H: Hasher>(&self, state: &mut H) {