Update GitHub workflows for rt pull requests

.github/workflows/proof.yml

@@ -5,18 +5,14 @@
 name: Proof PR
 
 on:
-  push:
-    paths-ignore:
-      - '**.md'
-      - '**.txt'
-    branches:
-      - rt
   # this action needs access to secrets.
   # The actual test runs in a no-privilege VM, so it's Ok to run on untrusted PRs.
   pull_request_target:
     paths-ignore:
       - '**.md'
       - '**.txt'
+    branches-ignore:
+      - rt
   workflow_dispatch:
     inputs:
       NUM_DOMAINS:

.github/workflows/rt-proof.yml

@@ -0,0 +1,62 @@
+# Copyright 2021, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+name: MCS Proof PR
+
+on:
+  # this action needs access to secrets.
+  # The actual test runs in a no-privilege VM, so it's Ok to run on untrusted PRs.
+  pull_request_target:
+    paths-ignore:
+      - '**.md'
+      - '**.txt'
+    branches:
+      - rt
+  workflow_dispatch:
+    inputs:
+      NUM_DOMAINS:
+        description: 'Number of domains to test'
+        type: number
+        default: 16
+
+jobs:
+  proofs:
+    name: MCS
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        arch: [ARM, RISCV64]
+    # test only most recent push to PR:
+    concurrency:
+      group: l4v-${{ github.workflow }}-${{ github.event.number }}-idx-${{ strategy.job-index }}
+      cancel-in-progress: true
+    steps:
+    - name: Proofs
+      uses: seL4/ci-actions/aws-proofs@master
+      with:
+        L4V_ARCH: ${{ matrix.arch }}
+        NUM_DOMAINS: ${{ inputs.NUM_DOMAINS }}
+        L4V_FEATURES: MCS
+        manifest: mcs-devel.xml
+        skip_dups: true
+        session: '-x AutoCorresSEL4' # exclude large AutoCorresSEL4 session for PRs
+        token: ${{ secrets.READ_TOKEN }}
+        cache_bucket: ${{ secrets.CACHE_BUCKET }}
+      env:
+        AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
+        AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
+        AWS_SSH: ${{ secrets.AWS_SSH }}
+        GH_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
+    - name: Upload kernel builds
+      uses: actions/upload-artifact@v4
+      with:
+        name: kernel-builds-${{ matrix.arch }}
+        path: artifacts/kernel-builds
+        if-no-files-found: ignore
+    - name: Upload logs
+      uses: actions/upload-artifact@v4
+      with:
+        name: logs-${{ matrix.arch }}
+        path: logs.tar.xz