From 4c2f1e2c104406475fde8cc16166bb57987cd7e5 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 6 Jun 2024 04:28:51 +0100 Subject: [PATCH] Split workflows for basic build+test and CBMC, add pqcp-arm64 runner Signed-off-by: Hanno Becker --- .../{build.yml => build_lint_kat.yml} | 22 ++++-------- .github/workflows/cbmc.yml | 36 +++++++++++++++++++ 2 files changed, 43 insertions(+), 15 deletions(-) rename .github/workflows/{build.yml => build_lint_kat.yml} (79%) create mode 100644 .github/workflows/cbmc.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build_lint_kat.yml similarity index 79% rename from .github/workflows/build.yml rename to .github/workflows/build_lint_kat.yml index 7336e97c0..44410e739 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build_lint_kat.yml @@ -1,18 +1,19 @@ # SPDX-License-Identifier: Apache-2.0 -name: Build +name: Basic on: push: branches: ["*"] pull_request: branches: ["main"] jobs: - build_test: - runs-on: macos-latest + build_lint_kat: + strategy: + matrix: + system: [macos-latest, pqcp-arm64] + runs-on: ${{ matrix.system }} steps: - uses: actions/checkout@v4 - - name: install native dependencies - run: brew install litani cbmc cbmc-viewer - name: Setup nix uses: ./.github/actions/setup-nix with: @@ -20,11 +21,9 @@ jobs: cat >> $GITHUB_STEP_SUMMARY << EOF ## Setup Architecture: $(uname -m) + - $(uname -a) - $(nix --version) - $(astyle --version) - - $(cbmc --version) - - $(litani --version) - - $(cadical --version) - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "") - $(bash --version | grep -m1 "") EOF @@ -60,10 +59,3 @@ 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/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml new file mode 100644 index 000000000..d68e005c7 --- /dev/null +++ b/.github/workflows/cbmc.yml @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: Apache-2.0 + +name: CBMC +on: + push: + branches: ["*"] + pull_request: + branches: ["main"] +jobs: + cbmc: + runs-on: macos-latest + steps: + - uses: actions/checkout@v4 + - name: install native dependencies + run: brew install litani cbmc cbmc-viewer + - name: Setup nix + uses: ./.github/actions/setup-nix + with: + script: | + cat >> $GITHUB_STEP_SUMMARY << EOF + ## Setup + Architecture: $(uname -m) + - $(nix --version) + - $(cbmc --version) + - $(litani --version) + - $(cadical --version) + - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "") + - $(bash --version | grep -m1 "") + 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;