From 78910a4925b0e5d96f291379e02d2327371d23d2 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Mon, 18 Aug 2025 16:23:36 -0700
Subject: [PATCH 1/7] LLM-generated contracts + type invariants

---
 .../tests/sort/known_good_stable_sort.rs      | 15 ++++++++++
 library/core/src/array/ascii.rs               | 29 +++++++++++++++++++
 library/core/src/array/drain.rs               |  7 +++++
 library/core/src/fmt/rt.rs                    | 20 +++++++++++++
 library/core/src/iter/adapters/map.rs         |  1 +
 library/core/src/iter/adapters/map_windows.rs |  9 ++++++
 .../src/iter/traits/unchecked_iterator.rs     |  8 +++++
 7 files changed, 89 insertions(+)

diff --git a/library/alloctests/tests/sort/known_good_stable_sort.rs b/library/alloctests/tests/sort/known_good_stable_sort.rs
index 2df891462538d..6054f52dd4b4b 100644
--- a/library/alloctests/tests/sort/known_good_stable_sort.rs
+++ b/library/alloctests/tests/sort/known_good_stable_sort.rs
@@ -4,6 +4,15 @@
 //
 // Based on https://github.com/voultapher/tiny-sort-rs.
 
+#![feature(ub_checks)]
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use alloc::alloc::{Layout, alloc, dealloc};
 use std::ptr;
 
