Sync the VeriFast proofs and provide guidance on same (#313)

Updates the VeriFast proofs after `linked_list.rs` was modified by
rust-lang@c39f33b
.

Also:
- Added a bash script that attempts to automatically patch the proofs
after the original file was changed.
- The VeriFast CI actions now produce an error alert suggesting to run
this script, if a source file that is the subject of a VeriFast proof is
changed.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: btj

.github/workflows/verifast-negative.yml

@@ -42,4 +42,4 @@ jobs:
         run: |
           export PATH=~/verifast-25.02/bin:$PATH
           cd verifast-proofs
-          mysh check-verifast-proofs-negative.mysh
+          bash check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

@@ -39,4 +39,29 @@ jobs:
         run: |
           export PATH=~/verifast-25.02/bin:$PATH
           cd verifast-proofs
-          mysh check-verifast-proofs.mysh
+          bash check-verifast-proofs.sh
+
+  notify-btj:
+    name: Notify @btj
+    runs-on: ubuntu-latest
+    needs: check-verifast-on-std
+    if: failure()
+    permissions:
+      id-token: write
+    
+    steps:
+      - name: Get GitHub OIDC token
+        id: get_token
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const audience = 'notify-bart-jacobs';
+            return await core.getIDToken(audience);
+          result-encoding: string
+
+      - name: Call notification endpoint
+        run: |
+          curl -X POST "https://verify-rust-std-verifast-monitor.bart-jacobs.workers.dev/" \
+            -H "Authorization: Bearer ${{ steps.get_token.outputs.result }}" \
+            -H "Content-Type: application/json" \
+            -d '{}'

verifast-proofs/README.md

@@ -2,6 +2,9 @@
 
 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.
+
 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

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

@@ -1140,7 +1140,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// Splitting a list into evens and odds, reusing the original list:
     ///
     /// ```
-    /// #![feature(extract_if)]
     /// use std::collections::LinkedList;
     ///
     /// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1152,7 +1151,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
     /// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
     /// ```
-    #[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+    #[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
     pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
     where
         F: FnMut(&mut T) -> bool,
@@ -1932,24 +1931,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
 }
 
 /// An iterator produced by calling `extract_if` on LinkedList.
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 #[must_use = "iterators are lazy and do nothing unless consumed"]
 pub struct ExtractIf<
     'a,
     T: 'a,
     F: 'a,
     #[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
-> where
-    F: FnMut(&mut T) -> bool,
-{
+> {
     list: &'a mut LinkedList<T, A>,
     it: Option<NonNull<Node<T>>>,
     pred: F,
     idx: usize,
     old_len: usize,
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
 where
     F: FnMut(&mut T) -> bool,
@@ -1978,11 +1975,8 @@ where
     }
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
-impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
-where
-    F: FnMut(&mut T) -> bool,
-{
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
+impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         f.debug_tuple("ExtractIf").field(&self.list).finish()
     }

verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs

@@ -1305,7 +1305,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// Splitting a list into evens and odds, reusing the original list:
     ///
     /// ```
-    /// #![feature(extract_if)]
     /// use std::collections::LinkedList;
     ///
     /// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1317,7 +1316,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
     /// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
     /// ```
-    #[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+    #[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
     pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
     where
         F: FnMut(&mut T) -> bool,
@@ -2097,24 +2096,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
 }
 
 /// An iterator produced by calling `extract_if` on LinkedList.
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 #[must_use = "iterators are lazy and do nothing unless consumed"]
 pub struct ExtractIf<
     'a,
     T: 'a,
     F: 'a,
     #[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
