Challenge 13: Verify safety of CStr

[Samuelsills]

Summary

Verify all 14 items listed in Challenge 13. 14 Kani proof harnesses, 0 failures. Bounded verification with MAX_SIZE=32 as permitted by challenge assumptions.

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

Part 2: Harnesses for all 9 safe methods (pre-existing).

Part 3: Contracts and harnesses for all 3 unsafe functions (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 could not be added because the safety crate's proc macro does not currently support methods inside unsafe impl Trait blocks. Safety is verified via CBMC's built-in memory model checks.

Resolves #150

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

[Samuelsills]

Verification Coverage Report

Functions Verified (14/14 ✅)

All public functions containing unsafe code in core::ffi::c_str verified:

• CStr construction, indexing, and conversion functions
• CloneToUninit implementation
• All SAFETY comment preconditions encoded

UBs Checked (automatic via Kani/CBMC)

• ✅ Accessing dangling or misaligned pointers
• ✅ Reading from uninitialized memory
• ✅ Mutating immutable bytes
• ✅ Producing an invalid value

Verification Approach

• Tool: Kani Rust Verifier
• 14 proof harnesses

[Copilot]

Pull request overview

Adds the remaining Kani proof harness coverage for Challenge 13 (CStr safety) by verifying trait-implementation behavior, and documents the verification status in the challenge write-up.

Changes:

• Adds Kani proof harness for CStr’s Index<RangeFrom<usize>> slicing behavior.
• Adds Kani proof harness for CStr’s CloneToUninit implementation.
• Extends the Challenge 13 markdown with a verification summary table covering all 14 items.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File	Description
library/core/src/ffi/c_str.rs	Adds new Kani harnesses for Index<RangeFrom<usize>> and CloneToUninit trait impl verification.
doc/src/challenges/0013-cstr.md	Documents the verification completion/status for all Challenge 13 checklist items.

[Copilot]

check_clone_to_uninit currently passes a destination buffer that is larger than size_of_val(c_str) (always MAX_SIZE). That can mask out-of-bounds writes: an implementation bug that writes past len bytes could still stay within the array and avoid triggering UB checks, even though it would be UB for callers that provide exactly size_of_val(self) bytes as allowed by the trait contract. Consider passing a pointer to a region with exactly len bytes of remaining space (e.g., offset into the fixed array), so any overwrite beyond len is detected, and compare the written region against bytes_with_nul.

Suggested change

	unsafe {
	c_str.clone_to_uninit(dest.as_mut_ptr());
	}
	// Verify the clone copied the correct bytes
	assert_eq!(&dest[..len], bytes_with_nul);
	// Provide exactly `len` bytes of space to `clone_to_uninit` by offsetting
	// into the fixed-size array. Any write past `len` will then be out of bounds.
	let start = MAX_SIZE - len;
	unsafe {
	c_str.clone_to_uninit(dest[start..].as_mut_ptr());
	}
	// Verify the clone copied the correct bytes into the region we passed in
	assert_eq!(&dest[start..start + len], bytes_with_nul);

[Copilot]

This summary hard-codes source line ranges (e.g., "Implemented (lines 193-207)") which will become stale as the file evolves. Prefer a stable reference (file path + item name/harness name) or a link/anchor rather than embedding line numbers in the challenge documentation.

Suggested change

	| `Invariant` trait for `&CStr` | Implemented (lines 193-207) |
	| `Invariant` trait for `&CStr` | Implemented in the `CStr` invariant verification harness |

[Copilot]

In this table you refer to from_bytes_with_nul_unchecked, but earlier in the challenge description the function name is misspelled as from_bytes_with_nul_uncheked. It would be clearer if the document used a consistent spelling throughout (and corrected the earlier typo).