From 6673bf03d43e3b68392607b84c0dfa186585ce65 Mon Sep 17 00:00:00 2001
From: Matthew Brecknell <matt@kry10.com>
Date: Sun, 13 Mar 2022 16:48:11 +1100
Subject: [PATCH] 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 | 36 +++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml
index b5424971e..7321502c9 100644
--- a/.github/workflows/proof-deploy.yml
+++ b/.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: