From f7f8c5d971cacaa8757c96d0b99981093e51b23e Mon Sep 17 00:00:00 2001 From: Bart Jacobs Date: Thu, 3 Apr 2025 18:12:45 +0200 Subject: [PATCH 1/3] Provide guidance on out-of-date VeriFast proofs --- .github/workflows/verifast-negative.yml | 2 +- .github/workflows/verifast.yml | 2 +- verifast-proofs/README.md | 3 +++ .../check-verifast-proofs-negative.mysh | 9 --------- verifast-proofs/check-verifast-proofs-negative.sh | 14 ++++++++++++++ verifast-proofs/check-verifast-proofs.mysh | 9 --------- verifast-proofs/check-verifast-proofs.sh | 14 ++++++++++++++ verifast-proofs/patch-verifast-proofs.sh | 14 ++++++++++++++ 8 files changed, 47 insertions(+), 20 deletions(-) delete mode 100644 verifast-proofs/check-verifast-proofs-negative.mysh create mode 100644 verifast-proofs/check-verifast-proofs-negative.sh delete mode 100644 verifast-proofs/check-verifast-proofs.mysh create mode 100644 verifast-proofs/check-verifast-proofs.sh create mode 100644 verifast-proofs/patch-verifast-proofs.sh diff --git a/.github/workflows/verifast-negative.yml b/.github/workflows/verifast-negative.yml index c3e718e53e010..c9ccf44cf0b7a 100644 --- a/.github/workflows/verifast-negative.yml +++ b/.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 diff --git a/.github/workflows/verifast.yml b/.github/workflows/verifast.yml index 93581b1029887..d05b19ef70986 100644 --- a/.github/workflows/verifast.yml +++ b/.github/workflows/verifast.yml @@ -39,4 +39,4 @@ jobs: run: | export PATH=~/verifast-25.02/bin:$PATH cd verifast-proofs - mysh check-verifast-proofs.mysh + bash check-verifast-proofs.sh diff --git a/verifast-proofs/README.md b/verifast-proofs/README.md index 9033192ac9ad9..ee3b573810552 100644 --- a/verifast-proofs/README.md +++ b/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 diff --git a/verifast-proofs/check-verifast-proofs-negative.mysh b/verifast-proofs/check-verifast-proofs-negative.mysh deleted file mode 100644 index 44bfd245e55ab..0000000000000 --- a/verifast-proofs/check-verifast-proofs-negative.mysh +++ /dev/null @@ -1,9 +0,0 @@ -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 - diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs - cd .. - cd .. -cd .. diff --git a/verifast-proofs/check-verifast-proofs-negative.sh b/verifast-proofs/check-verifast-proofs-negative.sh new file mode 100644 index 0000000000000..e1e36ad8d52cd --- /dev/null +++ b/verifast-proofs/check-verifast-proofs-negative.sh @@ -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 .. diff --git a/verifast-proofs/check-verifast-proofs.mysh b/verifast-proofs/check-verifast-proofs.mysh deleted file mode 100644 index bb05d2ec5fd83..0000000000000 --- a/verifast-proofs/check-verifast-proofs.mysh +++ /dev/null @@ -1,9 +0,0 @@ -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 - diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs - cd .. - cd .. -cd .. diff --git a/verifast-proofs/check-verifast-proofs.sh b/verifast-proofs/check-verifast-proofs.sh new file mode 100644 index 0000000000000..c8f393a3a9328 --- /dev/null +++ b/verifast-proofs/check-verifast-proofs.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 .. diff --git a/verifast-proofs/patch-verifast-proofs.sh b/verifast-proofs/patch-verifast-proofs.sh new file mode 100644 index 0000000000000..3e1f17f268e5f --- /dev/null +++ b/verifast-proofs/patch-verifast-proofs.sh @@ -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 From 3a6157ecc28ab3ab046b2be42e32157a4a9bb785 Mon Sep 17 00:00:00 2001 From: Bart Jacobs Date: Thu, 3 Apr 2025 18:16:47 +0200 Subject: [PATCH 2/3] Sync the VeriFast proofs --- .../original/linked_list.rs | 18 ++++++------------ .../verified/linked_list.rs | 18 ++++++------------ .../linked_list.rs/original/linked_list.rs | 18 ++++++------------ .../linked_list.rs/verified/linked_list.rs | 18 ++++++------------ 4 files changed, 24 insertions(+), 48 deletions(-) diff --git a/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs index ca0ea1ec8b2ba..3183268b4b32e 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs @@ -1140,7 +1140,6 @@ impl LinkedList { /// Splitting a list into evens and odds, reusing the original list: /// /// ``` - /// #![feature(extract_if)] /// use std::collections::LinkedList; /// /// let mut numbers: LinkedList = LinkedList::new(); @@ -1152,7 +1151,7 @@ impl LinkedList { /// assert_eq!(evens.into_iter().collect::>(), vec![2, 4, 6, 8, 14]); /// assert_eq!(odds.into_iter().collect::>(), 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(&mut self, filter: F) -> ExtractIf<'_, T, F, A> where F: FnMut(&mut T) -> bool, @@ -1932,16 +1931,14 @@ 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, it: Option>>, pred: F, @@ -1949,7 +1946,7 @@ pub struct ExtractIf< old_len: usize, } -#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")] +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] impl 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 fmt::Debug for ExtractIf<'_, T, F> -where - F: FnMut(&mut T) -> bool, -{ +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] +impl fmt::Debug for ExtractIf<'_, T, F> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { f.debug_tuple("ExtractIf").field(&self.list).finish() } diff --git a/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs index d5e4c6d63ba30..d56de1d3936d3 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs @@ -1305,7 +1305,6 @@ impl LinkedList { /// Splitting a list into evens and odds, reusing the original list: /// /// ``` - /// #![feature(extract_if)] /// use std::collections::LinkedList; /// /// let mut numbers: LinkedList = LinkedList::new(); @@ -1317,7 +1316,7 @@ impl LinkedList { /// assert_eq!(evens.into_iter().collect::>(), vec![2, 4, 6, 8, 14]); /// assert_eq!(odds.into_iter().collect::>(), 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(&mut self, filter: F) -> ExtractIf<'_, T, F, A> where F: FnMut(&mut T) -> bool, @@ -2097,16 +2096,14 @@ 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, it: Option>>, pred: F, @@ -2114,7 +2111,7 @@ pub struct ExtractIf< old_len: usize, } -#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")] +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] impl 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 fmt::Debug for ExtractIf<'_, T, F> -where - F: FnMut(&mut T) -> bool, -{ +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] +impl fmt::Debug for ExtractIf<'_, T, F> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { f.debug_tuple("ExtractIf").field(&self.list).finish() } diff --git a/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs index ca0ea1ec8b2ba..3183268b4b32e 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs @@ -1140,7 +1140,6 @@ impl LinkedList { /// Splitting a list into evens and odds, reusing the original list: /// /// ``` - /// #![feature(extract_if)] /// use std::collections::LinkedList; /// /// let mut numbers: LinkedList = LinkedList::new(); @@ -1152,7 +1151,7 @@ impl LinkedList { /// assert_eq!(evens.into_iter().collect::>(), vec![2, 4, 6, 8, 14]); /// assert_eq!(odds.into_iter().collect::>(), 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(&mut self, filter: F) -> ExtractIf<'_, T, F, A> where F: FnMut(&mut T) -> bool, @@ -1932,16 +1931,14 @@ 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, it: Option>>, pred: F, @@ -1949,7 +1946,7 @@ pub struct ExtractIf< old_len: usize, } -#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")] +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] impl 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 fmt::Debug for ExtractIf<'_, T, F> -where - F: FnMut(&mut T) -> bool, -{ +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] +impl fmt::Debug for ExtractIf<'_, T, F> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { f.debug_tuple("ExtractIf").field(&self.list).finish() } diff --git a/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs index fe27962480411..78436dc1799ad 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs @@ -1305,7 +1305,6 @@ impl LinkedList { /// Splitting a list into evens and odds, reusing the original list: /// /// ``` - /// #![feature(extract_if)] /// use std::collections::LinkedList; /// /// let mut numbers: LinkedList = LinkedList::new(); @@ -1317,7 +1316,7 @@ impl LinkedList { /// assert_eq!(evens.into_iter().collect::>(), vec![2, 4, 6, 8, 14]); /// assert_eq!(odds.into_iter().collect::>(), 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(&mut self, filter: F) -> ExtractIf<'_, T, F, A> where F: FnMut(&mut T) -> bool, @@ -2097,16 +2096,14 @@ 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, it: Option>>, pred: F, @@ -2114,7 +2111,7 @@ pub struct ExtractIf< old_len: usize, } -#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")] +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] impl 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 fmt::Debug for ExtractIf<'_, T, F> -where - F: FnMut(&mut T) -> bool, -{ +#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")] +impl fmt::Debug for ExtractIf<'_, T, F> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { f.debug_tuple("ExtractIf").field(&self.list).finish() } From a1e8d3d5561b78c0729cf5d6851caf15fb7d1006 Mon Sep 17 00:00:00 2001 From: Bart Jacobs Date: Fri, 4 Apr 2025 10:07:04 +0200 Subject: [PATCH 3/3] Notify @btj on failure --- .github/workflows/verifast.yml | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/.github/workflows/verifast.yml b/.github/workflows/verifast.yml index d05b19ef70986..728623ace2a66 100644 --- a/.github/workflows/verifast.yml +++ b/.github/workflows/verifast.yml @@ -40,3 +40,28 @@ jobs: export PATH=~/verifast-25.02/bin:$PATH cd verifast-proofs 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 '{}'