Add CBMC as dependency to nix #35
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: Apache-2.0 | |
| name: CI | |
| on: | |
| push: | |
| branches: ["*"] | |
| pull_request: | |
| branches: ["main"] | |
| jobs: | |
| build_kat: | |
| strategy: | |
| matrix: | |
| system: [macos-latest, 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: Build targets | |
| shell: nix develop .#ci -c bash -e {0} | |
| run: | | |
| make mlkem | |
| ./test/test_kyber512 | |
| ./test/test_kyber768 | |
| ./test/test_kyber1024 | |
| - name: Compare gen_KAT with known hash | |
| shell: nix develop .#ci -c bash -e {0} | |
| run: | | |
| make kat; | |
| cat >> $GITHUB_STEP_SUMMARY << EOF | |
| ## KAT tests | |
| $(checksum ./test/gen_KAT512 ec4ac397e595ac7457cb7d8830921faf3290898a10d7dd3864aab89ea61fe9a3) | |
| $(checksum ./test/gen_KAT768 9a0826ad3c5232dfd3b21bc4801408655c565a491b760f509b2ee2cd7180babe) | |
| $(checksum ./test/gen_KAT1024 6dafb867599b750a6a831b03e494cf41dea748c78a0e275e7b268bbb893cf37d) | |
| EOF | |
| - name: Compare gen_NISTKAT with known hash | |
| shell: nix develop .#ci -c bash -e {0} | |
| run: | | |
| make nistkat; | |
| cat >> $GITHUB_STEP_SUMMARY << EOF | |
| ## NISTKAT tests | |
| $(checksum ./test/gen_NISTKAT512 4b88ac7643ff60209af1175e025f354272e88df827a0ce1c056e403629b88e04) | |
| $(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: 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; |