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

[jrey8343]

Summary

Completes Challenge 13 (CStr safety) criterion 4: a verified safety contract for the unsafe CloneToUninit for CStr impl, plus the existing Index<RangeFrom<usize>> harness.

• check_clone_to_uninit_contract (new): #[kani::proof_for_contract(CStr::clone_to_uninit)] harness matching the existing contract-harness pattern in c_str.rs (check_from_bytes_with_nul_unchecked, check_from_ptr). The destination buffer is deliberately uninitialized (MaybeUninit): the contract claims validity for writes only, so the harness must not rely on dest's contents.
• check_clone_to_uninit: unchanged bounded functional check (exact byte-for-byte copy including the NUL terminator), with an initialized buffer.
• check_index_from: verifies ops::Index<RangeFrom<usize>> maintains is_safe() on the resulting sub-CStr.

Changes

• library/core/src/clone.rs: the clone_to_uninit contract is strengthened from #[requires(!dest.is_null())] to the documented precondition, using the repo's memory predicates:

  #[requires(crate::ub_checks::can_write(
      crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))
  ))]
  #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))))]

  can_write covers non-null, single-allocation bounds for size_of_val(self) bytes, and alignment (trivial for u8), in the same form as the NonNull::write_bytes contract; the old !dest.is_null() is subsumed. The modifies clause captures the exact write footprint of the body.
• library/core/src/ffi/c_str.rs: adds check_clone_to_uninit_contract alongside the existing harnesses.
• Merged with current main (Kani pin d4df833, 0.67): the previously pinned Kani 0.65 miscompiles contracts attached to this trait impl method — a proof_for_contract harness fails the builtin-memcpy assigns check regardless of the modifies clause, while the identical contract on a free function over the identical body verifies. Kani 0.67 checks the impl contract directly.

Verification

Local, pinned Kani 0.67.0 (d4df833), CI's exact flags (-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts --cbmc-args --object-bits 12):

Harness	Bound	Result
check_clone_to_uninit_contract	MAX_SIZE=16, unwind=17	306 checks, 0 failures, ~8s
check_clone_to_uninit (functional)	MAX_SIZE=8, unwind=9	290 checks, 0 failures, ~38s
check_index_from	MAX_SIZE=32, unwind=33	0 failures, ~132s
full ffi::c_str::verify suite (post-rebase regression)	—	15 of 15 harnesses verified, 0 failures

All harnesses are bounded, per Challenge 13's stated assumption ("Harnesses may be bounded"). The functional harness's bound is MAX_SIZE=8/unwind=9 — the description now matches the code (the earlier text incorrectly said 16/17).

Resolves

