Merge remote-tracking branch 'origin/main' into subtree/library

.github/workflows/verifast-negative.yml

@@ -0,0 +1,45 @@
+# This workflow runs some negative VeriFast test cases, to ensure
+# that VeriFast actually catches bugs.
+
+name: VeriFast (negative)
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/verifast.yml'
+      - 'verifast-proofs/**'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  check-verifast-on-std:
+    name: Verify std library
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - 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
+
+      - name: Install the Rust toolchain used by VeriFast
+        run: rustup toolchain install nightly-2024-11-23
+
+      - name: Run VeriFast Verification
+        run: |
+          export PATH=~/verifast-25.02/bin:$PATH
+          cd verifast-proofs
+          mysh check-verifast-proofs-negative.mysh

.github/workflows/verifast.yml

@@ -0,0 +1,42 @@
+name: VeriFast
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/verifast.yml'
+      - 'verifast-proofs/**'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  check-verifast-on-std:
+    name: Verify std library
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - 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
+
+      - name: Install the Rust toolchain used by VeriFast
+        run: rustup toolchain install nightly-2024-11-23
+
+      - name: Run VeriFast Verification
+        run: |
+          export PATH=~/verifast-25.02/bin:$PATH
+          cd verifast-proofs
+          mysh check-verifast-proofs.mysh

doc/src/SUMMARY.md

@@ -9,6 +9,7 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
   - [GOTO Transcoder](./tools/goto-transcoder.md)
+  - [VeriFast](./tools/verifast.md)
 
 ---
 

doc/src/tools.md

@@ -13,6 +13,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 |---------------------|-------|
  | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
  | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml)      |
+ | VeriFast for Rust   | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml)      |
 
 
 

doc/src/tools/verifast.md

