You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Challenge 18: Verify the safety of slice iter functions - part 1 #282
changed the title [-][Tracking Challenge] Challenge 18: Verify the safety of `slice` iter functions - part 1[/-][+]Challenge 18: Verify the safety of `slice` iter functions - part 1[/+]on Mar 18, 2025
Hi, I'm working on a Kani-based solution for this challenge and have a question about the "no monomorphization" requirement.
Kani fundamentally relies on monomorphization — #[kani::proof_for_contract] verifies a contract for a specific concrete type instantiation, not universally for all T. This is an architectural limitation of the CBMC backend (each monomorphized instance is a distinct function at the GOTO level).
Our current approach uses 4 representative types that cover all distinct memory layout categories:
() — ZST (size 0, align 1)
u8 — small primitive (size 1, align 1)
char — validity-constrained (size 4, align 4)
(char, u8) — compound with padding (size 5+, align 4)
The reasoning is that the unsafe pointer operations in these functions (ptr::copy, ptr.add, get_unchecked, set_len, etc.) depend only on size_of::<T>() and align_of::<T>(), not on T's identity. These 4 types exercise all distinct behaviors: ZST special-casing, different strides, alignment constraints, and padding.
Question for the committee: Does this representative-types approach satisfy the "no monomorphization" requirement for Kani-based solutions? Or is a tool with inherent generic reasoning (like VeriFast's separation logic) required?
I'm also exploring a VeriFast-based solution as an alternative, but wanted to clarify the acceptance criteria first. The only resolved challenge with this requirement (Ch19 RawVec) was solved with VeriFast, so I wanted to confirm whether Kani solutions are viable here.
Part 1: all 16 functions from the iterator! macro are proved for Iter and IterMut, and next/size_hint from forward_iterator! are proved for SplitN, SplitNMut, RSplitN, and RSplitNMut.
Part 2: the current snapshot contains 9 __iterator_get_unchecked impls (ArrayChunks/ArrayChunksMut no longer exist in slice/iter.rs). Each of the 9 carries a safety contract on a contracted inherent method, proved with #[kani::proof_for_contract]. All listed safe functions with unsafe bodies have harnesses.
On the earlier no-monomorphization question in this thread: the harnesses keep the source generic and instantiate each proof over representative types ((), u8, char, (char, u8)), the same pattern the merged challenge 16 and 17 style uses. Kani cannot prove one proof for all T; the per-representative-type spread is the accepted approach in this repository.
Element values are symbolic in every harness. Backing lengths are symbolic up to isize::MAX for () and u32::MAX for u8; looping harnesses use verified #[kani::unwind] bounds, which fail loudly if too small.
Following up on my question above (2026-03-15) about the "generic type T (no monomorphization)" clause, which is still unanswered and which the reviewer's 09-12/09-13 triage marks as the acceptance gate for every Kani submission to this challenge: I have consolidated it into one ruling request with a concrete proposed ruling text (per-type instantiation with a stated coverage argument, or tool-level polymorphism only), posted on the Ch25 PR because that submission is the furthest along: #681 (comment). The same ruling governs this challenge; please answer there so there is one thread.
Activity
[-][Tracking Challenge] Challenge 18: Verify the safety of `slice` iter functions - part 1[/-][+]Challenge 18: Verify the safety of `slice` iter functions - part 1[/+]jrey8343 commentedon Mar 15, 2026
Hi, I'm working on a Kani-based solution for this challenge and have a question about the "no monomorphization" requirement.
Kani fundamentally relies on monomorphization —
#[kani::proof_for_contract]verifies a contract for a specific concrete type instantiation, not universally for allT. This is an architectural limitation of the CBMC backend (each monomorphized instance is a distinct function at the GOTO level).Our current approach uses 4 representative types that cover all distinct memory layout categories:
()— ZST (size 0, align 1)u8— small primitive (size 1, align 1)char— validity-constrained (size 4, align 4)(char, u8)— compound with padding (size 5+, align 4)The reasoning is that the unsafe pointer operations in these functions (
ptr::copy,ptr.add,get_unchecked,set_len, etc.) depend only onsize_of::<T>()andalign_of::<T>(), not onT's identity. These 4 types exercise all distinct behaviors: ZST special-casing, different strides, alignment constraints, and padding.Question for the committee: Does this representative-types approach satisfy the "no monomorphization" requirement for Kani-based solutions? Or is a tool with inherent generic reasoning (like VeriFast's separation logic) required?
I'm also exploring a VeriFast-based solution as an alternative, but wanted to clarify the acceptance criteria first. The only resolved challenge with this requirement (Ch19 RawVec) was solved with VeriFast, so I wanted to confirm whether Kani solutions are viable here.
Verify safety of slice iterator functions with Kani (Challenge 18)
Verify safety of slice iterator functions with Kani (Challenge 18)
Challenge 18: Verify safety of Slice iterator functions
MavenRain commentedon Aug 21, 2026
I claim this challenge under the general rules, which allow more than one contributor to submit a solution.
My solution is PR #651. Coverage notes:
iterator!macro are proved forIterandIterMut, andnext/size_hintfromforward_iterator!are proved forSplitN,SplitNMut,RSplitN, andRSplitNMut.__iterator_get_uncheckedimpls (ArrayChunks/ArrayChunksMutno longer exist inslice/iter.rs). Each of the 9 carries a safety contract on a contracted inherent method, proved with#[kani::proof_for_contract]. All listed safe functions with unsafe bodies have harnesses.(),u8,char,(char, u8)), the same pattern the merged challenge 16 and 17 style uses. Kani cannot prove one proof for allT; the per-representative-type spread is the accepted approach in this repository.Element values are symbolic in every harness. Backing lengths are symbolic up to
isize::MAXfor()andu32::MAXforu8; looping harnesses use verified#[kani::unwind]bounds, which fail loudly if too small.jrey8343 commentedon Sep 13, 2026
Following up on my question above (2026-03-15) about the "generic type
T(no monomorphization)" clause, which is still unanswered and which the reviewer's 09-12/09-13 triage marks as the acceptance gate for every Kani submission to this challenge: I have consolidated it into one ruling request with a concrete proposed ruling text (per-type instantiation with a stated coverage argument, or tool-level polymorphism only), posted on the Ch25 PR because that submission is the furthest along: #681 (comment). The same ruling governs this challenge; please answer there so there is one thread.