ci.yml

# SPDX-License-Identifier: Apache-2.0

name: CI
permissions:
  contents: read
on:
  workflow_dispatch:
  push:
    branches: ["main"]
  pull_request:
    branches: ["main"]
    types: [ "opened", "synchronize" ]

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  lint:
    strategy:
      matrix:
        system: [ubuntu-latest]
    name: Linting
    runs-on: ${{ matrix.system }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: ./.github/actions/lint
        with:
          nix-shell: ci-linter
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          cross-prefix: "aarch64-unknown-linux-gnu-"
  lint-markdown-link:
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
    - uses: gaurav-nelson/github-action-markdown-link-check@1b916f2cf6c36510a6059943104e3c42ce6c16bc # v1.0.16
  quickcheck:
    strategy:
      fail-fast: false
      matrix:
        external:
         - ${{ github.repository_owner != 'pq-code-package' }}
        target:
         - runner: pqcp-arm64
           name: 'aarch64'
         - runner: ubuntu-latest
           name: 'x86_64'
        exclude:
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'aarch64'
             }}
    name: Quickcheck (${{ matrix.target.name }})
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: make quickcheck
        run: |
          OPT=0 make quickcheck
          make clean >/dev/null
          OPT=1 make quickcheck
      - uses: ./.github/actions/setup-apt
      - name: tests func
        run: |
          ./scripts/tests func
      - name: tests bench
        run: |
          ./scripts/tests bench -c NO
      - name: tests bench components
        run: |
          ./scripts/tests bench --components -c NO
      - name: check namespacing
        run: |
          ./scripts/check-namespace
  quickcheck-c90:
    strategy:
      fail-fast: false
      matrix:
        external:
         - ${{ github.repository_owner != 'pq-code-package' }}
        target:
         - runner: pqcp-arm64
           name: 'aarch64'
         - runner: ubuntu-latest
           name: 'x86_64'
        exclude:
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'aarch64'
             }}
    name: Quickcheck C90 (${{ matrix.target.name }})
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: make quickcheck
        run: |
          OPT=0 CFLAGS=-std=c90 make quickcheck
          make clean >/dev/null
          OPT=1 CFLAGS=-std=c90 make quickcheck
      - uses: ./.github/actions/setup-apt
      - name: tests func
        run: |
          ./scripts/tests func --cflags="-std=c90"
      - name: tests bench
        run: |
          ./scripts/tests bench -c NO --cflags="-std=c90"
      - name: tests bench components
        run: |
          ./scripts/tests bench --components -c NO --cflags="-std=c90"
      - name: check namespacing
        run: |
          ./scripts/check-namespace
  quickcheck-windows:
    name: Quickcheck windows-latest
    runs-on: windows-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: ilammy/msvc-dev-cmd@0b201ec74fa43914dc39ae48a89fd1d8cb592756 # v1.13.0
      - name: Build test
        shell: powershell
        run: |
          # print compiler version
          cl
          nmake /f ./Makefile.Microsoft_nmake quickcheck
  quickcheck-lib:
    name: Quickcheck lib
    strategy:
      matrix:
        system: [macos-latest, ubuntu-latest, ubuntu-24.04-arm]
    runs-on: ${{ matrix.system }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: make lib
        run: |
          make lib
  examples:
    name: Examples
    strategy:
      matrix:
        system: [macos-latest, ubuntu-latest, ubuntu-24.04-arm]
    runs-on: ${{ matrix.system }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: mlkem_native_as_code_package
        run: |
          make run -C examples/mlkem_native_as_code_package
      - name: bring_your_own_fips202
        run: |
          make run -C examples/bring_your_own_fips202
      - name: custom_backend
        run: |
          make run -C examples/custom_backend
      - name: monolithic_build
        run: |
          make run -C examples/monolithic_build
      - name: monolithic_build_multilevel
        run: |
          make run -C examples/monolithic_build_multilevel
      - name: multilevel_build
        run: |
          make run -C examples/multilevel_build
  aws_lc_integration:
    strategy:
      matrix:
        system: [Ubuntu-latest]
    name: AWS-LC integration test
    runs-on: ${{ matrix.system }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: ./.github/actions/setup-os
        with:
          packages: 'cmake'
      - uses: ./.github/actions/setup-aws-lc
        with:
          repository: 'hanno-becker/aws-lc'
          commit: 'mlkem_native'
      - name: Run importer
        run: |
          cd $AWSLC_DIR/crypto/fipsmodule/ml_kem
          GITHUB_REPOSITORY=$GITHUB_REPOSITORY GITHUB_SHA=$GITHUB_SHA ./importer.sh
      - name: Build AWS-LC (FIPS=1)
        run: |
          cd $AWSLC_DIR
          mkdir build_fips
          cd build_fips
          cmake -DFIPS=1 ..
          cd ..

          cmake --build ./build_fips --target all
          cmake --build ./build_fips --target run_tests
      - name: Build AWS-LC (FIPS=0)
        run: |
          cd $AWSLC_DIR
          mkdir build_no_fips
          cd build_no_fips
          cmake ..
          cd ..

          cmake --build ./build_no_fips --target all
          cmake --build ./build_no_fips --target run_tests
  build_kat:
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    strategy:
      fail-fast: false
      matrix:
        external:
         - ${{ github.repository_owner != 'pq-code-package' }}
        target:
         - runner: macos-latest
           name: 'MacOS'
           arch: mac
           mode: native
         - runner: ubuntu-24.04-arm
           name: 'ubuntu-24.04-arm'
           arch: aarch64
           mode: native
         - runner: pqcp-arm64
           name: 'ubuntu-latest (aarch64)'
           arch: aarch64
           mode: native
         - runner: pqcp-arm64
           name: 'ubuntu-latest (aarch64)'
           arch: x86_64
           mode: cross-x86_64
         - runner: pqcp-arm64
           name: 'ubuntu-latest (aarch64)'
           arch: riscv64
           mode: cross-riscv64
         - runner: pqcp-x64
           name: 'ubuntu-latest (x86_64)'
           arch: x86_64
           mode: native
         - runner: pqcp-x64
           name: 'ubuntu-latest (x86_64)'
           arch: aarch64
           mode: cross-aarch64
         - runner: pqcp-x64
           name: 'ubuntu-latest (x86_64)'
           arch: aarch64_be
           mode: cross-aarch64_be
        exclude:
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'ubuntu-latest (aarch64)',
               arch: aarch64,
               mode: native
             }}
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'ubuntu-latest (aarch64)',
               arch: x86_64,
               mode: cross-x86_64
             }}
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'ubuntu-latest (aarch64)',
               arch: riscv64,
               mode: cross-riscv64
             }}
          - {external: true,
             target: {
               runner: pqcp-x64,
               name: 'ubuntu-latest (x86_64)',
               arch: x86_64,
               mode: native
             }}
          - {external: true,
             target: {
               runner: pqcp-x64,
               name: 'ubuntu-latest (x86_64)',
               arch: aarch64,
               mode: cross-aarch64
             }}
          - {external: true,
             target: {
               runner: pqcp-x64,
               name: 'ubuntu-latest (x86_64)',
               arch: aarch64_be,
               mode: cross-aarch64_be
             }}
    name: Functional tests (${{ matrix.target.arch }}${{ matrix.target.mode != 'native' && ', cross' || ''}})
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: build + test
        uses: ./.github/actions/multi-functest
        with:
          nix-shell: ${{ matrix.target.mode == 'native' && 'ci' || 'ci-cross' }}
          nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: ${{ matrix.target.mode }}
          # There is no native code on R-V or AArch64_be yet, so no point running opt tests
          opt: ${{ (matrix.target.arch != 'riscv64' && matrix.target.arch != 'aarch64_be') && 'all' || 'no_opt' }}
      - name: build + test (+debug+memsan+ubsan)
        uses: ./.github/actions/multi-functest
        if: ${{ matrix.target.mode == 'native' }}
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          cflags: "-DMLKEM_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
  simpasm:
    name: ASM simplifier
    strategy:
      fail-fast: false
      matrix:
        target:
           - runner: ubuntu-24.04-arm
             arch: 'aarch64'
           - runner: ubuntu-latest
             arch: 'x86_64'
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: Simplify assembly
        run: |
          ./scripts/simpasm -d mlkem/native/${{ matrix.target.arch }}/src --cflags='-Imlkem/native/${{ matrix.target.arch }}/src/' -p
      - name: Test simplified assembly
        run: |
          OPT=1 make quickcheck
  compiler_tests:
    name: Compiler tests  (${{ matrix.compiler.name }}, ${{ matrix.target.name }})
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    strategy:
      fail-fast: false
      matrix:
        target:
         - runner: pqcp-arm64
           name: 'aarch64'
         - runner: ubuntu-24.04-arm
           name: 'ubuntu-24.04-arm'
         - runner: ubuntu-latest
           name: 'x86_64'
         - runner: macos-latest
           name: 'macos'
        compiler:
         - name: gcc-4.8
           shell: ci_gcc48
           darwin: False
           c17: False
         - name: gcc-4.9
           shell: ci_gcc49
           darwin: False
           c17: False
         - name: gcc-7
           shell: ci_gcc7
           darwin: False
           c17: False
         - name: gcc-11
           shell: ci_gcc11
           darwin: True
         - name: gcc-13
           shell: ci_gcc13
           darwin: True
         - name: gcc-14
           shell: ci_gcc14
           darwin: True
         - name: clang-18
           shell: ci_clang18
           darwin: True
         - name: clang-19
           shell: ci_clang19
           darwin: True
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: native build+functest (default)
        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          func: true
          nistkat: false
          kat: false
          acvp: false
          nix-shell: ${{ matrix.compiler.shell }}
      - name: native build+functest (C90)
        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          func: true
          nistkat: false
          kat: false
          acvp: false
          nix-shell: ${{ matrix.compiler.shell }}
          cflags: "-std=c90"
      - name: native build+functest (C99)
        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          func: true
          nistkat: false
          kat: false
          acvp: false
          nix-shell: ${{ matrix.compiler.shell }}
          cflags: "-std=c99"
      - name: native build+functest (C11)
        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          func: true
          nistkat: false
          kat: false
          acvp: false
          nix-shell: ${{ matrix.compiler.shell }}
          cflags: "-std=c11"
      - name: native build+functest (C17)
        if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') &&
                matrix.compiler.c17 }}
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          func: true
          nistkat: false
          kat: false
          acvp: false
          nix-shell: ${{ matrix.compiler.shell }}
          cflags: "-std=c17"
  config_variations:
    name: Non-standard configurations
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    strategy:
      fail-fast: false
      matrix:
        external:
         - ${{ github.repository_owner != 'pq-code-package' }}
        target:
         - runner: pqcp-arm64
           name: 'ubuntu-latest (aarch64)'
         - runner: pqcp-x64
           name: 'ubuntu-latest (x86_64)'
        exclude:
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'ubuntu-latest (aarch64)',
             }}
          - {external: true,
             target: {
               runner: pqcp-x64,
               name: 'ubuntu-latest (x86_64)',
             }}
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: "MLKEM_GEN_MATRIX_NBLOCKS=1"
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          cflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -DMLKEM_GEN_MATRIX_NBLOCKS=1"
          func: true
          nistkat: true
          kat: false
          acvp: false
      - name: "MLKEM_GEN_MATRIX_NBLOCKS=2"
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          cflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -DMLKEM_GEN_MATRIX_NBLOCKS=2"
          func: true
          nistkat: true
          kat: false
          acvp: false
      - name: "MLKEM_GEN_MATRIX_NBLOCKS=4"
        uses: ./.github/actions/multi-functest
        with:
          gh_token: ${{ secrets.GITHUB_TOKEN }}
          compile_mode: native
          cflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -DMLKEM_GEN_MATRIX_NBLOCKS=4"
          func: true
          nistkat: true
          kat: false
          acvp: false
  # ensure that kem.h and mlkem_native.h; api.h and native backends are compatible
  check-apis:
    strategy:
      fail-fast: false
      matrix:
        external:
         - ${{ github.repository_owner != 'pq-code-package' }}
        target:
         - runner: pqcp-arm64
           name: 'aarch64'
         - runner: ubuntu-latest
           name: 'x86_64'
        exclude:
          - {external: true,
             target: {
               runner: pqcp-arm64,
               name: 'aarch64'
             }}
    name: Check API consistency
    runs-on: ${{ matrix.target.runner }}
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: make quickcheck
        run: |
          OPT=0 CFLAGS="-DMLKEM_NATIVE_CHECK_APIS -Wno-redundant-decls" make quickcheck
          make clean >/dev/null
          OPT=1 CFLAGS="-DMLKEM_NATIVE_CHECK_APIS -Wno-redundant-decls" make quickcheck
      - uses: ./.github/actions/setup-apt
      - name: tests func
        run: |
          ./scripts/tests func --cflags="-DMLKEM_NATIVE_CHECK_APIS -Wno-redundant-decls"
  ec2_functests:
    strategy:
      fail-fast: false
      matrix:
        target:
          - name: AMD EPYC 4th gen (t3a)
            ec2_instance_type: t3a.small
            ec2_ami: ubuntu-latest (custom AMI)
            ec2_ami_id: ami-0d47e137a1108e078 # x86_64 ubuntu-latest, 32g
            compile_mode: native
            opt: all
          - name: Intel Xeon 4th gen (t3)
            ec2_instance_type: t3.small
            ec2_ami: ubuntu-latest (custom AMI)
            ec2_ami_id: ami-0d47e137a1108e078 # x86_64 ubuntu-latest, 32g
            compile_mode: native
            opt: all
          - name: Graviton2 (c6g.medium)
            ec2_instance_type: c6g.medium
            ec2_ami: ubuntu-latest (custom AMI)
            ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
            compile_mode: native
            opt: all
          - name: Graviton3 (c7g.medium)
            ec2_instance_type: c7g.medium
            ec2_ami: ubuntu-latest (custom AMI)
            ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
            compile_mode: native
            opt: all
    name: Platform tests  (${{ matrix.target.name }})
    permissions:
      contents: 'read'
      id-token: 'write'
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
    uses: ./.github/workflows/ci_ec2_reusable.yml
    with:
      name: ${{ matrix.target.name }}
      ec2_instance_type: ${{ matrix.target.ec2_instance_type }}
      ec2_ami: ${{ matrix.target.ec2_ami }}
      ec2_ami_id: ${{ matrix.target.ec2_ami_id }}
      compile_mode: ${{ matrix.target.compile_mode }}
      opt: ${{ matrix.target.opt }}
      functest: true
      kattest: true
      nistkattest: true
      acvptest: true
      lint: false
      verbose: true
    secrets: inherit
  compatibility_tests:
    strategy:
      max-parallel: 4
      fail-fast: false
      matrix:
        container:
          - id: debian:bullseye
          - id: debian:bookworm
    name: Compatibility tests (${{ matrix.container.id }})
    runs-on: ubuntu-latest
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    container:
      ${{ matrix.container.id }}
    steps:
      # We're not using the checkout action here because on it's not supported
      # on all containers we want to test. Resort to a manual checkout.

      # We can't hoist this into an action since calling an action can only
      # be done after checkout.
      - name: Manual checkout
        shell: bash
        run: |
          if (which yum > /dev/null); then
             yum install git -y
          elif (which apt > /dev/null); then
             apt update
             apt install git -y
          fi

          git config --global --add safe.directory $GITHUB_WORKSPACE
          git init
          git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
          git fetch origin --depth 1 $GITHUB_SHA
          git checkout FETCH_HEAD
      - uses: ./.github/actions/setup-os
        with:
          sudo: ""
      - name: make quickcheck
        run: |
          OPT=0 make quickcheck
          make clean >/dev/null
          OPT=1 make quickcheck
      - name: Functional Tests
        uses: ./.github/actions/multi-functest
        with:
          nix-shell: ""
          gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
  ec2_compatibilitytests:
    strategy:
      max-parallel: 8
      fail-fast: false
      matrix:
        container:
          - id: amazonlinux-2-aarch:base
          - id: amazonlinux-2-aarch:gcc-7x
          - id: amazonlinux-2-aarch:clang-7x
          - id: amazonlinux-2023-aarch:base
          - id: amazonlinux-2023-aarch:gcc-11x
          - id: amazonlinux-2023-aarch:clang-15x
          - id: amazonlinux-2023-aarch:clang-15x-sanitizer
          # - id: amazonlinux-2023-aarch:cryptofuzz Not yet supported
          - id: ubuntu-22.04-aarch:gcc-12x
          - id: ubuntu-22.04-aarch:gcc-11x
          - id: ubuntu-20.04-aarch:gcc-8x
          - id: ubuntu-20.04-aarch:gcc-7x
          - id: ubuntu-20.04-aarch:clang-9x
          - id: ubuntu-20.04-aarch:clang-8x
          - id: ubuntu-20.04-aarch:clang-7x-bm-framework
          - id: ubuntu-20.04-aarch:clang-7x
          - id: ubuntu-20.04-aarch:clang-10x
          - id: ubuntu-22.04-aarch:base
          - id: ubuntu-20.04-aarch:base
    name: Compatibility tests (${{ matrix.container.id }})
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    permissions:
      contents: 'read'
      id-token: 'write'
    uses: ./.github/workflows/ci_ec2_container.yml
    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
    with:
      container: ${{ matrix.container.id }}
      name: ${{ matrix.container.id }}
      ec2_instance_type: t4g.small
      ec2_ami: ubuntu-latest (custom AMI)
      ec2_ami_id: ami-0c9bc1901ef0d1066 # Has docker images preinstalled
      compile_mode: native
      opt: all
      functest: true
      kattest: true
      nistkattest: true
      acvptest: true
      lint: false
      verbose: true
      cflags: "-O0"
    secrets: inherit
  cbmc_k2:
    name: CBMC (ML-KEM-512)
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    permissions:
      contents: 'read'
      id-token: 'write'
    uses: ./.github/workflows/ci_ec2_reusable.yml
    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
    with:
      name: CBMC (MLKEM-512)
      ec2_instance_type: c7g.2xlarge
      ec2_ami: ubuntu-latest (custom AMI)
      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
      compile_mode: native
      opt: no_opt
      lint: false
      verbose: true
      functest: true
      kattest: false
      nistkattest: false
      acvptest: false
      cbmc: true
      cbmc_mlkem_k: 2
    secrets: inherit
  cbmc_k3:
    name: CBMC (ML-KEM-768)
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    permissions:
      contents: 'read'
      id-token: 'write'
    uses: ./.github/workflows/ci_ec2_reusable.yml
    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
    with:
      name: CBMC (MLKEM-768)
      ec2_instance_type: c7g.2xlarge
      ec2_ami: ubuntu-latest (custom AMI)
      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
      compile_mode: native
      opt: no_opt
      lint: false
      verbose: true
      functest: true
      kattest: false
      nistkattest: false
      acvptest: false
      cbmc: true
      cbmc_mlkem_k: 3
    secrets: inherit
  cbmc_k4:
    name: CBMC (ML-KEM-1024)
    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
    permissions:
      contents: 'read'
      id-token: 'write'
    uses: ./.github/workflows/ci_ec2_reusable.yml
    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
    with:
      name: CBMC (MLKEM-1024)
      ec2_instance_type: c7g.2xlarge
      ec2_ami: ubuntu-latest (custom AMI)
      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
      compile_mode: native
      opt: no_opt
      lint: false
      verbose: true
      functest: true
      kattest: false
      nistkattest: false
      acvptest: false
      cbmc: true
      cbmc_mlkem_k: 4
    secrets: inherit