Port all viable contracts from verify-rust-std

library/alloc/src/collections/vec_deque/iter.rs

@@ -144,6 +144,8 @@ impl<'a, T> Iterator for Iter<'a, T> {
     }
 
     #[inline]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // Safety: The TrustedRandomAccess contract requires that callers only pass an index
         // that is in bounds.

library/alloc/src/collections/vec_deque/iter_mut.rs

@@ -208,6 +208,8 @@ impl<'a, T> Iterator for IterMut<'a, T> {
     }
 
     #[inline]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // Safety: The TrustedRandomAccess contract requires that callers only pass an index
         // that is in bounds.

library/alloc/src/lib.rs

@@ -104,6 +104,7 @@
 #![feature(const_default)]
 #![feature(const_eval_select)]
 #![feature(const_heap)]
+#![feature(contracts)]
 #![feature(core_intrinsics)]
 #![feature(deprecated_suggestion)]
 #![feature(deref_pure_trait)]

library/alloc/src/vec/into_iter.rs

@@ -354,6 +354,8 @@ impl<T, A: Allocator> Iterator for IntoIter<T, A> {
         R::from_output(accum)
     }
 
+    #[allow(unused_parens)]
+    #[core::contracts::requires(i < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, i: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,

library/core/src/alloc/layout.rs

