Verify safety of CStr CloneToUninit and Index<RangeFrom> (Challenge 13)

Add the final 2 verification harnesses to complete Challenge 13:

- check_clone_to_uninit: Verifies the unsafe CloneToUninit impl for CStr
  correctly copies all bytes (including NUL terminator) and produces a
  valid CStr at the destination. Includes safety contract on
  clone_to_uninit requiring non-null dest pointer.

- check_index_from: Verifies ops::Index<RangeFrom<usize>> for CStr
  produces a valid CStr that maintains the safety invariant and
  matches the expected tail of the original bytes.

Both harnesses are bounded (MAX_SIZE=16/32) with appropriate unwind
limits and verify the CStr is_safe() invariant holds.

Author: jrey8343

library/core/src/clone.rs

@@ -37,6 +37,9 @@
 #![stable(feature = "rust1", since = "1.0.0")]
 
 use crate::marker::{Destruct, PointeeSized};
+#[cfg(kani)]
+use crate::kani;
+use safety::requires;
 
 mod uninit;
 
@@ -544,6 +547,7 @@ unsafe impl CloneToUninit for str {
 #[unstable(feature = "clone_to_uninit", issue = "126799")]
 unsafe impl CloneToUninit for crate::ffi::CStr {
     #[cfg_attr(debug_assertions, track_caller)]
+    #[requires(!dest.is_null())]
     unsafe fn clone_to_uninit(&self, dest: *mut u8) {
         // SAFETY: For now, CStr is just a #[repr(trasnsparent)] [c_char] with some invariants.
         // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul).

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,58 @@ 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_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 bytes_with_nul = c_str.to_bytes_with_nul();
+        let idx: usize = kani::any();
+        kani::assume(idx < bytes_with_nul.len());
+
+        let indexed = &c_str[idx..];
+        assert!(indexed.is_safe());
+        // The indexed result should correspond to the tail of the original bytes
+        assert_eq!(indexed.to_bytes_with_nul(), &bytes_with_nul[idx..]);
+    }
+
+    // CloneToUninit for CStr
+    #[kani::proof]
+    #[kani::unwind(17)]
+    fn check_clone_to_uninit() {
+        const MAX_SIZE: usize = 16;
+        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();
+
+        // Allocate destination buffer
+        let mut buf = [core::mem::MaybeUninit::<u8>::uninit(); MAX_SIZE];
+        let dest = buf.as_mut_ptr() as *mut u8;
+
+        // Call the unsafe clone_to_uninit
+        unsafe {
+            c_str.clone_to_uninit(dest);
+        }
+
+        // Verify the cloned bytes match the original
+        unsafe {
+            for i in 0..len {
+                assert_eq!(*dest.add(i), bytes_with_nul[i]);
+            }
+        }
+
+        // Verify we can reconstruct a valid CStr from the cloned data
+        let cloned_slice = unsafe { core::slice::from_raw_parts(dest, len) };
+        let cloned_cstr = CStr::from_bytes_with_nul(cloned_slice);
+        assert!(cloned_cstr.is_ok());
+        assert!(cloned_cstr.unwrap().is_safe());
+    }
 }