ci: add mcs-export workflow

This adds adds an mcs-export workflow, as a further step towards solving
issue #497. This replaces the mcs-export matrix job that was removed
from the proof-deploy workflow in #498.

This workflow has some similarities to the proof-deploy workflow:
- Both workflows check out a manifest, run some proofs, and trigger
  a binary verification workflow.
- Both workflows are triggered by an update to an l4v branch.
- Both workflows can be triggered by manual updates to the development
  verification-manifest, but not automatic updates due to a successful
  preprocess test.

The differences are:
- proof-deploy updates the default verification-manifest, whereas the
  mcs-export workflow does not.
- proof-deploy uses l4v master, whereas mcs-export uses the rt branch.

When MCS CRefine proofs are sufficiently advanced, the proof-deploy
workflow will need to be updated to check MCS proofs before updating the
default verification-manifest. At that point, this workflow could be
reintegrated into the proof-deploy workflow.

Signed-off-by: Matthew Brecknell <matt@kry10.com>

.github/workflows/mcs-export.yml

@@ -0,0 +1,129 @@
+# Copyright 2021 Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# MCS SimplExportAndRefine for binary verification.
+#
+# The first step in preparing inputs to binary verification is to run
+# SimplExportAndRefine. This workflow performs SimplExportAndRefine for
+# MCS configurations, and then triggers a downstream workflow to run the
+# next step (decompilation). Non-MCS configurations are covered by the
+# proof-deploy workflow.
+#
+# This workflow is similar to proof-deploy, except that this workflow is
+# not involved in deploying new verification-manifest versions. Later,
+# when MCS CRefine proofs are sufficiently advanced, proof-deploy will
+# need to check proofs in both rt and master branches before deploying a
+# new manifest version. At that point, this workflow should be
+# reintegrated into proof-deploy.
+#
+# This workflow is triggered by pushes to the l4v rt branch, just as
+# proof-deploy is triggered by pushes to the l4v master branch. Both
+# workflows are also triggered on manual updates to the verification
+# development manifest (devel.xml). This means that binary verification
+# will be initiated for any proof-visible change to the seL4 code, as
+# well as changes to the proofs. This might not include all changes to
+# the C code that might affect binary verification, but it should be
+# more than enough to keep the servers busy.
+
+name: MCS SimplExport
+
+on:
+  push:
+    branches:
+      - rt
+  repository_dispatch:
+    types:
+      - manifest-update
+
+jobs:
+  code:
+    name: Freeze Code
+    runs-on: ubuntu-latest
+    outputs:
+      xml: ${{ steps.repo.outputs.xml }}
+    steps:
+    - id: repo
+      uses: seL4/ci-actions/repo-checkout@master
+      with:
+        manifest_repo: verification-manifest
+        manifest: devel.xml
+        # Not a raw object ref, but should still work as expected.
+        # This effectively gives us an MCS manifest, but with an
+        # up-to-date seL4.
+        sha: rt
+
+  mcs-export:
+    name: MCS SimplExport
+    needs: code
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        arch: [ARM, RISCV64]
+    # test only most recent push:
+    concurrency: l4v-mcs-export-${{ github.ref }}-${{ strategy.job-index }}
+    steps:
+    - name: SimplExport
+      uses: seL4/ci-actions/aws-proofs@master
+      with:
+        L4V_ARCH: ${{ matrix.arch }}
+        L4V_FEATURES: MCS
+        xml: ${{ needs.code.outputs.xml }}
+        session: SimplExportAndRefine
+      env:
+        AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
+        AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
+        AWS_SSH: ${{ secrets.AWS_SSH }}
+    - name: Upload C graph-lang
+      uses: actions/upload-artifact@v3
+      with:
+        name: c-graph-lang
+        path: artifacts/simpl-export
+        if-no-files-found: ignore
+    - name: Upload logs
+      uses: actions/upload-artifact@v3
+      with:
+        name: logs-${{ matrix.arch }}-MCS
+        path: logs.tar.xz
+
+  binary-verification:
+    name: Trigger binary verification
+    runs-on: ubuntu-latest
+    needs: [code, proofs]
+    steps:
+    # download-artifact doesn't have an option to ignore missing artifacts,
+    # so we download them all to test if c-graph-lang exists.
+    - name: Fetch artifacts
+      uses: actions/download-artifact@v3
+      with:
+        path: artifacts
+    - name: Check for C graph-lang artifacts
+      id: enabled
+      env:
+        MANIFEST: ${{ needs.code.outputs.xml }}
+      run: |
+        # Check if there are any C graph-lang artifacts
+        if [ -e artifacts/c-graph-lang ]; then
+          echo "C graph-lang artifacts found, will trigger binary verification"
+          echo -n "${MANIFEST}" > verification-manifest.xml
+          echo "::set-output name=enabled::true"
+        else
+          echo "No C graph-lang artifacts found, will not trigger binary verification"
+        fi
+    - name: Upload manifest
+      if: steps.enabled.outputs.enabled
+      uses: actions/upload-artifact@v3
+      with:
+        name: manifest
+        path: verification-manifest.xml
+    - name: Trigger binary verification
+      if: steps.enabled.outputs.enabled
+      uses: peter-evans/repository-dispatch@v1
+      with:
+        token: ${{ secrets.PRIV_REPO_TOKEN }}
+        repository: ${{ github.repository }}
+        event-type: binary-verification
+        # binary-verification uses the run_id to retrieve this workflow's artifacts.
+        client-payload: |
+          { "repo": "${{ github.repository }}", "run_id": "${{ github.run_id }}" }