-> where
-    F: FnMut(&mut T) -> bool,
-{
+> {
     list: &'a mut LinkedList<T, A>,
     it: Option<NonNull<Node<T>>>,
     pred: F,
     idx: usize,
     old_len: usize,
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
 where
     F: FnMut(&mut T) -> bool,
@@ -2143,11 +2140,8 @@ where
     }
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
-impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
-where
-    F: FnMut(&mut T) -> bool,
-{
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
+impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         f.debug_tuple("ExtractIf").field(&self.list).finish()
     }

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

@@ -1140,7 +1140,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// Splitting a list into evens and odds, reusing the original list:
     ///
     /// ```
-    /// #![feature(extract_if)]
     /// use std::collections::LinkedList;
     ///
     /// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1152,7 +1151,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
     /// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
     /// ```
-    #[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+    #[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
     pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
     where
         F: FnMut(&mut T) -> bool,
@@ -1932,24 +1931,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
 }
 
 /// An iterator produced by calling `extract_if` on LinkedList.
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 #[must_use = "iterators are lazy and do nothing unless consumed"]
 pub struct ExtractIf<
     'a,
     T: 'a,
     F: 'a,
     #[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
-> where
-    F: FnMut(&mut T) -> bool,
-{
+> {
     list: &'a mut LinkedList<T, A>,
     it: Option<NonNull<Node<T>>>,
     pred: F,
     idx: usize,
     old_len: usize,
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
 where
     F: FnMut(&mut T) -> bool,
@@ -1978,11 +1975,8 @@ where
     }
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
-impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
-where
-    F: FnMut(&mut T) -> bool,
-{
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
+impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         f.debug_tuple("ExtractIf").field(&self.list).finish()
     }

verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs

@@ -1305,7 +1305,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// Splitting a list into evens and odds, reusing the original list:
     ///
     /// ```
-    /// #![feature(extract_if)]
     /// use std::collections::LinkedList;
     ///
     /// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1317,7 +1316,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
     /// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
     /// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
     /// ```
-    #[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+    #[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
     pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
     where
         F: FnMut(&mut T) -> bool,
@@ -2097,24 +2096,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
 }
 
 /// An iterator produced by calling `extract_if` on LinkedList.
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 #[must_use = "iterators are lazy and do nothing unless consumed"]
 pub struct ExtractIf<
     'a,
     T: 'a,
     F: 'a,
     #[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
-> where
-    F: FnMut(&mut T) -> bool,
-{
+> {
     list: &'a mut LinkedList<T, A>,
     it: Option<NonNull<Node<T>>>,
     pred: F,
     idx: usize,
     old_len: usize,
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
 impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
 where
     F: FnMut(&mut T) -> bool,
@@ -2143,11 +2140,8 @@ where
     }
 }
 
-#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
-impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
-where
-    F: FnMut(&mut T) -> bool,
-{
+#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
+impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         f.debug_tuple("ExtractIf").field(&self.list).finish()
     }

verifast-proofs/check-verifast-proofs-negative.mysh

@@ -0,0 +1,14 @@
+set -e -x
+
+cd alloc
+  cd collections
+    cd linked_list.rs-negative
+      ! 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
+      if ! diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs; then
+        echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please run verifast-proofs/patch-verifast-proofs.sh to update them."
+        false
+      fi
+    cd ..
+  cd ..
+cd ..

verifast-proofs/check-verifast-proofs-negative.sh

@@ -0,0 +1,14 @@
+set -e -x
+
+cd alloc
+  cd collections
+    cd linked_list.rs
+      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 > /dev/null
+      if ! diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs; then
+        echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please run verifast-proofs/patch-verifast-proofs.sh to update them."
+        false
+      fi
+    cd ..
+  cd ..
+cd ..

verifast-proofs/check-verifast-proofs.mysh

@@ -0,0 +1,14 @@
+set -e -x
+
+pushd alloc/collections/linked_list.rs
+  diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > linked_list.diff || [ "$?" = 1 ]
+  patch -p0 verified/linked_list.rs < linked_list.diff
+  patch -p0 original/linked_list.rs < linked_list.diff
+  rm linked_list.diff
+popd
+pushd alloc/collections/linked_list.rs-negative
+  diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > linked_list.diff || [ "$?" = 1 ]
+  patch -p0 verified/linked_list.rs < linked_list.diff
+  patch -p0 original/linked_list.rs < linked_list.diff
+  rm linked_list.diff
+popd