Challenge 13: Safety of CStr (#150), criterion 4 (CloneToUninit, Index<RangeFrom>), completing the criteria already covered by the existing harnesses in c_str.rs.

[jrey8343]

CI is passing — ready for review.

[Copilot]

Pull request overview

Completes Challenge 13 by adding Kani verification coverage for CStr’s CloneToUninit and Index<RangeFrom<usize>> safety properties, and by annotating the CStr CloneToUninit impl with an explicit precondition.

Changes:

• Added Kani harness check_index_from to verify &c_str[idx..] preserves CStr::is_safe() and matches the expected byte tail.
• Added Kani harness check_clone_to_uninit to exercise CStr’s CloneToUninit implementation.
• Added a #[requires(!dest.is_null())] contract on CStr’s clone_to_uninit implementation.

Reviewed changes

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

File	Description
library/core/src/ffi/c_str.rs	Adds two new Kani harnesses for CStr indexing safety and CloneToUninit behavior.
library/core/src/clone.rs	Adds a requires precondition to the CloneToUninit impl for CStr (plus supporting imports).

[feliperodri]

Thanks — this is solid, real verification work: the two harnesses exercise the actual CStr impls with symbolic inputs and meaningful assertions (is_safe() plus exact byte-for-byte assert_eq!), the arbitrary_cstr helper isn't over-constrained, and you've already addressed the earlier automated-review notes (typo, exact-byte check, initialized destination buffer to keep the harness itself UB-free). Bounded verification is the right fit for Challenge 13 here.

I'm requesting changes on one substantive point plus a minor one, both around the clone_to_uninit safety contract.

1. The clone_to_uninit contract is both too weak and never verified

Challenge 13's criterion 4 requires the unsafe CloneToUninit impl to have a verified safety contract (footnote: "Unsafe functions will require safety contracts"). As written, the contract doesn't meet that bar:

(a) Too weak. #[requires(!dest.is_null())] under-specifies the documented precondition. clone_to_uninit requires dest to be valid for size_of_val(self) writes and properly aligned — non-nullness alone doesn't capture that. Please strengthen it using the repo's memory predicates (e.g. kani::mem::can_write / ub_checks::can_write for size_of_val(self) bytes), consistent with how pointer-based contracts are written elsewhere in core.

(b) Never verified. There is no #[kani::proof_for_contract(CStr::clone_to_uninit)]. In Kani, #[requires]/#[ensures] are only exercised by a proof_for_contract harness (or when the contract is used as a stub); a plain #[kani::proof] that calls the function runs the real body and ignores its contract. So check_clone_to_uninit does not check this contract — the annotation is currently decorative. This is inconsistent with the other unsafe functions in the same file (from_bytes_with_nul_unchecked, strlen, from_ptr), which are all verified via #[kani::proof_for_contract].

Please add a #[kani::proof_for_contract(CStr::clone_to_uninit)] harness that verifies the (strengthened) contract, matching the existing pattern. check_clone_to_uninit is a good functional/bounded check and can stay alongside it.

2. PR description doesn't match the code

The description states check_clone_to_uninit uses MAX_SIZE=16, unwind=17 (~159s), but the code uses MAX_SIZE=8, unwind=9. Please reconcile so the stated verification evidence matches what's actually run.

Nits (already mostly handled)

• Typo fix trasnsparent → transparent: 👍
• check_index_from looks good — idx < bytes_with_nul.len() keeps the tail NUL-terminated, and the assert_eq! against &bytes_with_nul[idx..] is a nice functional check.

Once the contract is faithful and verified (and the numbers reconciled), this should be good to go — the harness structure itself is sound.

[jrey8343]

@feliperodri Thanks for the review — both points are addressed, and the description is reconciled with the code.

1(a) — contract strengthened. clone_to_uninit now requires dest valid for writes of size_of_val(self) bytes using the repo's memory predicates, in the same form as the NonNull::write_bytes contract:

#[requires(crate::ub_checks::can_write(
    crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))
))]
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))))]

can_write subsumes the old !dest.is_null() (non-null + single-allocation bounds + alignment), and the modifies clause captures the body's exact write footprint.

1(b) — contract now verified. Added check_clone_to_uninit_contract, a #[kani::proof_for_contract(CStr::clone_to_uninit)] harness following the existing pattern (check_from_bytes_with_nul_unchecked, check_from_ptr), with a deliberately uninitialized MaybeUninit destination — the contract claims writes-only validity, so the harness must not rely on dest's contents. check_clone_to_uninit stays as the functional byte-for-byte check, as you suggested.

One finding worth flagging: under the previously pinned Kani 0.65, a contract attached to this trait impl method cannot be verified — the proof_for_contract harness fails the builtin-memcpy assigns check regardless of the modifies clause. We isolated it empirically: the identical contract on a free function over the identical body verifies, and with any #[requires] present on the impl, even contract proofs that never call it fail the same check. The current pin (d4df833, Kani 0.67) handles the impl contract correctly, so this branch is merged with current main and the harness targets the impl directly. Happy to file a minimized repro upstream against 0.65 if that's useful.

2 — description numbers reconciled. The functional harness runs MAX_SIZE=8/unwind=9 (the code was right; the description was stale). The new contract harness runs MAX_SIZE=16/unwind=17. The updated description lists fresh local results for every harness under CI's exact flags (including --no-assert-contracts and --object-bits 12), plus a post-rebase regression run of the whole ffi::c_str::verify suite.