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 24: Verify the safety of Vec functions part 2 #285
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.
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
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.
Challenge 24: Verify safety of Vec IntoIter functions part 2
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.