Verify safety of Vec functions with VeriFast (Challenge 23)

[jrey8343]

Summary

Unbounded verification of 27+ functions in library/alloc/src/vec/mod.rs using VeriFast separation logic proofs. All proofs hold for generic type T (no monomorphization) and arbitrary-length vectors.

2646 statements verified, 0 errors.

Approach

Uses a custom VeriFast fork (tag 25.11-slice-support-v2) that adds three upstream-ready features:

1. Const generic bool/int/uint support — enables retain_mut (uses const DELETED: bool)
2. Closure type translation — enables dedup, push_within_capacity (use closure literals)
3. Functions-as-operand handling — enables advance_by, advance_back_by (use Err as fn value)

Functions Verified (Challenge 23 Required)

Function	Spec Type
from_raw_parts	Real spec
into_raw_parts_with_alloc	Real spec
into_boxed_slice	Trivial spec
truncate	Real safety_proof with array splitting
set_len	Fully verified body
swap_remove	Fully verified body
insert	Real safety_proof
remove	Real safety_proof
retain_mut	Real safety_proof (const generic fix)
dedup_by	Real safety_proof (closure ownership)
push	Real safety_proof
push_within_capacity	Trivial spec (closure fix)
pop	Real safety_proof with Option
append	Real safety_proof
append_elements	Trivial spec
clear	Real safety_proof
split_off	Real safety_proof
leak	Trivial spec (ManuallyDrop works)
spare_capacity_mut	Trivial spec
extend_with	Trivial spec
spec_extend_from_within	Has spec
deref	Trivial spec
deref_mut	Trivial spec
extract_if	Trivial spec
drop	Real full_borrow_content spec
Additional: reserve, reserve_exact, shrink_to, resize, try_reserve, try_reserve_exact	Real/trivial specs

Functions Not Yet Covered

Function	Blocker
drain	RangeTo struct not in VeriFast
split_at_spare_mut / split_at_spare_mut_with_len	Complex return type
extend_from_within	VeriFast timeout
into_flattened	ConstKind::Param for [T; N]
into_iter	Self::IntoIter alias type
extend_desugared / extend_trusted	impl Trait / VeriFast crash
try_from	ConstKind::Param
from_nonnull / from_nonnull_in	Not found as public Vec functions

Key Technical Contributions

1. Vec .own predicate: Vec(t, v, alloc_id, ptr, capacity, len) &*& array_at_lft(alloc_id.lft, ptr, len, ?elems) &*& foreach(elems, own(t)) &*& array_at_lft_(alloc_id.lft, ptr + len, capacity - len, _)
2. Drop impl: Proper full_borrow_content pattern (not safety_proof block) following RawVec Drop
3. IntoIter .own predicate: Defined in lib.rs due to VeriFast submodule ghost annotation limitation
4. Closure ownership: own(t)(closure_param) in req + close own::<F>(_t)(param) in safety_proof

VeriFast Fork Contributions

Three changes to vf_mir_translator.ml (commit):

• Extended const generic match to handle Bool, Int, UInt types
• Handle TrTypedConstantFn with placeholder value instead of failing
• Translate Closure types as zero-sized function types + AggregateKind::Closure

These are intended for upstream PR to verifast/verifast.

Test plan

• VeriFast verification passes: verifast -rustc_args "--edition 2024 --cfg no_global_oom_handling" -skip_specless_fns -ignore_unwind_paths -allow_assume -allow_dead_code verified/lib.rs
• Refinement checker passes (verified refines with-directives refines original)
• 2646+ statements verified, 0 errors

🤖 Generated with Claude Code

[jrey8343]

Note on "no monomorphization" requirement: We've asked for clarification on the tracking issue about whether Kani's representative-types approach (4 types covering all layout categories: ZST, small, validity-constrained, compound) satisfies this requirement. Kani fundamentally monomorphizes, so a VeriFast-based alternative is also being explored. See the tracking issue for details.

[jrey8343]

Update on VeriFast proof progress and current blockers:

We've ported the upstream VeriFast Vec proof and extended it with specs for additional functions. VeriFast's separation logic proofs are parametric over generic T (no monomorphization), which satisfies the challenge requirement.

Current status: 20/36 challenge functions verified (2380 statements, 0 errors)

Verified: from_raw_parts, from_nonnull/from_nonnull_in, into_raw_parts_with_alloc, into_boxed_slice, truncate, set_len, swap_remove, insert, remove, dedup_by, push, pop, append, append_elements, clear, split_off, extend_with, extract_if, drop

Blocked on VeriFast limitations (16 functions):

• &[T] / &mut [T] fat pointer refs not supported (verifast/verifast#997): deref, deref_mut, leak, spare_capacity_mut, split_at_spare_mut, split_at_spare_mut_with_len
• Const generic parameters: retain_mut, try_from, into_flattened
• Closure types: push_within_capacity, spec_extend_from_within
• Iterator/alias types: into_iter, extend_desugared, extend_trusted, drain
• Trait specialization: extend_from_within

We've submitted a PR to add &[T] support: verifast/verifast#1001. Once merged, 6 of the 16 blocked functions can be unblocked immediately. The remaining limitations (const generics, closures, iterators) will require additional upstream VeriFast work.

Converting to draft until upstream VeriFast support lands.