Skip to content

Sync the VeriFast proofs and provide guidance on same #313

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

Merged
merged 3 commits into from
Apr 8, 2025
Merged

Sync the VeriFast proofs and provide guidance on same #313

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f7f8c5d
Provide guidance on out-of-date VeriFast proofs
btj Apr 3, 2025
3a6157e
Sync the VeriFast proofs
btj Apr 3, 2025
a1e8d3d
Notify @btj on failure
btj Apr 4, 2025
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
2 changes: 1 addition & 1 deletion .github/workflows/verifast-negative.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion .github/workflows/verifast.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 3 additions & 0 deletions verifast-proofs/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 6 additions & 12 deletions verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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()
}
Expand Down
18 changes: 6 additions & 12 deletions verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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()
}
Expand Down
18 changes: 6 additions & 12 deletions verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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()
}
Expand Down
18 changes: 6 additions & 12 deletions verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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()
}
Expand Down
9 changes: 0 additions & 9 deletions verifast-proofs/check-verifast-proofs-negative.mysh
View file
Open in desktop

This file was deleted.

14 changes: 14 additions & 0 deletions verifast-proofs/check-verifast-proofs-negative.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 ..
9 changes: 0 additions & 9 deletions verifast-proofs/check-verifast-proofs.mysh
View file
Open in desktop

This file was deleted.

14 changes: 14 additions & 0 deletions verifast-proofs/check-verifast-proofs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 ..
14 changes: 14 additions & 0 deletions verifast-proofs/patch-verifast-proofs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading