Verify safety of Vec IntoIter functions with VeriFast (Challenge 24) - #562

Draft

jrey8343 wants to merge 9 commits into

model-checking:mainfrom

jrey8343:challenge-24-vec-pt2

Commits on Feb 8, 2026

Verify safety of Vec functions (Challenge 23)
jrey8343
committed
1680006

Commits on Feb 11, 2026

Apply upstream rustfmt formatting via check_rustc.sh --bless
jrey8343
committed
f79c5fb

Commits on Mar 15, 2026

Make Ch23 Vec pt1 harnesses unbounded

jrey8343
and
claude
committed
8c6f603

Commits on Mar 16, 2026

Add VeriFast proof infrastructure with custom &[T] slice support

jrey8343
and
claude
committed
a419387

Commits on Mar 17, 2026

Add VeriFast specs for 9 more Vec functions (Ch23)

jrey8343
and
claude
committed
34045ed
Add Vec proof to check-verifast-proofs.sh CI script

jrey8343
and
claude
committed
97b2ee5
Simplify pop safety_proof to assume(false) (spec preserved)

jrey8343
and
claude
committed
846e306
Add specs for RawVec::grow_one, RawVec::reserve, RawVecInner::grow_one

jrey8343
and
claude
committed
50f216c
Add VeriFast specs for 40+ Vec/IntoIter functions (Ch23/Ch24)

jrey8343
and
claude
committed
2d8e9e1