Merge branch 'main' into sync-2025-10-09

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
 

doc/src/challenges/0001-core-transmutation.md

@@ -4,7 +4,7 @@
 - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
 - **Start date:** *2024/06/12*
 - **End date:** *2025/04/10*
-- **Reward:** *N/A*
+- **Reward:** *10000 USD*
 - **Contributors**: [Alex Le Blanc](https://github.com/AlexLB99), [Patrick Lam](https://github.com/patricklam)
 
 -------------------

library/core/src/ub_checks.rs

@@ -193,7 +193,7 @@ pub use predicates::*;
 #[cfg(not(kani))]
 mod predicates {
     /// Checks if a pointer can be dereferenced, ensuring:
-    ///   * `src` is valid for reads (see [`crate::ptr`] documentation).
+    ///   * `src` is valid for reads and writes (see [`crate::ptr`] documentation).
     ///   * `src` is properly aligned (use `read_unaligned` if not).
     ///   * `src` points to a properly initialized value of type `T`.
     ///

scripts/kani-std-analysis/metrics-data-core.json

@@ -732,6 +732,94 @@
       "verified_safe_fns_under_contract": 111,
       "verified_safe_fns_with_loop_under_contract": 0,
       "total_functions_under_contract_all_crates": 417
+    },
+    {
+      "date": "2025-10-19",
+      "total_unsafe_fns": 7235,
+      "total_unsafe_fns_with_loop": 22,
+      "total_safe_abstractions": 1936,
+      "total_safe_abstractions_with_loop": 90,
+      "total_safe_fns": 16014,
+      "total_safe_fns_with_loop": 778,
+      "unsafe_fns_under_contract": 290,
+      "unsafe_fns_with_loop_under_contract": 3,
+      "verified_unsafe_fns_under_contract": 254,
+      "verified_unsafe_fns_with_loop_under_contract": 1,
+      "safe_abstractions_under_contract": 77,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 77,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 115,
+      "safe_fns_with_loop_under_contract": 1,
+      "verified_safe_fns_under_contract": 112,
+      "verified_safe_fns_with_loop_under_contract": 1,
+      "total_functions_under_contract_all_crates": 424
+    },
+    {
+      "date": "2025-11-09",
+      "total_unsafe_fns": 7235,
+      "total_unsafe_fns_with_loop": 22,
+      "total_safe_abstractions": 1936,
+      "total_safe_abstractions_with_loop": 90,
+      "total_safe_fns": 16014,
+      "total_safe_fns_with_loop": 778,
+      "unsafe_fns_under_contract": 290,
+      "unsafe_fns_with_loop_under_contract": 3,
+      "verified_unsafe_fns_under_contract": 254,
+      "verified_unsafe_fns_with_loop_under_contract": 1,
+      "safe_abstractions_under_contract": 77,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 77,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 115,
+      "safe_fns_with_loop_under_contract": 1,
+      "verified_safe_fns_under_contract": 112,
+      "verified_safe_fns_with_loop_under_contract": 1,
+      "total_functions_under_contract_all_crates": 424
+    },
+    {
+      "date": "2025-11-16",
+      "total_unsafe_fns": 7235,
+      "total_unsafe_fns_with_loop": 22,
+      "total_safe_abstractions": 1936,
+      "total_safe_abstractions_with_loop": 90,
+      "total_safe_fns": 16014,
+      "total_safe_fns_with_loop": 778,
+      "unsafe_fns_under_contract": 290,
+      "unsafe_fns_with_loop_under_contract": 3,
+      "verified_unsafe_fns_under_contract": 254,
+      "verified_unsafe_fns_with_loop_under_contract": 1,
+      "safe_abstractions_under_contract": 77,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 77,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 115,
+      "safe_fns_with_loop_under_contract": 1,
+      "verified_safe_fns_under_contract": 112,
+      "verified_safe_fns_with_loop_under_contract": 1,
+      "total_functions_under_contract_all_crates": 424
+    },
+    {
+      "date": "2025-11-23",
+      "total_unsafe_fns": 7235,
+      "total_unsafe_fns_with_loop": 22,
+      "total_safe_abstractions": 1936,
+      "total_safe_abstractions_with_loop": 90,
+      "total_safe_fns": 16014,
+      "total_safe_fns_with_loop": 778,
+      "unsafe_fns_under_contract": 290,
+      "unsafe_fns_with_loop_under_contract": 3,
+      "verified_unsafe_fns_under_contract": 254,
+      "verified_unsafe_fns_with_loop_under_contract": 1,
+      "safe_abstractions_under_contract": 77,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 77,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 115,
+      "safe_fns_with_loop_under_contract": 1,
+      "verified_safe_fns_under_contract": 112,
+      "verified_safe_fns_with_loop_under_contract": 1,
+      "total_functions_under_contract_all_crates": 424
     }
   ]
 }

