Nicer automated snapshot of files from Verus + weekly auto-updates (#40)

This PR does a few things:

- Moves away from the older snapshot of vstd (that collapsed all of vstd
to a single file using
[inline-crate](https://github.com/jaybosamiya/inline-crate/)) to instead
hold each file individually
- Sets up a script that makes it easy to get the latest vstd from Verus
(and also a helper script to format it)
- Moves `syntax.rs` to be part of this automatically-get-this-from-Verus
setup
- Updates the snapshot tests to account for this move
- Sets up a CI job that runs once every night (at UTC 00:00) to see if
our snapshot has diverged from Verus's. If it has, then it opens up a PR
to call our attention to it

.github/workflows/snapshot-refresh.yml

@@ -0,0 +1,40 @@
+name: SnapshotRefresh
+
+on:
+  # Run either manually upon being dispatched by user
+  workflow_dispatch:
+  # Or on schedule
+  schedule:
+    - cron: '0 0 * * 1'  # Run every Monday night at midnight UTC
+
+jobs:
+  check-and-refresh-snapshot:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v4
+
+    - name: Run script and check for changes
+      id: nightly-check
+      run: |
+        cd examples/verus-snapshot
+        ./get_latest.sh
+        if git diff --exit-code; then
+          echo "No changes"
+          echo "changes=false" >> $GITHUB_OUTPUT
+        else
+          echo "Changes found"
+          echo "changes=true" >> $GITHUB_OUTPUT
+        fi
+
+    - name: Create Pull Request
+      if: ${{ steps.nightly-check.outputs.changes == 'true' }}
+      uses: peter-evans/create-pull-request@v6
+      with:
+        commit-message: "chore: update to latest Verus snapshot"
+        branch: verus-snapshot-update
+        delete-branch: true
+        title: "Verus snapshot update"
+        body: "Automated verus snapshot update by GitHub Actions."
+        base: main

Cargo.toml

@@ -36,6 +36,7 @@ tracing-subscriber = { version = "0.3.17" }
 [dev-dependencies]
 insta = { version = "1.30.0" }
 similar = { version = "2.2.1" }
+glob = "0.3.1"
 
 # Spend more time on initial compilation in exchange for faster runs
 [profile.dev.package.insta]

examples/verus-snapshot/.gitignore

@@ -0,0 +1,2 @@
+verus.zip
+verus-main

examples/verus-snapshot/get_latest.sh

@@ -0,0 +1,37 @@
+#! /bin/bash
+
+set -e
+set -o pipefail
+
+echo "[INFO] Cleaning any existing files"
+rm -rf verus.zip verus-main source
+
+echo "[INFO] Downloading latest version of Verus"
+wget --quiet -O verus.zip https://github.com/verus-lang/verus/archive/refs/heads/main.zip
+
+echo "[INFO] Unzipping Verus"
+unzip -q verus.zip
+
+MOVE_PATHS="source/rust_verify/example/syntax.rs source/vstd"
+
+echo "[INFO] Moving files"
+for path in $MOVE_PATHS; do
+    echo "       ... $path"
+    if [ -d "verus-main/$path" ]; then
+        # Directory, move all the .rs files, including those in subdirectories, creating the necessary directories
+        mkdir -p "$path"
+        find "verus-main/$path" -name '*.rs' -print0 | while IFS= read -r -d '' file; do
+            relative_path=$(realpath --relative-to="verus-main" "$file")
+            dirname=$(dirname "$relative_path")
+            mkdir -p "$path/$dirname"
+            mv "$file" "$path/$relative_path"
+        done
+    else
+        # File
+        mkdir -p "$(dirname "$path")"
+        mv "verus-main/$path" "$path"
+    fi
+done
+
+echo "[INFO] Cleaning up"
+rm -rf verus-main verus.zip

examples/verus-snapshot/run_verusfmt_on_all.sh

@@ -0,0 +1,20 @@
+#! /bin/bash
+
+set -e
+set -o pipefail
+
+if [ $# -eq 1 ]; then
+    if [ "$1" == "--check" ]; then
+        echo "Checking all files with verusfmt..."
+        cargo build --release
+        find . -name "*.rs" -exec cargo run --release --quiet -- --check {} \;
+    else
+        echo "Invalid argument: $1"
+    fi
+elif [ $# -eq 0 ]; then
+    echo "Running verusfmt on all files..."
+    cargo build --release
+    find . -name "*.rs" -print0 | xargs -0 cargo run --release --quiet --
+else
+    echo "Invalid number of arguments: $#"
+fi