Skip to content

Commit 9500327

Browse files
btjbtj
authored
Sync the VeriFast proofs and provide guidance on same (model-checking#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.
1 parent 0acfa26 commit 9500327

File tree

12 files changed

+96
-68
lines changed

12 files changed

+96
-68
lines changed

‎.github/workflows/verifast-negative.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,4 +42,4 @@ jobs:
4242
run: |
4343
export PATH=~/verifast-25.02/bin:$PATH
4444
cd verifast-proofs
45-
mysh check-verifast-proofs-negative.mysh
45+
bash check-verifast-proofs-negative.sh

‎.github/workflows/verifast.yml

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,4 +39,29 @@ jobs:
3939
run: |
4040
export PATH=~/verifast-25.02/bin:$PATH
4141
cd verifast-proofs
42-
mysh check-verifast-proofs.mysh
42+
bash check-verifast-proofs.sh
43+
44+
notify-btj:
45+
name: Notify @btj
46+
runs-on: ubuntu-latest
47+
needs: check-verifast-on-std
48+
if: failure()
49+
permissions:
50+
id-token: write
51+
52+
steps:
53+
- name: Get GitHub OIDC token
54+
id: get_token
55+
uses: actions/github-script@v7
56+
with:
57+
script: |
58+
const audience = 'notify-bart-jacobs';
59+
return await core.getIDToken(audience);
60+
result-encoding: string
61+
62+
- name: Call notification endpoint
63+
run: |
64+
curl -X POST "https://verify-rust-std-verifast-monitor.bart-jacobs.workers.dev/" \
65+
-H "Authorization: Bearer ${{ steps.get_token.outputs.result }}" \
66+
-H "Content-Type: application/json" \
67+
-d '{}'

‎verifast-proofs/README.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@
22

33
This directory contains [VeriFast](../doc/src/tools/verifast.md) proofs for (currently a very, very small) part of the standard library.
44

5+
> [!NOTE]
6+
> 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.
7+
58
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.
69

710
## Applying VeriFast

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

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1140,7 +1140,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
11401140
/// Splitting a list into evens and odds, reusing the original list:
11411141
///
11421142
/// ```
1143-
/// #![feature(extract_if)]
11441143
/// use std::collections::LinkedList;
11451144
///
11461145
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1152,7 +1151,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
11521151
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
11531152
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
11541153
/// ```
1155-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1154+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
11561155
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
11571156
where
11581157
F: FnMut(&mut T) -> bool,
@@ -1932,24 +1931,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
19321931
}
19331932

19341933
/// An iterator produced by calling `extract_if` on LinkedList.
1935-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1934+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19361935
#[must_use = "iterators are lazy and do nothing unless consumed"]
19371936
pub struct ExtractIf<
19381937
'a,
19391938
T: 'a,
19401939
F: 'a,
19411940
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
1942-
> where
1943-
F: FnMut(&mut T) -> bool,
1944-
{
1941+
> {
19451942
list: &'a mut LinkedList<T, A>,
19461943
it: Option<NonNull<Node<T>>>,
19471944
pred: F,
19481945
idx: usize,
19491946
old_len: usize,
19501947
}
19511948

1952-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1949+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19531950
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
19541951
where
19551952
F: FnMut(&mut T) -> bool,
@@ -1978,11 +1975,8 @@ where
19781975
}
19791976
}
19801977

1981-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1982-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
1983-
where
1984-
F: FnMut(&mut T) -> bool,
1985-
{
1978+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
1979+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
19861980
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
19871981
f.debug_tuple("ExtractIf").field(&self.list).finish()
19881982
}

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

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1305,7 +1305,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
13051305
/// Splitting a list into evens and odds, reusing the original list:
13061306
///
13071307
/// ```
1308-
/// #![feature(extract_if)]
13091308
/// use std::collections::LinkedList;
13101309
///
13111310
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1317,7 +1316,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
13171316
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
13181317
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
13191318
/// ```
1320-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1319+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
13211320
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
13221321
where
13231322
F: FnMut(&mut T) -> bool,
@@ -2097,24 +2096,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
20972096
}
20982097

20992098
/// An iterator produced by calling `extract_if` on LinkedList.
2100-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2099+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21012100
#[must_use = "iterators are lazy and do nothing unless consumed"]
21022101
pub struct ExtractIf<
21032102
'a,
21042103
T: 'a,
21052104
F: 'a,
21062105
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
2107-
> where
2108-
F: FnMut(&mut T) -> bool,
2109-
{
2106+
> {
21102107
list: &'a mut LinkedList<T, A>,
21112108
it: Option<NonNull<Node<T>>>,
21122109
pred: F,
21132110
idx: usize,
21142111
old_len: usize,
21152112
}
21162113

2117-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2114+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21182115
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
21192116
where
21202117
F: FnMut(&mut T) -> bool,
@@ -2143,11 +2140,8 @@ where
21432140
}
21442141
}
21452142

