VeriFast solution for challenge 19 (RawVec)

.github/workflows/verifast-negative.yml

@@ -30,16 +30,16 @@ jobs:
       - name: Install VeriFast
         run: |
           cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/4911733
-          echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8  verifast-25.02-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.02-linux.tar.gz
+          curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/8998468
+          echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b  verifast-25.07-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.07-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2024-11-23
+        run: rustup toolchain install nightly-2025-04-09
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.02/bin:$PATH
+          export PATH=~/verifast-25.07/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

@@ -27,17 +27,17 @@ jobs:
       - name: Install VeriFast
         run: |
           cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/4911733
-          echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8  verifast-25.02-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.02-linux.tar.gz
+          curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/8998468
+          echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b  verifast-25.07-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.07-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2024-11-23
+        run: rustup toolchain install nightly-2025-04-09
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.02/bin:$PATH
+          export PATH=~/verifast-25.07/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs.sh
 

doc/src/challenges/0019-rawvec.md

@@ -1,10 +1,11 @@
-# Challenge 25: Verify the safety of `RawVec` functions
+# Challenge 19: Verify the safety of `RawVec` functions
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
+- **End date:** *2025-08-12*
 - **Reward:** *10000 USD*
+- **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------
 

verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs

@@ -23,7 +23,7 @@ use super::SpecExtend;
 use crate::alloc::{Allocator, Global};
 use crate::boxed::Box;
 
-//@ use std::alloc::{alloc_block_in, Layout, Global, Allocator};
+//@ use std::alloc::{alloc_id_t, alloc_block_in, Layout, Global, Allocator};
 //@ use std::option::{Option, Option::None, Option::Some};
 //@ use std::ptr::{NonNull, NonNull_ptr};
 
@@ -70,7 +70,7 @@ struct Node<T> {
 
 /*@
 
-pred Nodes<T>(alloc_id: any, n: Option<NonNull<Node<T>>>, prev: Option<NonNull<Node<T>>>, last: Option<NonNull<Node<T>>>, next: Option<NonNull<Node<T>>>; nodes: list<NonNull<Node<T>>>) =
+pred Nodes<T>(alloc_id: alloc_id_t, n: Option<NonNull<Node<T>>>, prev: Option<NonNull<Node<T>>>, last: Option<NonNull<Node<T>>>, next: Option<NonNull<Node<T>>>; nodes: list<NonNull<Node<T>>>) =
     if n == next {
         nodes == [] &*& last == prev
     } else {

verifast-proofs/alloc/raw_vec/mod.rs/README.md

@@ -0,0 +1,18 @@
+# Partial verification of RawVec with VeriFast
+
+With certain [caveats](#caveats), this proof proves functional correctness as well as [soundness](https://doc.rust-lang.org/nomicon/working-with-unsafe.html) of RawVec associated functions `new_in`, `with_capacity_in`, `try_reserve`, `try_reserve_exact`, and `drop`, as well as functional correctness of RawVec associated functions `into_box`, `from_raw_parts_in`, `from_nonnull_in`, `ptr`, and `capacity`, RawVecInner associated functions `new_in`, `with_capacity_in`, `try_allocate_in`, `from_raw_parts_in`, `from_nonnull_in`, `ptr`, `non_null`, `capacity`, `current_memory`, `try_reserve`, `try_reserve_exact`, `needs_to_grow`, `set_ptr_and_cap`, `grow_amortized`, `grow_exact`, `shrink`, `shrink_unchecked`, and `deallocate`, and functions `capacity_overflow`, `new_cap`, `finish_grow`, `handle_error`, `alloc_guard`, and `layout_array`.
+
+## Caveats
+
+First of all, this proof was performed with the following VeriFast command-line flags:
+- `-skip_specless_fns`: VeriFast ignores the functions that do not have a `req` or `ens` clause.
+- `-ignore_unwind_paths`: This proof ignores code that is reachable only when unwinding.
+- `-allow_assume`: This proof uses a number of `assume` ghost statements and `assume_correct` clauses. These must be carefully audited.
+
+Secondly, since VeriFast uses the `rustc` frontend, which assumes a particular target architecture, VeriFast's results hold only for the used Rust toolchain's target architecture. When VeriFast reports "0 errors found" for a Rust program, it always reports the targeted architecture as well (e.g. `0 errors found (2149 statements verified) (target: x86_64-unknown-linux-gnu (LP64))`).
+
+Thirdly, VeriFast has a number of [known unsoundnesses](https://github.com/verifast/verifast/issues?q=is%3Aissue+is%3Aopen+label%3Aunsoundness) (reasons why VeriFast might in some cases incorrectly accept a program), including the following:
+- VeriFast does not yet fully verify compliance with Rust's [pointer aliasing rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html).
+- VeriFast does not yet properly verify compliance of custom type interpretations with Rust's [variance](https://doc.rust-lang.org/reference/subtyping.html#variance) rules.
+
+Fourthly, unlike foundational tools such as [RefinedRust](https://plv.mpi-sws.org/refinedrust/), VeriFast has not itself been verified, so there are undoubtedly also unknown unsoundnesses. Such unsoundnesses might exist in VeriFast's [symbolic execution engine](https://github.com/model-checking/verify-rust-std/issues/213#issuecomment-2531006855) [itself](https://github.com/model-checking/verify-rust-std/issues/213#issuecomment-2534922580) or in its [prelude](https://github.com/verifast/verifast/tree/master/bin/rust) (definitions and axioms automatically imported at the start of every verification run) or in the [specifications](https://github.com/verifast/verifast/blob/master/bin/rust/std/lib.rsspec) it uses for the Rust standard library functions called by the program being verified.

verifast-proofs/alloc/raw_vec/mod.rs/original/lib.rs

@@ -0,0 +1,39 @@
+// verifast_options{skip_specless_fns}
+
+#![allow(dead_code)]
+#![no_std]
+#![allow(internal_features)]
+#![allow(incomplete_features)]
+#![feature(allocator_api)]
+#![feature(staged_api)]
+#![feature(rustc_attrs)]
+#![feature(dropck_eyepatch)]
+#![feature(specialization)]
+#![feature(extend_one)]
+#![feature(exact_size_is_empty)]
+#![feature(hasher_prefixfree_extras)]
+#![feature(box_into_inner)]
+#![feature(try_trait_v2)]
+#![feature(optimize_attribute)]
+#![feature(temporary_niche_types)]
+#![feature(ptr_internals)]
+#![feature(try_reserve_kind)]
+#![feature(ptr_alignment_type)]
+#![feature(sized_type_properties)]
+#![feature(std_internals)]
+#![feature(alloc_layout_extra)]
+#![feature(nonnull_provenance)]
+#![feature(panic_internals)]
+
+#![stable(feature = "rust1", since = "1.0.0")]
+
+extern crate alloc as std;
+
+#[stable(feature = "rust1", since = "1.0.0")]
+pub use std::alloc as alloc;
+#[stable(feature = "rust1", since = "1.0.0")]
+pub use std::boxed as boxed;
+#[stable(feature = "rust1", since = "1.0.0")]
+pub use std::collections as collections;
+
+pub mod raw_vec;