From 4c2f1e2c104406475fde8cc16166bb57987cd7e5 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 6 Jun 2024 04:28:51 +0100 Subject: [PATCH 1/2] 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; From f2a395977cadbbf8d35ad19b2bf7fb2b4ef8628c Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 6 Jun 2024 05:09:37 +0100 Subject: [PATCH 2/2] CI: Split jobs for Linting and Build+KAT This way, if the lint check fails, the build+kat jobs still runs. Fixes #48 Signed-off-by: Hanno Becker --- .github/workflows/cbmc.yml | 36 ----------- .../workflows/{build_lint_kat.yml => ci.yml} | 64 +++++++++++++++++-- 2 files changed, 57 insertions(+), 43 deletions(-) delete mode 100644 .github/workflows/cbmc.yml rename .github/workflows/{build_lint_kat.yml => ci.yml} (57%) diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml deleted file mode 100644 index d68e005c7..000000000 --- a/.github/workflows/cbmc.yml +++ /dev/null @@ -1,36 +0,0 @@ -# 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; diff --git a/.github/workflows/build_lint_kat.yml b/.github/workflows/ci.yml similarity index 57% rename from .github/workflows/build_lint_kat.yml rename to .github/workflows/ci.yml index 44410e739..eb598d0b7 100644 --- a/.github/workflows/build_lint_kat.yml +++ b/.github/workflows/ci.yml @@ -1,13 +1,13 @@ # SPDX-License-Identifier: Apache-2.0 -name: Basic +name: CI on: push: branches: ["*"] pull_request: branches: ["main"] jobs: - build_lint_kat: + build_kat: strategy: matrix: system: [macos-latest, pqcp-arm64] @@ -27,11 +27,6 @@ jobs: - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "") - $(bash --version | grep -m1 "") EOF - - name: Lint - shell: nix develop .#ci -c bash -e {0} - run: | - echo "## Lint & Checks" >> $GITHUB_STEP_SUMMARY - lint - name: Build targets shell: nix develop .#ci -c bash -e {0} run: | @@ -59,3 +54,58 @@ jobs: $(checksum ./test/gen_NISTKAT768 21b4a1e1ea34a13c26a9da5eeb9325afb5ca11596ca6f3704c3f2637e3ea7524) $(checksum ./test/gen_NISTKAT1024 6471398b0a728ee1ef39e93bb89b526fbf59587a3662edadbcfc6c88a512cd71) EOF + lint: + strategy: + matrix: + system: [pqcp-arm64] + runs-on: ${{ matrix.system }} + steps: + - uses: actions/checkout@v4 + - name: Setup nix + uses: ./.github/actions/setup-nix + with: + script: | + cat >> $GITHUB_STEP_SUMMARY << EOF + ## Setup + Architecture: $(uname -m) + - $(uname -a) + - $(nix --version) + - $(astyle --version) + - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "") + - $(bash --version | grep -m1 "") + EOF + - name: Lint + shell: nix develop .#ci -c bash -e {0} + run: | + echo "## Lint & Checks" >> $GITHUB_STEP_SUMMARY + lint + cbmc: + strategy: + matrix: + system: [macos-latest] + 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: + 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;