scripts/kani-std-analysis/metrics-data-std.json

@@ -615,6 +615,94 @@
       "verified_safe_fns_under_contract": 0,
       "verified_safe_fns_with_loop_under_contract": 0,
       "total_functions_under_contract_all_crates": 417
+    },
+    {
+      "date": "2025-10-19",
+      "total_unsafe_fns": 180,
+      "total_unsafe_fns_with_loop": 12,
+      "total_safe_abstractions": 510,
+      "total_safe_abstractions_with_loop": 42,
+      "total_safe_fns": 4115,
+      "total_safe_fns_with_loop": 185,
+      "unsafe_fns_under_contract": 10,
+      "unsafe_fns_with_loop_under_contract": 1,
+      "verified_unsafe_fns_under_contract": 7,
+      "verified_unsafe_fns_with_loop_under_contract": 0,
+      "safe_abstractions_under_contract": 0,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 0,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 0,
+      "safe_fns_with_loop_under_contract": 0,
+      "verified_safe_fns_under_contract": 0,
+      "verified_safe_fns_with_loop_under_contract": 0,
+      "total_functions_under_contract_all_crates": 424
+    },
+    {
+      "date": "2025-11-09",
+      "total_unsafe_fns": 180,
+      "total_unsafe_fns_with_loop": 12,
+      "total_safe_abstractions": 510,
+      "total_safe_abstractions_with_loop": 42,
+      "total_safe_fns": 4115,
+      "total_safe_fns_with_loop": 185,
+      "unsafe_fns_under_contract": 10,
+      "unsafe_fns_with_loop_under_contract": 1,
+      "verified_unsafe_fns_under_contract": 7,
+      "verified_unsafe_fns_with_loop_under_contract": 0,
+      "safe_abstractions_under_contract": 0,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 0,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 0,
+      "safe_fns_with_loop_under_contract": 0,
+      "verified_safe_fns_under_contract": 0,
+      "verified_safe_fns_with_loop_under_contract": 0,
+      "total_functions_under_contract_all_crates": 424
+    },
+    {
+      "date": "2025-11-16",
+      "total_unsafe_fns": 180,
+      "total_unsafe_fns_with_loop": 12,
+      "total_safe_abstractions": 510,
+      "total_safe_abstractions_with_loop": 42,
+      "total_safe_fns": 4115,
+      "total_safe_fns_with_loop": 185,
+      "unsafe_fns_under_contract": 10,
+      "unsafe_fns_with_loop_under_contract": 1,
+      "verified_unsafe_fns_under_contract": 7,
+      "verified_unsafe_fns_with_loop_under_contract": 0,
+      "safe_abstractions_under_contract": 0,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 0,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 0,
+      "safe_fns_with_loop_under_contract": 0,
+      "verified_safe_fns_under_contract": 0,
+      "verified_safe_fns_with_loop_under_contract": 0,
+      "total_functions_under_contract_all_crates": 424
+    },
+    {
+      "date": "2025-11-23",
+      "total_unsafe_fns": 180,
+      "total_unsafe_fns_with_loop": 12,
+      "total_safe_abstractions": 510,
+      "total_safe_abstractions_with_loop": 42,
+      "total_safe_fns": 4115,
+      "total_safe_fns_with_loop": 185,
+      "unsafe_fns_under_contract": 10,
+      "unsafe_fns_with_loop_under_contract": 1,
+      "verified_unsafe_fns_under_contract": 7,
+      "verified_unsafe_fns_with_loop_under_contract": 0,
+      "safe_abstractions_under_contract": 0,
+      "safe_abstractions_with_loop_under_contract": 0,
+      "verified_safe_abstractions_under_contract": 0,
+      "verified_safe_abstractions_with_loop_under_contract": 0,
+      "safe_fns_under_contract": 0,
+      "safe_fns_with_loop_under_contract": 0,
+      "verified_safe_fns_under_contract": 0,
+      "verified_safe_fns_with_loop_under_contract": 0,
+      "total_functions_under_contract_all_crates": 424
     }
   ]
 }

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.