Add a tour of the RawVec proof

Also:
- Bumps VeriFast to 25.08
- Polishes the RawVec proof
- Links to the VeriFast proofs from verifast-proofs/README.md

Author: btj

.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.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
+          curl -OL https://github.com/verifast/verifast/releases/download/25.08/verifast-25.08-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/10123891
+          echo '1e40019d6add91bf72141c86f4007f2fe1eef67f453cb7fb8f1f5ab7d31d509f  verifast-25.08-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.08-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
         run: rustup toolchain install nightly-2025-04-09
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.07/bin:$PATH
+          export PATH=~/verifast-25.08/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.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
+          curl -OL https://github.com/verifast/verifast/releases/download/25.08/verifast-25.08-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/10123891
+          echo '1e40019d6add91bf72141c86f4007f2fe1eef67f453cb7fb8f1f5ab7d31d509f  verifast-25.08-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.08-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
         run: rustup toolchain install nightly-2025-04-09
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.07/bin:$PATH
+          export PATH=~/verifast-25.08/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs.sh
 

verifast-proofs/README.md

@@ -2,8 +2,18 @@
 
 This directory contains [VeriFast](../doc/src/tools/verifast.md) proofs for (currently a very, very small) part of the standard library.
 
-> [!NOTE]  
-> TL;DR: If the VeriFast CI action fails because of a failing diff, please run `verifast-proofs/patch-verifast-proofs.sh` to fix the problem.
+Specifically, it currently contains the following proofs:
+
+- Partial proof of [LinkedList](alloc/collections/linked_list.rs/)
+- Partial proof of [RawVec](alloc/raw_vec/mod.rs/)
+
+See each proof's accompanying README for a tour of the proof and applicable caveats.
+
+## Maintaining the proofs
+
+ If the VeriFast CI action fails because of a failing diff, please run `cd verifast-proofs; ./patch-verifast-proofs.sh` to fix the problem.
+
+## `-skip_specless_fns`
 
 VeriFast supports selecting the code to verify on a function-by-function basis. By default, when given a `.rs` file VeriFast will try to verify [semantic well-typedness](https://verifast.github.io/verifast/rust-reference/non-unsafe-funcs.html) of all non-`unsafe` functions in that file (and in any submodules), and will require that the user provide specifications for all `unsafe` functions, which it will then verify against those specifications. However, when given the `-skip_specless_fns` command-line flag, VeriFast will skip all functions for which the user did not provide a specification.
 

verifast-proofs/alloc/collections/linked_list.rs/README.md

@@ -382,7 +382,7 @@ fn pop_front_node<'a>(&'a mut self) -> Option<Box<Node<T>, &'a A>>
         //@ open [?f]ref_initialized_::<A>(alloc_ref1)();
         let alloc_ref = &self.alloc;
 
-        r = match  head {
+        r = match head {
             None => {
                 //@ close [f]ref_initialized_::<A>(alloc_ref)();
                 //@ close_frac_borrow(f, ref_initialized_(alloc_ref));
@@ -572,13 +572,12 @@ closes it back up afterwards.
 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.
+- `-allow_assume`: This proof uses a number of `assume` ghost statements and `assume_correct` clauses. These must be carefully audited. Specifically, this proof uses `assume` statements to assume that the lifetime of the allocator used by the LinkedList value equals `'static`, i.e. this proof only applies if the global allocator or another allocator that lasts forever is used.
 
 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.
-- The current standard library specifications do not [prevent an allocated memory block from outliving its allocator](https://github.com/verifast/verifast/issues/829). This is sound only if the global allocator is used.
 
 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.