Add safety preconditions to core/src/iter/range.rs (model-checking#331)

For the signed and unsigned methods in the macros, I added contracts
that require the checked operations to succeed, which is what the safety
comments are stating.

These contracts formalize the safety requirements that were previously
only documented in comments.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <carolynzech@gmail.com>

Author: tautschnig

.github/workflows/kani.yml

@@ -102,6 +102,8 @@ jobs:
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
             --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \
+            --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::backward_unchecked" \
+            --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::forward_unchecked" \
             --include-pattern alloc::__default_lib_allocator:: \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \

library/core/src/iter/range.rs

@@ -1,7 +1,11 @@
+use safety::requires;
+
 use super::{
     FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, TrustedStep,
 };
 use crate::ascii::Char as AsciiChar;
+#[cfg(kani)]
+use crate::kani;
 use crate::mem;
 use crate::net::{Ipv4Addr, Ipv6Addr};
 use crate::num::NonZero;
@@ -184,12 +188,14 @@ pub trait Step: Clone + PartialOrd + Sized {
 // than the signed::MAX value. Therefore `as` casting to the signed type would be incorrect.
 macro_rules! step_signed_methods {
     ($unsigned: ty) => {
+        #[requires(start.checked_add_unsigned(n as $unsigned).is_some())]
         #[inline]
         unsafe fn forward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start + n` doesn't overflow.
             unsafe { start.checked_add_unsigned(n as $unsigned).unwrap_unchecked() }
         }
 
+        #[requires(start.checked_sub_unsigned(n as $unsigned).is_some())]
         #[inline]
         unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start - n` doesn't overflow.
@@ -200,12 +206,14 @@ macro_rules! step_signed_methods {
 
 macro_rules! step_unsigned_methods {
     () => {
+        #[requires(start.checked_add(n as Self).is_some())]
         #[inline]
         unsafe fn forward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start + n` doesn't overflow.
             unsafe { start.unchecked_add(n as Self) }
         }
 
+        #[requires(start >= (n as Self))]
         #[inline]
         unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start - n` doesn't overflow.
@@ -495,6 +503,13 @@ impl Step for char {
         Some(unsafe { char::from_u32_unchecked(res) })
     }
 
+    #[requires({
+        (start as u32).checked_add(count as u32).is_some_and(|dist|
+            (start as u32) >= 0xD800 ||
+            dist < 0xD800 ||
+            dist.checked_add(0x800).is_some()
+         )
+    })]
     #[inline]
     unsafe fn forward_unchecked(start: char, count: usize) -> char {
         let start = start as u32;
@@ -511,6 +526,13 @@ impl Step for char {
         unsafe { char::from_u32_unchecked(res) }
     }
 
+    #[requires({
+        (start as u32).checked_sub(count as u32).is_some_and(|dist|
+            (start as u32) < 0xE000 ||
+            dist >= 0xE000 ||
+            dist.checked_sub(0x800).is_some()
+         )
+    })]
     #[inline]
     unsafe fn backward_unchecked(start: char, count: usize) -> char {
         let start = start as u32;
@@ -549,6 +571,7 @@ impl Step for AsciiChar {
         Some(unsafe { AsciiChar::from_u8_unchecked(end) })
     }
 
+    #[requires(count < 256 && start.to_u8().checked_add(count as u8).is_some())]
     #[inline]
     unsafe fn forward_unchecked(start: AsciiChar, count: usize) -> AsciiChar {
         // SAFETY: Caller asserts that result is a valid ASCII character,
@@ -559,6 +582,7 @@ impl Step for AsciiChar {
         unsafe { AsciiChar::from_u8_unchecked(end) }
     }
 
+    #[requires(count < 256 && start.to_u8().checked_sub(count as u8).is_some())]
     #[inline]
     unsafe fn backward_unchecked(start: AsciiChar, count: usize) -> AsciiChar {
         // SAFETY: Caller asserts that result is a valid ASCII character,
@@ -587,13 +611,15 @@ impl Step for Ipv4Addr {
         u32::backward_checked(start.to_bits(), count).map(Ipv4Addr::from_bits)
     }
 
+    #[requires(start.to_bits().checked_add(count as u32).is_some())]
     #[inline]
     unsafe fn forward_unchecked(start: Ipv4Addr, count: usize) -> Ipv4Addr {
         // SAFETY: Since u32 and Ipv4Addr are losslessly convertible,
         //   this is as safe as the u32 version.
         Ipv4Addr::from_bits(unsafe { u32::forward_unchecked(start.to_bits(), count) })
     }
 
+    #[requires(start.to_bits().checked_sub(count as u32).is_some())]
     #[inline]
     unsafe fn backward_unchecked(start: Ipv4Addr, count: usize) -> Ipv4Addr {
         // SAFETY: Since u32 and Ipv4Addr are losslessly convertible,
@@ -619,13 +645,15 @@ impl Step for Ipv6Addr {
         u128::backward_checked(start.to_bits(), count).map(Ipv6Addr::from_bits)
     }
 
+    #[requires(start.to_bits().checked_add(count as u128).is_some())]
     #[inline]
     unsafe fn forward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {
         // SAFETY: Since u128 and Ipv6Addr are losslessly convertible,
         //   this is as safe as the u128 version.
         Ipv6Addr::from_bits(unsafe { u128::forward_unchecked(start.to_bits(), count) })
     }
 
+    #[requires(start.to_bits().checked_sub(count as u128).is_some())]
     #[inline]
     unsafe fn backward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {
         // SAFETY: Since u128 and Ipv6Addr are losslessly convertible,