Challenge 24: Verify the safety of Vec functions part 2 #285

Activity

1. thanhnguyen-aws

   added

   ChallengeUsed to tag a challengeUsed to tag a challenge

   on Mar 18, 2025
2. jrey8343 commented on Mar 15, 2026

   

   jrey8343

   on Mar 15, 2026

   More actions

   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.
3. Samuelsills

   added a commit that references this issue on Mar 26, 2026

   Challenge 24: Verify safety of Vec IntoIter functions part 2

   ...

   This issue will close once commit a191053 is merged into the 'main' branch.

   a191053
4. jrey8343 commented on Sep 13, 2026

   

   jrey8343

   on Sep 13, 2026

   More actions

   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.