update-subtree action: patch VeriFast proofs (#371)

When preparing a merge subtree PR, try to patch the VeriFast proofs.

Also tweaks `patch-verifast-proofs.sh` to ensure that no temporary files
are left behind inside the working directory, even when the script fails
mid-way.

Note: I did not test this.

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 <[email protected]>

Author: btj

.github/workflows/update-subtree.yml

@@ -194,6 +194,20 @@ jobs:
         sed -i "s/commit = .*/commit = \"${KANI_COMMIT_HASH}\"/" tool_config/kani-version.toml
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
+        
+        # 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.
+          fi
+        else
+          # Patching the VeriFast proofs failed; requires manual intervention.
+        fi
+        popd
 
     - name: Create Pull Request without conflicts
       if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}

verifast-proofs/patch-verifast-proofs.sh

@@ -1,14 +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
+  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
 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
+  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
 popd