Merge branch 'main' into verifast-scripts

Author: btj

library/core/src/ub_checks.rs

@@ -192,7 +192,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

@@ -754,6 +754,72 @@
       "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

@@ -637,6 +637,72 @@
       "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-negative/verify.sh

@@ -1,6 +1,6 @@
 set -e -x
 
-export VFVERSION=25.07
+export VFVERSION=25.08
 
 ! verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns verified/lib.rs
 ! refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs

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.