Update to nixpkgs 25.05

.github/workflows/all.yml

@@ -0,0 +1,45 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: CI
+permissions:
+  contents: read
+on:
+  workflow_dispatch:
+  push:
+    branches: ["main"]
+  pull_request:
+    branches: ["main"]
+    types: [ "opened", "synchronize" ]
+
+jobs:
+  base:
+    name: Base
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/base.yml
+    secrets: inherit
+  nix:
+    name: Nix
+    permissions:
+      actions: 'write'
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/nix.yml
+    secrets: inherit
+  ci:
+    name: Extended
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    needs: [ base, nix ]
+    uses: ./.github/workflows/ci.yml
+    secrets: inherit
+  cbmc:
+    name: CBMC
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    needs: [ base, nix ]
+    uses: ./.github/workflows/cbmc.yml
+    secrets: inherit

.github/workflows/base.yml

@@ -0,0 +1,173 @@
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: Base
+permissions:
+  contents: read
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  lint:
+    strategy:
+      fail-fast: false
+      matrix:
+        system: [ubuntu-latest, pqcp-arm64]
+    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@3c3b66f1f7d0900e37b71eca45b63ea9eedfce31 # v1.0.17
+  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'
+         - runner: macos-latest
+           name: 'macos (aarch64)'
+         - runner: macos-13
+           name: 'macos (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-os
+      - name: tests func
+        run: |
+          ./scripts/tests func
+  quickcheck_bench:
+    strategy:
+      fail-fast: false
+      matrix:
+        external:
+         - ${{ github.repository_owner != 'pq-code-package' }}
+        target:
+         - runner: pqcp-arm64
+           name: 'aarch64'
+         - runner: pqcp-arm64
+           name: 'aarch64'
+         - runner: ubuntu-latest
+           name: 'x86_64'
+         - runner: macos-latest
+           name: 'macos (aarch64)'
+         - runner: macos-13
+           name: 'macos (x86_64)'
+        exclude:
+          - {external: true,
+             target: {
+               runner: pqcp-arm64,
+               name: 'aarch64'
+             }}
+    name: Quickcheck bench (${{ matrix.target.name }})
+    runs-on: ${{ matrix.target.runner }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: "tests bench (cycles: NO)"
+        run: |
+          ./scripts/tests bench -c NO
+      - name: "tests bench (build only, cycles: PMU)"
+        if: ${{ matrix.target.name != 'macos (aarch64)' && matrix.target.name != 'macos (x86_64)' }}
+        run: |
+          make clean
+          ./scripts/tests bench -c PMU --no-run
+      - name: "tests bench (build only, cycles: PERF)"
+        if: ${{ matrix.target.name != 'macos (aarch64)' && matrix.target.name != 'macos (x86_64)' }}
+        run: |
+          make clean
+          ./scripts/tests bench -c PERF --no-run
+      - name: "tests bench (build only, cycles: MAC)"
+        if: ${{ matrix.target.name == 'macos (aarch64)' || matrix.target.name == 'macos (x86_64)' }}
+        run: |
+          make clean
+          ./scripts/tests bench -c MAC --no-run
+      - name: tests bench components
+        run: |
+          make clean
+          ./scripts/tests bench --components -c NO
+  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"
+  scan-build:
+    strategy:
+      fail-fast: false
+      matrix:
+        external:
+         - ${{ github.repository_owner != 'pq-code-package' }}
+        target:
+         - runner: pqcp-arm64
+           name: 'aarch64'
+         - runner: ubuntu-latest
+           name: 'x86_64'
+    name: scan-build (${{ matrix.target.name }})
+    runs-on: ${{ matrix.target.runner }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ./.github/actions/setup-apt
+        with:
+          packages: clang-tools clang
+      - name: make quickcheck
+        run: |
+          scan-build --status-bugs make quickcheck OPT=0
+          make clean >/dev/null
+          scan-build --status-bugs make quickcheck OPT=1

.github/workflows/cbmc.yml

@@ -0,0 +1,79 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: CBMC
+permissions:
+  contents: read
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  cbmc_44:
+    name: CBMC (ML-DSA-44)
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC (ML-DSA-44)
+      ec2_instance_type: c7g.8xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-0d7f502261b31b27f # 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_mldsa_mode: 2
+    secrets: inherit
+  cbmc_65:
+    name: CBMC (ML-DSA-65)
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC (ML-DSA-65)
+      ec2_instance_type: c7g.8xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-0d7f502261b31b27f # 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_mldsa_mode: 3
+    secrets: inherit
+  cbmc_87:
+    name: CBMC (ML-DSA-87)
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC (ML-DSA-87)
+      ec2_instance_type: c7g.8xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-0d7f502261b31b27f # 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_mldsa_mode: 5
+    secrets: inherit