Skip to content

Commit e5f3c15

Browse files
btjbtj
committed
Improve the VeriFast scripts
- Fixes a bug in the Subtree Update action where a failed patch of the VeriFast proofs would cause an obscurely named, unhelpful commit to be added to the PR. - patch-verifast-proofs.sh now uses `git merge-file` instead of `patch` and can be called from anywhere - patch-verifast-proofs.sh now checks the updated proofs and rolls back the changes back if the proof fails - Each VeriFast proof can now use a different version of VeriFast
1 parent 3bb48f0 commit e5f3c15

File tree

15 files changed

+158
-67
lines changed

15 files changed

+158
-67
lines changed

‎.github/workflows/update-subtree.yml‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -214,18 +214,14 @@ jobs:
214214
215215
# Try to automatically patch the VeriFast proofs
216216
pushd verifast-proofs
217-
if bash ./patch-verifast-proofs.sh; then
217+
./patch-verifast-proofs.sh
218218
if ! git diff --quiet; then
219219
git -c user.name=gitbot -c user.email=git@bot \
220220
commit . -m "Update VeriFast proofs"
221221
else
222222
# The original files have not changed; no updates to the VeriFast proofs are necessary.
223223
true
224224
fi
225-
else
226-
# Patching the VeriFast proofs failed; requires manual intervention.
227-
true
228-
fi
229225
popd
230226
231227
- name: Create Pull Request without conflicts

‎.github/workflows/verifast-negative.yml‎

Lines changed: 1 addition & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -27,19 +27,5 @@ jobs:
2727
- name: Checkout Repository
2828
uses: actions/checkout@v4
2929

30-
- name: Install VeriFast
31-
run: |
32-
cd ~
33-
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
34-
# https://github.com/verifast/verifast/attestations/8998468
35-
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
36-
tar xf verifast-25.07-linux.tar.gz
37-
38-
- name: Install the Rust toolchain used by VeriFast
39-
run: rustup toolchain install nightly-2025-04-09
40-
4130
- name: Run VeriFast Verification
42-
run: |
43-
export PATH=~/verifast-25.07/bin:$PATH
44-
cd verifast-proofs
45-
bash check-verifast-proofs-negative.sh
31+
run: verifast-proofs/check-verifast-proofs-negative.sh

‎.github/workflows/verifast.yml‎

Lines changed: 1 addition & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -24,22 +24,8 @@ jobs:
2424
- name: Checkout Repository
2525
uses: actions/checkout@v4
2626

27-
- name: Install VeriFast
28-
run: |
29-
cd ~
30-
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
31-
# https://github.com/verifast/verifast/attestations/8998468
32-
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
33-
tar xf verifast-25.07-linux.tar.gz
34-
35-
- name: Install the Rust toolchain used by VeriFast
36-
run: rustup toolchain install nightly-2025-04-09
37-
3827
- name: Run VeriFast Verification
39-
run: |
40-
export PATH=~/verifast-25.07/bin:$PATH
41-
cd verifast-proofs
42-
bash check-verifast-proofs.sh
28+
run: verifast-proofs/check-verifast-proofs.sh
4329

4430
notify-btj:
4531
name: Notify @btj

‎verifast-proofs/alloc/collections/linked_list.rs-negative/update.sh‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
set -x -e
2+
3+
if ! git diff --quiet .; then
4+
echo "Working directory not clean. Please stash your changes and try again"
5+
false
6+
else
7+
UPSTREAM=../../../../library/alloc/src/collections/linked_list.rs
8+
git merge-file --diff3 verified/linked_list.rs original/linked_list.rs $UPSTREAM
9+
cp $UPSTREAM original/linked_list.rs
10+
fi

‎verifast-proofs/alloc/collections/linked_list.rs-negative/verify.sh‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
set -e -x
2+
3+
export VFVERSION=25.07
4+
5+
! verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns verified/lib.rs
6+
! refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs
7+
if ! diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs; then
8+
echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
9+
false
10+
fi

‎verifast-proofs/alloc/collections/linked_list.rs/update.sh‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
set -x -e
2+
3+
if ! git diff --quiet .; then
4+
echo "Working directory not clean. Please stash your changes and try again"
5+
false
6+
else
7+
UPSTREAM=../../../../library/alloc/src/collections/linked_list.rs
8+
git merge-file --diff3 verified/linked_list.rs original/linked_list.rs $UPSTREAM
9+
cp $UPSTREAM original/linked_list.rs
10+
fi

‎verifast-proofs/alloc/collections/linked_list.rs/verify.sh‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
set -e -x
2+
3+
export VFVERSION=25.07
4+
5+
verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
6+
refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs > /dev/null
7+
if ! diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs; then
8+
echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
9+
false
10+
fi

‎verifast-proofs/alloc/raw_vec/mod.rs/update.sh‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
set -x -e
2+
3+
if ! git diff --quiet .; then
4+
echo "Working directory not clean. Please stash your changes and try again"
5+
false
6+
else
7+
UPSTREAM=../../../../library/alloc/src/raw_vec/mod.rs
8+
git merge-file --diff3 with-directives/raw_vec.rs original/raw_vec.rs $UPSTREAM
9+
git merge-file --diff3 verified/raw_vec.rs original/raw_vec.rs $UPSTREAM
10+
cp $UPSTREAM original/raw_vec.rs
11+
fi

‎verifast-proofs/alloc/raw_vec/mod.rs/verify.sh‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
set -e -x
2+
3+
export VFVERSION=25.07
4+
5+
verifast -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
6+
refinement-checker with-directives/lib.rs verified/lib.rs > /dev/null
7+
refinement-checker --ignore-directives original/lib.rs with-directives/lib.rs > /dev/null
8+
if ! diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs; then
9+
echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
10+
false
11+
fi

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

100644100755
Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1+
#!/bin/bash
2+
13
set -e -x
24

5+
cd "$(dirname "$0")"
6+
export PATH=`pwd`:$PATH
7+
38
cd alloc
49
cd collections
510
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 chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
10-
false
11-
fi
11+
bash verify.sh
1212
cd ..
1313
cd ..
1414
cd ..

0 commit comments

Comments
 (0)