A bunch of LLM-generated contracts

Author: Fedor Ryabinin

library/core/src/hint.rs

@@ -4,6 +4,12 @@
 //!
 //! Hints may be compile time or runtime.
 
+use safety::{ensures,requires};
+#[cfg(kani)]
+use crate::kani;
+#[allow(unused_imports)]
+use crate::ub_checks::*;
+
 use crate::mem::MaybeUninit;
 use crate::{intrinsics, ub_checks};
 
@@ -99,6 +105,7 @@ use crate::{intrinsics, ub_checks};
 #[stable(feature = "unreachable", since = "1.27.0")]
 #[rustc_const_stable(feature = "const_unreachable_unchecked", since = "1.57.0")]
 #[track_caller]
+#[requires(false)]
 pub const unsafe fn unreachable_unchecked() -> ! {
     ub_checks::assert_unsafe_precondition!(
         check_language_ub,
@@ -198,6 +205,7 @@ pub const unsafe fn unreachable_unchecked() -> ! {
 #[doc(alias = "assume")]
 #[stable(feature = "hint_assert_unchecked", since = "1.81.0")]
 #[rustc_const_stable(feature = "hint_assert_unchecked", since = "1.81.0")]
+#[requires(cond == true)]
 pub const unsafe fn assert_unchecked(cond: bool) {
     // SAFETY: The caller promised `cond` is true.
     unsafe {

library/core/src/iter/adapters/step_by.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::{TrustedLen, TrustedRandomAccess, from_fn};
 use crate::num::NonZero;
@@ -40,6 +46,7 @@ impl<I> StepBy<I> {
     /// The `step` that was originally passed to `Iterator::step_by(step)`,
     /// aka `self.step_minus_one + 1`.
     #[inline]
+    #[requires(self.step_minus_one != usize::MAX)]
     fn original_step(&self) -> NonZero<usize> {
         // SAFETY: By type invariant, `step_minus_one` cannot be `MAX`, which
         // means the addition cannot overflow and the result cannot be zero.

library/core/src/ops/index_range.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, TrustedLen};
 use crate::num::NonZero;
 use crate::ops::{NeverShortCircuit, Try};
@@ -20,6 +26,7 @@ impl IndexRange {
     /// - `start <= end`
     #[inline]
     #[track_caller]
+    #[requires(start <= end)]
     pub(crate) const unsafe fn new_unchecked(start: usize, end: usize) -> Self {
         ub_checks::assert_unsafe_precondition!(
             check_library_ub,
@@ -54,6 +61,8 @@ impl IndexRange {
     /// # Safety
     /// - Can only be called when `start < end`, aka when `len > 0`.
     #[inline]
+    #[requires(self.start < self.end)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> usize {
         debug_assert!(self.start < self.end);
 
@@ -66,6 +75,8 @@ impl IndexRange {
     /// # Safety
     /// - Can only be called when `start < end`, aka when `len > 0`.
     #[inline]
+    #[requires(self.start < self.end)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_back_unchecked(&mut self) -> usize {
         debug_assert!(self.start < self.end);
 
@@ -225,3 +236,34 @@ impl ExactSizeIterator for IndexRange {
 unsafe impl TrustedLen for IndexRange {}
 
 impl FusedIterator for IndexRange {}
+#[cfg(kani)]
+mod verify {
+    use super::*;
+    #[kani::proof_for_contract(IndexRange::new_unchecked)]
+    fn proof_for_index_range_new_unchecked() {
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+
+        unsafe { IndexRange::new_unchecked(start, end) };
+    }
+
+    #[kani::proof_for_contract(IndexRange::next_unchecked)]
+    fn proof_for_index_range_next_unchecked() {
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+
+        let mut range = unsafe { IndexRange::new_unchecked(start, end) };
+
+        unsafe { range.next_unchecked() };
+    }
+
+    #[kani::proof_for_contract(IndexRange::next_back_unchecked)]
+    fn proof_for_index_range_next_back_unchecked() {
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+
+        let mut range = unsafe { IndexRange::new_unchecked(start, end) };
+
+        unsafe { range.next_back_unchecked() };
+    }
+}

library/std/src/sync/mpmc/context.rs

@@ -1,5 +1,14 @@
 //! Thread-local channel context.
 
+#![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 super::select::Selected;
 use super::waker::current_thread_id;
 use crate::cell::Cell;
@@ -116,6 +125,7 @@ impl Context {
     /// # Safety
     /// This may only be called from the thread this `Context` belongs to.
     #[inline]
+    #[requires(self.thread_id() == current_thread_id())]
     pub unsafe fn wait_until(&self, deadline: Option<Instant>) -> Selected {
         loop {
             // Check whether an operation has been selected.

library/stdarch/crates/core_arch/src/x86/sse3.rs

@@ -1,5 +1,14 @@
 //! Streaming SIMD Extensions 3 (SSE3)
 
+#![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 crate::core_arch::{simd::*, x86::*};
 use crate::intrinsics::simd::*;
 
@@ -99,6 +108,7 @@ pub fn _mm_hsub_ps(a: __m128, b: __m128) -> __m128 {
 #[target_feature(enable = "sse3")]
 #[cfg_attr(test, assert_instr(lddqu))]
 #[stable(feature = "simd_x86", since = "1.27.0")]
+#[requires(can_dereference(mem_addr))]
 pub unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i {
     transmute(lddqu(mem_addr as *const _))
 }
@@ -260,3 +270,37 @@ mod tests {
         assert_eq_m128d(r, _mm_setr_pd(d, d));
     }
 }
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    #[cfg(kani)]
+    #[kani::proof_for_contract(unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i)]
+    fn proof_mm_lddqu_si128() {
+        // Create a valid __m128i value
+        let mut value = [0i32; 4];
+
+        // Get a pointer to the value
+        let ptr: *const __m128i = value.as_ptr() as *const __m128i;
+
+        // Call the function with the valid pointer
+        unsafe {
+            let _result = _mm_lddqu_si128(ptr);
+        }
+    }
+
+    #[cfg(kani)]
+    #[kani::proof_for_contract(unsafe fn _mm_loadddup_pd(mem_addr: *const f64) -> __m128d)]
+    fn proof_mm_loadddup_pd() {
+        // Create a valid f64 value
+        let value: f64 = 0.0;
+
+        // Get a pointer to the value
+        let ptr: *const f64 = &value;
+
+        // Call the function with the valid pointer
+        unsafe {
+            let _result = _mm_loadddup_pd(ptr);
+        }
+    }
+}

library/stdarch/crates/core_arch/src/x86/sse41.rs

@@ -1,5 +1,14 @@
 //! Streaming SIMD Extensions 4.1 (SSE4.1)
 
+#![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 crate::core_arch::{simd::*, x86::*};
 use crate::intrinsics::simd::*;
 
@@ -1132,6 +1141,8 @@ pub fn _mm_test_mix_ones_zeros(a: __m128i, mask: __m128i) -> i32 {
 #[target_feature(enable = "sse4.1")]
 #[cfg_attr(test, assert_instr(movntdqa))]
 #[stable(feature = "simd_x86_updates", since = "1.82.0")]
+#[requires(can_dereference(mem_addr))]
+#[requires(mem_addr as usize % 16 == 0)]
 pub unsafe fn _mm_stream_load_si128(mem_addr: *const __m128i) -> __m128i {
     let dst: __m128i;
     crate::arch::asm!(
@@ -1939,3 +1950,26 @@ mod tests {
         assert_eq_m128i(a, r);
     }
 }
+#[cfg(kani)]
+mod verify {
+    use super::*;
+    #[cfg(kani)]
+    #[repr(align(16))]
+    struct Aligned16Bytes {
+        data: [u8; 16],
+    }
+
+    #[cfg(kani)]
+    #[kani::proof_for_contract(_mm_stream_load_si128)]
+    fn verify_mm_stream_load_si128() {
+        // Allocate memory for __m128i (16 bytes) with proper alignment
+        let mut aligned_data = Aligned16Bytes { data: [0u8; 16] };
+        let ptr = &aligned_data.data as *const _ as *const __m128i;
+
+        // Call the function with our properly aligned pointer
+        unsafe {
+            let _result = _mm_stream_load_si128(ptr);
+            // No postconditions to verify
+        }
+    }
+}