Repository navigation
Challenge 23: Verify the safety of Vec functions part 1 #284
Description
Activity
This challenge will be open shortly. Thank you for being interested.
I started working on this. So far, I have a proof of
from_raw_parts,from_parts,from_parts_in,into_raw_parts_with_alloc,into_boxed_slice,truncate, andset_len.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.
- added a commit that references this issue
on Mar 26, 2026 Hi, this issue seems still open, but the book says it has an end date "2025-10-17".
I am just wondering that is this challenge still open, or, as it past the end date, stopped receiving solutions?
I find the fact that it is open but has a past end data quite confusing.Thanks for opening this challenge!
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.@btj, following up on your 2025-11-26 note here. Your
tests/rust/safe_abstraction/vectree at VeriFast 26.10 proves 8 of this challenge's 36 functions (from_raw_parts,from_parts,from_parts_in,into_raw_parts_with_allocator,into_boxed_slice,truncate,set_len,swap_remove), generic and unbounded, on the same rust-lang commit as this repo'slibrary/alloc, and it is the only credible base for a Challenge 23 solution. The slice-reference support I needed (verifast/verifast#1001, rust-lang#1015) is now released, and I have rewritten #561/#562 to say plainly that nothing beyond your functions is verified in them.Two questions before I invest further:
- Do you intend to complete the Vec proof yourself and submit it for Challenges 23/24? If so I would rather feed you function proofs and the upstream pieces than compete with you.
- If not, would this split work? I vendor your tree into
verifast-proofs/alloc/vechere (full crate,cargo verifast,original/byte-identical tolibrary/alloc/srcby building this repo'ssafetyproc-macro crate as a path dependency), add functions there and send each one upstream to your test so your tree stays canonical, and open the upstream changes the next functions need — in particularAllocator::growpreserving the firstold_layout.size()bytes (lib.rsspec, with matchingfinish_grow/grow_amortizedpostconditions andgrow_onespecs, whichpush/insert/appendneed), andRvalue::RawPtrin the refinement checker (needed becauseinto_iter.rs'snon_null!macro uses&raw const). Would you be able to review those two in the next release window? Talha's Comparison of by-ref single-variant nullary tag does not work rust-lang/rust#1035–Higher-order generic functions disobey kind system rust-lang/rust#1037 cover the other blockers and I am reviewing them.
Happy to be told a different layout or split is preferable.
Runbook Link
https://model-checking.github.io/verify-rust-std/challenges/0023-vec-pt1.html