Add CBMC to CI

Signed-off-by: Hanno Becker <[email protected]>
pq-code-package · May 31, 2024 · 7da476d · 7da476d
1 parent 1a3a2bb
commit 7da476d
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -11,6 +11,8 @@ jobs:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@v4
+      - name: install native dependencies
+        run: brew install litani
       - name: Setup nix
         uses: ./.github/actions/setup-nix
         with:
@@ -20,6 +22,9 @@ jobs:
               Architecture: $(uname -m)
               - $(nix --version)
               - $(astyle --version)
+              - $(cbmc --version)
+              - $(litani --version)
+              - $(cadical --version)
               - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "")
               - $(bash --version | grep -m1 "")
             EOF
@@ -55,3 +60,10 @@ jobs:
             $(checksum ./test/gen_NISTKAT768  21b4a1e1ea34a13c26a9da5eeb9325afb5ca11596ca6f3704c3f2637e3ea7524)
             $(checksum ./test/gen_NISTKAT1024 6471398b0a728ee1ef39e93bb89b526fbf59587a3662edadbcfc6c88a512cd71)
           EOF
+      - name: Run CBMC proofs
+        shell: nix develop .#ci -c bash -e {0}
+        run: |
+          cd cbmc/proofs;
+          KYBER_K=2 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=3 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=4 ./run-cbmc-proofs.py --summarize;
diff --git a/flake.nix b/flake.nix
@@ -23,6 +23,8 @@
               inherit (pkgs)
                 # formatter & linters
                 astyle# 3.4.10
+                cbmc
+                cadical
                 nixpkgs-fmt
                 shfmt;
             }