diff --git a/.github/workflows/cbmc_core_reusable.yml b/.github/workflows/cbmc_core_reusable.yml new file mode 100644 index 000000000..4bbdf2504 --- /dev/null +++ b/.github/workflows/cbmc_core_reusable.yml @@ -0,0 +1,41 @@ +name: cbmc-core-reusable +on: + workflow_call: + inputs: + runner: + type: string + description: Name of the runner to use + cross-prefix: + type: string + description: Cross-compilation binary prefix, if any + default: ' ' +jobs: + cbmc: + name: CBMC ${{ inputs.runner }} + runs-on: ${{ inputs.runner }} + defaults: + run: + shell: nix develop .#ci-cbmc -c bash -e {0} + steps: + - uses: actions/checkout@v4 + - name: Setup nix + uses: ./.github/actions/setup-nix + with: + devShell: ci-cbmc + script: | + cat >> $GITHUB_STEP_SUMMARY << EOF + ## Setup + Architecture: $(uname -m) + - $(nix --version) + - $(cbmc --version) + - litani Version $(litani --version) + - Cadical Version $(cadical --version) + - $(${{ inputs.cross_prefix }}gcc --version | grep -m1 "") + - $(bash --version | grep -m1 "") + EOF + - name: Run CBMC proofs + 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/ci.yml b/.github/workflows/ci.yml index 2fb9cc000..fb40dd8db 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -34,96 +34,25 @@ jobs: target: - runner: 'pqcp-arm64' name: 'ubuntu-latest (aarch64)' - name: build_kat (${{ matrix.target.name }}) - runs-on: ${{ matrix.target.runner }} - defaults: - run: - shell: nix develop .#ci -c bash -e {0} - steps: - - uses: actions/checkout@v4 - - name: Setup nix - uses: ./.github/actions/setup-nix - with: - devShell: ci - script: | - ARCH=$(uname -m) - cat >> $GITHUB_STEP_SUMMARY <<-EOF - ## Setup - Architecture: $ARCH - - $(uname -a) - - $(nix --version) - - $(astyle --version) - - $(${{ matrix.target.cross-prefix }}gcc --version | grep -m1 "") - - $(bash --version | grep -m1 "") - EOF - - if [[ "$ARCH" != ${{ matrix.target.arch }} ]]; then - echo ":x: Expecting to run on ${{ matrix.target.arch }}, but instead running on $ARCH" >> $GITHUB_STEP_SUMMARY - exit 1 - fi - - name: Run functional tests - uses: ./.github/actions/functest - with: - cflags: ${{ matrix.target.cflags }} - cross-prefix: ${{ matrix.target.cross-prefix }} + name: Functional tests (${{ matrix.target.name }}) + uses: ./.github/workflows/functest_core_reusable.yml + with: + runner: ${{ matrix.target.runner }} + cflags: ${{ matrix.target.cflags }} + cross-prefix: ${{ matrix.target.cross-prefix }} lint: strategy: matrix: system: [ubuntu-latest] - runs-on: ${{ matrix.system }} - defaults: - run: - shell: nix develop .#ci-linter -c bash -e {0} - env: - CROSS_PREFIX: "${{ (matrix.system == 'ubuntu-latest' && 'aarch64-unknown-linux-gnu-') || '' }}" - steps: - - uses: actions/checkout@v4 - - name: Setup nix - uses: ./.github/actions/setup-nix - with: - devShell: ci-linter - script: | - cat >> $GITHUB_STEP_SUMMARY << EOF - ## Setup - Architecture: $(uname -m) - - $(uname -a) - - $(nix --version) - - $(astyle --version) - - $(${{ matrix.target.cross-prefix }}gcc --version | grep -m1 "") - - $(bash --version | grep -m1 "") - EOF - - name: Lint - run: | - echo "## Lint & Checks" >> $GITHUB_STEP_SUMMARY - lint + uses: ./.github/workflows/lint_core_reusable.yml + with: + runner: ${{ matrix.system }} + cross-prefix: "aarch64-unknown-linux-gnu-" cbmc: strategy: matrix: system: [macos-latest] - runs-on: ${{ matrix.system }} - defaults: - run: - shell: nix develop .#ci-cbmc -c bash -e {0} - steps: - - uses: actions/checkout@v4 - - name: Setup nix - uses: ./.github/actions/setup-nix - with: - devShell: ci-cbmc - script: | - cat >> $GITHUB_STEP_SUMMARY << EOF - ## Setup - Architecture: $(uname -m) - - $(nix --version) - - $(cbmc --version) - - litani Version $(litani --version) - - Cadical Version $(cadical --version) - - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "") - - $(bash --version | grep -m1 "") - EOF - - name: Run CBMC proofs - 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; + uses: ./.github/workflows/cbmc_core_reusable.yml + with: + runner: ${{ matrix.system }} + cross-prefix: "aarch64-unknown-linux-gnu-" diff --git a/.github/workflows/functest_core_reusable.yml b/.github/workflows/functest_core_reusable.yml new file mode 100644 index 000000000..70514fa87 --- /dev/null +++ b/.github/workflows/functest_core_reusable.yml @@ -0,0 +1,44 @@ +name: functest-core-reusable +on: + workflow_call: + inputs: + runner: + type: string + description: Name of the runner to use + cflags: + type: string + description: CFLAGS to pass to compilation + default: '' + cross-prefix: + type: string + description: Cross-compilation binary prefix, if any + default: ' ' +jobs: + functest: + name: Bench ${{ inputs.runner }} + runs-on: ${{ inputs.runner }} + defaults: + run: + shell: nix develop .#ci -c bash -e {0} + steps: + - uses: actions/checkout@v4 + - name: Setup nix + uses: ./.github/actions/setup-nix + with: + devShell: ci + script: | + ARCH=$(uname -m) + cat >> $GITHUB_STEP_SUMMARY <<-EOF + ## Setup + Architecture: $ARCH + - $(uname -a) + - $(nix --version) + - $(astyle --version) + - $(${{ inputs.cross-prefix }}gcc --version | grep -m1 "") + - $(bash --version | grep -m1 "") + EOF + - name: Run functional tests + uses: ./.github/actions/functest + with: + cflags: ${{ inputs.cflags }} + cross-prefix: ${{ inputs.cross-prefix }} diff --git a/.github/workflows/lint_core_reusable.yml b/.github/workflows/lint_core_reusable.yml new file mode 100644 index 000000000..171d0871a --- /dev/null +++ b/.github/workflows/lint_core_reusable.yml @@ -0,0 +1,38 @@ +name: lint-core-reusable +on: + workflow_call: + inputs: + runner: + type: string + description: Name of the runner to use + cross-prefix: + type: string + description: Cross-compilation binary prefix, if any + default: ' ' +jobs: + lint: + name: Lint ${{ inputs.runner }} + runs-on: ${{ inputs.runner }} + defaults: + run: + shell: nix develop .#ci-linter -c bash -e {0} + steps: + - uses: actions/checkout@v4 + - name: Setup nix + uses: ./.github/actions/setup-nix + with: + devShell: ci-linter + script: | + cat >> $GITHUB_STEP_SUMMARY << EOF + ## Setup + Architecture: $(uname -m) + - $(uname -a) + - $(nix --version) + - $(astyle --version) + - $(${{ matrix.target.cross-prefix }}gcc --version | grep -m1 "") + - $(bash --version | grep -m1 "") + EOF + - name: Lint + run: | + echo "## Lint & Checks" >> $GITHUB_STEP_SUMMARY + lint