From d68a755b14d4e9927a99b58033a4139d8f2a893d Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Fri, 31 May 2024 21:10:03 +0100 Subject: [PATCH] Add CBMC to CI Signed-off-by: Hanno Becker --- .github/workflows/build.yml | 8 ++++++++ flake.nix | 1 + 2 files changed, 9 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index c3fb38184..133e632e8 100644 --- 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 index 3e6928982..dff7fd10f 100644 --- a/flake.nix +++ b/flake.nix @@ -23,6 +23,7 @@ inherit (pkgs) # formatter & linters astyle# 3.4.10 + cbmc nixpkgs-fmt shfmt; }