Merge pull request #127 from GaloisInc/gus/update-cn-version

Update CN version
GaloisInc · Oct 28, 2024 · 0a113bf · 0a113bf
2 parents 87c4be6 + 7ae95e6
commit 0a113bf
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 10 deletions.
diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
@@ -21,10 +21,8 @@ jobs:
       - name: Prove MPS Components
         uses: addnab/docker-run-action@v3
         with:
-          image: ghcr.io/galoisinc/verse-opensut/cerberus:release
+          image: ghcr.io/rems-project/cerberus/cn@sha256:7f999b2d3126458f364bfd177edeef3a161f0b4fd306e942e07d81311f24b325
           registry: ghcr.io
-          username: ${{ github.actor }}
-          password: ${{ secrets.VERSE_OPENSUT_ACCESS_TOKEN }}
           options: -v ${{ github.workspace }}:/data
           # This action seems to override the docker image entrypoint, as a result
           # we need to run "eval `opam env`" first

diff --git a/components/mission_protection_system/src/cn.mk b/components/mission_protection_system/src/cn.mk
@@ -1,5 +1,5 @@
 CN_FLAGS=-I include --include=include/wars.h --magic-comment-char-dollar
-CN=cn $(CN_FLAGS)
+CN=cn verify $(CN_FLAGS)
 
 proofs: components/actuator.cn \
  components/instrumentation_common.cn \

diff --git a/components/mission_protection_system/src/include/models.acsl b/components/mission_protection_system/src/include/models.acsl
@@ -69,27 +69,27 @@
   @*/
 
 /*$
-function (bool) ActuateActuator(u8 input) {
+function (boolean) ActuateActuator(u8 input) {
   ((bw_and_uf(input, 1u8) != 0u8) || (bw_and_uf(input, 2u8) != 0u8))
 }
 
-function (bool) Coincidence_2_4(map<u64,u8> trips) {
+function (boolean) Coincidence_2_4(map<u64,u8> trips) {
   let a = trips[0u64] != 0u8;
   let b = trips[1u64] != 0u8;
   let c = trips[2u64] != 0u8;
   let d = trips[3u64] != 0u8;
   (a&&b) || ((a||b) && (c||d)) || (c&&d)
 }
 
-function (bool) Actuate_D0(map<u64,u8> tripsT, map<u64,u8> tripsP, map<u64,u8> tripsS, bool old) {
+function (boolean) Actuate_D0(map<u64,u8> tripsT, map<u64,u8> tripsP, map<u64,u8> tripsS, boolean old) {
   Coincidence_2_4(tripsT) || Coincidence_2_4(tripsP) || old
 }
 
-function (bool) Actuate_D1(map<u64,u8> tripsT, map<u64,u8> tripsP, map<u64,u8> tripsS, bool old) {
+function (boolean) Actuate_D1(map<u64,u8> tripsT, map<u64,u8> tripsP, map<u64,u8> tripsS, boolean old) {
   Coincidence_2_4(tripsS) || old
 }
 
-function (bool) Trip(map<u64,u32> vals, map<u64,u32> setpoints, u64 channel) {
+function (boolean) Trip(map<u64,u32> vals, map<u64,u32> setpoints, u64 channel) {
   channel == 2u64 ? (vals[channel] < setpoints[channel])
                   : (setpoints[channel] < vals[channel])
 }
@@ -101,7 +101,7 @@ function (u8) Generate_Sensor_Trips(map<u64,u32> vals, map<u64,u32> setpoints) {
   (t ? 1u8 : 0u8) + (p ? 2u8 : 0u8) + (s ? 4u8 : 0u8)
 }
 
-function (bool) Is_Ch_Tripped(u8 mode, bool tripped) {
+function (boolean) Is_Ch_Tripped(u8 mode, boolean tripped) {
   ((mode == 2u8) || ((mode == 1u8) && tripped))
 }
 $*/