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 23: Verify the safety of Vec functions part 1 #284
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.
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.
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/vec tree 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's library/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/vec here (full crate, cargo verifast, original/ byte-identical to library/alloc/src by building this repo's safety proc-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 particular Allocator::grow preserving the first old_layout.size() bytes (lib.rsspec, with matching finish_grow / grow_amortized postconditions and grow_one specs, which push/insert/append need), and Rvalue::RawPtr in the refinement checker (needed because into_iter.rs's non_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.
Activity
Lysxia commentedon May 15, 2025
The link responds 404 because #267 has not been merged. Is this challenge considered open already?
thanhnguyen-aws commentedon Jun 4, 2025
This challenge will be open shortly. Thank you for being interested.
btj commentedon Nov 26, 2025
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.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 23: Verify safety of Vec functions part 1
bongjunj commentedon Aug 20, 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!
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.jrey8343 commentedon Oct 7, 2026
@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:
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.