From ecca3a2ce93c4afb656643dc2717e1fe6ddebd3a Mon Sep 17 00:00:00 2001
From: Gus O'Hanley <guso@galois.com>
Date: Wed, 29 May 2024 12:28:04 -0500
Subject: [PATCH] MPS: verify CN proofs in CI

We use a simple shell script to manage cn invocations
---
 .github/workflows/cn.yml                         | 16 +---------------
 .../mission_protection_system/run_cn_proofs.sh   | 14 ++++++++------
 .../mission_protection_system/src/common.c       | 12 ------------
 .../src/include/common.h                         | 14 ++++++++++----
 4 files changed, 19 insertions(+), 37 deletions(-)

diff --git a/.github/workflows/cn.yml b/.github/workflows/cn.yml
index 2e0a4071..352e9fd6 100644
--- a/.github/workflows/cn.yml
+++ b/.github/workflows/cn.yml
@@ -30,20 +30,6 @@ jobs:
           # Use `>` so newlines will be replaced with spaces
           run: >
             eval `opam env` &&
-            cn -I components/mission_protection_system/src/include
-            --include=components/mission_protection_system/src/include/wars.h
-            components/mission_protection_system/src/components/actuator.c
-          # Unclear if `continue-on-error` actually works
-          # continue-on-error: true
-      - name: Prove Instrumentation Unit
-        uses: addnab/docker-run-action@v3
-        with:
-          image: podhrmic/cerberus:release
-          options: -v ${{ github.workspace }}:/data
-          run: >
-            eval `opam env` &&
-            cn -I components/mission_protection_system/src/include
-            --include=components/mission_protection_system/src/include/wars.h
-            components/mission_protection_system/src/components/instrumentation.c
+            ./components/mission_protection_system/run_cn_proofs.sh
           # Unclear if `continue-on-error` actually works
           # continue-on-error: true
diff --git a/components/mission_protection_system/run_cn_proofs.sh b/components/mission_protection_system/run_cn_proofs.sh
index fcbe8647..8dbc4409 100755
--- a/components/mission_protection_system/run_cn_proofs.sh
+++ b/components/mission_protection_system/run_cn_proofs.sh
@@ -1,11 +1,13 @@
 #!/usr/bin/env bash
 
-cd src/components || exit 1
+set -euo
+cd components/mission_protection_system || exit 1
 
-files=( actuator.c
-instrumentation_common.c
-actuation_unit.c
-instrumentation.c
+files=(
+src/components/actuator.c
 )
 
-cn -I ../include --include=../include/wars.h "${files[@]}"
+for file in "${files[@]}"
+do
+cn -I src/include --include=src/include/wars.h  --batch "${file}"
+done
diff --git a/components/mission_protection_system/src/common.c b/components/mission_protection_system/src/common.c
index 55d090df..b789c991 100644
--- a/components/mission_protection_system/src/common.c
+++ b/components/mission_protection_system/src/common.c
@@ -35,18 +35,6 @@ struct core_state core = {0};
 struct instrumentation_state instrumentation[4];
 struct actuation_logic actuation_logic[2];
 
-/*@ function (u8) NINSTR() @*/
-uint8_t c_NINSTR() /*@ cn_function NINSTR; @*/ { return NINSTR; }
-
-/*@ function (u8) NTRIP() @*/
-uint8_t c_NTRIP() /*@ cn_function NTRIP; @*/ { return NTRIP; }
-
-/*@ function (u8) NVOTE_LOGIC() @*/
-uint8_t c_NVOTE_LOGIC() /*@ cn_function NVOTE_LOGIC; @*/ { return NVOTE_LOGIC; }
-
-/*@ function (u8) NDEV() @*/
-uint8_t c_NDEV() /*@ cn_function NDEV; @*/ { return NDEV; }
-
 // channel -> sensor # -> val
 uint32_t sensors[2][2];
 // channel -> sensor # -> demux output # -> val
diff --git a/components/mission_protection_system/src/include/common.h b/components/mission_protection_system/src/include/common.h
index 197341dc..c0a90ddc 100644
--- a/components/mission_protection_system/src/include/common.h
+++ b/components/mission_protection_system/src/include/common.h
@@ -26,7 +26,10 @@
 // Instrumentation
 // Trip modes:
 #define NINSTR 4
-uint8_t c_NINSTR();
+// These wrapper functions need their definitions exposed to CN, but this causes
+// multiple definition errors in the linker because this is a header file.
+/*@ function (u8) NINSTR() @*/
+uint8_t c_NINSTR() /*@ cn_function NINSTR; @*/ { return NINSTR; }
 #define NMODES 3
 #define BYPASS 0
 #define OPERATE 1
@@ -39,16 +42,19 @@ uint8_t c_NINSTR();
 
 // Channel/Trip signal IDs
 #define NTRIP 3
-uint8_t c_NTRIP();
+/*@ function (u8) NTRIP() @*/
+uint8_t c_NTRIP() /*@ cn_function NTRIP; @*/ { return NTRIP; }
 #define T 0
 #define P 1
 #define S 2
 
 // Actuation
 #define NVOTE_LOGIC 2
-uint8_t c_NVOTE_LOGIC();
+/*@ function (u8) NVOTE_LOGIC() @*/
+uint8_t c_NVOTE_LOGIC() /*@ cn_function NVOTE_LOGIC; @*/ { return NVOTE_LOGIC; }
 #define NDEV 2
-uint8_t c_NDEV();
+/*@ function (u8) NDEV() @*/
+uint8_t c_NDEV() /*@ cn_function NDEV; @*/ { return NDEV; }
 
 // Core
 // Command Types