Add CBMC to CI

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

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -20,6 +20,7 @@ jobs:
               Architecture: $(uname -m)
               - $(nix --version)
               - $(astyle --version)
+              - $(cbmc --version)
               - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "")
               - $(bash --version | grep -m1 "")
             EOF
@@ -55,3 +56,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,7 @@
               inherit (pkgs)
                 # formatter & linters
                 astyle# 3.4.10
+                cbmc
                 nixpkgs-fmt
                 shfmt;
             }