From 1b1cfe60711d9c81ce9865db93f6255dc228a816 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Wed, 30 Jul 2025 13:28:13 -0700
Subject: [PATCH 1/6] LLM-generated contracts for __iterator_get_unchecked

---
 library/alloc/src/collections/vec_deque/iter.rs     | 11 +++++++++++
 library/alloc/src/collections/vec_deque/iter_mut.rs | 11 +++++++++++
 library/alloc/src/vec/into_iter.rs                  | 11 +++++++++++
 library/core/src/array/iter.rs                      | 10 ++++++++++
 library/core/src/char/mod.rs                        |  9 +++++++++
 library/core/src/iter/adapters/cloned.rs            |  7 +++++++
 library/core/src/iter/adapters/enumerate.rs         |  7 +++++++
 library/core/src/iter/adapters/fuse.rs              |  7 +++++++
 library/core/src/iter/adapters/map.rs               |  7 +++++++
 library/core/src/iter/adapters/skip.rs              |  7 +++++++
 library/core/src/iter/adapters/zip.rs               |  8 ++++++++
 library/core/src/range/iter.rs                      |  7 +++++++
 12 files changed, 102 insertions(+)

diff --git a/library/alloc/src/collections/vec_deque/iter.rs b/library/alloc/src/collections/vec_deque/iter.rs
index d3dbd10c863fb..3ad9d22883575 100644
--- a/library/alloc/src/collections/vec_deque/iter.rs
+++ b/library/alloc/src/collections/vec_deque/iter.rs
@@ -1,3 +1,12 @@
+#![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 core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use core::num::NonZero;
 use core::ops::Try;
@@ -144,6 +153,8 @@ impl<'a, T> Iterator for Iter<'a, T> {
     }
 
     #[inline]
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     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.
diff --git a/library/alloc/src/collections/vec_deque/iter_mut.rs b/library/alloc/src/collections/vec_deque/iter_mut.rs
index 0c5f06e752b7b..33aafcdec86f1 100644
--- a/library/alloc/src/collections/vec_deque/iter_mut.rs
+++ b/library/alloc/src/collections/vec_deque/iter_mut.rs
@@ -1,3 +1,12 @@
+#![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 core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use core::num::NonZero;
 use core::ops::Try;
@@ -208,6 +217,8 @@ impl<'a, T> Iterator for IterMut<'a, T> {
     }
 
     #[inline]
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     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.
diff --git a/library/alloc/src/vec/into_iter.rs b/library/alloc/src/vec/into_iter.rs
index 37df928228d9c..d3ea78d8a654c 100644
--- a/library/alloc/src/vec/into_iter.rs
+++ b/library/alloc/src/vec/into_iter.rs
@@ -1,3 +1,12 @@
+#![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 core::iter::{
     FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen,
     TrustedRandomAccessNoCoerce,
@@ -354,6 +363,8 @@ impl<T, A: Allocator> Iterator for IntoIter<T, A> {
         R::from_output(accum)
     }
 
+    #[requires(i < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, i: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/array/iter.rs b/library/core/src/array/iter.rs
index fdae5c08f1e8e..a0d02422bd204 100644
--- a/library/core/src/array/iter.rs
+++ b/library/core/src/array/iter.rs
@@ -1,5 +1,11 @@
 //! Defines the `IntoIter` owned iterator for arrays.
 
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::intrinsics::transmute_unchecked;
 use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccessNoCoerce};
 use crate::mem::MaybeUninit;
@@ -138,6 +144,8 @@ impl<T, const N: usize> IntoIter<T, N> {
     /// ```
     #[unstable(feature = "array_into_iter_constructors", issue = "91583")]
     #[inline]
+    #[requires(initialized.start <= initialized.end)]
+    #[requires(initialized.end <= N)]
     pub const unsafe fn new_unchecked(
         buffer: [MaybeUninit<T>; N],
         initialized: Range<usize>,
@@ -279,6 +287,8 @@ impl<T, const N: usize> Iterator for IntoIter<T, N> {
     }
 
     #[inline]
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     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) };
diff --git a/library/core/src/char/mod.rs b/library/core/src/char/mod.rs
index 82a3f6f916be3..3829bf05eac3b 100644
--- a/library/core/src/char/mod.rs
+++ b/library/core/src/char/mod.rs
@@ -41,6 +41,12 @@ pub use self::methods::encode_utf16_raw; // perma-unstable
 pub use self::methods::{encode_utf8_raw, encode_utf8_raw_unchecked}; // perma-unstable
 
 #[rustfmt::skip]
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::ascii;
 pub(crate) use self::methods::EscapeDebugExtArgs;
 use crate::error::Error;