@@ -48,6 +57,7 @@ fn stable_sort<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], mut is_less: F) {
 ///
 /// SAFETY: The caller has to ensure that len is > 0 and that T is not a ZST.
 #[inline(never)]
+#[requires(len > 0 && size_of::<T>() > 0)]
 unsafe fn mergesort_main<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
     // While it would be nice to have a merge implementation that only requires N / 2 auxiliary
     // memory. Doing so would make the merge implementation significantly more complex and
@@ -66,6 +76,7 @@ unsafe fn mergesort_main<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut
 ///
 /// Buffer as pointed to by `scratch` must have space for `v.len()` writes. And must not alias `v`.
 #[inline(always)]
+#[requires(can_dereference(scratch_ptr) && !same_allocation(scratch_ptr, v.as_ptr()))]
 unsafe fn mergesort_core<T, F: FnMut(&T, &T) -> bool>(
     v: &mut [T],
     scratch_ptr: *mut T,
@@ -97,6 +108,7 @@ unsafe fn mergesort_core<T, F: FnMut(&T, &T) -> bool>(
 /// SAFETY: The caller must ensure that `scratch_ptr` is valid for `v.len()` writes. And that mid is
 /// in-bounds.
 #[inline(always)]
+#[requires(mid <= len && can_dereference(scratch_ptr) && !same_allocation(scratch_ptr, v.as_ptr()))]
 unsafe fn merge<T, F>(v: &mut [T], scratch_ptr: *mut T, is_less: &mut F, mid: usize)
 where
     F: FnMut(&T, &T) -> bool,
@@ -143,6 +155,7 @@ where
 }
 
 // SAFETY: The caller has to ensure that Option is Some, UB otherwise.
+#[requires(opt_val.is_some())]
 unsafe fn unwrap_unchecked<T>(opt_val: Option<T>) -> T {
     match opt_val {
         Some(val) => val,
@@ -165,6 +178,7 @@ struct BufGuard<T> {
 
 impl<T> BufGuard<T> {
     // SAFETY: The caller has to ensure that len is not 0 and that T is not a ZST.
+    #[requires(len > 0 && size_of::<T>() > 0)]
     unsafe fn new(len: usize) -> Self {
         debug_assert!(len > 0 && size_of::<T>() > 0);
 
@@ -183,6 +197,7 @@ impl<T> BufGuard<T> {
 }
 
 impl<T> Drop for BufGuard<T> {
+    #[requires(size_of::<T>() > 0)]
     fn drop(&mut self) {
         // SAFETY: We checked that T is not a ZST.
         unsafe {
diff --git a/library/core/src/array/ascii.rs b/library/core/src/array/ascii.rs
index 792a57e3fa25c..aadc27924d985 100644
--- a/library/core/src/array/ascii.rs
+++ b/library/core/src/array/ascii.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::ascii;
 
 impl<const N: usize> [u8; N] {
@@ -36,6 +42,7 @@ impl<const N: usize> [u8; N] {
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[must_use]
     #[inline]
+    #[requires(self.iter().all(|&b| b <= 127))]
     pub const unsafe fn as_ascii_unchecked(&self) -> &[ascii::Char; N] {
         let byte_ptr: *const [u8; N] = self;
         let ascii_ptr = byte_ptr as *const [ascii::Char; N];
@@ -43,3 +50,25 @@ impl<const N: usize> [u8; N] {
         unsafe { &*ascii_ptr }
     }
 }
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    #[cfg(kani)]
+    #[kani::proof_for_contract(<[u8; 4]>::as_ascii_unchecked)]
+    #[kani::unwind(10)]
+    fn proof_for_as_ascii_unchecked() {
+        // Create a small array of bytes that are all ASCII (0-127)
+        let mut bytes = [0u8; 4];
+
+        // Fill the array with arbitrary ASCII bytes
+        for i in 0..4 {
+            bytes[i] = kani::any::<u8>() & 0x7F; // Ensure value is in range 0-127
+        }
+
+        // The precondition self.iter().all(|&b| b <= 127) is automatically assumed by Kani
+
+        // Call the function - if preconditions are met, this should not cause undefined behavior
+        unsafe { bytes.as_ascii_unchecked() };
+    }
+}
diff --git a/library/core/src/array/drain.rs b/library/core/src/array/drain.rs
index 5fadf907b6219..69bda0ef6e44d 100644
--- a/library/core/src/array/drain.rs
+++ b/library/core/src/array/drain.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::iter::{TrustedLen, UncheckedIterator};
 use crate::mem::ManuallyDrop;
 use crate::ptr::drop_in_place;
@@ -66,6 +72,7 @@ impl<T> ExactSizeIterator for Drain<'_, T> {
 unsafe impl<T> TrustedLen for Drain<'_, T> {}
 
 impl<T> UncheckedIterator for Drain<'_, T> {
+    #[requires(self.0.len() > 0)]
     unsafe fn next_unchecked(&mut self) -> T {
         // SAFETY: `Drain` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
diff --git a/library/core/src/fmt/rt.rs b/library/core/src/fmt/rt.rs
index fb858a0572612..5a0c67f55bfd6 100644
--- a/library/core/src/fmt/rt.rs
+++ b/library/core/src/fmt/rt.rs
@@ -6,6 +6,14 @@
 //!
 //! Do not modify them without understanding the consequences for the format_args!() macro.
 
+use crate::ub_checks::Invariant;
+
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use super::*;
 use crate::hint::unreachable_unchecked;
 use crate::ptr::NonNull;
@@ -161,6 +169,7 @@ impl Argument<'_> {
     ///
     /// This argument must actually be a placeholder argument.
     #[inline]
+    #[requires(matches!(self.ty, ArgumentType::Placeholder { .. }))]
     pub(super) unsafe fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         match self.ty {
             // SAFETY:
@@ -228,6 +237,7 @@ impl<'a> Arguments<'a> {
     /// const _: () = if false { panic!("a {:1}", "a") };
     /// ```
     #[inline]
+    #[requires(pieces.len() >= fmt.len())]
     pub unsafe fn new_v1_formatted(
         pieces: &'a [&'static str],
         args: &'a [rt::Argument<'a>],
@@ -236,3 +246,13 @@ impl<'a> Arguments<'a> {
         Arguments { pieces, fmt: Some(fmt), args }
     }
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<'a> Invariant for ArgumentType<'a> {
+    fn is_safe(&self) -> bool {
+        match self {
+            ArgumentType::Placeholder { value, formatter, .. } => true,
+            ArgumentType::Count(_) => true
+        }
+    }
+}
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index c738b8cda957b..bf9f0c48fec3b 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -204,6 +204,7 @@ where
     I: UncheckedIterator,
     F: FnMut(I::Item) -> B,
 {
+    #[requires(self.iter.size_hint().0 > 0)]
     unsafe fn next_unchecked(&mut self) -> B {
         // SAFETY: `Map` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index a9c07fee2a91e..be48aea8fdbfe 100644
--- a/library/core/src/iter/adapters/map_windows.rs
+++ b/library/core/src/iter/adapters/map_windows.rs
@@ -1,3 +1,5 @@
+use crate::ub_checks::Invariant;
+
 use crate::iter::FusedIterator;
 use crate::mem::MaybeUninit;
 use crate::{fmt, ptr};
@@ -289,3 +291,10 @@ where
         Self { f: self.f.clone(), inner: self.inner.clone() }
     }
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T, const N: usize> Invariant for Buffer<T, N> {
+    fn is_safe(&self) -> bool {
+        self.start + N <= 2 * N
+    }
+}
\ No newline at end of file
diff --git a/library/core/src/iter/traits/unchecked_iterator.rs b/library/core/src/iter/traits/unchecked_iterator.rs
index ae4bfcad4e68f..0836538ab135b 100644
--- a/library/core/src/iter/traits/unchecked_iterator.rs
+++ b/library/core/src/iter/traits/unchecked_iterator.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::iter::TrustedLen;
 
 /// [`TrustedLen`] cannot have methods, so this allows augmenting it.
@@ -27,6 +33,8 @@ pub(crate) trait UncheckedIterator: TrustedLen {
     /// point you might want to implement this manually instead.
     #[unstable(feature = "trusted_len_next_unchecked", issue = "37572")]
     #[inline]
+    #[requires(self.size_hint().0 > 0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> Self::Item {
         let opt = self.next();
         // SAFETY: The caller promised that we're not empty, and

From 1b72505a57fcd3dd53e399c6e0dc8046b8ceb4d3 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Mon, 18 Aug 2025 16:37:41 -0700
Subject: [PATCH 2/7] Fix imports

---
 library/core/src/array/ascii.rs                    |  8 +++-----
 library/core/src/array/drain.rs                    |  8 +++-----
 library/core/src/fmt/rt.rs                         | 11 ++++-------
 library/core/src/iter/adapters/map_windows.rs      |  5 ++---
 library/core/src/iter/traits/unchecked_iterator.rs |  8 +++-----
 5 files changed, 15 insertions(+), 25 deletions(-)

diff --git a/library/core/src/array/ascii.rs b/library/core/src/array/ascii.rs
index aadc27924d985..6bc96d143ea4c 100644
--- a/library/core/src/array/ascii.rs
+++ b/library/core/src/array/ascii.rs
@@ -1,10 +1,8 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::ascii;
+#[cfg(kani)]
+use crate::kani;
 
 impl<const N: usize> [u8; N] {
     /// Converts this array of bytes into an array of ASCII characters,
diff --git a/library/core/src/array/drain.rs b/library/core/src/array/drain.rs
index 69bda0ef6e44d..6545ebebed425 100644
--- a/library/core/src/array/drain.rs
+++ b/library/core/src/array/drain.rs
@@ -1,10 +1,8 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::iter::{TrustedLen, UncheckedIterator};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::ManuallyDrop;
 use crate::ptr::drop_in_place;
 use crate::slice;
diff --git a/library/core/src/fmt/rt.rs b/library/core/src/fmt/rt.rs
index 5a0c67f55bfd6..598f3087cbbc4 100644
--- a/library/core/src/fmt/rt.rs
+++ b/library/core/src/fmt/rt.rs
@@ -6,17 +6,14 @@
 //!
 //! Do not modify them without understanding the consequences for the format_args!() macro.
 
-use crate::ub_checks::Invariant;
-
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use super::*;
 use crate::hint::unreachable_unchecked;
+#[cfg(kani)]
+use crate::kani;
 use crate::ptr::NonNull;
+use crate::ub_checks::Invariant;
 
 #[lang = "format_placeholder"]
 #[derive(Copy, Clone)]
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index be48aea8fdbfe..1396ab3addd37 100644
--- a/library/core/src/iter/adapters/map_windows.rs
+++ b/library/core/src/iter/adapters/map_windows.rs
@@ -1,8 +1,7 @@
-use crate::ub_checks::Invariant;
-
 use crate::iter::FusedIterator;
 use crate::mem::MaybeUninit;
 use crate::{fmt, ptr};
+use crate::ub_checks::Invariant;
 
 /// An iterator over the mapped windows of another iterator.
 ///
@@ -297,4 +296,4 @@ impl<T, const N: usize> Invariant for Buffer<T, N> {
     fn is_safe(&self) -> bool {
         self.start + N <= 2 * N
     }
-}
\ No newline at end of file
+}
diff --git a/library/core/src/iter/traits/unchecked_iterator.rs b/library/core/src/iter/traits/unchecked_iterator.rs
index 0836538ab135b..ee94f7191349e 100644
--- a/library/core/src/iter/traits/unchecked_iterator.rs
+++ b/library/core/src/iter/traits/unchecked_iterator.rs
@@ -1,10 +1,8 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::iter::TrustedLen;
+#[cfg(kani)]
+use crate::kani;
 
 /// [`TrustedLen`] cannot have methods, so this allows augmenting it.
 ///

From 9346adc16ef0a55bcdc7cdec1092847487b93376 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Mon, 18 Aug 2025 16:47:01 -0700
Subject: [PATCH 3/7] Fix imports

---
 .../alloctests/tests/sort/known_good_stable_sort.rs    | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/library/alloctests/tests/sort/known_good_stable_sort.rs b/library/alloctests/tests/sort/known_good_stable_sort.rs
index 6054f52dd4b4b..9dc5236e347e2 100644
--- a/library/alloctests/tests/sort/known_good_stable_sort.rs
+++ b/library/alloctests/tests/sort/known_good_stable_sort.rs
@@ -5,17 +5,17 @@
 // Based on https://github.com/voultapher/tiny-sort-rs.
 
 #![feature(ub_checks)]
-use safety::{ensures,requires};
+use alloc::alloc::{Layout, alloc, dealloc};
+use safety::requires;
+use std::ptr;
+
 #[cfg(kani)]
-#[unstable(feature="kani", issue="none")]
+#[unstable(feature = "kani", issue = "none")]
 use core::kani;
 #[allow(unused_imports)]
 #[unstable(feature = "ub_checks", issue = "none")]
 use core::ub_checks::*;
 
-use alloc::alloc::{Layout, alloc, dealloc};
-use std::ptr;
-
 /// Sort `v` preserving initial order of equal elements.
 ///
 /// - Guaranteed O(N * log(N)) worst case perf

From 367ce3e7e2532b58aa0b0e718fe8d560fe5a0214 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Tue, 19 Aug 2025 09:50:49 -0700
Subject: [PATCH 4/7] Fix imports

---
 library/alloctests/tests/sort/known_good_stable_sort.rs | 5 +++--
 library/core/src/fmt/rt.rs                              | 2 +-
 library/core/src/iter/adapters/map_windows.rs           | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/library/alloctests/tests/sort/known_good_stable_sort.rs b/library/alloctests/tests/sort/known_good_stable_sort.rs
index 9dc5236e347e2..9d4ee07675b80 100644
--- a/library/alloctests/tests/sort/known_good_stable_sort.rs
+++ b/library/alloctests/tests/sort/known_good_stable_sort.rs
@@ -6,8 +6,6 @@
 
 #![feature(ub_checks)]
 use alloc::alloc::{Layout, alloc, dealloc};
-use safety::requires;
-use std::ptr;
 
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
@@ -15,6 +13,9 @@ use core::kani;
 #[allow(unused_imports)]
 #[unstable(feature = "ub_checks", issue = "none")]
 use core::ub_checks::*;
+use std::ptr;
+
+use safety::requires;
 
 /// Sort `v` preserving initial order of equal elements.
 ///
diff --git a/library/core/src/fmt/rt.rs b/library/core/src/fmt/rt.rs
index 598f3087cbbc4..651928b7ea8fc 100644
--- a/library/core/src/fmt/rt.rs
+++ b/library/core/src/fmt/rt.rs
@@ -249,7 +249,7 @@ impl<'a> Invariant for ArgumentType<'a> {
     fn is_safe(&self) -> bool {
         match self {
             ArgumentType::Placeholder { value, formatter, .. } => true,
-            ArgumentType::Count(_) => true
+            ArgumentType::Count(_) => true,
         }
     }
 }
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index 1396ab3addd37..6d623c24d022e 100644
--- a/library/core/src/iter/adapters/map_windows.rs
+++ b/library/core/src/iter/adapters/map_windows.rs
@@ -1,7 +1,7 @@
 use crate::iter::FusedIterator;
 use crate::mem::MaybeUninit;
-use crate::{fmt, ptr};
 use crate::ub_checks::Invariant;
+use crate::{fmt, ptr};
 
 /// An iterator over the mapped windows of another iterator.
 ///

From 751d1a70a1210ed6020184a9d7d9e76a94d4d772 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Tue, 19 Aug 2025 09:59:15 -0700
Subject: [PATCH 5/7] Fix imports

---
 library/alloctests/tests/sort/known_good_stable_sort.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/alloctests/tests/sort/known_good_stable_sort.rs b/library/alloctests/tests/sort/known_good_stable_sort.rs
index 9d4ee07675b80..ac13abdb9b6c7 100644
--- a/library/alloctests/tests/sort/known_good_stable_sort.rs
+++ b/library/alloctests/tests/sort/known_good_stable_sort.rs
@@ -6,7 +6,6 @@
 
 #![feature(ub_checks)]
 use alloc::alloc::{Layout, alloc, dealloc};
-
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 use core::kani;

From 81301b00a31f6e60a657b74ae2c8388bed1a917d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Aug 2025 14:27:38 +0200
Subject: [PATCH 6/7] Update library/core/src/fmt/rt.rs

---
 library/core/src/fmt/rt.rs | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/library/core/src/fmt/rt.rs b/library/core/src/fmt/rt.rs
index 651928b7ea8fc..ecd08eaef8f1d 100644
--- a/library/core/src/fmt/rt.rs
+++ b/library/core/src/fmt/rt.rs
@@ -243,13 +243,3 @@ impl<'a> Arguments<'a> {
         Arguments { pieces, fmt: Some(fmt), args }
     }
 }
-
-#[unstable(feature = "ub_checks", issue = "none")]
-impl<'a> Invariant for ArgumentType<'a> {
-    fn is_safe(&self) -> bool {
-        match self {
-            ArgumentType::Placeholder { value, formatter, .. } => true,
-            ArgumentType::Count(_) => true,
-        }
-    }
-}

From 18a102ce60af691271a6b2c7988f080e06bf806d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Aug 2025 14:27:45 +0200
Subject: [PATCH 7/7] Update
 library/alloctests/tests/sort/known_good_stable_sort.rs

---
 library/alloctests/tests/sort/known_good_stable_sort.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/alloctests/tests/sort/known_good_stable_sort.rs b/library/alloctests/tests/sort/known_good_stable_sort.rs
index ac13abdb9b6c7..bc40f3874847b 100644
--- a/library/alloctests/tests/sort/known_good_stable_sort.rs
+++ b/library/alloctests/tests/sort/known_good_stable_sort.rs
@@ -197,7 +197,6 @@ impl<T> BufGuard<T> {
 }
 
 impl<T> Drop for BufGuard<T> {
-    #[requires(size_of::<T>() > 0)]
     fn drop(&mut self) {
         // SAFETY: We checked that T is not a ZST.
         unsafe {