2146-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2147-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
2148-
where
2149-
F: FnMut(&mut T) -> bool,
2150-
{
2143+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
2144+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
21512145
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
21522146
f.debug_tuple("ExtractIf").field(&self.list).finish()
21532147
}

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

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1140,7 +1140,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
11401140
/// Splitting a list into evens and odds, reusing the original list:
11411141
///
11421142
/// ```
1143-
/// #![feature(extract_if)]
11441143
/// use std::collections::LinkedList;
11451144
///
11461145
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1152,7 +1151,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
11521151
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
11531152
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
11541153
/// ```
1155-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1154+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
11561155
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
11571156
where
11581157
F: FnMut(&mut T) -> bool,
@@ -1932,24 +1931,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
19321931
}
19331932

19341933
/// An iterator produced by calling `extract_if` on LinkedList.
1935-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1934+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19361935
#[must_use = "iterators are lazy and do nothing unless consumed"]
19371936
pub struct ExtractIf<
19381937
'a,
19391938
T: 'a,
19401939
F: 'a,
19411940
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
1942-
> where
1943-
F: FnMut(&mut T) -> bool,
1944-
{
1941+
> {
19451942
list: &'a mut LinkedList<T, A>,
19461943
it: Option<NonNull<Node<T>>>,
19471944
pred: F,
19481945
idx: usize,
19491946
old_len: usize,
19501947
}
19511948

1952-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1949+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19531950
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
19541951
where
19551952
F: FnMut(&mut T) -> bool,
@@ -1978,11 +1975,8 @@ where
19781975
}
19791976
}
19801977

1981-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1982-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
1983-
where
1984-
F: FnMut(&mut T) -> bool,
1985-
{
1978+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
1979+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
19861980
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
19871981
f.debug_tuple("ExtractIf").field(&self.list).finish()
19881982
}

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

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1305,7 +1305,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
13051305
/// Splitting a list into evens and odds, reusing the original list:
13061306
///
13071307
/// ```
1308-
/// #![feature(extract_if)]
13091308
/// use std::collections::LinkedList;
13101309
///
13111310
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1317,7 +1316,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
13171316
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
13181317
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
13191318
/// ```
1320-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1319+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
13211320
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
13221321
where
13231322
F: FnMut(&mut T) -> bool,
@@ -2097,24 +2096,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
20972096
}
20982097

20992098
/// An iterator produced by calling `extract_if` on LinkedList.
2100-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2099+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21012100
#[must_use = "iterators are lazy and do nothing unless consumed"]
21022101
pub struct ExtractIf<
21032102
'a,
21042103
T: 'a,
21052104
F: 'a,
21062105
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
2107-
> where
2108-
F: FnMut(&mut T) -> bool,
2109-
{
2106+
> {
21102107
list: &'a mut LinkedList<T, A>,
21112108
it: Option<NonNull<Node<T>>>,
21122109
pred: F,
21132110
idx: usize,
21142111
old_len: usize,
21152112
}
21162113

2117-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2114+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21182115
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
21192116
where
21202117
F: FnMut(&mut T) -> bool,
@@ -2143,11 +2140,8 @@ where
21432140
}
21442141
}
21452142

2146-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2147-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
2148-
where
2149-
F: FnMut(&mut T) -> bool,
2150-
{
2143+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
2144+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
21512145
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
21522146
f.debug_tuple("ExtractIf").field(&self.list).finish()
21532147
}

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

Lines changed: 0 additions & 9 deletions
This file was deleted.

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
set -e -x
2+
3+
cd alloc
4+
cd collections
5+
cd linked_list.rs-negative
6+
! verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns verified/lib.rs
7+
! refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs
8+
if ! diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs; then
9+
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."
10+
false
11+
fi
12+
cd ..
13+
cd ..
14+
cd ..

‎verifast-proofs/check-verifast-proofs.mysh

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎verifast-proofs/check-verifast-proofs.sh

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
set -e -x
2+
3+
cd alloc
4+
cd collections
5+
cd linked_list.rs
6+
verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns verified/lib.rs
7+
refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs > /dev/null
8+
if ! diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs; then
9+
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."
10+
false
11+
fi
12+
cd ..
13+
cd ..
14+
cd ..

‎verifast-proofs/patch-verifast-proofs.sh

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
set -e -x
2+
3+
pushd alloc/collections/linked_list.rs
4+
diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > linked_list.diff || [ "$?" = 1 ]
5+
patch -p0 verified/linked_list.rs < linked_list.diff
6+
patch -p0 original/linked_list.rs < linked_list.diff
7+
rm linked_list.diff
8+
popd
9+
pushd alloc/collections/linked_list.rs-negative
10+
diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > linked_list.diff || [ "$?" = 1 ]
11+
patch -p0 verified/linked_list.rs < linked_list.diff
12+
patch -p0 original/linked_list.rs < linked_list.diff
13+
rm linked_list.diff
14+
popd

0 commit comments

Comments
 (0)