@@ -138,6 +144,7 @@ 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]
+#[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) }
@@ -533,6 +540,8 @@ impl Iterator for CaseMappingIter {
         self.0.advance_by(n)
     }
 
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // SAFETY: just forwarding requirements to caller
         unsafe { self.0.__iterator_get_unchecked(idx) }
diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs
index aea6d64281aec..3f91d0a847ea0 100644
--- a/library/core/src/iter/adapters/cloned.rs
+++ b/library/core/src/iter/adapters/cloned.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use core::num::NonZero;
 
 use crate::iter::adapters::zip::try_get_unchecked;
@@ -61,6 +67,7 @@ where
         self.it.map(T::clone).fold(init, f)
     }
 
+    #[requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs
index f7b9f0b7a5e9d..71fe5735a8d9e 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen};
@@ -160,6 +166,7 @@ where
 
     #[rustc_inherit_overflow_checks]
     #[inline]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs
index 0072a95e8dfe0..2509441b0b976 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::intrinsics;
 use crate::iter::adapters::SourceIter;
 use crate::iter::adapters::zip::try_get_unchecked;
@@ -109,6 +115,7 @@ where
     }
 
     #[inline]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index 007c2d5acc2d0..3eb5a69c909f0 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::fmt;
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
@@ -129,6 +135,7 @@ where
     }
 
     #[inline]
+    #[requires(idx < self.iter.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> B
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs
index 55c4a7f14fbd6..bfc59f568cb4b 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::intrinsics::unlikely;
 use crate::iter::adapters::SourceIter;
 use crate::iter::adapters::zip::try_get_unchecked;
@@ -158,6 +164,7 @@ where
     }
 
     #[doc(hidden)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs
index c5e199c30821d..b44c33add9c6a 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::cmp;
 use crate::fmt::{self, Debug};
 use crate::iter::{
@@ -104,6 +110,7 @@ where
     }
 
     #[inline]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,
@@ -264,6 +271,7 @@ where
     }
 
     #[inline]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item {
         let idx = self.index + idx;
         // SAFETY: the caller must uphold the contract for
diff --git a/library/core/src/range/iter.rs b/library/core/src/range/iter.rs
index 1e261d8c1d93a..993936cdd1843 100644
--- a/library/core/src/range/iter.rs
+++ b/library/core/src/range/iter.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::iter::{
     FusedIterator, Step, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, TrustedStep,
 };
@@ -104,6 +110,7 @@ impl<A: Step> Iterator for IterRange<A> {
     }
 
     #[inline]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,

From ab019e2e3d59b07dbba6684b7c4f31a93100c258 Mon Sep 17 00:00:00 2001
From: Fedor Ryabinin <rfedor@amazon.com>
Date: Wed, 30 Jul 2025 15:57:31 -0700
Subject: [PATCH 2/6] Another pass with Claude 3.7 as an arbiter

---
 library/core/src/iter/traits/iterator.rs | 7 +++++++
 library/core/src/range/iter.rs           | 1 +
 2 files changed, 8 insertions(+)

