Skip to content

Commit dd1e82c

Browse files
btjtautschnig
btj
and
tautschnig
authored
Improve the VeriFast scripts (#507)
- 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 if the proof fails - Move the VeriFast invocation for checking a particular proof into a `verify.sh` script in that proof's directory. Makes the proof easier to audit. - Each VeriFast proof can now use a different version of VeriFast By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
1 parent ac622da commit dd1e82c

File tree

15 files changed

+177
-71
lines changed

15 files changed

+177
-71
lines changed

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

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -214,16 +214,12 @@ jobs:
214214
215215
# Try to automatically patch the VeriFast proofs
216216
pushd verifast-proofs
217-
if bash ./patch-verifast-proofs.sh; then
218-
if ! git diff --quiet; then
219-
git -c user.name=gitbot -c user.email=git@bot \
220-
commit . -m "Update VeriFast proofs"
221-
else
222-
# The original files have not changed; no updates to the VeriFast proofs are necessary.
223-
true
224-
fi
217+
./patch-verifast-proofs.sh
218+
if ! git diff --quiet; then
219+
git -c user.name=gitbot -c user.email=git@bot \
220+
commit . -m "Update VeriFast proofs"
225221
else
226-
# Patching the VeriFast proofs failed; requires manual intervention.
222+
# The original files have not changed; no updates to the VeriFast proofs are necessary.
227223
true
228224
fi
229225
popd

‎.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.11/verifast-25.11-linux.tar.gz
34-
# https://github.com/verifast/verifast/attestations/14103492
35-
echo '990c3cadba7cfc9ef9c19d5f1ff039fd746155164fe4a5ec365c625182400f3e verifast-25.11-linux.tar.gz' | shasum -a 256 -c
36-
tar xf verifast-25.11-linux.tar.gz
37-
38-
- name: Install the Rust toolchain used by VeriFast
39-
run: rustup toolchain install nightly-2025-10-09
40-
4130
- name: Run VeriFast Verification
42-
run: |
43-
export PATH=~/verifast-25.11/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.11/verifast-25.11-linux.tar.gz
31-
# https://github.com/verifast/verifast/attestations/14103492
32-
echo '990c3cadba7cfc9ef9c19d5f1ff039fd746155164fe4a5ec365c625182400f3e verifast-25.11-linux.tar.gz' | shasum -a 256 -c
33-
tar xf verifast-25.11-linux.tar.gz
34-
35-
- name: Install the Rust toolchain used by VeriFast
36-
run: rustup toolchain install nightly-2025-10-09
37-
3827
- name: Run VeriFast Verification
39-
run: |
40-
export PATH=~/verifast-25.11/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.11
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.11
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.11
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)