Automate subtree update

There should not be a need for manual processes for the first stage of
the subtree update, i.e., updating our subtree/library branch.

Merge conflicts (which might require a human to intervene) will only
happen once attempting to merge from subtree/library back into main.
Automation for this stage has been added, will create a PR separate from
the above one, and will likely require manual intervention.

.github/workflows/update-subtree.yml

@@ -0,0 +1,147 @@
+name: Subtree Update
+
+on:
+  schedule:
+    - cron: '0 14 * * *'  # Run at 14:00 UTC every day
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  update-subtree-library:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout Repository
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        path: verify-rust-std
+        submodules: true
+
+    - name: Checkout Kani
+      uses: actions/checkout@v4
+      with:
+        repository: model-checking/kani
+        path: kani-tmp
+
+    - name: Checkout Rust
+      uses: actions/checkout@v4
+      with:
+        repository: rust-lang/rust
+        fetch-depth: 0
+        path: rust-tmp
+
+    - name: Checkout git-filter-repo
+      uses: actions/checkout@v4
+      with:
+        repository: newren/git-filter-repo
+        path: git-filter-repo
+
+    - name: Fetch Kani toolchain version
+      run: |
+        cd kani-tmp
+        TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' rust-toolchain.toml)
+        COMMIT_HASH=$(curl https://static.rust-lang.org/dist/$TOOLCHAIN_DATE/channel-rust-nightly-git-commit-hash.txt)
+        if [ -z "$COMMIT_HASH" ]; then
+          echo "Could not find commit hash on static.rust-lang.org"
+          exit 1
+        fi
+        echo "Kani toolchain date: ${TOOLCHAIN_DATE}"
+        echo "TOOLCHAIN_DATE=${TOOLCHAIN_DATE}" >> $GITHUB_ENV
+        echo "Kani toolchain hash: ${COMMIT_HASH}"
+        echo "COMMIT_HASH=${COMMIT_HASH}" >> $GITHUB_ENV
+
+    - name: Update subtree/library locally
+      run: |
+        cd rust-tmp
+
+        # Ensure "upstream/master" branch contains the target commit
+        if ! git show ${COMMIT_HASH} --oneline --no-patch; then
+          echo "Rust commit ${COMMIT_HASH} cannot be found."
+          exit 1
+        fi
+
+        git checkout ${COMMIT_HASH}
+        ../git-filter-repo/git-filter-repo --subdirectory-filter library --force
+        git checkout -b subtree/library
+
+        cd ../verify-rust-std
+        git remote add rust-filtered ../rust-tmp/
+        git fetch rust-filtered
+        git checkout -b subtree/library rust-filtered/subtree/library
+        SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
+        UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
+        UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
+        if [ "${UPSTREAM_HEAD}" = "${UPSTREAM_FROM}" ]; then
+          echo "Nothing to do, ${UPSTREAM_FROM} matches ${UPSTREAM_HEAD} (${SUBTREE_HEAD_MSG})"
+          echo "MERGE_CONFLICTS=noop" >> $GITHUB_ENV
+        else
+          git branch --set-upstream-to=origin/subtree/library
+          git -c user.name=gitbot -c user.email=git@bot rebase
+          echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
+        fi
+
+    - name: Create Pull Request
+      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: 'Update subtree/library'
+        body: |
+          This is an automated PR to update the subtree/library branch to the changes
+          up to and including ${{ env.COMMIT_HASH }} of ${{ env.TOOLCHAIN_DATE }}.
+        branch: update-subtree/library
+        delete-branch: true
+        base: subtree/library
+        path: verify-rust-std
+
+    - name: Merge subtree/library changes
+      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+      run: |
+        cd verify-rust-std
+        git checkout main
+
+        # This command may fail, which will require human intervention.
+        if ! git \
+            -c user.name=gitbot -c user.email=git@bot \
+            subtree merge --prefix=library update-subtree/library --squash; then
+          echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
+          git -c user.name=gitbot -c user.email=git@bot commit -a -m "Merge from $COMMIT_HASH with conflicts"
+        else
+          echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
+        fi
+
+        sed -i "s/^channel = \"nightly-.*\"/channel = \"${TOOLCHAIN_DATE}\"/" rust-toolchain.toml
+        git -c user.name=gitbot -c user.email=git@bot \
+          commit -m "Update toolchain to ${TOOLCHAIN_DATE}" rust-toolchain.toml
+
+    - name: Create Pull Request without conflicts
+      if: ${{ env.MERGE_CONFLICTS == 'no' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: 'Merge subtree update'
+        body: |
+          This is an automated PR to merge library subtree updates
+          up to and including ${{ env.COMMIT_HASH }} of ${{ env.TOOLCHAIN_DATE }}
+          into main. This is a clean merge, no conflicts were detected.
+        branch: sync-${{ env.TOOLCHAIN_DATE }}
+        delete-branch: true
+        base: main
+        path: verify-rust-std
+
+    - name: Create Pull Request with conflicts
+      if: ${{ env.MERGE_CONFLICTS == 'yes' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: 'Merge subtree update'
+        body: |
+          This is an automated PR to merge library subtree updates
+          up to and including ${{ env.COMMIT_HASH }} of ${{ env.TOOLCHAIN_DATE }}
+          into main. `git merge` resulted in conflicts, which require manual resolution.
+          Files were commited with merge conflict markers.
+        branch: sync-${{ env.TOOLCHAIN_DATE }}
+        delete-branch: true
+        base: main
+        path: verify-rust-std