@@ -66,6 +66,14 @@ impl Layout {
     #[stable(feature = "alloc_layout", since = "1.28.0")]
     #[rustc_const_stable(feature = "const_alloc_layout_size_align", since = "1.50.0")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(
+        move |result: &Result<Self, LayoutError>|
+        result.is_err() || (
+            align.is_power_of_two() &&
+            size <= isize::MAX as usize - (align - 1) &&
+            result.as_ref().unwrap().size() == size &&
+            result.as_ref().unwrap().align() == align))]
     pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError> {
         if Layout::is_size_align_valid(size, align) {
             // SAFETY: Layout::is_size_align_valid checks the preconditions for this call.
@@ -127,6 +135,11 @@ impl Layout {
     #[must_use]
     #[inline]
     #[track_caller]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(Layout::from_size_align(size, align).is_ok())]
+    #[core::contracts::ensures(
+        move |result: &Self| result.size() == size && result.align() == align)]
     pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
         assert_unsafe_precondition!(
             check_library_ub,
@@ -167,6 +180,10 @@ impl Layout {
     #[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")]
     #[must_use]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(
+        |result: &Self|
+        result.size() == mem::size_of::<T>() && result.align() == mem::align_of::<T>())]
     pub const fn new<T>() -> Self {
         let (size, align) = size_align::<T>();
         // SAFETY: if the type is instantiated, rustc already ensures that its
@@ -182,6 +199,11 @@ impl Layout {
     #[rustc_const_stable(feature = "const_alloc_layout", since = "1.85.0")]
     #[must_use]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(mem::align_of_val(t).is_power_of_two())]
+    // FIXME: requires `&self` to be `'static`
+    // #[core::contracts::ensures(move |result: &Self| result.align() == mem::align_of_val(t))]
     pub const fn for_value<T: ?Sized>(t: &T) -> Self {
         let (size, align) = (size_of_val(t), align_of_val(t));
         // SAFETY: see rationale in `new` for why this is using the unsafe variant
@@ -217,6 +239,8 @@ impl Layout {
     /// [extern type]: ../../unstable-book/language-features/extern-types.html
     #[unstable(feature = "layout_for_ptr", issue = "69835")]
     #[must_use]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(|result: &Self| result.align().is_power_of_two())]
     pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
         // SAFETY: we pass along the prerequisites of these functions to the caller
         let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) };
@@ -233,6 +257,8 @@ impl Layout {
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[must_use]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(|result: &NonNull<u8>| result.is_aligned())]
     pub const fn dangling(&self) -> NonNull<u8> {
         NonNull::without_provenance(self.align.as_nonzero())
     }
@@ -254,6 +280,12 @@ impl Layout {
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[rustc_const_stable(feature = "const_alloc_layout", since = "1.85.0")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(
+        move |result: &Result<Self, LayoutError>|
+        result.is_err() || (
+            result.as_ref().unwrap().align() >= align &&
+            result.as_ref().unwrap().align().is_power_of_two()))]
     pub const fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
         if let Some(align) = Alignment::new(align) {
             Layout::from_size_alignment(self.size, Alignment::max(self.align, align))
@@ -282,6 +314,8 @@ impl Layout {
     #[must_use = "this returns the padding needed, \
                   without modifying the `Layout`"]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(move |result| *result <= align)]
     pub const fn padding_needed_for(&self, align: usize) -> usize {
         // FIXME: Can we just change the type on this to `Alignment`?
         let Some(align) = Alignment::new(align) else { return usize::MAX };
@@ -331,6 +365,14 @@ impl Layout {
     #[must_use = "this returns a new `Layout`, \
                   without modifying the original"]
     #[inline]
+    // FIXME: requires `&self` to be `'static`
+    // #[rustc_allow_const_fn_unstable(contracts)]
+    // #[core::contracts::ensures(
+    //     move |result: &Layout|
+    //     result.size() >= self.size() &&
+    //     result.align() == self.align() &&
+    //     result.size() % result.align() == 0 &&
+    //     self.size() + self.padding_needed_for(self.align()) == result.size())]
     pub const fn pad_to_align(&self) -> Layout {
         // This cannot overflow. Quoting from the invariant of Layout:
         // > `size`, when rounded up to the nearest multiple of `align`,
@@ -371,6 +413,12 @@ impl Layout {
     /// ```
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(
+        move |result: &Result<(Self, usize), LayoutError>|
+        result.is_err() || (
+            (n == 0 || result.as_ref().unwrap().0.size() % n == 0) &&
+            result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1))]
     pub const fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
         let padded = self.pad_to_align();
         if let Ok(repeated) = padded.repeat_packed(n) {
@@ -428,6 +476,15 @@ impl Layout {
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[rustc_const_stable(feature = "const_alloc_layout", since = "1.85.0")]
     #[inline]
+    // FIXME: requires `&self` to be `'static`
+    // #[rustc_allow_const_fn_unstable(contracts)]
+    // #[core::contracts::ensures(
+    //     move |result: &Result<(Self, usize), LayoutError>|
+    //     result.is_err() || (
+    //         result.as_ref().unwrap().0.align() == cmp::max(self.align(), next.align()) &&
+    //         result.as_ref().unwrap().0.size() >= self.size() + next.size() &&
+    //         result.as_ref().unwrap().1 >= self.size() &&
+    //         result.as_ref().unwrap().1 <= result.as_ref().unwrap().0.size()))]
     pub const fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> {
         let new_align = Alignment::max(self.align, next.align);
         let offset = self.size_rounded_up_to_custom_align(next.align);
@@ -459,6 +516,13 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    // FIXME: requires `&self` to be `'static`
+    // #[rustc_allow_const_fn_unstable(contracts)]
+    // #[core::contracts::ensures(
+    //     move |result: &Result<Self, LayoutError>|
+    //     result.is_err() || (
+    //         result.as_ref().unwrap().size() == n * self.size() &&
+    //         result.as_ref().unwrap().align() == self.align()))]
     pub const fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
         if let Some(size) = self.size.checked_mul(n) {
             // The safe constructor is called here to enforce the isize size limit.
@@ -476,6 +540,13 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
+    // FIXME: requires `&self` to be `'static`
+    // #[rustc_allow_const_fn_unstable(contracts)]
+    // #[core::contracts::ensures(
+    //     move |result: &Result<Self, LayoutError>|
+    //     result.is_err() || (
+    //         result.as_ref().unwrap().size() == self.size() + next.size() &&
+    //         result.as_ref().unwrap().align() == self.align()))]
     pub const fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {
         // SAFETY: each `size` is at most `isize::MAX == usize::MAX/2`, so the
         // sum is at most `usize::MAX/2*2 == usize::MAX - 1`, and cannot overflow.
@@ -491,6 +562,12 @@ impl Layout {
     #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
     #[rustc_const_stable(feature = "const_alloc_layout", since = "1.85.0")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(
+        move |result: &Result<Self, LayoutError>|
+        result.is_err() || (
+            result.as_ref().unwrap().size() == n * mem::size_of::<T>() &&
+            result.as_ref().unwrap().align() == mem::align_of::<T>()))]
     pub const fn array<T>(n: usize) -> Result<Self, LayoutError> {
         // Reduce the amount of code we need to monomorphize per `T`.
         return inner(T::LAYOUT, n);

library/core/src/array/iter.rs

@@ -138,6 +138,9 @@ impl<T, const N: usize> IntoIter<T, N> {
     /// ```
     #[unstable(feature = "array_into_iter_constructors", issue = "91583")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(initialized.start <= initialized.end && initialized.end <= N)]
     pub const unsafe fn new_unchecked(
         buffer: [MaybeUninit<T>; N],
         initialized: Range<usize>,
@@ -279,6 +282,8 @@ impl<T, const N: usize> Iterator for IntoIter<T, N> {
     }
 
     #[inline]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // SAFETY: The caller must provide an idx that is in bound of the remainder.
         let elem_ref = unsafe { self.as_mut_slice().get_unchecked_mut(idx) };

library/core/src/ascii/ascii_char.rs

@@ -458,6 +458,10 @@ impl AsciiChar {
     /// or returns `None` if it's too large.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(
+        move |result: &Option<AsciiChar>|
+        (b <= 127) == (result.is_some() && result.unwrap() as u8 == b))]
     pub const fn from_u8(b: u8) -> Option<Self> {
         if b <= 127 {
             // SAFETY: Just checked that `b` is in-range
@@ -475,6 +479,10 @@ impl AsciiChar {
     /// `b` must be in `0..=127`, or else this is UB.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(b <= 127)]
+    #[core::contracts::ensures(move |result: &Self| *result as u8 == b)]
     pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
         // SAFETY: Our safety precondition is that `b` is in-range.
         unsafe { transmute(b) }
@@ -513,6 +521,12 @@ impl AsciiChar {
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
     #[track_caller]
+    // Only `d < 64` is required for safety as described above, but we use `d < 10` as in the
+    // `assert_unsafe_precondition` inside. See https://github.com/rust-lang/rust/pull/129374 for
+    // some context about the discrepancy.
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(d < 10)]
     pub const unsafe fn digit_unchecked(d: u8) -> Self {
         assert_unsafe_precondition!(
             check_library_ub,
@@ -532,6 +546,8 @@ impl AsciiChar {
     /// Gets this ASCII character as a byte.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[core::contracts::ensures(|result: &u8| *result <= 127)]
     pub const fn to_u8(self) -> u8 {
         self as u8
     }

library/core/src/char/convert.rs

@@ -23,6 +23,10 @@ pub(super) const fn from_u32(i: u32) -> Option<char> {
 #[must_use]
 #[allow(unnecessary_transmutes)]
 #[track_caller]
+#[rustc_allow_const_fn_unstable(contracts)]
+#[allow(unused_parens)]
+#[core::contracts::requires(char_try_from_u32(i).is_ok())]
+#[core::contracts::ensures(move |result: &char| *result as u32 == i)]
 pub(super) const unsafe fn from_u32_unchecked(i: u32) -> char {
     // SAFETY: the caller must guarantee that `i` is a valid char value.
     unsafe {

library/core/src/char/mod.rs

@@ -138,6 +138,9 @@ pub const fn from_u32(i: u32) -> Option<char> {
 #[rustc_const_stable(feature = "const_char_from_u32_unchecked", since = "1.81.0")]
 #[must_use]
 #[inline]
+#[rustc_allow_const_fn_unstable(contracts)]
+#[allow(unused_parens)]
+#[core::contracts::requires(i <= 0x10FFFF && (i < 0xD800 || i > 0xDFFF))]
 pub const unsafe fn from_u32_unchecked(i: u32) -> char {
     // SAFETY: the safety contract must be upheld by the caller.
     unsafe { self::convert::from_u32_unchecked(i) }
@@ -399,6 +402,7 @@ macro_rules! casemappingiter_impls {
                 self.0.advance_by(n)
             }
 
+            #[core::contracts::requires(idx < self.0.len())]
             unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                 // SAFETY: just forwarding requirements to caller
                 unsafe { self.0.__iterator_get_unchecked(idx) }
@@ -533,6 +537,8 @@ impl Iterator for CaseMappingIter {
         self.0.advance_by(n)
     }
 
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // SAFETY: just forwarding requirements to caller
         unsafe { self.0.__iterator_get_unchecked(idx) }

library/core/src/ffi/c_str.rs

@@ -250,6 +250,14 @@ impl CStr {
     #[must_use]
     #[stable(feature = "rust1", since = "1.0.0")]
     #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(!ptr.is_null())]
+    #[core::contracts::ensures(
+        |result: &&CStr|
+        !result.inner.is_empty() &&
+        result.inner[result.inner.len() - 1] == 0 &&
+        !result.inner[..result.inner.len() - 1].contains(&0))]
     pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr {
         // SAFETY: The caller has provided a pointer that points to a valid C
         // string with a NUL terminator less than `isize::MAX` from `ptr`.
@@ -385,6 +393,15 @@ impl CStr {
     #[stable(feature = "cstr_from_bytes", since = "1.10.0")]
     #[rustc_const_stable(feature = "const_cstr_unchecked", since = "1.59.0")]
     #[rustc_allow_const_fn_unstable(const_eval_select)]
+    #[rustc_allow_const_fn_unstable(contracts)]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(
+        !bytes.is_empty() && bytes[bytes.len() - 1] == 0 && !bytes[..bytes.len()-1].contains(&0))]
+    #[core::contracts::ensures(
+        |result: &&CStr|
+        !result.inner.is_empty() &&
+        result.inner[result.inner.len() - 1] == 0 &&
+        !result.inner[..result.inner.len() - 1].contains(&0))]
     pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr {
         const_eval_select!(
             @capture { bytes: &[u8] } -> &CStr:
@@ -723,6 +740,12 @@ impl const AsRef<CStr> for CStr {
 #[inline]
 #[unstable(feature = "cstr_internals", issue = "none")]
 #[rustc_allow_const_fn_unstable(const_eval_select)]
+#[rustc_allow_const_fn_unstable(contracts)]
+#[core::contracts::ensures(
+    move |&result|
+    result < isize::MAX as usize &&
+    // SAFETY: result is within isize::MAX
+    unsafe { *ptr.add(result) } == 0)]
 const unsafe fn strlen(ptr: *const c_char) -> usize {
     const_eval_select!(
         @capture { s: *const c_char = ptr } -> usize:

library/core/src/intrinsics/fallback.rs

@@ -130,6 +130,7 @@ macro_rules! impl_disjoint_bitor {
         impl const DisjointBitOr for $t {
             #[cfg_attr(miri, track_caller)]
             #[inline]
+            #[core::contracts::requires((self & other) == zero!($t))]
             unsafe fn disjoint_bitor(self, other: Self) -> Self {
                 // Note that the assume here is required for UB detection in Miri!
 

library/core/src/intrinsics/mod.rs

@@ -2559,6 +2559,9 @@ pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
 #[inline]
 #[rustc_intrinsic]
 #[rustc_intrinsic_const_stable_indirect]
+#[allow(unused_parens)]
+#[rustc_allow_const_fn_unstable(contracts)]
+#[core::contracts::requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
 pub const unsafe fn typed_swap_nonoverlapping<T>(x: *mut T, y: *mut T) {
     // SAFETY: The caller provided single non-overlapping items behind
     // pointers, so swapping them with `count: 1` is fine.

library/core/src/iter/adapters/cloned.rs

@@ -61,6 +61,8 @@ where
         self.it.map(T::clone).fold(init, f)
     }
 
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
         Self: TrustedRandomAccessNoCoerce,

library/core/src/iter/adapters/copied.rs

@@ -92,6 +92,8 @@ where
         self.it.advance_by(n)
     }
 
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
         Self: TrustedRandomAccessNoCoerce,

library/core/src/iter/adapters/enumerate.rs

@@ -160,6 +160,8 @@ where
 
     #[rustc_inherit_overflow_checks]
     #[inline]
+    #[allow(unused_parens)]
+    #[core::contracts::requires(idx < self.iter.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item
     where
         Self: TrustedRandomAccessNoCoerce,