Challenge 13: Verify safety of CStr

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

@@ -875,6 +875,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 +1097,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);
+    }
 }