MPS: verify CN proofs in CI

We use a simple shell script to manage cn invocations

.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

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

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

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