Challenge 13: contracts and proofs for CStr trait implementations and safe methods

[kasimte]

Towards #150.

Challenge 13's two criterion-4 trait implementations had no verification, and the criterion-2 methods were exercised by test harnesses but carried no contracts stating what they guarantee. This PR adds the missing contracts and trait-implementation proofs.

This PR adds:

• Trait-implementation contracts. Safety contracts for CloneToUninit and Index<RangeFrom<usize>>, both proven with proof_for_contract. Index<RangeFrom<usize>> is a proof_for_contract on a generic trait method, which needs the resolver fix I upstreamed (kani#4865), now in this repo's pinned Kani via the Merge subtree update for toolchain nightly-2026-09-25 #687 toolchain sync. Slicing a CStr from an out-of-bounds position is documented to panic, and that panic path has its own should_panic proof.
• Contracts on seven safe methods stating what each one guarantees. For example, count_bytes agrees with the length of the byte view, and the pointer from as_ptr covers the whole string including its final NUL byte. Each receiver contract states the safety invariant as a #[requires(self.is_safe())] precondition, keeping it sound to reuse under stub_verified.
• A fidelity check for the safety invariant itself. On arbitrary bytes, is_safe accepts exactly the well-formed strings (non-empty, NUL at the end, no NUL in the middle) and rejects everything else, with both outcomes proven reachable.
• A reachability witness (kani::cover) next to every assumption, confirming the assumed input sets are non-empty.

Challenge success criterion	Status in this PR
1. Implement the Invariant trait for CStr	Every harness producing a CStr asserts it, and the fidelity check compares is_safe to its documented meaning. The trait implementation was already in-tree.
2. Invariant holds after each of the 9 listed safe methods	7 gain contracts (from_bytes_until_nul, from_bytes_with_nul, count_bytes, is_empty, to_bytes, to_bytes_with_nul, as_ptr). bytes and to_str stay harness-proven, with the reason in a comment at each.
3. Safety contracts for the 3 unsafe functions (from_ptr, from_bytes_with_nul_unchecked, strlen)	Their contracts and proofs were already in-tree, unchanged. The fidelity check verifies the is_safe predicate their postconditions use.
4. The two trait implementations are safe (CloneToUninit, Index<RangeFrom<usize>>)	Both contracted and proven with proof_for_contract (see above). The out-of-bounds panic has a should_panic proof.

Bounds: the challenge allows bounded harnesses ("Harnesses may be bounded"). Inputs go up to 32 bytes. The pre-existing from_bytes_with_nul harness keeps its in-tree bound of 8, two new harnesses use 16, and one uses 8 to fit CI's per-harness time limit, each bound explained in a comment where it appears.

All 23 harnesses (22 in ffi::c_str::verify, 1 in clone::verify) pass via scripts/run-kani.sh, with every cover property satisfied.

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

[feliperodri]

Thanks @kasimte — this is a strong, sound submission for Challenge 13. It's complete and clean on our vacuity checks (no cfg(kani) body swaps, no trivial invariant, no decorative contracts, symbolic inputs), it's purely additive (+246/−0), it upgrades 7 of the 9 safe methods from plain proofs to real #[ensures] + proof_for_contract, and the OOB #[should_panic] Index harness plus qualified-path contract proofs on both trait methods are nice touches.

Heads-up for transparency: we reviewed all four open Challenge 13 solutions together, and we're prioritizing #638 in the review process as the front-runner — it's the most complete (it also contracts bytes/to_str, which this PR leaves as base plain proofs, and adds an invariant-fidelity harness). Your low-churn approach is genuinely appealing, so we're keeping this open as the strong alternative; if #638 stalls or we find it weakens any base coverage, this is our fallback. Really appreciate the work.

[kasimte]

A small note that might help the comparison: #670 also carries an invariant-fidelity harness, the same kind noted for #638. check_invariant_fidelity cross-checks is_safe() against an independent structural oracle (nonempty, NUL-terminated, no interior NUL) on arbitrary, possibly-invalid bytes, covering both the well-formed and malformed cases.

[kasimte]

Index harness plus qualified-path contract proofs on both trait methods are nice touches.

@feliperodri - #687 landed, so the pin now includes model-checking/kani#4865, the resolver fix I upstreamed. That's what the Index<RangeFrom> contract proof needed: it had fallen back to a plain proof when the September pin jump predated the fix. I've updated #670 to current main and restored index to proof_for_contract, so both trait methods are back in contract form.

It stays low-churn and purely additive (+252/−0). The existing harnesses are untouched, with the new contracts added alongside them. Kani is green on both OSes at the new pin.

Ready in case it's useful.