Repository navigation
Ruling needed: "mutating immutable bytes" in Kani-based solutions #733
Description
24 challenge specs require proofs to rule out "mutating immutable bytes". Kani has no aliasing model (model-checking/kani#314), so it can't check this in general. Ch6, Ch9, Ch11 and Ch14 were resolved with Kani-only solutions anyway. #638 (Ch13) and #582 (Ch26) are waiting on a decision.
Using Ch13 (CStr) as the example, the property splits into three obligations. I checked each one locally with Kani 6ce55b9, VeriFast 26.10 and Verus 0.2026.10.18:
| Obligation | Kani | VeriFast | Verus |
|---|---|---|---|
| 1. Methods don't write the bytes they borrow | ✅ a contract with no modifies fails on any write |
✅ | ✅ |
2. clone_to_uninit's dest doesn't overlap self |
only with an explicit non-overlap requires (model-checking/kani#5040 would check it automatically) |
✅ by construction | ✅ by construction |
3. After from_ptr, the caller doesn't mutate the bytes while the &'a CStr lives |
❌ can't be expressed | expressible | ✅ a write while the reference is in use is rejected |
| Runs on the unmodified std file | ✅ | ❌ blocked by verifast/verifast#1047, and needs 3 edits to compile a copy | ❌ code must be rewritten inside verus! |
The VeriFast and Verus results come from small models of these functions, not from the real core/src/ffi/c_str.rs.
Covering the property doesn't mean rewriting a Kani solution. Obligations 1 and 2 need at most one extra requires. Obligation 3 would be a separate, small proof: about 20 lines of VeriFast annotations on strlen, from_ptr and clone_to_uninit, once verifast/verifast#1047 is fixed. Verus would need the code rewritten, and it isn't an approved tool yet (#554).
Question for the committee: should we accept a solution that covers everything Kani can express (obligations 1 and 2 here), and treat caller-side obligations like 3 as out of scope? Or should challenges with this criterion require a complementary proof, for example in VeriFast, for those obligations?
Recommendation: accept, which is consistent with Ch6, Ch9, Ch11 and Ch14, and say so in the challenge book. A complementary VeriFast proof for obligations like 3 could then be a separate, optional contribution.
Activity
feliperodri commentedon Oct 21, 2026
any thoughts? @btj @patricklam @tautschnig @rajath-mk @HuStmpHrrr @celinval @remi-delmas-3000 @rahulku @rafaelsamenezes @lucasccordeiro @dkcumming @DiuDiu777
feliperodri commentedon Oct 23, 2026
Two more items on the same lists can't be established with Kani today, and two approved PRs already leave them out:
-Z valid-value-checks, but CI doesn't enable it. I tried it on 277 of Challenge 27: Verify Arc/Weak safety in alloc::sync with Kani #587's harnesses: 148 fail. 141 of the failing checks are "Kani currently doesn't support checking validity of …" (copy_nonoverlapping, raw-pointer dereferences, mutable casts). The other 7 report an invalidArcInner<bool>inside std's ownWeak::innerandArc::initialize_arcinner, which only reach fields through a raw pointer, so they look like false positives. Run time is about the same with and without the flag. The flag can't be adopted until Kani supports these constructs.Proposal: extend the question above to these two items. Accept solutions that cover everything Kani can check, and list data races and invalid values as out of scope for Kani until a tool can establish them. That matches how #683 and #587 were approved, and it settles #582 (Ch26) the same way.
docs(ch8): fix working requirements interpretation from organizer sta…
docs(ch8): apply review corrections to plan revision 7
feliperodri commentedon Oct 30, 2026
An update from the Kani side: Kani now has an experimental aliasing model,
-Z aliasing-checks. It checks Tree Borrows' rules, including writes to immutable bytes, inside each harness. It isn't merged in Kani yet: it's on a branch, and the speed-up it needs (diffblue/cbmc#9238) is merged in CBMC but not yet in a release. I ran the existing harnesses of the challenges above with it, with contracts and harnesses unchanged and the same flags as CI. Kani commit0e902a603, 2 jobs, 12 GB and 900 s per harness:&dyn, not followed yet)No harness reports aliasing UB.
A harness that verifies with the checks has no execution that breaks the implemented rules at any byte, among the inputs it allows and under the contract's preconditions. Where the checks can't tell which reference a pointer came from, the result is inconclusive, never a pass. The rules are tested against Miri's own borrow tests: of 165, Kani misses none of the UB Miri reports, and reports none that Miri doesn't. They are not proved equivalent to Miri.
For Ch11 and Ch14 this covers "mutating immutable bytes" without changing the solutions. Those functions mostly take and return plain values, though, so the code that does real pointer work (Ch6, Ch9, Ch13, Ch26) is where it matters, and that's still blocked on cost. I'm working on that next.
Where I'd like input: once the inconclusive cases are resolved, would this evidence (tested against Miri, inconclusive rather than unsound where the checks give up) be enough for Kani-based solutions to claim the property? If not, what would be?