ci proof-deploy: add MCS C graph export

Add a second matrix job that runs SimplExportAndRefine for MCS C kernel
configurations that support it (currently ARM and RISCV64).

Note that this uses the master branch of l4v to generate the CSpec, and
to run SimplExportAndRefine, not the rt branch. This works because the
rt branch does not yet connect to the CSpec, and there are no meaningful
differences between rt and master in CSpec or SimplExportAndRefine. For
now, this simplifies workflows for binary verification. But when MCS
proofs connect to the CSpec, this will need to be refactored to use the
rt branch.

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

.github/workflows/proof-deploy.yml

@@ -60,10 +60,44 @@ jobs:
         name: logs-${{ matrix.arch }}
         path: logs.tar.xz
 
+  mcs-export:
+    name: MCS
+    needs: code
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        arch: [ARM, RISCV64]
+    # test only most recent push:
+    concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }}-mcs
+    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@v2
+      with:
+        name: c-graph-lang-${{ matrix.arch }}-MCS
+        path: artifacts/CFunctions.txt.xz
+        if-no-files-found: ignore
+    - name: Upload logs
+      uses: actions/upload-artifact@v2
+      with:
+        name: logs-${{ matrix.arch }}-MCS
+        path: logs.tar.xz
+
   deploy:
     name: Deploy manifest
     runs-on: ubuntu-latest
-    needs: [code, proofs]
+    needs: [code, proofs, mcs-export]
     steps:
     - uses: seL4/ci-actions/l4v-deploy@master
       with: