Challenge 13: safety of CStr

[stefanzetzsche]

Towards #150. Solves Challenge 13: Safety of CStr: a fidelity harness for the safety invariant (criterion 1), contracts and Kani harnesses for all 9 safe methods (criterion 2), safety contracts for the 3 unsafe functions (criterion 3), and proofs for the 2 trait implementations (criterion 4). All 15 harnesses (14 in ffi::c_str::verify, 1 in clone::verify) pass via scripts/run-kani.sh.

Changes

File	Change
c_str.rs	Contracts on the 6 view methods and the 3 unsafe functions; invariant fidelity harness; existing plain harnesses upgraded to contract form (the deletions in the diff are those replaced harness bodies — no runtime logic is touched anywhere)
clone.rs	Safety contract on unsafe impl CloneToUninit for CStr plus a proof_for_contract harness in a new clone::verify module

Criterion 1: safety invariant

CStr already implements Invariant (is_safe: non-empty, nul-terminated, no interior nul). What was missing is evidence that the predicate itself is right: every existing harness only ever evaluates is_safe() on an already-valid CStr obtained from a constructor, so a too-loose invariant (e.g. one missing the interior-nul clause) would pass all of them. The new check_invariant harness reinterprets an arbitrary — possibly invalid — byte sequence as &CStr (the exact cast from_bytes_with_nul_unchecked performs; is_safe only reads initialized bytes, so this is sound) and pins down exactly when is_safe() holds against two independent oracles: a structural one (the FIRST nul sits at the final index, phrased with position rather than the invariant's own form, so the equivalence is a theorem and not a restatement) and a semantic one (is_safe() agrees with from_bytes_with_nul(..).is_ok() — the invariant accepts exactly what the safe constructor accepts).

Criterion 2: the 9 safe methods

Each harness feeds an arbitrary valid CStr (any content length in 0..=31, via from_bytes_until_nul over a bounded nul-terminated array) and confirms the invariant still holds after the call.

Functions	Approach
from_bytes_until_nul, from_bytes_with_nul	#[ensures] contracts characterizing both result branches exactly (Ok: prefix up to and including the first nul / the whole slice, satisfying the invariant; each Err variant pinned to the first-nul position), verified with proof_for_contract
count_bytes, is_empty, to_bytes, to_bytes_with_nul	#[ensures] contracts pinning each result to the public byte views so no method can silently drift from the others (to_bytes_with_nul, the most primitive view, gets the invariant restated on its output; the others are phrased against it, keeping the specification acyclic), verified with proof_for_contract
bytes, to_str, as_ptr	Behavioral harnesses — their return types (opaque iterator, Result<&str, _>, raw pointer) cannot carry a return-value #[ensures]. bytes yields exactly to_bytes() and stops at the terminator; to_str on Ok returns byte-for-byte to_bytes() (a nul is valid UTF-8, so only exact equality proves the terminator is excluded) and on Err reports a failure position inside the content; as_ptr is non-null and valid for reads of the full nul-terminated view, reproduced byte-for-byte

Criterion 3: the 3 unsafe functions

Function	Contract
from_bytes_with_nul_unchecked	requires: the safety invariant restated on the input slice (its documented safety requirement); ensures: the result upholds the invariant. The harness adds a round-trip check (output view == input bytes), kept out of the shared contract so the callers that stub this function are unaffected
from_ptr	requires: non-null and nul-terminated within isize::MAX (pre-existing); ensures: is_safe(). Verifying the contract also covers the internal strlen walk and the from_raw_parts projection
strlen	requires: nul-terminated (pre-existing); ensures: the result is a legal offset pointing at a nul. The harness additionally asserts the FIRST-nul property — a mutant returning a later nul index would satisfy the contract but break the semantics from_ptr's is_safe relies on; it stays in the harness so stubbing callers are unaffected

Criterion 4: the 2 trait implementations

Index<RangeFrom<usize>> is a safe fn, so its harness is behavioral, on the defined (non-panicking) path start < len where the body performs the unsafe reinterpret: the sub-CStr upholds the invariant, and its nul-terminated view is exactly the suffix bytes[start..] — which kills a wrong-offset mutant that would still be is_safe().

CloneToUninit::clone_to_uninit is an unsafe fn and gets a safety contract (per the challenge's [^unsafe-fn] footnote): requires demands dest be writable for size_of_val(self) bytes (ub_checks::can_write over exactly the write footprint, which also carries the kani::modifies clause), ensures states the written bytes equal the source's nul-terminated view, so *dest is left a valid CStr — the trait's documented promise. The proof_for_contract harness clones into a fresh, deliberately uninitialized buffer (MaybeUninit — the contract claims validity for writes only, so the proof must not rely on dest's contents) and additionally asserts that the written bytes reinterpreted as &CStr uphold the invariant: cloning a valid CStr yields a valid CStr.

All harnesses are bounded (explicitly allowed by the challenge's stated assumptions), with backing arrays of 16 or 32 bytes and matching unwind bounds that fully unroll every scan. Wherever a harness restricts its inputs, kani::cover witnesses confirm that the interesting shapes — empty and non-empty C strings, both result branches, valid and invalid byte sequences — are actually reachable, so no proof passes vacuously.

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

[feliperodri]

Approving — leading solution for Challenge 13

Thanks @stefanzetzsche. After reviewing all four open Challenge 13 (CStr safety) submissions, this is the most complete and we're prioritizing it in the review process.

What stood out:

• All four success criteria covered. The Invariant impl is a real predicate (non-empty + NUL-terminated + no interior NUL, correctly not requiring UTF-8), all 9 safe methods are contract- or behaviorally-verified (including bytes/to_str, which other submissions leave as plain proofs), the 3 unsafe fns keep their real contracts + proof_for_contract, and both trait impls (CloneToUninit, Index<RangeFrom>) are verified via genuine proof_for_contract — including CloneToUninit write-validity on a MaybeUninit destination.
• Sound. Clean on our vacuity checks (no cfg(kani) body swaps, no trivial invariant, no decorative/unverified contracts, no assume-the-conclusion); inputs are fully symbolic with kani::cover non-vacuity anchors; no runtime std logic changed.
• Nice addition: the two-oracle invariant-fidelity harness that cross-checks is_safe() against independent structural/semantic oracles on arbitrary (possibly-invalid) bytes.

One non-blocking note: since main already ships harnesses for criteria 1–3, the −80 lines here rewrite some already-merged harnesses into contract form. Reviewers should diff each replaced harness against main to confirm no existing coverage is weakened (e.g. a smaller bound). This doesn't hold up the approval.

Bounded harnesses are explicitly allowed for this challenge, so the documented bounds are fine.

[feliperodri]

@patricklam could you review this PR proposed solution? I believe it's the winner for Challenge 13.

[patricklam]

Will aim to get to it later this week. Thanks for your patience.