Skip to content

Add a tour of the RawVec proof #481

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add a tour of the RawVec proof #481

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions .github/workflows/verifast-negative.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
10 changes: 5 additions & 5 deletions .github/workflows/verifast.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
14 changes: 12 additions & 2 deletions verifast-proofs/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
5 changes: 2 additions & 3 deletions verifast-proofs/alloc/collections/linked_list.rs/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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.
Loading
Loading