diff --git a/library/core/src/iter/traits/iterator.rs b/library/core/src/iter/traits/iterator.rs
index 10f9d464f7d7f..4e1866395d9bc 100644
--- a/library/core/src/iter/traits/iterator.rs
+++ b/library/core/src/iter/traits/iterator.rs
@@ -1,3 +1,9 @@
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use super::super::{
     ArrayChunks, ByRefSized, Chain, Cloned, Copied, Cycle, Enumerate, Filter, FilterMap, FlatMap,
     Flatten, Fuse, Inspect, Intersperse, IntersperseWith, Map, MapWhile, MapWindows, Peekable,
@@ -1709,6 +1715,7 @@ pub trait Iterator {
     /// ```
     #[inline]
     #[unstable(feature = "iter_map_windows", reason = "recently added", issue = "87155")]
+    #[requires(N > 0)]
     fn map_windows<F, R, const N: usize>(self, f: F) -> MapWindows<Self, F, N>
     where
         Self: Sized,
diff --git a/library/core/src/range/iter.rs b/library/core/src/range/iter.rs
index 993936cdd1843..b5a3ab47b4856 100644
--- a/library/core/src/range/iter.rs
+++ b/library/core/src/range/iter.rs
@@ -110,6 +110,7 @@ impl<A: Step> Iterator for IterRange<A> {
     }
 
     #[inline]
+    #[requires(idx < self.size_hint().0)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where

From 80f8368bee1ccbcb97a6218ad840f50e7ec7dfae Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Aug 2025 08:52:38 +0000
Subject: [PATCH 3/6] Additional contracts

---
 library/core/src/char/mod.rs                |  1 +
 library/core/src/iter/adapters/copied.rs    |  4 ++++
 library/core/src/iter/adapters/enumerate.rs |  1 +
 library/core/src/iter/adapters/fuse.rs      |  1 +
 library/core/src/iter/adapters/skip.rs      |  1 +
 library/core/src/iter/adapters/zip.rs       |  1 +
 library/core/src/iter/range.rs              |  1 +
 library/core/src/slice/iter.rs              | 11 ++++++++++-
 library/core/src/str/iter.rs                |  4 ++++
 9 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/library/core/src/char/mod.rs b/library/core/src/char/mod.rs
index 3829bf05eac3b..62637e70bb413 100644
--- a/library/core/src/char/mod.rs
+++ b/library/core/src/char/mod.rs
@@ -406,6 +406,7 @@ macro_rules! casemappingiter_impls {
                 self.0.advance_by(n)
             }
 
+            #[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) }
diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs
index 23e4e25ab5388..51d60dc589ea4 100644
--- a/library/core/src/iter/adapters/copied.rs
+++ b/library/core/src/iter/adapters/copied.rs
@@ -1,3 +1,6 @@
+use safety::requires;
+#[cfg(kani)]
+use crate::kani;
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedLen};
@@ -92,6 +95,7 @@ where
         self.it.advance_by(n)
     }
 
+    #[requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs
index 71fe5735a8d9e..82f8339f4d906 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -166,6 +166,7 @@ where
 
     #[rustc_inherit_overflow_checks]
     #[inline]
+    #[requires(idx < self.iter.size_hint().0)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item
     where
diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs
index 2509441b0b976..cb862e17eddea 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -115,6 +115,7 @@ where
     }
 
     #[inline]
+    #[requires(self.iter.is_some() && idx < self.iter.as_ref().unwrap().size_hint().0)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs
index bfc59f568cb4b..9e1764af80762 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -164,6 +164,7 @@ where
     }
 
     #[doc(hidden)]
+    #[requires(idx + self.n < self.iter.size_hint().0)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs
index b44c33add9c6a..76d93056fea23 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -110,6 +110,7 @@ where
     }
 
     #[inline]
+    #[requires(idx < self.size_hint().0)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs
index 70a38eafaa443..79cc6873adc7d 100644
--- a/library/core/src/iter/range.rs
+++ b/library/core/src/iter/range.rs
@@ -933,6 +933,7 @@ impl<A: Step> Iterator for ops::Range<A> {
     }
 
     #[inline]
+    #[requires(idx < self.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,
diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index 22b78418d67ee..bcc5251cf8eaf 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -2,7 +2,7 @@
 
 #[macro_use] // import iterator! and forward_iterator!
 mod macros;
