Improve the VeriFast scripts

.github/workflows/update-subtree.yml

@@ -214,16 +214,12 @@ jobs:
 
         # Try to automatically patch the VeriFast proofs
         pushd verifast-proofs
-        if bash ./patch-verifast-proofs.sh; then
-          if ! git diff --quiet; then
-            git -c user.name=gitbot -c user.email=git@bot \
-              commit . -m "Update VeriFast proofs"
-          else
-            # The original files have not changed; no updates to the VeriFast proofs are necessary.
-            true
-          fi
+        ./patch-verifast-proofs.sh
+        if ! git diff --quiet; then
+          git -c user.name=gitbot -c user.email=git@bot \
+            commit . -m "Update VeriFast proofs"
         else
-          # Patching the VeriFast proofs failed; requires manual intervention.
+          # The original files have not changed; no updates to the VeriFast proofs are necessary.
           true
         fi
         popd

.github/workflows/verifast-negative.yml

@@ -27,19 +27,5 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
 
-      - name: Install VeriFast
-        run: |
-          cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/8998468
-          echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b  verifast-25.07-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.07-linux.tar.gz
-
-      - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2025-04-09
-
       - name: Run VeriFast Verification
-        run: |
-          export PATH=~/verifast-25.07/bin:$PATH
-          cd verifast-proofs
-          bash check-verifast-proofs-negative.sh
+        run: verifast-proofs/check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

@@ -24,22 +24,8 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
 
-      - name: Install VeriFast
-        run: |
-          cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/8998468
-          echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b  verifast-25.07-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.07-linux.tar.gz
-
-      - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2025-04-09
-
       - name: Run VeriFast Verification
-        run: |
-          export PATH=~/verifast-25.07/bin:$PATH
-          cd verifast-proofs
-          bash check-verifast-proofs.sh
+        run: verifast-proofs/check-verifast-proofs.sh
 
   notify-btj:
     name: Notify @btj

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

@@ -0,0 +1,10 @@
+set -x -e
+
+if ! git diff --quiet .; then
+  echo "Working directory not clean. Please stash your changes and try again"
+  false
+else
+  UPSTREAM=../../../../library/alloc/src/collections/linked_list.rs
+  git merge-file --diff3 verified/linked_list.rs original/linked_list.rs $UPSTREAM
+  cp $UPSTREAM original/linked_list.rs
+fi

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

@@ -0,0 +1,10 @@
+set -e -x
+
+export VFVERSION=25.07
+
+! 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 chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
+  false
+fi

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

@@ -0,0 +1,10 @@
+set -x -e
+
+if ! git diff --quiet .; then
+  echo "Working directory not clean. Please stash your changes and try again"
+  false
+else
+  UPSTREAM=../../../../library/alloc/src/collections/linked_list.rs
+  git merge-file --diff3 verified/linked_list.rs original/linked_list.rs $UPSTREAM
+  cp $UPSTREAM original/linked_list.rs
+fi

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

@@ -0,0 +1,10 @@
+set -e -x
+
+export VFVERSION=25.07
+
+verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns -ignore_unwind_paths -allow_assume 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 chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
+  false
+fi

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

@@ -0,0 +1,11 @@
+set -x -e
+
+if ! git diff --quiet .; then
+  echo "Working directory not clean. Please stash your changes and try again"
+  false
+else
+  UPSTREAM=../../../../library/alloc/src/raw_vec/mod.rs
+  git merge-file --diff3 with-directives/raw_vec.rs original/raw_vec.rs $UPSTREAM
+  git merge-file --diff3 verified/raw_vec.rs original/raw_vec.rs $UPSTREAM
+  cp $UPSTREAM original/raw_vec.rs
+fi

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

@@ -0,0 +1,11 @@
+set -e -x
+
+export VFVERSION=25.07
+
+verifast -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
+refinement-checker with-directives/lib.rs verified/lib.rs > /dev/null
+refinement-checker --ignore-directives original/lib.rs with-directives/lib.rs > /dev/null
+if ! diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs; then
+  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."
+  false
+fi

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

@@ -1,14 +1,14 @@
+#!/bin/bash
+
 set -e -x
 
+cd "$(dirname "$0")"
+export PATH=`pwd`:$PATH
+
 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 chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
-        false
-      fi
+      bash verify.sh
     cd ..
   cd ..
 cd ..

verifast-proofs/check-verifast-proofs.sh

@@ -1,25 +1,20 @@
+#!/bin/bash
+
 set -e -x
 
+cd "$(dirname "$0")"
+
+export PATH=`pwd`:$PATH
+
 cd alloc
   cd collections
     cd linked_list.rs
