From ec53992030061677d6c2cc089156030d22b789b4 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Wed, 2 Sep 2026 13:50:39 -0400 Subject: [PATCH 1/6] Challenge 13: contracts and proofs for CStr trait implementations and safe methods --- library/core/src/clone.rs | 52 +++++++++ library/core/src/ffi/c_str.rs | 194 ++++++++++++++++++++++++++++++++++ 2 files changed, 246 insertions(+) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index bd6d929c6d2b0..0c9d80378e1bf 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -36,6 +36,10 @@ #![stable(feature = "rust1", since = "1.0.0")] +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; use crate::marker::{Destruct, PointeeSized}; mod uninit; @@ -677,6 +681,24 @@ 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)] + // Safety precondition per the trait docs: `dest` must be valid for + // writes of `size_of_val(self)` bytes (alignment is 1 for [c_char]). + // The docs state no non-overlap condition; the contract mirrors the + // documented obligations. + #[requires(crate::ub_checks::can_write(crate::ptr::slice_from_raw_parts_mut( + dest, + crate::mem::size_of_val(self) + )))] + // The clone reproduces the full NUL-terminated contents at `dest`. + #[ensures(|_| unsafe { + crate::slice::from_raw_parts(dest, self.to_bytes_with_nul().len()) + } == self.to_bytes_with_nul())] + // The safety crate has no `modifies` wrapper; kani's form is applied + // directly under cfg_attr so the non-kani build is untouched. + #[cfg_attr( + kani, + kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))) + )] 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). @@ -797,3 +819,33 @@ mod impls { #[stable(feature = "rust1", since = "1.0.0")] impl !Clone for &mut T {} } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::CloneToUninit; + use crate::ffi::CStr; + use crate::kani; + use crate::ub_checks::Invariant; + + // ::clone_to_uninit — byte-copy of the full + // NUL-terminated contents into caller-provided storage. + #[kani::proof_for_contract(::clone_to_uninit)] + #[kani::unwind(33)] + fn check_clone_to_uninit_contract() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + kani::assume(slice.len() > 0 && slice[slice.len() - 1] == 0); + kani::cover(true, "nul-terminated source slice admitted"); + let c_str = CStr::from_bytes_until_nul(slice).unwrap(); + assert!(c_str.is_safe()); + let len = c_str.to_bytes_with_nul().len(); + + let mut dest = [0u8; MAX_SIZE]; + unsafe { c_str.clone_to_uninit(dest.as_mut_ptr()) }; + // Semantic: the clone reproduces the source bytes including the NUL. + assert_eq!(&dest[..len], c_str.to_bytes_with_nul()); + kani::cover(true, "clone completed with byte-equal contents"); + } +} diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index e299f44e03181..cc3dab63474e1 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -14,6 +14,8 @@ use crate::num::niche_types::UsizeNoHighBitMinusOne; use crate::ptr::NonNull; use crate::slice::memchr; use crate::ub_checks::Invariant; +// Used only in contract attributes and cfg(kani) code, which compile away +// in normal builds; the allow keeps the non-kani build warning-free. #[allow(unused_imports)] use crate::ub_checks::can_dereference; use crate::{fmt, ops, range, slice, str}; @@ -347,6 +349,8 @@ impl CStr { /// #[stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")] #[rustc_const_stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")] + // Postcondition: on success the returned CStr satisfies the safety invariant. + #[ensures(|result| result.as_ref().map_or(true, |c| c.is_safe()))] pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> { let nul_pos = memchr::memchr(0, bytes); match nul_pos { @@ -400,6 +404,8 @@ impl CStr { /// ``` #[stable(feature = "cstr_from_bytes", since = "1.10.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + // Postcondition: on success the returned CStr satisfies the safety invariant. + #[ensures(|result| result.as_ref().map_or(true, |c| c.is_safe()))] pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> { let nul_pos = memchr::memchr(0, bytes); match nul_pos { @@ -536,6 +542,12 @@ impl CStr { #[rustc_const_stable(feature = "const_str_as_ptr", since = "1.32.0")] #[rustc_as_ptr] #[rustc_never_returns_null_ptr] + // The returned pointer addresses the string's full NUL-terminated + // contents, `self.inner.len()` bytes ending in the terminator; `inner` + // is nonempty by the type's safety invariant, so the index below + // cannot underflow. + #[ensures(|&result| can_dereference(crate::ptr::slice_from_raw_parts(result, self.inner.len())))] + #[ensures(|&result| unsafe { *result.add(self.inner.len() - 1) } == 0)] pub const fn as_ptr(&self) -> *const c_char { self.inner.as_ptr() } @@ -567,6 +579,10 @@ impl CStr { #[doc(alias("len", "strlen"))] #[stable(feature = "cstr_count_bytes", since = "1.79.0")] #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")] + // Cross-accessor consistency: the count excludes the terminating NUL that + // `to_bytes_with_nul` includes; `result + 1` cannot overflow since + // `result == self.inner.len() - 1`. + #[ensures(|&result| result + 1 == self.to_bytes_with_nul().len())] pub const fn count_bytes(&self) -> usize { // SAFETY: This length includes the nul-terminator, so it's at least one. unsafe { self.inner.len().unchecked_sub(1) } @@ -583,6 +599,8 @@ impl CStr { #[inline] #[stable(feature = "cstr_is_empty", since = "1.71.0")] #[rustc_const_stable(feature = "cstr_is_empty", since = "1.71.0")] + // Empty means exactly zero content bytes before the NUL. + #[ensures(|&result| result == (self.count_bytes() == 0))] pub const fn is_empty(&self) -> bool { // SAFETY: We know there is at least one byte; for empty strings it // is the NUL terminator. @@ -609,6 +627,10 @@ impl CStr { without modifying the original"] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + // The content bytes contain no NUL and exclude the terminator; + // `result.len() + 1` cannot overflow since the full view includes the NUL. + #[ensures(|result| !result.contains(&0))] + #[ensures(|result| result.len() + 1 == self.to_bytes_with_nul().len())] pub const fn to_bytes(&self) -> &[u8] { let bytes = self.to_bytes_with_nul(); // FIXME(const-hack) replace with range index @@ -635,6 +657,9 @@ impl CStr { without modifying the original"] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + // The full byte view is the invariant shape: NUL-terminated, no interior NUL. + #[ensures(|result| result.len() > 0 && result[result.len() - 1] == 0 + && !result[..result.len() - 1].contains(&0))] pub const fn to_bytes_with_nul(&self) -> &[u8] { // SAFETY: Transmuting a slice of `c_char`s to a slice of `u8`s // is safe on all supported targets. @@ -660,6 +685,8 @@ impl CStr { /// ``` #[inline] #[unstable(feature = "cstr_bytes", issue = "112115")] + // Deliberately uncontracted: the iterator's invariant-relevant behavior is + // proven by the `check_bytes` harness. pub fn bytes(&self) -> Bytes<'_> { Bytes::new(self) } @@ -679,6 +706,8 @@ impl CStr { /// ``` #[stable(feature = "cstr_to_str", since = "1.4.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + // Deliberately uncontracted: UTF-8/round-trip behavior is proven by the + // `check_to_str` harness. pub const fn to_str(&self) -> Result<&str, str::Utf8Error> { // N.B., when `CStr` is changed to perform the length check in `.to_bytes()` // instead of in `from_ptr()`, it may be worth considering if this should @@ -760,6 +789,11 @@ impl ops::Index> for CStr { type Output = CStr; #[inline] + // The tail of a valid `CStr` is itself a valid `CStr`; the postcondition + // binds on normal return only — the out-of-bounds panic path is proven + // separately by the `check_index_range_from_out_of_bounds` harness. + #[ensures(|result: &&CStr| result.is_safe())] + #[ensures(|result: &&CStr| result.to_bytes_with_nul() == &self.to_bytes_with_nul()[index.start..])] fn index(&self, index: ops::RangeFrom) -> &CStr { let bytes = self.to_bytes_with_nul(); // we need to manually check the starting index to account for the null @@ -955,6 +989,7 @@ mod verify { fn arbitrary_cstr(slice: &[u8]) -> &CStr { // At a minimum, the slice has a null terminator to form a valid CStr. kani::assume(slice.len() > 0 && slice[slice.len() - 1] == 0); + kani::cover(true, "arbitrary_cstr admitted a nul-terminated slice"); let result = CStr::from_bytes_until_nul(&slice); // Given the assumption, from_bytes_until_nul should never fail assert!(result.is_ok()); @@ -975,7 +1010,10 @@ mod verify { let result = CStr::from_bytes_until_nul(slice); if let Ok(c_str) = result { + kani::cover(true, "from_bytes_until_nul constructed a CStr"); assert!(c_str.is_safe()); + } else { + kani::cover(true, "from_bytes_until_nul rejected a nul-free slice"); } } @@ -1028,7 +1066,10 @@ mod verify { // a double conversion here and assertion, if the bytes are still the same, function is valid let str_result = c_str.to_str(); if let Ok(s) = str_result { + kani::cover(true, "to_str produced a valid str"); assert_eq!(s.as_bytes(), c_str.to_bytes()); + } else { + kani::cover(true, "to_str rejected non-UTF-8 contents"); } assert!(c_str.is_safe()); } @@ -1074,7 +1115,10 @@ mod verify { let result = CStr::from_bytes_with_nul(slice); if let Ok(c_str) = result { + kani::cover(true, "from_bytes_with_nul accepted a well-formed slice"); assert!(c_str.is_safe()); + } else { + kani::cover(true, "from_bytes_with_nul rejected a malformed slice"); } } @@ -1175,4 +1219,154 @@ mod verify { assert_eq!(expected_is_empty, c_str.is_empty()); assert!(c_str.is_safe()); } + + // impl ops::Index> for CStr — in-bounds tail slicing + #[kani::proof_for_contract(>>::index)] + #[kani::unwind(17)] // bounded at 16: at 32 this harness took 263s. + fn check_index_range_from_contract() { + 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 len = c_str.to_bytes_with_nul().len(); + let start: usize = kani::any_where(|&s: &usize| s < len); + kani::cover(true, "in-bounds start index admitted"); + + let tail: &CStr = &c_str[start..]; + // Semantic: the tail is exactly the byte suffix, still NUL-terminated. + assert_eq!(tail.to_bytes_with_nul(), &c_str.to_bytes_with_nul()[start..]); + assert!(tail.is_safe()); + kani::cover(true, "tail CStr produced and validated"); + } + + // The documented out-of-bounds branch of RangeFrom indexing panics. + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(17)] // bounded at 16: at 32 this harness took 30s. + fn check_index_range_from_out_of_bounds() { + 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 len = c_str.to_bytes_with_nul().len(); + let start: usize = kani::any_where(|&s: &usize| s >= len); + kani::cover(true, "out-of-bounds start index admitted"); + let _ = &c_str[start..]; + } + + // The postcondition on from_bytes_until_nul: success implies the safety invariant. + #[kani::proof_for_contract(CStr::from_bytes_until_nul)] + #[kani::unwind(33)] + fn check_from_bytes_until_nul_contract() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + match CStr::from_bytes_until_nul(slice) { + Ok(c_str) => { + kani::cover(true, "until_nul constructed a CStr"); + assert!(c_str.is_safe()); + } + Err(_) => kani::cover(true, "until_nul rejected a nul-free slice"), + } + } + + // The postcondition on from_bytes_with_nul: success implies the safety invariant. + #[kani::proof_for_contract(CStr::from_bytes_with_nul)] + // Bounded at 8: at 16 this proof runs 269-328s locally and exceeded CI's + // 10-minute harness timeout; at 8 it verifies in under a minute. + #[kani::unwind(9)] + fn check_from_bytes_with_nul_contract() { + const MAX_SIZE: usize = 8; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + match CStr::from_bytes_with_nul(slice) { + Ok(c_str) => { + kani::cover(true, "with_nul accepted a well-formed slice"); + assert!(c_str.is_safe()); + } + Err(_) => kani::cover(true, "with_nul rejected a malformed slice"), + } + } + + #[kani::proof_for_contract(CStr::count_bytes)] + #[kani::unwind(33)] + fn check_count_bytes_contract() { + 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 n = c_str.count_bytes(); + kani::cover(true, "count_bytes returned"); + assert_eq!(n + 1, c_str.to_bytes_with_nul().len()); + } + + #[kani::proof_for_contract(CStr::is_empty)] + #[kani::unwind(33)] + fn check_is_empty_contract() { + 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 e = c_str.is_empty(); + kani::cover(e, "empty CStr reached"); + kani::cover(!e, "non-empty CStr reached"); + assert_eq!(e, c_str.count_bytes() == 0); + } + + #[kani::proof_for_contract(CStr::to_bytes)] + #[kani::unwind(33)] + fn check_to_bytes_contract() { + 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 b = c_str.to_bytes(); + kani::cover(true, "to_bytes returned"); + assert!(!b.contains(&0)); + assert_eq!(b.len() + 1, c_str.to_bytes_with_nul().len()); + } + + #[kani::proof_for_contract(CStr::to_bytes_with_nul)] + #[kani::unwind(33)] + fn check_to_bytes_with_nul_contract() { + 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 b = c_str.to_bytes_with_nul(); + kani::cover(true, "to_bytes_with_nul returned"); + assert!(b.len() > 0 && b[b.len() - 1] == 0 && !b[..b.len() - 1].contains(&0)); + } + + #[kani::proof_for_contract(CStr::as_ptr)] + #[kani::unwind(33)] + fn check_as_ptr_contract() { + 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); + kani::cover(true, "as_ptr contract exercised"); + let _ = c_str.as_ptr(); + } + + // `is_safe` matches the conditions documented on the `Invariant` impl — + // nonempty, NUL-terminated, no interior NUL — checked from both sides + // on arbitrary bytes. `is_safe` is itself the specification, so it is + // checked directly rather than through a contract. + #[kani::proof] + #[kani::unwind(33)] + fn check_invariant_fidelity() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let well_formed = !slice.is_empty() + && slice[slice.len() - 1] == 0 + && !slice[..slice.len() - 1].contains(&0); + // SAFETY: the same layout cast `from_bytes_with_nul_unchecked` uses; + // the reference is only passed to `is_safe`, which handles any shape. + let c_str: &CStr = unsafe { &*(slice as *const [u8] as *const CStr) }; + assert_eq!(c_str.is_safe(), well_formed); + kani::cover(well_formed, "well-formed shape reached"); + kani::cover(!well_formed, "malformed shape reached"); + } } From 32096e0a81fa762b665e4077bcf475b021467f79 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Mon, 14 Sep 2026 23:31:41 -0400 Subject: [PATCH 2/6] Verify Index as a plain proof at the pinned Kani proof_for_contract on a generic trait's method fails to resolve at the pin (model-checking/kani#1997); the two #[ensures] postconditions are asserted directly on the result. The non-generic CloneToUninit pfc and all inherent-method pfc resolve and are unchanged. --- library/core/src/ffi/c_str.rs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index cc3dab63474e1..24748420f6960 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1220,8 +1220,15 @@ mod verify { assert!(c_str.is_safe()); } - // impl ops::Index> for CStr — in-bounds tail slicing - #[kani::proof_for_contract(>>::index)] + // impl ops::Index> for CStr — in-bounds tail slicing. + // Verified as a plain proof rather than proof_for_contract: at the pinned + // Kani, a pfc target on a generic trait's method (Index>) + // fails to resolve (model-checking/kani#1997) — "unable to find + // implementation of associated function Index::index for CStr". The two + // #[ensures] postconditions on `index` are asserted directly on the result + // below. (Non-generic trait pfc, e.g. CloneToUninit, still resolves and is + // kept in contract form.) + #[kani::proof] #[kani::unwind(17)] // bounded at 16: at 32 this harness took 263s. fn check_index_range_from_contract() { const MAX_SIZE: usize = 16; From 393a57ea08d59a40e17d60dfac696f952e2e44a6 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 29 Sep 2026 22:09:04 -0400 Subject: [PATCH 3/6] Challenge 13: add requires(self.is_safe()) to CStr receiver contracts --- library/core/src/ffi/c_str.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 24748420f6960..f092038edbfe9 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -546,6 +546,7 @@ impl CStr { // contents, `self.inner.len()` bytes ending in the terminator; `inner` // is nonempty by the type's safety invariant, so the index below // cannot underflow. + #[requires(self.is_safe())] #[ensures(|&result| can_dereference(crate::ptr::slice_from_raw_parts(result, self.inner.len())))] #[ensures(|&result| unsafe { *result.add(self.inner.len() - 1) } == 0)] pub const fn as_ptr(&self) -> *const c_char { @@ -582,6 +583,7 @@ impl CStr { // Cross-accessor consistency: the count excludes the terminating NUL that // `to_bytes_with_nul` includes; `result + 1` cannot overflow since // `result == self.inner.len() - 1`. + #[requires(self.is_safe())] #[ensures(|&result| result + 1 == self.to_bytes_with_nul().len())] pub const fn count_bytes(&self) -> usize { // SAFETY: This length includes the nul-terminator, so it's at least one. @@ -600,6 +602,7 @@ impl CStr { #[stable(feature = "cstr_is_empty", since = "1.71.0")] #[rustc_const_stable(feature = "cstr_is_empty", since = "1.71.0")] // Empty means exactly zero content bytes before the NUL. + #[requires(self.is_safe())] #[ensures(|&result| result == (self.count_bytes() == 0))] pub const fn is_empty(&self) -> bool { // SAFETY: We know there is at least one byte; for empty strings it @@ -629,6 +632,7 @@ impl CStr { #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] // The content bytes contain no NUL and exclude the terminator; // `result.len() + 1` cannot overflow since the full view includes the NUL. + #[requires(self.is_safe())] #[ensures(|result| !result.contains(&0))] #[ensures(|result| result.len() + 1 == self.to_bytes_with_nul().len())] pub const fn to_bytes(&self) -> &[u8] { @@ -658,6 +662,7 @@ impl CStr { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] // The full byte view is the invariant shape: NUL-terminated, no interior NUL. + #[requires(self.is_safe())] #[ensures(|result| result.len() > 0 && result[result.len() - 1] == 0 && !result[..result.len() - 1].contains(&0))] pub const fn to_bytes_with_nul(&self) -> &[u8] { From 28ab1a619c8290fd84f6a042a99b0381b926bf6f Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 29 Sep 2026 22:10:50 -0400 Subject: [PATCH 4/6] Challenge 13: drop decorative ensures on Index::index (plain proof at pinned Kani) --- library/core/src/ffi/c_str.rs | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index f092038edbfe9..36c3b60acba86 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -794,11 +794,12 @@ impl ops::Index> for CStr { type Output = CStr; #[inline] - // The tail of a valid `CStr` is itself a valid `CStr`; the postcondition - // binds on normal return only — the out-of-bounds panic path is proven - // separately by the `check_index_range_from_out_of_bounds` harness. - #[ensures(|result: &&CStr| result.is_safe())] - #[ensures(|result: &&CStr| result.to_bytes_with_nul() == &self.to_bytes_with_nul()[index.start..])] + // No `#[ensures]` contract on this trait method: at the pinned Kani, + // `proof_for_contract` on a generic trait method fails to resolve + // (model-checking/kani#1997), so the tail-is-a-valid-`CStr` and byte-suffix + // properties are proven in the `check_index_range_from_contract` harness + // instead of as a contract. Restore the contract form when the pin includes + // the resolver fix. fn index(&self, index: ops::RangeFrom) -> &CStr { let bytes = self.to_bytes_with_nul(); // we need to manually check the starting index to account for the null @@ -1229,9 +1230,10 @@ mod verify { // Verified as a plain proof rather than proof_for_contract: at the pinned // Kani, a pfc target on a generic trait's method (Index>) // fails to resolve (model-checking/kani#1997) — "unable to find - // implementation of associated function Index::index for CStr". The two - // #[ensures] postconditions on `index` are asserted directly on the result - // below. (Non-generic trait pfc, e.g. CloneToUninit, still resolves and is + // implementation of associated function Index::index for CStr". The + // tail-is-a-valid-`CStr` and byte-suffix postconditions are asserted + // directly on the result below rather than as method contracts. + // (Non-generic trait pfc, e.g. CloneToUninit, still resolves and is // kept in contract form.) #[kani::proof] #[kani::unwind(17)] // bounded at 16: at 32 this harness took 263s. From a9ddf14444d8b1749211361d38feba072238bd7a Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 29 Sep 2026 23:04:05 -0400 Subject: [PATCH 5/6] Challenge 13: cite the merged kani#4865 resolver fix in the Index comments --- library/core/src/ffi/c_str.rs | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 36c3b60acba86..6f56c7aff6d85 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -794,12 +794,12 @@ impl ops::Index> for CStr { type Output = CStr; #[inline] - // No `#[ensures]` contract on this trait method: at the pinned Kani, - // `proof_for_contract` on a generic trait method fails to resolve - // (model-checking/kani#1997), so the tail-is-a-valid-`CStr` and byte-suffix - // properties are proven in the `check_index_range_from_contract` harness - // instead of as a contract. Restore the contract form when the pin includes - // the resolver fix. + // No `#[ensures]` contract on this trait method: `proof_for_contract` on a + // generic trait method isn't resolvable at this Kani pin, which predates the + // resolver fix (model-checking/kani#4865), so the tail-is-a-valid-`CStr` and + // byte-suffix properties are proven in the `check_index_range_from_contract` + // harness instead of as a contract. Restore the contract form once the pin + // includes kani#4865. fn index(&self, index: ops::RangeFrom) -> &CStr { let bytes = self.to_bytes_with_nul(); // we need to manually check the starting index to account for the null @@ -1227,10 +1227,11 @@ mod verify { } // impl ops::Index> for CStr — in-bounds tail slicing. - // Verified as a plain proof rather than proof_for_contract: at the pinned - // Kani, a pfc target on a generic trait's method (Index>) - // fails to resolve (model-checking/kani#1997) — "unable to find - // implementation of associated function Index::index for CStr". The + // Verified as a plain proof rather than proof_for_contract: a pfc target on + // a generic trait's method (Index>) isn't resolvable at + // this Kani pin, which predates the resolver fix (model-checking/kani#4865) + // — "unable to find implementation of associated function Index::index for + // CStr". The // tail-is-a-valid-`CStr` and byte-suffix postconditions are asserted // directly on the result below rather than as method contracts. // (Non-generic trait pfc, e.g. CloneToUninit, still resolves and is From ab40ea54f3b147c6f4dde5d159b13216781b955c Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Mon, 5 Oct 2026 22:32:40 -0400 Subject: [PATCH 6/6] Challenge 13: restore the Index contract and proof_for_contract at the kani#4865 pin --- library/core/src/ffi/c_str.rs | 25 ++++++++----------------- 1 file changed, 8 insertions(+), 17 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 6f56c7aff6d85..fe5023d1a2eec 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -794,12 +794,12 @@ impl ops::Index> for CStr { type Output = CStr; #[inline] - // No `#[ensures]` contract on this trait method: `proof_for_contract` on a - // generic trait method isn't resolvable at this Kani pin, which predates the - // resolver fix (model-checking/kani#4865), so the tail-is-a-valid-`CStr` and - // byte-suffix properties are proven in the `check_index_range_from_contract` - // harness instead of as a contract. Restore the contract form once the pin - // includes kani#4865. + // The tail of a valid `CStr` is itself a valid `CStr`; the postcondition + // binds on normal return only — the out-of-bounds panic path is proven + // separately by the `check_index_range_from_out_of_bounds` harness. + #[requires(self.is_safe())] + #[ensures(|result: &&CStr| result.is_safe())] + #[ensures(|result: &&CStr| result.to_bytes_with_nul() == &self.to_bytes_with_nul()[index.start..])] fn index(&self, index: ops::RangeFrom) -> &CStr { let bytes = self.to_bytes_with_nul(); // we need to manually check the starting index to account for the null @@ -1226,17 +1226,8 @@ mod verify { assert!(c_str.is_safe()); } - // impl ops::Index> for CStr — in-bounds tail slicing. - // Verified as a plain proof rather than proof_for_contract: a pfc target on - // a generic trait's method (Index>) isn't resolvable at - // this Kani pin, which predates the resolver fix (model-checking/kani#4865) - // — "unable to find implementation of associated function Index::index for - // CStr". The - // tail-is-a-valid-`CStr` and byte-suffix postconditions are asserted - // directly on the result below rather than as method contracts. - // (Non-generic trait pfc, e.g. CloneToUninit, still resolves and is - // kept in contract form.) - #[kani::proof] + // impl ops::Index> for CStr — in-bounds tail slicing + #[kani::proof_for_contract(>>::index)] #[kani::unwind(17)] // bounded at 16: at 32 this harness took 263s. fn check_index_range_from_contract() { const MAX_SIZE: usize = 16;