-
+use safety::requires;
 use super::{from_raw_parts, from_raw_parts_mut};
 use crate::hint::assert_unchecked;
 use crate::iter::{
@@ -1455,6 +1455,7 @@ impl<'a, T> Iterator for Windows<'a, T> {
         }
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // SAFETY: since the caller guarantees that `i` is in bounds,
         // which means that `i` cannot overflow an `isize`, and the
@@ -1612,6 +1613,7 @@ impl<'a, T> Iterator for Chunks<'a, T> {
         }
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let start = idx * self.chunk_size;
         // SAFETY: the caller guarantees that `i` is in bounds,
@@ -1801,6 +1803,7 @@ impl<'a, T> Iterator for ChunksMut<'a, T> {
         }
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let start = idx * self.chunk_size;
         // SAFETY: see comments for `Chunks::__iterator_get_unchecked` and `self.v`.
@@ -1999,6 +2002,7 @@ impl<'a, T> Iterator for ChunksExact<'a, T> {
         self.next_back()
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let start = idx * self.chunk_size;
         // SAFETY: mostly identical to `Chunks::__iterator_get_unchecked`.
@@ -2160,6 +2164,7 @@ impl<'a, T> Iterator for ChunksExactMut<'a, T> {
         self.next_back()
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let start = idx * self.chunk_size;
         // SAFETY: see comments for `Chunks::__iterator_get_unchecked` and `self.v`.
@@ -2466,6 +2471,7 @@ impl<'a, T> Iterator for RChunks<'a, T> {
         }
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let end = self.v.len() - idx * self.chunk_size;
         let start = match end.checked_sub(self.chunk_size) {
@@ -2646,6 +2652,7 @@ impl<'a, T> Iterator for RChunksMut<'a, T> {
         }
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let end = self.v.len() - idx * self.chunk_size;
         let start = match end.checked_sub(self.chunk_size) {
@@ -2839,6 +2846,7 @@ impl<'a, T> Iterator for RChunksExact<'a, T> {
         self.next_back()
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let end = self.v.len() - idx * self.chunk_size;
         let start = end - self.chunk_size;
@@ -3005,6 +3013,7 @@ impl<'a, T> Iterator for RChunksExactMut<'a, T> {
         self.next_back()
     }
 
+    #[requires(idx < self.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         let end = self.v.len() - idx * self.chunk_size;
         let start = end - self.chunk_size;
diff --git a/library/core/src/str/iter.rs b/library/core/src/str/iter.rs
index d2985d8a18669..c9aed66c4af8b 100644
--- a/library/core/src/str/iter.rs
+++ b/library/core/src/str/iter.rs
@@ -1,5 +1,8 @@
 //! Iterators for `str` methods.
 
+use safety::requires;
+#[cfg(kani)]
+use crate::kani;
 use super::pattern::{DoubleEndedSearcher, Pattern, ReverseSearcher, Searcher};
 use super::validations::{next_code_point, next_code_point_reverse};
 use super::{
@@ -356,6 +359,7 @@ impl Iterator for Bytes<'_> {
     }
 
     #[inline]
+    #[requires(idx < self.0.len())]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> u8 {
         // SAFETY: the caller must uphold the safety contract
         // for `Iterator::__iterator_get_unchecked`.

From 4c4db85ac3d40960feb525c3b708ca75e926bb28 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Aug 2025 08:59:16 +0000
Subject: [PATCH 4/6] fmt

---
 library/alloc/src/collections/vec_deque/iter_mut.rs | 10 ++--------
 library/alloc/src/vec/into_iter.rs                  | 13 ++++---------
 library/core/src/array/iter.rs                      |  9 +++------
 library/core/src/char/mod.rs                        | 10 +++-------
 library/core/src/range/iter.rs                      |  9 +++------
 5 files changed, 15 insertions(+), 36 deletions(-)

diff --git a/library/alloc/src/collections/vec_deque/iter_mut.rs b/library/alloc/src/collections/vec_deque/iter_mut.rs
index 33aafcdec86f1..f51a9a382054c 100644
--- a/library/alloc/src/collections/vec_deque/iter_mut.rs
+++ b/library/alloc/src/collections/vec_deque/iter_mut.rs
@@ -1,16 +1,10 @@
-#![feature(ub_checks)]
-use safety::{ensures,requires};
+use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 #[cfg(kani)]
-#[unstable(feature="kani", issue="none")]
 use core::kani;
-#[allow(unused_imports)]
-#[unstable(feature = "ub_checks", issue = "none")]
-use core::ub_checks::*;
-
-use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use core::num::NonZero;
 use core::ops::Try;
 use core::{fmt, mem, slice};
+use safety::requires;
 
 /// A mutable iterator over the elements of a `VecDeque`.
 ///
diff --git a/library/alloc/src/vec/into_iter.rs b/library/alloc/src/vec/into_iter.rs
index d3ea78d8a654c..35ff96027d804 100644
--- a/library/alloc/src/vec/into_iter.rs
+++ b/library/alloc/src/vec/into_iter.rs
@@ -1,16 +1,9 @@
-#![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 core::iter::{
     FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen,
     TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use core::kani;
 use core::marker::PhantomData;
 use core::mem::{ManuallyDrop, MaybeUninit, SizedTypeProperties};
 use core::num::NonZero;
@@ -20,6 +13,8 @@ use core::ptr::{self, NonNull};
 use core::slice::{self};
 use core::{array, fmt};
 
+use safety::requires;
+
 #[cfg(not(no_global_oom_handling))]
 use super::AsVecIntoIter;
 use crate::alloc::{Allocator, Global};
diff --git a/library/core/src/array/iter.rs b/library/core/src/array/iter.rs
index a0d02422bd204..2b9b37c1a89e2 100644
--- a/library/core/src/array/iter.rs
+++ b/library/core/src/array/iter.rs
@@ -1,17 +1,14 @@
 //! Defines the `IntoIter` owned iterator for arrays.
 
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
-
 use crate::intrinsics::transmute_unchecked;
 use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::MaybeUninit;
 use crate::num::NonZero;
 use crate::ops::{IndexRange, Range, Try};
 use crate::{fmt, ptr};
+use safety::requires;
 
 mod iter_inner;
 
diff --git a/library/core/src/char/mod.rs b/library/core/src/char/mod.rs
index 62637e70bb413..185091dd96e5c 100644
--- a/library/core/src/char/mod.rs
+++ b/library/core/src/char/mod.rs
@@ -40,20 +40,16 @@ pub use self::methods::encode_utf16_raw; // perma-unstable
 #[unstable(feature = "char_internals", reason = "exposed only for libstd", issue = "none")]
 pub use self::methods::{encode_utf8_raw, encode_utf8_raw_unchecked}; // perma-unstable
 
-#[rustfmt::skip]
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
-
 use crate::ascii;
 pub(crate) use self::methods::EscapeDebugExtArgs;
 use crate::error::Error;
 use crate::escape::{AlwaysEscaped, EscapeIterInner, MaybeEscaped};
 use crate::fmt::{self, Write};
 use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
+use safety::requires;
 
 // UTF-8 ranges and tags for encoding characters
 const TAG_CONT: u8 = 0b1000_0000;
diff --git a/library/core/src/range/iter.rs b/library/core/src/range/iter.rs
index b5a3ab47b4856..270425612540f 100644
--- a/library/core/src/range/iter.rs
+++ b/library/core/src/range/iter.rs
@@ -1,14 +1,11 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
-
 use crate::iter::{
     FusedIterator, Step, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, TrustedStep,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::range::{Range, RangeFrom, RangeInclusive, legacy};
+use safety::requires;
 
 /// By-value [`Range`] iterator.
 #[unstable(feature = "new_range_api", issue = "125687")]

From f66c8233bb98b7634b08b5ddbd2aa6aa83174bb7 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Aug 2025 09:14:31 +0000
Subject: [PATCH 5/6] fmt

---
 library/alloc/src/collections/vec_deque/iter.rs     | 11 +++--------
 library/alloc/src/collections/vec_deque/iter_mut.rs |  1 +
 library/core/src/array/iter.rs                      |  3 ++-
 library/core/src/char/mod.rs                        |  3 ++-
 library/core/src/iter/adapters/cloned.rs            | 10 ++++------
 library/core/src/iter/adapters/copied.rs            |  5 +++--
 library/core/src/iter/adapters/enumerate.rs         |  8 +++-----
 library/core/src/iter/adapters/fuse.rs              |  8 +++-----
 library/core/src/iter/adapters/map.rs               |  8 +++-----
 library/core/src/iter/adapters/skip.rs              |  8 +++-----
 library/core/src/iter/adapters/zip.rs               |  8 +++-----
 library/core/src/iter/traits/iterator.rs            |  8 +++-----
 library/core/src/range/iter.rs                      |  3 ++-
 library/core/src/slice/iter.rs                      |  2 ++
 library/core/src/str/iter.rs                        |  5 +++--
 15 files changed, 40 insertions(+), 51 deletions(-)

diff --git a/library/alloc/src/collections/vec_deque/iter.rs b/library/alloc/src/collections/vec_deque/iter.rs
index 3ad9d22883575..dcf7480f8e931 100644
--- a/library/alloc/src/collections/vec_deque/iter.rs
+++ b/library/alloc/src/collections/vec_deque/iter.rs
@@ -1,17 +1,12 @@
-#![feature(ub_checks)]
-use safety::{ensures,requires};
+use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 #[cfg(kani)]
-#[unstable(feature="kani", issue="none")]
 use core::kani;
-#[allow(unused_imports)]
-#[unstable(feature = "ub_checks", issue = "none")]
-use core::ub_checks::*;
-
-use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use core::num::NonZero;
 use core::ops::Try;
 use core::{fmt, mem, slice};
 
+use safety::requires;
+
 /// An iterator over the elements of a `VecDeque`.
 ///
 /// This `struct` is created by the [`iter`] method on [`super::VecDeque`]. See its
diff --git a/library/alloc/src/collections/vec_deque/iter_mut.rs b/library/alloc/src/collections/vec_deque/iter_mut.rs
index f51a9a382054c..844c5ce32aab5 100644
--- a/library/alloc/src/collections/vec_deque/iter_mut.rs
+++ b/library/alloc/src/collections/vec_deque/iter_mut.rs
@@ -4,6 +4,7 @@ use core::kani;
 use core::num::NonZero;
 use core::ops::Try;
 use core::{fmt, mem, slice};
+
 use safety::requires;
 
 /// A mutable iterator over the elements of a `VecDeque`.
diff --git a/library/core/src/array/iter.rs b/library/core/src/array/iter.rs
index 2b9b37c1a89e2..111a6735f5186 100644
--- a/library/core/src/array/iter.rs
+++ b/library/core/src/array/iter.rs
@@ -1,5 +1,7 @@
 //! Defines the `IntoIter` owned iterator for arrays.
 
+use safety::requires;
+
 use crate::intrinsics::transmute_unchecked;
 use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccessNoCoerce};
 #[cfg(kani)]
@@ -8,7 +10,6 @@ use crate::mem::MaybeUninit;
 use crate::num::NonZero;
 use crate::ops::{IndexRange, Range, Try};
 use crate::{fmt, ptr};
-use safety::requires;
 
 mod iter_inner;
 
diff --git a/library/core/src/char/mod.rs b/library/core/src/char/mod.rs
index 185091dd96e5c..93d64bc80c33d 100644
--- a/library/core/src/char/mod.rs
+++ b/library/core/src/char/mod.rs
@@ -40,6 +40,8 @@ pub use self::methods::encode_utf16_raw; // perma-unstable
 #[unstable(feature = "char_internals", reason = "exposed only for libstd", issue = "none")]
 pub use self::methods::{encode_utf8_raw, encode_utf8_raw_unchecked}; // perma-unstable
 
+use safety::requires;
+
 use crate::ascii;
 pub(crate) use self::methods::EscapeDebugExtArgs;
 use crate::error::Error;
@@ -49,7 +51,6 @@ use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomA
 #[cfg(kani)]
 use crate::kani;
 use crate::num::NonZero;
-use safety::requires;
 
 // UTF-8 ranges and tags for encoding characters
 const TAG_CONT: u8 = 0b1000_0000;
diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs
index 3f91d0a847ea0..0f05260059880 100644
--- a/library/core/src/iter/adapters/cloned.rs
+++ b/library/core/src/iter/adapters/cloned.rs
@@ -1,14 +1,12 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
-
 use core::num::NonZero;
 
+use safety::requires;
+
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedLen, UncheckedIterator};
+#[cfg(kani)]
+use crate::kani;
 use crate::ops::Try;
 
 /// An iterator that clones the elements of an underlying iterator.
diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs
index 51d60dc589ea4..0b9da45acaa06 100644
--- a/library/core/src/iter/adapters/copied.rs
+++ b/library/core/src/iter/adapters/copied.rs
@@ -1,9 +1,10 @@
 use safety::requires;
-#[cfg(kani)]
-use crate::kani;
+
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::{MaybeUninit, SizedTypeProperties};
 use crate::num::NonZero;
 use crate::ops::Try;
diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs
index 82f8339f4d906..e7e18d178031f 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -1,12 +1,10 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs
index cb862e17eddea..fcad6168d85cd 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -1,8 +1,4 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::intrinsics;
 use crate::iter::adapters::SourceIter;
@@ -10,6 +6,8 @@ use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::{
     FusedIterator, TrustedFused, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::ops::Try;
 
 /// An iterator that yields `None` forever after the underlying iterator
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index 3eb5a69c909f0..c738b8cda957b 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -1,13 +1,11 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::fmt;
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, UncheckedIterator};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs
index 9e1764af80762..ac3cc4c4f1152 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -1,8 +1,4 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::intrinsics::unlikely;
 use crate::iter::adapters::SourceIter;
@@ -11,6 +7,8 @@ use crate::iter::{
     FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, TrustedRandomAccess,
     TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, Try};
 
diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs
index 76d93056fea23..e39f1535bd95d 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -1,14 +1,12 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use crate::cmp;
 use crate::fmt::{self, Debug};
 use crate::iter::{
     FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen, UncheckedIterator,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 
 /// An iterator that iterates two other iterators simultaneously.
diff --git a/library/core/src/iter/traits/iterator.rs b/library/core/src/iter/traits/iterator.rs
index 4e1866395d9bc..b86926e0daf14 100644
--- a/library/core/src/iter/traits/iterator.rs
+++ b/library/core/src/iter/traits/iterator.rs
@@ -1,8 +1,4 @@
-use safety::{ensures,requires};
-#[cfg(kani)]
-use crate::kani;
-#[allow(unused_imports)]
-use crate::ub_checks::*;
+use safety::requires;
 
 use super::super::{
     ArrayChunks, ByRefSized, Chain, Cloned, Copied, Cycle, Enumerate, Filter, FilterMap, FlatMap,
@@ -12,6 +8,8 @@ use super::super::{
 };
 use crate::array;
 use crate::cmp::{self, Ordering};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ChangeOutputType, ControlFlow, FromResidual, Residual, Try};
 
diff --git a/library/core/src/range/iter.rs b/library/core/src/range/iter.rs
index 270425612540f..622a8a95d5cad 100644
--- a/library/core/src/range/iter.rs
+++ b/library/core/src/range/iter.rs
@@ -1,3 +1,5 @@
+use safety::requires;
+
 use crate::iter::{
     FusedIterator, Step, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, TrustedStep,
 };
@@ -5,7 +7,6 @@ use crate::iter::{
 use crate::kani;
 use crate::num::NonZero;
 use crate::range::{Range, RangeFrom, RangeInclusive, legacy};
-use safety::requires;
 
 /// By-value [`Range`] iterator.
 #[unstable(feature = "new_range_api", issue = "125687")]
diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index bcc5251cf8eaf..6f6366ff45386 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -2,7 +2,9 @@
 
 #[macro_use] // import iterator! and forward_iterator!
 mod macros;
+
 use safety::requires;
+
 use super::{from_raw_parts, from_raw_parts_mut};
 use crate::hint::assert_unchecked;
 use crate::iter::{
diff --git a/library/core/src/str/iter.rs b/library/core/src/str/iter.rs
index c9aed66c4af8b..34e2ab79b9d34 100644
--- a/library/core/src/str/iter.rs
+++ b/library/core/src/str/iter.rs
@@ -1,8 +1,7 @@
 //! Iterators for `str` methods.
 
 use safety::requires;
-#[cfg(kani)]
-use crate::kani;
+
 use super::pattern::{DoubleEndedSearcher, Pattern, ReverseSearcher, Searcher};
 use super::validations::{next_code_point, next_code_point_reverse};
 use super::{
@@ -14,6 +13,8 @@ use crate::iter::{
     Chain, Copied, Filter, FlatMap, Flatten, FusedIterator, Map, TrustedLen, TrustedRandomAccess,
     TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 use crate::slice::{self, Split as SliceSplit};

From 616a43ce20b94850cd17575c15a334b868b9dcc0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Aug 2025 09:25:23 +0000
Subject: [PATCH 6/6] fmt

---
 library/core/src/char/mod.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/core/src/char/mod.rs b/library/core/src/char/mod.rs
index 93d64bc80c33d..eed3514716838 100644
--- a/library/core/src/char/mod.rs
+++ b/library/core/src/char/mod.rs
@@ -24,6 +24,8 @@ mod convert;
 mod decode;
 mod methods;
 
+use safety::requires;
+
 // stable re-exports
 #[rustfmt::skip]
 #[stable(feature = "try_from", since = "1.34.0")]
@@ -40,8 +42,7 @@ pub use self::methods::encode_utf16_raw; // perma-unstable
 #[unstable(feature = "char_internals", reason = "exposed only for libstd", issue = "none")]
 pub use self::methods::{encode_utf8_raw, encode_utf8_raw_unchecked}; // perma-unstable
 
-use safety::requires;
-
+#[rustfmt::skip]
 use crate::ascii;
 pub(crate) use self::methods::EscapeDebugExtArgs;
 use crate::error::Error;