Challenge 13: Verify safety of CStr

Verify all 14 items listed in the challenge specification.
14 Kani proof harnesses, 0 failures. Bounded verification with MAX_SIZE=32.

Part 1: Invariant trait for CStr (pre-existing).

Part 2: Harnesses for all 9 safe methods — from_bytes_until_nul,
from_bytes_with_nul, count_bytes, is_empty, to_bytes,
to_bytes_with_nul, bytes, to_str, as_ptr (pre-existing).

Part 3: Contracts and harnesses for all 3 unsafe functions —
from_ptr, from_bytes_with_nul_unchecked, strlen (pre-existing).

Part 4: New harnesses for trait implementations:
- check_index_range_from: verifies Index<RangeFrom<usize>> preserves
  the CStr invariant when slicing from any valid start index.
- check_clone_to_uninit: verifies CloneToUninit copies correct bytes
  to the destination with no undefined behavior.

Note: A formal #[requires] contract on CloneToUninit::clone_to_uninit
could not be added because the safety crate's proc macro does not
currently support methods inside unsafe impl Trait blocks. The
harness verifies safety via CBMC's built-in memory model checks.

Resolves #150

Author: Samuelsills

doc/src/challenges/0013-cstr.md

@@ -84,3 +84,44 @@ All proofs must automatically ensure the absence of the following undefined beha
 
 Note: All solutions to verification challenges need to satisfy the criteria established in the
 [challenge book](../general-rules.md) in addition to the ones listed above.
+
+-------------------
+
+## Verification Summary
+
+All 14 items verified using Kani proof harnesses with bounded verification (MAX_SIZE=32).
+
+### Part 1: Invariant
+
+| Item | Status |
+|------|--------|
+| `Invariant` trait for `&CStr` | Implemented (lines 193-207) |
+
+### Part 2: Safe Methods
+
+| Function | Harness | Status |
+|----------|---------|--------|
+| `from_bytes_until_nul` | `check_from_bytes_until_nul` | VERIFIED |
+| `from_bytes_with_nul` | `check_from_bytes_with_nul` | VERIFIED |
+| `count_bytes` | `check_count_bytes` | VERIFIED |
+| `is_empty` | `check_is_empty` | VERIFIED |
+| `to_bytes` | `check_to_bytes` | VERIFIED |
+| `to_bytes_with_nul` | `check_to_bytes_with_nul` | VERIFIED |
+| `bytes` | `check_bytes` | VERIFIED |
+| `to_str` | `check_to_str` | VERIFIED |
+| `as_ptr` | `check_as_ptr` | VERIFIED |
+
+### Part 3: Unsafe Functions
+
+| Function | Contract | Harness | Status |
+|----------|----------|---------|--------|
+| `from_ptr` | `#[requires]` + `#[ensures]` | `check_from_ptr_contract` | VERIFIED |
+| `from_bytes_with_nul_unchecked` | `#[requires]` + `#[ensures]` | `check_from_bytes_with_nul_unchecked` | VERIFIED |
+| `strlen` | `#[requires]` + `#[ensures]` | `check_strlen_contract` | VERIFIED |
+
+### Part 4: Trait Implementations
+
+| Trait | Harness | Status |
+|-------|---------|--------|
+| `ops::Index<ops::RangeFrom<usize>>` | `check_index_range_from` | VERIFIED |
+| `CloneToUninit` | `check_clone_to_uninit` | VERIFIED |

library/core/src/ffi/c_str.rs

@@ -146,7 +146,10 @@ impl fmt::Display for FromBytesWithNulError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             Self::InteriorNul { position } => {
-                write!(f, "data provided contains an interior nul byte at byte position {position}")
+                write!(
+                    f,
+                    "data provided contains an interior nul byte at byte position {position}"
+                )
             }
             Self::NotNulTerminated => write!(f, "data provided is not nul terminated"),
         }
@@ -821,7 +824,10 @@ unsafe impl Sync for Bytes<'_> {}
 impl<'a> Bytes<'a> {
     #[inline]
     fn new(s: &'a CStr) -> Self {
-        Self { ptr: s.as_non_null_ptr().cast(), phantom: PhantomData }
+        Self {
+            ptr: s.as_non_null_ptr().cast(),
+            phantom: PhantomData,
+        }
     }
 
     #[inline]
@@ -858,7 +864,11 @@ impl Iterator for Bytes<'_> {
 
     #[inline]
     fn size_hint(&self) -> (usize, Option<usize>) {
-        if self.is_empty() { (0, Some(0)) } else { (1, None) }
+        if self.is_empty() {
+            (0, Some(0))
+        } else {
+            (1, None)
+        }
     }
 
     #[inline]
@@ -875,6 +885,7 @@ impl FusedIterator for Bytes<'_> {}
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
+    use crate::clone::CloneToUninit;
 
     // Helper function
     fn arbitrary_cstr(slice: &[u8]) -> &CStr {
@@ -1096,4 +1107,46 @@ mod verify {
         assert_eq!(expected_is_empty, c_str.is_empty());
         assert!(c_str.is_safe());
     }
+
+    // ops::Index<ops::RangeFrom<usize>> for CStr
+    #[kani::proof]
+    #[kani::unwind(33)]
+    fn check_index_range_from() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        let start: usize = kani::any();
+        let bytes_with_nul = c_str.to_bytes_with_nul();
+
+        if start < bytes_with_nul.len() {
+            let sub_cstr = &c_str[start..];
+            assert!(sub_cstr.is_safe());
+            assert_eq!(sub_cstr.to_bytes_with_nul(), &bytes_with_nul[start..]);
+        }
+        // else: would panic (expected behavior, not UB)
+    }
+
+    // CloneToUninit for CStr
+    #[kani::proof]
+    #[kani::unwind(33)]
+    fn check_clone_to_uninit() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        let bytes_with_nul = c_str.to_bytes_with_nul();
+        let len = bytes_with_nul.len();
+        kani::assume(len <= MAX_SIZE);
+
+        let mut dest: [u8; MAX_SIZE] = [0u8; MAX_SIZE];
+        unsafe {
+            c_str.clone_to_uninit(dest.as_mut_ptr());
+        }
+
+        // Verify the clone copied the correct bytes
+        assert_eq!(&dest[..len], bytes_with_nul);
+    }
 }