-      verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns -ignore_unwind_paths -allow_assume 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 chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
-        false
-      fi
+      bash verify.sh
     cd ..
   cd ..
   cd raw_vec
     cd mod.rs
-      verifast -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
-      refinement-checker with-directives/lib.rs verified/lib.rs > /dev/null
-      refinement-checker --ignore-directives original/lib.rs with-directives/lib.rs > /dev/null
-      if ! diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs; then
-        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."
-        false
-      fi
+      bash verify.sh
     cd ..
   cd ..
 cd ..

verifast-proofs/patch-verifast-proofs.sh

@@ -1,21 +1,24 @@
+#!/bin/bash
+
 set -e -x
 
+cd "$(dirname "$0")"
+export PATH=`pwd`:$PATH
+
+patch_proof() {
+  if ! git diff --quiet .; then
+    echo "Directory not clean. Please stash changes and try again"
+  else
+    bash update.sh && bash verify.sh || git restore .
+  fi
+}
+
 pushd alloc/collections/linked_list.rs
-  diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > /tmp/linked_list.diff || [ "$?" = 1 ]
-  patch -p0 verified/linked_list.rs < /tmp/linked_list.diff
-  patch -p0 original/linked_list.rs < /tmp/linked_list.diff
-  rm /tmp/linked_list.diff
+  patch_proof
 popd
 pushd alloc/collections/linked_list.rs-negative
-  diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > /tmp/linked_list.diff || [ "$?" = 1 ]
-  patch -p0 verified/linked_list.rs < /tmp/linked_list.diff
-  patch -p0 original/linked_list.rs < /tmp/linked_list.diff
-  rm /tmp/linked_list.diff
+  patch_proof
 popd
 pushd alloc/raw_vec/mod.rs
-  diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs > /tmp/raw_vec.diff || [ "$?" = 1 ]
-  patch -p0 verified/raw_vec.rs < /tmp/raw_vec.diff
-  patch -p0 with-directives/raw_vec.rs < /tmp/raw_vec.diff
-  patch -p0 original/raw_vec.rs < /tmp/raw_vec.diff
-  rm /tmp/raw_vec.diff
+  patch_proof
 popd

verifast-proofs/refinement-checker

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+set -e -x
+. "$(dirname "$0")/setup-verifast-home"
+"$VERIFAST_HOME/bin/refinement-checker" "$@"

verifast-proofs/setup-verifast-home

@@ -0,0 +1,53 @@
+set -e -x
+
+: "${VFTOOLCHAINS=$HOME/.verifast/toolchains}"
+: "${VERIFAST_HOME=$VFTOOLCHAINS/verifast-$VFVERSION}"
+
+if [[ ! -d "$VERIFAST_HOME" ]]; then
+
+  if [[ -z $VFPLATFORM ]]; then
+    if [[ "$(uname)" == "Darwin" ]]; then
+      if [[ "$(uname -m)" == "arm64" ]]; then
+        : "${VFPLATFORM=macos-aarch}"
+      else
+        : "${VFPLATFORM=macos}"
+      fi
+    else
+      : "${VFPLATFORM=linux}"
+    fi
+  fi
+
+  case "$VFVERSION,$VFPLATFORM" in
+    25.07,macos-aarch)
+      # https://github.com/verifast/verifast/attestations/8998438
+      VFHASH=6129fe538fb0b47ddf57e223dd628d991c74d9c835c991dd65871d5dc56c6d3f
+      RUST_VERSION=nightly-2025-04-09
+      ;;
+    25.07,linux)
+      # https://github.com/verifast/verifast/attestations/8998468
+      VFHASH=48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b
+      RUST_VERSION=nightly-2025-04-09
+      ;;
+    *)
+      echo 'Unknown VeriFast version "'"$VFVERSION"'". Please set VFVERSION to a support version'
+      false
+      ;;
+  esac
+
+  if ! rustup toolchain list | grep $RUST_VERSION; then
+    rustup toolchain install $RUST_VERSION
+  fi
+
+  VFASSET=verifast-$VFVERSION-$VFPLATFORM.tar.gz
+  pushd "${TMPDIR:-/tmp}"
+    if [[ ! -d verifast-$VFVERSION ]]; then
+      if [[ ! -e $VFASSET ]]; then
+        curl -OL https://github.com/verifast/verifast/releases/download/$VFVERSION/$VFASSET
+      fi
+      echo "$VFHASH  $VFASSET" | shasum -a 256 -c
+      tar xf $VFASSET
+    fi
+    mkdir -p "$VFTOOLCHAINS"
+    mv verifast-$VFVERSION "$VFTOOLCHAINS"
+  popd
+fi

verifast-proofs/verifast

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+set -e -x
+. "$(dirname "$0")/setup-verifast-home"
+"$VERIFAST_HOME/bin/verifast" "$@"