@@ -0,0 +1,186 @@
+# VeriFast for Rust
+
+[VeriFast](https://github.com/verifast/verifast) is a tool for verifying the
+absence of [undefined
+behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html)
+in single-threaded or multithreaded Rust programs that use `unsafe` blocks, and
+for verifying
+[soundness](https://doc.rust-lang.org/nomicon/working-with-unsafe.html) of Rust
+crates/modules that use `unsafe` blocks. VeriFast performs *modular
+verification*: it verifies one function at a time; during the verification of
+one function, if that function calls another function, VeriFast uses the
+callee's *specification*, not its implementation, to reason about the call.
+VeriFast verifies each function against its specification: it verifies that, if
+started in a state that satisfies the precondition, the function does not have
+undefined behavior and any state in which it returns satisfies the
+postcondition.
+
+Besides requiring that the user annotate each function with a precondition and
+a postcondition, VeriFast also requires that the user annotate each loop with a
+loop invariant. This enables its modular symbolic execution algorithm to
+perform only a single symbolic execution of the loop's body to cover all
+possible real executions of the loop. Furthermore, the use of function
+specifications means a single symbolic execution of a function covers all
+possible real executions, even if the function is recursive. In summary, these
+annotations enable VeriFast to perform unbounded verification (i.e. of
+arbitrarily long, including infinitely long, executions) in finite time.
+
+VeriFast function specifications and loop invariants are expressed in a form of
+[*separation logic*](https://en.wikipedia.org/wiki/Separation_logic), and it
+performs symbolic execution using a separation logic-based representation of
+memory. Separation logic addresses the problem of *aliasing*, which is that in
+programs involving pointers or references, different expressions can denote the
+same variable. By enabling assertions to express exclusive *ownership* of
+memory regions, separation logic enables concise specifications, proper
+information hiding, and efficient verification for pointer-manipulating
+programs.
+
+## Verifying `unsafe` functions
+
+Consider, for example, the function `Node::reverse_in_place` below that reverses the
+given linked list in-place and returns a pointer to the first node (which
+was the originally the last node).
+
+```rust
+struct Node {
+    next: *mut Node,
+}
+
+/*@
+
+pred Nodes(n: *mut Node; nodes: list<*mut Node>) =
+    if n == 0 {
+        nodes == nil
+    } else {
+        (*n).next |-> ?next &*& Nodes(next, ?nodes0) &*& nodes == cons(n, nodes0)
+    };
+
+@*/
+
+impl Node {
+
+    unsafe fn reverse_in_place(mut n: *mut Node) -> *mut Node
+    //@ req Nodes(n, ?nodes);
+    //@ ens Nodes(result, reverse(nodes));
+    //@ on_unwind_ens false;
+    {
+        let mut m = std::ptr::null_mut();
+        loop {
+            //@ inv Nodes(n, ?n_nodes) &*& Nodes(m, ?m_nodes) &*& reverse(nodes) == append(reverse(n_nodes), m_nodes);
+            //@ open Nodes(n, _);
+            if n.is_null() {
+                return m;
+            }
+            let k = (*n).next;
+            //@ append_assoc(reverse(tail(n_nodes)), [n], m_nodes);
+            (*n).next = m;
+            m = n;
+            n = k;
+        }
+    }
+
+}
+```
+
+VeriFast interprets comments of the form `/*@ ... @*/` or `//@ ...` as VeriFast annotations. This example illustrates four types of annotations:
+- Three *specification clause annotations* specify the function's precondition, postcondition, and unwind postcondition, respectively. The function never unwinds, so its
+  unwind postcondition is `false`.
+- The precondition and postcondition are specified in terms of the separation logic predicate `Nodes`, defined in a *ghost declaration annotation*. This predicate
+  recursively defines the memory footprint of the linked list starting at a given node `n` and associates it with a mathematical list `nodes` of node locations.
+  The separating conjunction `&*&` implies that the first node of the linked list is *separate* from the remainder of the linked list. It follows that mutating the first node does not affect
+  the remainder of the linked list. The *variable pattern* `?next` binds logical variable `next` to the value of field `(*n).next`; its scope extends to the end of the assertion.
+  If a logical variable is introduced in a precondition, its scope includes the postcondition.
+- At the start of the loop body, a *block annotation* specifies the loop invariant, expressing that `n` and `m` point to disjoint linked lists and expressing the relationship between their contents and that of the original linked list.
+- *Ghost command annotations* provide hints needed for the symbolic execution algorithm to succeed. `open Nodes(n, _)` unfolds the `Nodes` predicate application whose first argument equals `n`. `append_assoc` invokes a library *lemma* expressing the associativity of the `append` operation on mathematical lists.
+
+The generic mathematical datatype `list` is defined in file [`list.rsspec`](https://github.com/verifast/verifast/blob/master/bin/rust/list.rsspec), part of VeriFast's *prelude*, as follows:
+```
+inductive list<t> = nil | cons(t, list<t>);
+```
+A list of `t` values is either empty, denoted by *constructor* `nil`, or nonempty, with first element (or *head*) `v` and remainder (or *tail*) `vs`, denoted by `cons(v, vs)`.
+
+Mathematical functions `append` and `reverse` are defined in the same file as follows:
+```
+fix append<t>(xs: list<t>, ys: list<t>) -> list<t> {
+    match xs {
+        nil => ys,
+        cons(x, xs0) => cons(x, append(xs0, ys))
+    }
+}
+
+fix reverse<t>(xs: list<t>) -> list<t> {
+    match xs {
+        nil => nil,
+        cons(x, xs0) => append(reverse(xs0), cons(x, nil))
+    }
+}
+```
+Lemma `append_assoc` is declared (but not proven) in the same file. Here is a proof:
+```
+lem append_assoc<t>(xs: list<t>, ys: list<t>, zs: list<t>)
+    req true;
+    ens append(append(xs, ys), zs) == append(xs, append(ys, zs));
+{
+    match xs {
+        nil => {}
+        cons(x, xs0) => {
+            append_assoc(xs0, ys, zs);
+        }
+    }
+}
+```
+A lemma is like a regular Rust function, except that it is declared inside an annotation. VeriFast checks that it has no side effects and that it terminates.
+
+## Verifying safe abstractions
+
+Consider the following broken implementation of [`std::mem::replace`](https://doc.rust-lang.org/std/mem/fn.replace.html):
+```rust
+fn replace<T>(dest: &mut T, src: T) -> T {
+    unsafe {
+        let result = (dest as *mut T).read();
+        (dest as *mut T).write(src);
+        (dest as *mut T).read() // should be `result`
+    }
+}
+```
+The Rust compiler accepts it just fine, but VeriFast complains that it cannot prove that when this function returns, the ownership of the value pointed to by `dest` is *separate* from the ownership of the return value. If we replace the final line by `result`, VeriFast accepts the code.
+
+For a function not marked as `unsafe`, VeriFast generates a specification expressing that the function is *semantically well-typed* per [RustBelt](https://research.ralfj.de/thesis.html)'s definition of what Rust's types mean in separation logic. If no specification clause annotations are provided for the function, VeriFast verifies the function against the generated specification; otherwise, VeriFast first verifies that the provided specification implies the generated one, and then verifies the function against the provided specification.
+
+The generated specification for `replace` is as follows:
+```rust
+fn replace<T>(dest: &mut T, src: T) -> T
+//@ req thread_token(?_t) &*& *dest |-> ?dest0 &*& <T>.own(_t, dest0) &*& <T>.own(_t, src) &*& _t == currentThread;
+//@ ens thread_token(_t) &*& *dest |-> ?dest1 &*& <T>.own(_t, dest1) &*& <T>.own(_t, result);
+```
+`<T>.own(t, v)` expresses ownership of the T value `v` accessible to thread `t` (in case T is not [Send](https://doc.rust-lang.org/nomicon/send-and-sync.html)).
+`thread_token(t)` represents permission to open *nonatomic invariants* and *nonatomic borrows* at thread `t`; these contain resources shared in a non-thread-safe way at thread `t`.
+
+For more information on how to verify safe abstractions in VeriFast, see the relevant [chapter](https://verifast.github.io/verifast/rust-reference/non-unsafe-funcs.html) in the VeriFast for Rust Reference and the [examples](https://github.com/verifast/verifast/tree/master/tests/rust/safe_abstraction) (in `tests/rust/safe_abstraction` in the VeriFast binary distributions). (See [`testsuite.mysh`](https://github.com/verifast/verifast/blob/master/tests/rust/testsuite.mysh) to learn the command line to use to verify a particular example.)
+
+## Running VeriFast
+
+To run VeriFast, download a binary distribution for your platform, either the
+[nightly build](https://github.com/verifast/verifast/releases/tag/nightly) or
+the [latest named
+release](https://github.com/verifast/verifast/releases/latest). Extract the
+archive to any folder on your computer. (On Macs, first [remove the quarantine
+bit](https://github.com/verifast/verifast?tab=readme-ov-file#binaries).) Then,
+either use the VeriFast IDE at `bin/vfide`, the command-line tool at
+`bin/verifast`, or the [VSCode
+extension](https://marketplace.visualstudio.com/items?itemName=VeriFast.verifast).
+In the IDE, open a file and press F5 to verify it. VeriFast will then either
+report "0 errors found" or show a debugger-like GUI that allows you to step
+through the failed symbolic execution path and inspect the symbolic state at
+each step. If verification succeeds, choose Show execution tree to see the tree
+of symbolic execution paths traversed for each function that was verified.
+
+In the IDE, the Verify menu allows you to postpone dealing with certain
+complexities of the verification task. Specifically, you can tell VeriFast to
+ignore unwind paths, ignore arithmetic overflow, and treat shared reference
+creation like raw pointer creation (which ignores the complexities of Rust's
+[pointer aliasing
+rules](https://marketplace.visualstudio.com/items?itemName=VeriFast.verifast)).
+(Many of the other options are only relevant when verifying C programs and have
+no effect when verifying Rust programs.) All of these options can also be
+specified on the command line.

verifast-proofs/.gitignore

@@ -0,0 +1,2 @@
+*.stripped.rs
+*.computed.diff

verifast-proofs/README.md

@@ -0,0 +1,46 @@
+# VeriFast proofs
+
+This directory contains [VeriFast](../doc/src/tools/verifast.md) proofs for (currently a very, very small) part of the standard library.
+
+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.
+
+## Applying VeriFast
+
+To verify a function in a file <code>library/<i>crate</i>/src/<i>mod</i>/<i>file</i>.rs</code>, proceed as follows:
+1. Copy that file to <code>verifast-proofs/<i>crate</i>/<i>mod</i>/<i>file</i>.rs/original/<i>file</i>.rs</code> as well as to <code>verifast-proofs/<i>crate</i>/<i>mod</i>/<i>file</i>.rs/verified/<i>file</i>.rs</code>.
+2. Create a file <code>verifast-proofs/<i>crate</i>/<i>mod</i>/<i>file</i>.rs/original/lib.rs</code> to serve as crate root for verification, and include <code><b>mod</b> <i>file</i>;</code>. (See the existing proofs for examples.) Copy it to <code>verifast-proofs/<i>crate</i>/<i>mod</i>/<i>file</i>.rs/verified/lib.rs</code>.
+2. Add a VeriFast specification to the function(s) you want to verify, and any other VeriFast annotations to make the proof go through, in <code>verifast-proofs/<i>crate</i>/<i>mod</i>/<i>file</i>.rs/verified/<i>file</i>.rs</code>. While doing so, you will need to change the code slightly so as to be able to insert ghost commands in the correct places. 
+3. Add commands for checking your proof to `verifast-proofs/check-verifast-proofs.mysh`. This includes the following:
+    1. A `verifast` invocation for checking the VeriFast proof.
+    2. A `refinement-checker` invocation for checking that the code changes you made in the verified version do not change the meaning of the program. Specifically, this tool checks that the original code *refines* the verified code, i.e. that each behavior of a function in the original version is also a behavior of the corresponding function in the verified version. As a result, if the verified version has been verified to have no bad behaviors, the original version also has no bad behaviors.
+    3. A `diff` invocation for checking that the version in `original` is identical to the original version in `library`.
+
+### Example
+
+Take the VeriFast proof of `linked_list.rs` as an example. The file structure is:
+
+```
+linked_list.rs
+  original
+    lib.rs
+    linked_list.rs
+    linked_list
+      tests.rs
+  verified
+    lib.rs
+    linked_list.rs
+    linked_list
+      tests.rs
+```
+- The `lib.rs` files are the crate roots we created for verification.
+- The `linked_list.rs` files contain the `LinkedList` implementation code. `verified/linked_list.rs` adds VeriFast annotations and includes minor code changes with respect to the implementation in `original/linked_list.rs` when necessary to make it possible for annotations to be inserted in the right places and to make the proof go through.
+- Since the original `linked_list.rs` contains a `tests` module, we create empty `tests.rs` files.
+
+We then:
+1. Run VeriFast to ensure the proof in `verified/linked_list.rs` goes through.
+2. Run the refinement checker to make sure that `verified/linked_list.rs` refines `original/linked_list.rs`. Since we made changes to `verified/linked_list.rs` to make the proof go through, we want to be sure that those changes did not affect the implementation behavior--i.e., we want to be sure that our proof of the verified version of the file actually allows us to make claims about the original version.
+3. Run the diff tool to ensure that `original/linked_list.rs` matches the file in `library/`, i.e., check that we're verifying the most recent version of the `LinkedList` implementation available in this repository.
+
+Separating steps 2) and 3) lets us distinguish between CI failures caused by incorrect modifications to the verified files (failure in step 2) versus a proof that was once correct, but is just out of date (failure in step 3). Without the copy of the original file, when the `library/` files change, there would be no easy way to tell whether the VeriFast proofs are wrong or just stale.
+
+The [VeriFast](../.github/workflows/verifast.yml) GitHub action will run `verifast-proofs/check-verifast-proofs.mysh`. Check that file to see which version of VeriFast is used.

verifast-proofs/alloc/collections/linked_list.rs-negative/original/lib.rs

@@ -0,0 +1,29 @@
+// verifast_options{skip_specless_fns}
+
+#![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)]
+
+#![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;
+
+trait SpecExtend<I> {
+    fn spec_extend(&mut self, iter: I);
+}
+
+pub mod linked_list;