diff --git a/.github/actions/config-variations/action.yml b/.github/actions/config-variations/action.yml index f7ad591d9..4c985731b 100644 --- a/.github/actions/config-variations/action.yml +++ b/.github/actions/config-variations/action.yml @@ -18,35 +18,35 @@ inputs: runs: using: 'composite' steps: - - name: "PCT enabled" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'pct-enabled') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-DMLD_CONFIG_KEYGEN_PCT -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: true - extra_args: "--exclude-example basic_deterministic" - - name: "PCT enabled + broken" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'pct-enabled-broken') }} - shell: bash - run: | - make clean - CFLAGS='-Itest -DMLD_CONFIG_FILE=\"break_pct_config.h\"' make func -j4 - # PCT breakage is done at runtime via MLD_BREAK_PCT - make run_func # Should be OK - MLD_BREAK_PCT=0 make run_func # Should be OK - if (MLD_BREAK_PCT=1 make run_func 2>&1 >/dev/null); then - echo "PCT failure expected" - exit 1 - else - echo "PCT failed as expected" - fi + # - name: "PCT enabled" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'pct-enabled') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-DMLD_CONFIG_KEYGEN_PCT -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: true + # extra_args: "--exclude-example basic_deterministic" + # - name: "PCT enabled + broken" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'pct-enabled-broken') }} + # shell: bash + # run: | + # make clean + # CFLAGS='-Itest -DMLD_CONFIG_FILE=\"break_pct_config.h\"' make func -j4 + # # PCT breakage is done at runtime via MLD_BREAK_PCT + # make run_func # Should be OK + # MLD_BREAK_PCT=0 make run_func # Should be OK + # if (MLD_BREAK_PCT=1 make run_func 2>&1 >/dev/null); then + # echo "PCT failure expected" + # exit 1 + # else + # echo "PCT failed as expected" + # fi - name: "Custom allocation (heap based)" if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-alloc-heap') }} uses: ./.github/actions/multi-functest @@ -61,146 +61,146 @@ runs: opt: ${{ inputs.opt }} extra_env: 'ASAN_OPTIONS=detect_leaks=1' examples: false # Some examples use a custom config themselves - - name: "Custom zeroization (explicit_bzero)" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-zeroize') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_zeroize_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom native capability functions (static ON)" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'native-cap-ON') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_1.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom native capability functions (static OFF)" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'native-cap-OFF') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_0.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom native capability functions (ID_AA64PFR1_EL1 detection)" - if: ${{ (inputs.tests == 'all' || contains(inputs.tests, 'native-cap-ID_AA64PFR1_EL1')) && runner.os == 'Linux' && runner.arch == 'ARM64' }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -march=armv8.4-a+sha3 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_ID_AA64PFR1_EL1.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom native capability functions (CPUID AVX2 detection)" - if: ${{ (inputs.tests == 'all' || contains(inputs.tests, 'native-cap-CPUID_AVX2')) && runner.os == 'Linux' && runner.arch == 'X64' }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -mavx2 -mbmi2 -mpopcnt -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_CPUID_AVX2.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "No ASM" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'no-asm') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"no_asm_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Serial FIPS202 (no batched Keccak)" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'serial-fips202') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"serial_fips202_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom randombytes" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-randombytes') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_randombytes_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom memcpy" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-memcpy') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_memcpy_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom memset" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-memset') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_memset_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves - - name: "Custom stdlib (memcpy + memset)" - if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-stdlib') }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ inputs.gh_token }} - compile_mode: native - cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_stdlib_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - func: true - kat: true - acvp: true - opt: ${{ inputs.opt }} - examples: false # Some examples use a custom config themselves + # - name: "Custom zeroization (explicit_bzero)" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-zeroize') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_zeroize_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom native capability functions (static ON)" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'native-cap-ON') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_1.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom native capability functions (static OFF)" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'native-cap-OFF') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_0.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom native capability functions (ID_AA64PFR1_EL1 detection)" + # if: ${{ (inputs.tests == 'all' || contains(inputs.tests, 'native-cap-ID_AA64PFR1_EL1')) && runner.os == 'Linux' && runner.arch == 'ARM64' }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -march=armv8.4-a+sha3 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_ID_AA64PFR1_EL1.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom native capability functions (CPUID AVX2 detection)" + # if: ${{ (inputs.tests == 'all' || contains(inputs.tests, 'native-cap-CPUID_AVX2')) && runner.os == 'Linux' && runner.arch == 'X64' }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -mavx2 -mbmi2 -mpopcnt -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_native_capability_config_CPUID_AVX2.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "No ASM" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'no-asm') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"no_asm_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Serial FIPS202 (no batched Keccak)" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'serial-fips202') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"serial_fips202_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom randombytes" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-randombytes') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_randombytes_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom memcpy" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-memcpy') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_memcpy_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom memset" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-memset') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_memset_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves + # - name: "Custom stdlib (memcpy + memset)" + # if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'custom-stdlib') }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ inputs.gh_token }} + # compile_mode: native + # cflags: "-std=c11 -D_GNU_SOURCE -Itest -DMLD_CONFIG_FILE=\\\\\\\"custom_stdlib_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # func: true + # kat: true + # acvp: true + # opt: ${{ inputs.opt }} + # examples: false # Some examples use a custom config themselves diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml index 1afcd318e..46da0a9c5 100644 --- a/.github/workflows/all.yml +++ b/.github/workflows/all.yml @@ -20,26 +20,26 @@ jobs: id-token: 'write' uses: ./.github/workflows/base.yml secrets: inherit - lint-markdown: - name: Lint Markdown - permissions: - contents: 'read' - id-token: 'write' - uses: ./.github/workflows/lint_markdown.yml - nix: - name: Nix - permissions: - actions: 'write' - contents: 'read' - id-token: 'write' - uses: ./.github/workflows/nix.yml - secrets: inherit + # lint-markdown: + # name: Lint Markdown + # permissions: + # contents: 'read' + # id-token: 'write' + # uses: ./.github/workflows/lint_markdown.yml + # 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 ] +# needs: [ base, nix ] uses: ./.github/workflows/ci.yml secrets: inherit cbmc: @@ -47,38 +47,38 @@ jobs: permissions: contents: 'read' id-token: 'write' - needs: [ base, nix ] +# needs: [ base, nix ] uses: ./.github/workflows/cbmc.yml secrets: inherit - oqs_integration: - name: libOQS - permissions: - contents: 'read' - id-token: 'write' - needs: [ base ] - uses: ./.github/workflows/integration-liboqs.yml - secrets: inherit - ct-test: - name: Constant-time - permissions: - contents: 'read' - id-token: 'write' - needs: [ base, nix ] - uses: ./.github/workflows/ct-tests.yml - secrets: inherit - slothy: - name: SLOTHY - permissions: - contents: 'read' - id-token: 'write' - needs: [ base, nix ] - uses: ./.github/workflows/slothy.yml - secrets: inherit - baremetal: - name: Baremetal - permissions: - contents: 'read' - id-token: 'write' - needs: [ base ] - uses: ./.github/workflows/baremetal.yml - secrets: inherit + # oqs_integration: + # name: libOQS + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base ] + # uses: ./.github/workflows/integration-liboqs.yml + # secrets: inherit + # ct-test: + # name: Constant-time + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base, nix ] + # uses: ./.github/workflows/ct-tests.yml + # secrets: inherit + # slothy: + # name: SLOTHY + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base, nix ] + # uses: ./.github/workflows/slothy.yml + # secrets: inherit + # baremetal: + # name: Baremetal + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base ] + # uses: ./.github/workflows/baremetal.yml + # secrets: inherit diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c1c770acb..8bfc2bfb3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,434 +10,434 @@ on: workflow_dispatch: jobs: - build_kat: - strategy: - fail-fast: false - matrix: - external: - - ${{ github.repository_owner != 'pq-code-package' }} - target: - - runner: macos-latest - name: 'MacOS (aarch64)' - arch: mac - mode: native - nix_shell: ci - - runner: macos-15-intel - name: 'MacOS (x86_64)' - arch: mac - mode: native - nix_shell: ci - - runner: ubuntu-24.04-arm - name: 'ubuntu-latest (aarch64)' - arch: aarch64 - mode: native - nix_shell: ci - - runner: ubuntu-24.04-arm - name: 'ubuntu-latest (aarch64)' - arch: x86_64 - mode: cross-x86_64 - nix_shell: ci-cross-x86_64 - - runner: ubuntu-24.04-arm - name: 'ubuntu-latest (aarch64)' - arch: riscv64 - mode: cross-riscv64 - nix_shell: ci-cross-riscv64 - - runner: ubuntu-24.04-arm - name: 'ubuntu-latest (aarch64)' - arch: riscv32 - mode: cross-riscv32 - nix_shell: ci-cross-riscv32 - - runner: ubuntu-24.04-arm - name: 'ubuntu-latest (ppc64le)' - arch: ppc64le - mode: cross-ppc64le - nix_shell: ci-cross-ppc64le - - runner: ubuntu-latest - name: 'ubuntu-latest (x86_64)' - arch: x86_64 - mode: native - nix_shell: ci - - runner: ubuntu-latest - name: 'ubuntu-latest (x86_64)' - arch: aarch64 - mode: cross-aarch64 - nix_shell: ci-cross-aarch64 - - runner: ubuntu-latest - name: 'ubuntu-latest (x86_64)' - arch: aarch64_be - mode: cross-aarch64_be - nix_shell: ci-cross-aarch64_be - exclude: - - {external: true, - target: { - runner: ubuntu-24.04-arm, - name: 'ubuntu-latest (aarch64)', - arch: aarch64, - mode: native, - nix_shell: ci - }} - - {external: true, - target: { - runner: ubuntu-24.04-arm, - name: 'ubuntu-latest (aarch64)', - arch: x86_64, - mode: cross-x86_64, - nix_shell: ci-cross-x86_64 - }} - - {external: true, - target: { - runner: ubuntu-24.04-arm, - name: 'ubuntu-latest (aarch64)', - arch: riscv64, - mode: cross-riscv64, - nix_shell: ci-cross-riscv64 - }} - - {external: true, - target: { - runner: ubuntu-24.04-arm, - name: 'ubuntu-latest (aarch64)', - arch: riscv32, - mode: cross-riscv32, - nix_shell: ci-cross-riscv32 - }} - - {external: true, - target: { - runner: ubuntu-24.04-arm, - name: 'ubuntu-latest (ppc64le)', - arch: ppc64le, - mode: cross-ppc64le, - nix_shell: ci-cross-ppc64le - }} - - {external: true, - target: { - runner: ubuntu-latest, - name: 'ubuntu-latest (x86_64)', - arch: x86_64, - mode: native, - nix_shell: ci - }} - - {external: true, - target: { - runner: ubuntu-latest, - name: 'ubuntu-latest (x86_64)', - arch: aarch64, - mode: cross-aarch64, - nix_shell: ci-cross-aarch64 - }} - - {external: true, - target: { - runner: ubuntu-latest, - name: 'ubuntu-latest (x86_64)', - arch: aarch64_be, - mode: cross-aarch64_be, - nix_shell: ci-cross-aarch64_be - }} - name: Functional tests (${{ matrix.target.arch }}${{ matrix.target.mode != 'native' && ', cross' || ''}}) - runs-on: ${{ matrix.target.runner }} - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - name: build + test (no-opt) - uses: ./.github/actions/multi-functest - with: - nix-shell: ${{ matrix.target.nix_shell }} - nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }} - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: ${{ matrix.target.mode }} - opt: 'no_opt' - - name: build + test (+debug+memsan+ubsan, native) - uses: ./.github/actions/multi-functest - if: ${{ matrix.target.mode == 'native' }} - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: native - cflags: "-DMLDSA_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - check_namespace: 'false' - - name: build + test (cross, opt) - uses: ./.github/actions/multi-functest - # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests - if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }} - with: - nix-shell: ${{ matrix.target.nix_shell }} - nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }} - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: ${{ matrix.target.mode }} - opt: 'opt' - - name: build + test (cross, opt, +debug) - uses: ./.github/actions/multi-functest - # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests - if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }} - with: - nix-shell: ${{ matrix.target.nix_shell }} - nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }} - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: ${{ matrix.target.mode }} - cflags: "-DMLDSA_DEBUG" - opt: 'opt' - backend_tests: - name: AArch64 FIPS202 backends (${{ matrix.backend }}) - strategy: - fail-fast: false - matrix: - backend: [x1_scalar, x1_v84a, x2_v84a, x4_v8a_scalar, x4_v8a_v84a_scalar] - runs-on: macos-latest - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - name: build + test - uses: ./.github/actions/multi-functest - with: - nix-shell: 'ci' - nix-cache: 'false' - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: 'native' - opt: 'opt' - examples: 'false' - cflags: "-DMLDSA_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" - check_namespace: 'false' - extra_args: "--fips202-aarch64-backend ${{ matrix.backend }}" - compiler_tests: - name: Compiler tests (${{ matrix.compiler.name }}, ${{ matrix.target.name }}, ${{ matrix.cflags }}) - strategy: - fail-fast: false - matrix: - cflags: [ "-O0", "-Os", "-O3" ] - target: - - runner: ubuntu-24.04-arm - name: 'aarch64' - - runner: ubuntu-latest - name: 'x86_64' - - runner: macos-latest - name: 'macos' - compiler: - - name: gcc-4.8 - shell: ci_gcc48 - darwin: False - c17: False - c23: False - opt: all - examples: true - - name: gcc-4.9 - shell: ci_gcc49 - darwin: False - c17: False - c23: False - opt: all - examples: true - - name: gcc-7 - shell: ci_gcc7 - darwin: False - c17: False - c23: False - opt: all - examples: true - - name: gcc-11 - shell: ci_gcc11 - darwin: True - c17: True - c23: False - opt: all - examples: true - - name: gcc-13 - shell: ci_gcc13 - darwin: True - c17: True - c23: False - opt: all - examples: true - - name: gcc-14 - shell: ci_gcc14 - darwin: True - c17: True - c23: True - opt: all - examples: true - - name: gcc-15 - shell: ci_gcc15 - # TODO: Add this once gcc15 is supported in nix on aarch64-Darwin - darwin: False - c17: True - c23: True - opt: all - examples: true - - name: clang-18 - shell: ci_clang18 - darwin: True - c17: True - c23: True - opt: all - examples: true - - name: clang-19 - shell: ci_clang19 - darwin: True - c17: True - c23: True - opt: all - examples: true - - name: clang-20 - shell: ci_clang20 - darwin: True - c17: True - c23: True - opt: all - examples: true - - name: clang-21 - shell: ci_clang21 - darwin: True - c17: True - c23: True - opt: all - examples: true - # CPU flags are not correctly passed to the zig assembler - # https://github.com/ziglang/zig/issues/23576 - # We therefore only test the C backend - # - # We omit all examples since there is currently no way to run - # only those examples not involving native code. - - name: zig-0.12 - shell: ci_zig0_12 - darwin: True - c17: True - c23: False - examples: False - opt: no_opt - - name: zig-0.13 - shell: ci_zig0_13 - darwin: True - c17: True - c23: False - examples: False - opt: no_opt - - name: zig-0.14 - shell: ci_zig0_14 - darwin: True - c17: True - c23: True - examples: False - opt: no_opt - - name: zig-0.15 - shell: ci_zig0_15 - darwin: True - c17: True - c23: True - examples: False - opt: no_opt - runs-on: ${{ matrix.target.runner }} - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - 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 - kat: false - acvp: false - examples: ${{ matrix.compiler.examples }} - opt: ${{ matrix.compiler.opt }} - nix-shell: ${{ matrix.compiler.shell }} - cflags: "${{ matrix.cflags }}" - - 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 - kat: false - acvp: false - examples: ${{ matrix.compiler.examples }} - opt: ${{ matrix.compiler.opt }} - nix-shell: ${{ matrix.compiler.shell }} - cflags: "-std=c90 ${{ matrix.cflags }}" - - 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 - kat: false - acvp: false - examples: ${{ matrix.compiler.examples }} - opt: ${{ matrix.compiler.opt }} - nix-shell: ${{ matrix.compiler.shell }} - cflags: "-std=c99 ${{ matrix.cflags }}" - - 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 - kat: false - acvp: false - examples: ${{ matrix.compiler.examples }} - opt: ${{ matrix.compiler.opt }} - nix-shell: ${{ matrix.compiler.shell }} - cflags: "-std=c11 ${{ matrix.cflags }}" - - 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 - kat: false - acvp: false - examples: ${{ matrix.compiler.examples }} - opt: ${{ matrix.compiler.opt }} - nix-shell: ${{ matrix.compiler.shell }} - cflags: "-std=c17 ${{ matrix.cflags }}" - - name: native build+functest (C23) - if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') && - matrix.compiler.c23 }} - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: native - func: true - kat: false - acvp: false - examples: ${{ matrix.compiler.examples }} - opt: ${{ matrix.compiler.opt }} - nix-shell: ${{ matrix.compiler.shell }} - cflags: "-std=c23 ${{ matrix.cflags }}" - stack_analysis: - name: Stack analysis (${{ matrix.target.name }}, ${{ matrix.cflags }}) - strategy: - fail-fast: false - matrix: - external: - - ${{ github.repository_owner != 'pq-code-package' }} - target: - - runner: ubuntu-latest - name: x86_64 - - runner: ubuntu-24.04-arm - name: aarch64 - cflags: ['-O3', '-Os'] - exclude: - - external: true - runs-on: ${{ matrix.target.runner }} - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - name: Stack analysis - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: native - nix-shell: ci_valgrind-varlat_gcc15 - nix-cache: false - opt: all - cflags: "${{ matrix.cflags }}" - func: false - kat: false - acvp: false - examples: false - stack: true - check_namespace: false + # build_kat: + # strategy: + # fail-fast: false + # matrix: + # external: + # - ${{ github.repository_owner != 'pq-code-package' }} + # target: + # - runner: macos-latest + # name: 'MacOS (aarch64)' + # arch: mac + # mode: native + # nix_shell: ci + # - runner: macos-15-intel + # name: 'MacOS (x86_64)' + # arch: mac + # mode: native + # nix_shell: ci + # - runner: ubuntu-24.04-arm + # name: 'ubuntu-latest (aarch64)' + # arch: aarch64 + # mode: native + # nix_shell: ci + # - runner: ubuntu-24.04-arm + # name: 'ubuntu-latest (aarch64)' + # arch: x86_64 + # mode: cross-x86_64 + # nix_shell: ci-cross-x86_64 + # - runner: ubuntu-24.04-arm + # name: 'ubuntu-latest (aarch64)' + # arch: riscv64 + # mode: cross-riscv64 + # nix_shell: ci-cross-riscv64 + # - runner: ubuntu-24.04-arm + # name: 'ubuntu-latest (aarch64)' + # arch: riscv32 + # mode: cross-riscv32 + # nix_shell: ci-cross-riscv32 + # - runner: ubuntu-24.04-arm + # name: 'ubuntu-latest (ppc64le)' + # arch: ppc64le + # mode: cross-ppc64le + # nix_shell: ci-cross-ppc64le + # - runner: ubuntu-latest + # name: 'ubuntu-latest (x86_64)' + # arch: x86_64 + # mode: native + # nix_shell: ci + # - runner: ubuntu-latest + # name: 'ubuntu-latest (x86_64)' + # arch: aarch64 + # mode: cross-aarch64 + # nix_shell: ci-cross-aarch64 + # - runner: ubuntu-latest + # name: 'ubuntu-latest (x86_64)' + # arch: aarch64_be + # mode: cross-aarch64_be + # nix_shell: ci-cross-aarch64_be + # exclude: + # - {external: true, + # target: { + # runner: ubuntu-24.04-arm, + # name: 'ubuntu-latest (aarch64)', + # arch: aarch64, + # mode: native, + # nix_shell: ci + # }} + # - {external: true, + # target: { + # runner: ubuntu-24.04-arm, + # name: 'ubuntu-latest (aarch64)', + # arch: x86_64, + # mode: cross-x86_64, + # nix_shell: ci-cross-x86_64 + # }} + # - {external: true, + # target: { + # runner: ubuntu-24.04-arm, + # name: 'ubuntu-latest (aarch64)', + # arch: riscv64, + # mode: cross-riscv64, + # nix_shell: ci-cross-riscv64 + # }} + # - {external: true, + # target: { + # runner: ubuntu-24.04-arm, + # name: 'ubuntu-latest (aarch64)', + # arch: riscv32, + # mode: cross-riscv32, + # nix_shell: ci-cross-riscv32 + # }} + # - {external: true, + # target: { + # runner: ubuntu-24.04-arm, + # name: 'ubuntu-latest (ppc64le)', + # arch: ppc64le, + # mode: cross-ppc64le, + # nix_shell: ci-cross-ppc64le + # }} + # - {external: true, + # target: { + # runner: ubuntu-latest, + # name: 'ubuntu-latest (x86_64)', + # arch: x86_64, + # mode: native, + # nix_shell: ci + # }} + # - {external: true, + # target: { + # runner: ubuntu-latest, + # name: 'ubuntu-latest (x86_64)', + # arch: aarch64, + # mode: cross-aarch64, + # nix_shell: ci-cross-aarch64 + # }} + # - {external: true, + # target: { + # runner: ubuntu-latest, + # name: 'ubuntu-latest (x86_64)', + # arch: aarch64_be, + # mode: cross-aarch64_be, + # nix_shell: ci-cross-aarch64_be + # }} + # name: Functional tests (${{ matrix.target.arch }}${{ matrix.target.mode != 'native' && ', cross' || ''}}) + # runs-on: ${{ matrix.target.runner }} + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - name: build + test (no-opt) + # uses: ./.github/actions/multi-functest + # with: + # nix-shell: ${{ matrix.target.nix_shell }} + # nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }} + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: ${{ matrix.target.mode }} + # opt: 'no_opt' + # - name: build + test (+debug+memsan+ubsan, native) + # uses: ./.github/actions/multi-functest + # if: ${{ matrix.target.mode == 'native' }} + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: native + # cflags: "-DMLDSA_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # check_namespace: 'false' + # - name: build + test (cross, opt) + # uses: ./.github/actions/multi-functest + # # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests + # if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }} + # with: + # nix-shell: ${{ matrix.target.nix_shell }} + # nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }} + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: ${{ matrix.target.mode }} + # opt: 'opt' + # - name: build + test (cross, opt, +debug) + # uses: ./.github/actions/multi-functest + # # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests + # if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }} + # with: + # nix-shell: ${{ matrix.target.nix_shell }} + # nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }} + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: ${{ matrix.target.mode }} + # cflags: "-DMLDSA_DEBUG" + # opt: 'opt' + # backend_tests: + # name: AArch64 FIPS202 backends (${{ matrix.backend }}) + # strategy: + # fail-fast: false + # matrix: + # backend: [x1_scalar, x1_v84a, x2_v84a, x4_v8a_scalar, x4_v8a_v84a_scalar] + # runs-on: macos-latest + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - name: build + test + # uses: ./.github/actions/multi-functest + # with: + # nix-shell: 'ci' + # nix-cache: 'false' + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: 'native' + # opt: 'opt' + # examples: 'false' + # cflags: "-DMLDSA_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all" + # check_namespace: 'false' + # extra_args: "--fips202-aarch64-backend ${{ matrix.backend }}" + # compiler_tests: + # name: Compiler tests (${{ matrix.compiler.name }}, ${{ matrix.target.name }}, ${{ matrix.cflags }}) + # strategy: + # fail-fast: false + # matrix: + # cflags: [ "-O0", "-Os", "-O3" ] + # target: + # - runner: ubuntu-24.04-arm + # name: 'aarch64' + # - runner: ubuntu-latest + # name: 'x86_64' + # - runner: macos-latest + # name: 'macos' + # compiler: + # - name: gcc-4.8 + # shell: ci_gcc48 + # darwin: False + # c17: False + # c23: False + # opt: all + # examples: true + # - name: gcc-4.9 + # shell: ci_gcc49 + # darwin: False + # c17: False + # c23: False + # opt: all + # examples: true + # - name: gcc-7 + # shell: ci_gcc7 + # darwin: False + # c17: False + # c23: False + # opt: all + # examples: true + # - name: gcc-11 + # shell: ci_gcc11 + # darwin: True + # c17: True + # c23: False + # opt: all + # examples: true + # - name: gcc-13 + # shell: ci_gcc13 + # darwin: True + # c17: True + # c23: False + # opt: all + # examples: true + # - name: gcc-14 + # shell: ci_gcc14 + # darwin: True + # c17: True + # c23: True + # opt: all + # examples: true + # - name: gcc-15 + # shell: ci_gcc15 + # # TODO: Add this once gcc15 is supported in nix on aarch64-Darwin + # darwin: False + # c17: True + # c23: True + # opt: all + # examples: true + # - name: clang-18 + # shell: ci_clang18 + # darwin: True + # c17: True + # c23: True + # opt: all + # examples: true + # - name: clang-19 + # shell: ci_clang19 + # darwin: True + # c17: True + # c23: True + # opt: all + # examples: true + # - name: clang-20 + # shell: ci_clang20 + # darwin: True + # c17: True + # c23: True + # opt: all + # examples: true + # - name: clang-21 + # shell: ci_clang21 + # darwin: True + # c17: True + # c23: True + # opt: all + # examples: true + # # CPU flags are not correctly passed to the zig assembler + # # https://github.com/ziglang/zig/issues/23576 + # # We therefore only test the C backend + # # + # # We omit all examples since there is currently no way to run + # # only those examples not involving native code. + # - name: zig-0.12 + # shell: ci_zig0_12 + # darwin: True + # c17: True + # c23: False + # examples: False + # opt: no_opt + # - name: zig-0.13 + # shell: ci_zig0_13 + # darwin: True + # c17: True + # c23: False + # examples: False + # opt: no_opt + # - name: zig-0.14 + # shell: ci_zig0_14 + # darwin: True + # c17: True + # c23: True + # examples: False + # opt: no_opt + # - name: zig-0.15 + # shell: ci_zig0_15 + # darwin: True + # c17: True + # c23: True + # examples: False + # opt: no_opt + # runs-on: ${{ matrix.target.runner }} + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - 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 + # kat: false + # acvp: false + # examples: ${{ matrix.compiler.examples }} + # opt: ${{ matrix.compiler.opt }} + # nix-shell: ${{ matrix.compiler.shell }} + # cflags: "${{ matrix.cflags }}" + # - 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 + # kat: false + # acvp: false + # examples: ${{ matrix.compiler.examples }} + # opt: ${{ matrix.compiler.opt }} + # nix-shell: ${{ matrix.compiler.shell }} + # cflags: "-std=c90 ${{ matrix.cflags }}" + # - 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 + # kat: false + # acvp: false + # examples: ${{ matrix.compiler.examples }} + # opt: ${{ matrix.compiler.opt }} + # nix-shell: ${{ matrix.compiler.shell }} + # cflags: "-std=c99 ${{ matrix.cflags }}" + # - 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 + # kat: false + # acvp: false + # examples: ${{ matrix.compiler.examples }} + # opt: ${{ matrix.compiler.opt }} + # nix-shell: ${{ matrix.compiler.shell }} + # cflags: "-std=c11 ${{ matrix.cflags }}" + # - 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 + # kat: false + # acvp: false + # examples: ${{ matrix.compiler.examples }} + # opt: ${{ matrix.compiler.opt }} + # nix-shell: ${{ matrix.compiler.shell }} + # cflags: "-std=c17 ${{ matrix.cflags }}" + # - name: native build+functest (C23) + # if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') && + # matrix.compiler.c23 }} + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: native + # func: true + # kat: false + # acvp: false + # examples: ${{ matrix.compiler.examples }} + # opt: ${{ matrix.compiler.opt }} + # nix-shell: ${{ matrix.compiler.shell }} + # cflags: "-std=c23 ${{ matrix.cflags }}" + # stack_analysis: + # name: Stack analysis (${{ matrix.target.name }}, ${{ matrix.cflags }}) + # strategy: + # fail-fast: false + # matrix: + # external: + # - ${{ github.repository_owner != 'pq-code-package' }} + # target: + # - runner: ubuntu-latest + # name: x86_64 + # - runner: ubuntu-24.04-arm + # name: aarch64 + # cflags: ['-O3', '-Os'] + # exclude: + # - external: true + # runs-on: ${{ matrix.target.runner }} + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - name: Stack analysis + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: native + # nix-shell: ci_valgrind-varlat_gcc15 + # nix-cache: false + # opt: all + # cflags: "${{ matrix.cflags }}" + # func: false + # kat: false + # acvp: false + # examples: false + # stack: true + # check_namespace: false config_variations: name: Non-standard configurations strategy: @@ -468,269 +468,269 @@ jobs: uses: ./.github/actions/config-variations with: gh_token: ${{ secrets.GITHUB_TOKEN }} - check-cf-protections: - name: Test control-flow protections (${{ matrix.compiler.name }}, x86_64) - strategy: - fail-fast: false - matrix: - compiler: - - name: gcc-14 - shell: ci_gcc14 - - name: gcc-15 - shell: ci_gcc15 - - name: clang-19 - shell: ci_clang19 - # On AArch64 -fcf-protection is not supported anyway - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - name: Test control-flow protections - uses: ./.github/actions/multi-functest - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - compile_mode: native - cflags: "-Wl,-z,cet-report=error -fcf-protection=full" - func: true - kat: true - acvp: true - nix-shell: ${{ matrix.compiler.shell }} - # ensure that sign.h and mldsa_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: ubuntu-24.04-arm - name: 'aarch64' - - runner: ubuntu-latest - name: 'x86_64' - exclude: - - {external: true, - target: { - runner: ubuntu-24.04-arm, - name: 'aarch64' - }} - name: Check API consistency - runs-on: ${{ matrix.target.runner }} - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - name: make quickcheck - run: | - OPT=0 CFLAGS="-Imldsa -DMLD_CHECK_APIS -Wno-redundant-decls" make quickcheck - make clean >/dev/null - OPT=1 CFLAGS="-Imldsa -DMLD_CHECK_APIS -Wno-redundant-decls" make quickcheck - - uses: ./.github/actions/setup-apt - - name: tests func - run: | - ./scripts/tests func --cflags="-Imldsa -DMLD_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 (x86_64) - ec2_volume_size: 20 - compile_mode: native - opt: all - config_variations: 'native-cap-CPUID_AVX2' - - name: Intel Xeon 4th gen (t3) - ec2_instance_type: t3.small - ec2_ami: ubuntu-latest (x86_64) - ec2_volume_size: 20 - compile_mode: native - opt: all - config_variations: 'native-cap-CPUID_AVX2' - - name: Graviton2 (c6g.medium) - ec2_instance_type: c6g.medium - ec2_ami: ubuntu-latest (aarch64) - ec2_volume_size: 20 - compile_mode: native - opt: all - config_variations: 'native-cap-ON native-cap-OFF native-cap-ID_AA64PFR1_EL1' - - name: Graviton3 (c7g.medium) - ec2_instance_type: c7g.medium - ec2_ami: ubuntu-latest (aarch64) - ec2_volume_size: 20 - compile_mode: native - opt: all - config_variations: 'native-cap-ID_AA64PFR1_EL1' - name: Platform tests (${{ matrix.target.name }}) - permissions: - contents: 'read' - id-token: 'write' - 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 }} - config_variations: ${{ matrix.target.config_variations || '' }} - functest: true - kattest: 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 - - id: nixos/nix:latest - nix_shell: 'nix-shell -p python3 gcc gnumake perl' - name: Compatibility tests (${{ matrix.container.id }}) - runs-on: ubuntu-latest - 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. + # check-cf-protections: + # name: Test control-flow protections (${{ matrix.compiler.name }}, x86_64) + # strategy: + # fail-fast: false + # matrix: + # compiler: + # - name: gcc-14 + # shell: ci_gcc14 + # - name: gcc-15 + # shell: ci_gcc15 + # - name: clang-19 + # shell: ci_clang19 + # # On AArch64 -fcf-protection is not supported anyway + # runs-on: ubuntu-latest + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - name: Test control-flow protections + # uses: ./.github/actions/multi-functest + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # compile_mode: native + # cflags: "-Wl,-z,cet-report=error -fcf-protection=full" + # func: true + # kat: true + # acvp: true + # nix-shell: ${{ matrix.compiler.shell }} + # # ensure that sign.h and mldsa_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: ubuntu-24.04-arm + # name: 'aarch64' + # - runner: ubuntu-latest + # name: 'x86_64' + # exclude: + # - {external: true, + # target: { + # runner: ubuntu-24.04-arm, + # name: 'aarch64' + # }} + # name: Check API consistency + # runs-on: ${{ matrix.target.runner }} + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - name: make quickcheck + # run: | + # OPT=0 CFLAGS="-Imldsa -DMLD_CHECK_APIS -Wno-redundant-decls" make quickcheck + # make clean >/dev/null + # OPT=1 CFLAGS="-Imldsa -DMLD_CHECK_APIS -Wno-redundant-decls" make quickcheck + # - uses: ./.github/actions/setup-apt + # - name: tests func + # run: | + # ./scripts/tests func --cflags="-Imldsa -DMLD_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 (x86_64) + # ec2_volume_size: 20 + # compile_mode: native + # opt: all + # config_variations: 'native-cap-CPUID_AVX2' + # - name: Intel Xeon 4th gen (t3) + # ec2_instance_type: t3.small + # ec2_ami: ubuntu-latest (x86_64) + # ec2_volume_size: 20 + # compile_mode: native + # opt: all + # config_variations: 'native-cap-CPUID_AVX2' + # - name: Graviton2 (c6g.medium) + # ec2_instance_type: c6g.medium + # ec2_ami: ubuntu-latest (aarch64) + # ec2_volume_size: 20 + # compile_mode: native + # opt: all + # config_variations: 'native-cap-ON native-cap-OFF native-cap-ID_AA64PFR1_EL1' + # - name: Graviton3 (c7g.medium) + # ec2_instance_type: c7g.medium + # ec2_ami: ubuntu-latest (aarch64) + # ec2_volume_size: 20 + # compile_mode: native + # opt: all + # config_variations: 'native-cap-ID_AA64PFR1_EL1' + # name: Platform tests (${{ matrix.target.name }}) + # permissions: + # contents: 'read' + # id-token: 'write' + # 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 }} + # config_variations: ${{ matrix.target.config_variations || '' }} + # functest: true + # kattest: 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 + # - id: nixos/nix:latest + # nix_shell: 'nix-shell -p python3 gcc gnumake perl' + # name: Compatibility tests (${{ matrix.container.id }}) + # runs-on: ubuntu-latest + # 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 + # # 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 - shell: bash - run: | - if [ -n "${{ matrix.container.nix_shell }}" ]; then - ${{ matrix.container.nix_shell }} --run "CC=gcc OPT=0 make quickcheck && make clean >/dev/null && CC=gcc OPT=1 make quickcheck" - else - CC=gcc OPT=0 make quickcheck - make clean >/dev/null - CC=gcc OPT=1 make quickcheck - fi - - name: Functional Tests - uses: ./.github/actions/multi-functest - with: - nix-shell: "" - custom_shell: ${{ matrix.container.nix_shell && format('{0} --run \"bash -e {{0}}\"', matrix.container.nix_shell) || 'bash' }} - gh_token: ${{ secrets.GITHUB_TOKEN }} - ec2_compatibilitytests: - strategy: - max-parallel: 8 - fail-fast: false - matrix: - container: - - id: amazonlinux-2-aarch:base - # TODO: Python 3.7 on Amazon Linux 2 lacks `sha512_224` in hashlib; set to false to skip acvp. - quickcheck: false - acvptest: false - - id: amazonlinux-2-aarch:gcc-7x - # TODO: Python 3.7 on Amazon Linux 2 lacks `sha512_224` in hashlib; set to false to skip acvp. - quickcheck: false - acvptest: false - - id: amazonlinux-2-aarch:clang-7x - # TODO: Python 3.7 on Amazon Linux 2 lacks `sha512_224` in hashlib; set to false to skip acvp. - quickcheck: false - acvptest: false - - id: amazonlinux-2023-aarch:base - quickcheck: true - acvptest: true - - id: amazonlinux-2023-aarch:gcc-11x - quickcheck: true - acvptest: true - - id: amazonlinux-2023-aarch:clang-15x - quickcheck: true - acvptest: true - - id: amazonlinux-2023-aarch:clang-15x-sanitizer - quickcheck: true - acvptest: true - # - id: amazonlinux-2023-aarch:cryptofuzz Not yet supported - - id: ubuntu-22.04-aarch:gcc-12x - quickcheck: true - acvptest: true - - id: ubuntu-22.04-aarch:gcc-11x - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:gcc-8x - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:gcc-7x - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:clang-9x - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:clang-8x - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:clang-7x-bm-framework - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:clang-7x - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:clang-10x - quickcheck: true - acvptest: true - - id: ubuntu-22.04-aarch:base - quickcheck: true - acvptest: true - - id: ubuntu-20.04-aarch:base - quickcheck: true - acvptest: true - name: Compatibility tests (${{ matrix.container.id }}) - 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 - acvptest: ${{ matrix.container.acvptest }} - quickcheck: ${{ matrix.container.quickcheck }} - lint: false - verbose: true - cflags: "-O0" - secrets: inherit - check_autogenerated_files: - strategy: - fail-fast: false - matrix: - system: [ubuntu-latest, ubuntu-24.04-arm] - runs-on: ${{ matrix.system }} - name: Check autogenerated files - steps: - - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 - - uses: ./.github/actions/setup-shell - with: - nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification - nix-cache: 'true' - gh_token: ${{ secrets.GITHUB_TOKEN }} - script: | - python3 ./scripts/autogen --dry-run --force-cross + # 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 + # shell: bash + # run: | + # if [ -n "${{ matrix.container.nix_shell }}" ]; then + # ${{ matrix.container.nix_shell }} --run "CC=gcc OPT=0 make quickcheck && make clean >/dev/null && CC=gcc OPT=1 make quickcheck" + # else + # CC=gcc OPT=0 make quickcheck + # make clean >/dev/null + # CC=gcc OPT=1 make quickcheck + # fi + # - name: Functional Tests + # uses: ./.github/actions/multi-functest + # with: + # nix-shell: "" + # custom_shell: ${{ matrix.container.nix_shell && format('{0} --run \"bash -e {{0}}\"', matrix.container.nix_shell) || 'bash' }} + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # ec2_compatibilitytests: + # strategy: + # max-parallel: 8 + # fail-fast: false + # matrix: + # container: + # - id: amazonlinux-2-aarch:base + # # TODO: Python 3.7 on Amazon Linux 2 lacks `sha512_224` in hashlib; set to false to skip acvp. + # quickcheck: false + # acvptest: false + # - id: amazonlinux-2-aarch:gcc-7x + # # TODO: Python 3.7 on Amazon Linux 2 lacks `sha512_224` in hashlib; set to false to skip acvp. + # quickcheck: false + # acvptest: false + # - id: amazonlinux-2-aarch:clang-7x + # # TODO: Python 3.7 on Amazon Linux 2 lacks `sha512_224` in hashlib; set to false to skip acvp. + # quickcheck: false + # acvptest: false + # - id: amazonlinux-2023-aarch:base + # quickcheck: true + # acvptest: true + # - id: amazonlinux-2023-aarch:gcc-11x + # quickcheck: true + # acvptest: true + # - id: amazonlinux-2023-aarch:clang-15x + # quickcheck: true + # acvptest: true + # - id: amazonlinux-2023-aarch:clang-15x-sanitizer + # quickcheck: true + # acvptest: true + # # - id: amazonlinux-2023-aarch:cryptofuzz Not yet supported + # - id: ubuntu-22.04-aarch:gcc-12x + # quickcheck: true + # acvptest: true + # - id: ubuntu-22.04-aarch:gcc-11x + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:gcc-8x + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:gcc-7x + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:clang-9x + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:clang-8x + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:clang-7x-bm-framework + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:clang-7x + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:clang-10x + # quickcheck: true + # acvptest: true + # - id: ubuntu-22.04-aarch:base + # quickcheck: true + # acvptest: true + # - id: ubuntu-20.04-aarch:base + # quickcheck: true + # acvptest: true + # name: Compatibility tests (${{ matrix.container.id }}) + # 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 + # acvptest: ${{ matrix.container.acvptest }} + # quickcheck: ${{ matrix.container.quickcheck }} + # lint: false + # verbose: true + # cflags: "-O0" + # secrets: inherit + # check_autogenerated_files: + # strategy: + # fail-fast: false + # matrix: + # system: [ubuntu-latest, ubuntu-24.04-arm] + # runs-on: ${{ matrix.system }} + # name: Check autogenerated files + # steps: + # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 + # - uses: ./.github/actions/setup-shell + # with: + # nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification + # nix-cache: 'true' + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # script: | + # python3 ./scripts/autogen --dry-run --force-cross diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index b1208440b..96a5d55a2 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -108,6 +108,91 @@ /*************************************************** * Convenience macros for common contract patterns ***************************************************/ + +/* Helper to chain conditions with && */ +#define _OBJS_NO_ALIAS_1(x) memory_no_alias((x), sizeof(*(x))) +#define _OBJS_NO_ALIAS_2(x, y) \ + (_OBJS_NO_ALIAS_1(x) && _OBJS_NO_ALIAS_1(y)) +#define _OBJS_NO_ALIAS_3(x, y, z) \ + (_OBJS_NO_ALIAS_2(x, y) && _OBJS_NO_ALIAS_1(z)) +#define _OBJS_NO_ALIAS_4(x, y, z, w) \ + (_OBJS_NO_ALIAS_3(x, y, z) && _OBJS_NO_ALIAS_1(w)) +#define _OBJS_NO_ALIAS_5(x, y, z, w, v) \ + (_OBJS_NO_ALIAS_4(x, y, z, w) && _OBJS_NO_ALIAS_1(v)) +#define _OBJS_NO_ALIAS_6(x, y, z, w, v, u) \ + (_OBJS_NO_ALIAS_5(x, y, z, w, v) && _OBJS_NO_ALIAS_1(u)) +#define _OBJS_NO_ALIAS_7(x, y, z, w, v, u, t) \ + (_OBJS_NO_ALIAS_6(x, y, z, w, v, u) && _OBJS_NO_ALIAS_1(t)) +#define _OBJS_NO_ALIAS_8(x, y, z, w, v, u, t, s) \ + (_OBJS_NO_ALIAS_7(x, y, z, w, v, u, t) && _OBJS_NO_ALIAS_1(s)) +#define _OBJS_NO_ALIAS_9(x, y, z, w, v, u, t, s, r) \ + (_OBJS_NO_ALIAS_8(x, y, z, w, v, u, t, s) && _OBJS_NO_ALIAS_1(r)) +#define _OBJS_NO_ALIAS_10(x, y, z, w, v, u, t, s, r, q) \ + (_OBJS_NO_ALIAS_9(x, y, z, w, v, u, t, s, r) && _OBJS_NO_ALIAS_1(q)) + +#define _GET_OBJS_MACRO(_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,NAME,...) NAME +#define objs_no_alias(...) \ + _GET_OBJS_MACRO(__VA_ARGS__, _OBJS_NO_ALIAS_10, _OBJS_NO_ALIAS_9, \ + _OBJS_NO_ALIAS_8, _OBJS_NO_ALIAS_7, _OBJS_NO_ALIAS_6, \ + _OBJS_NO_ALIAS_5, _OBJS_NO_ALIAS_4, _OBJS_NO_ALIAS_3, \ + _OBJS_NO_ALIAS_2, _OBJS_NO_ALIAS_1)(__VA_ARGS__) + +#define _ARRAYS_NO_ALIAS_1(x, sz) memory_no_alias((x), (sz)) +#define _ARRAYS_NO_ALIAS_2(x0, sz0, x1, sz1) \ + (_ARRAYS_NO_ALIAS_1(x0, sz0) && _ARRAYS_NO_ALIAS_1(x1, sz1)) +#define _ARRAYS_NO_ALIAS_3(x0, sz0, x1, sz1, x2, sz2) \ + (_ARRAYS_NO_ALIAS_2(x0, sz0, x1, sz1) && _ARRAYS_NO_ALIAS_1(x2, sz2)) +#define _ARRAYS_NO_ALIAS_4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \ + (_ARRAYS_NO_ALIAS_3(x0, sz0, x1, sz1, x2, sz2) && \ + _ARRAYS_NO_ALIAS_1(x3, sz3)) +#define _ARRAYS_NO_ALIAS_5(x0, sz0, x1, sz1, x2, sz2, x3, sz3, x4, sz4) \ + (_ARRAYS_NO_ALIAS_4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) && \ + _ARRAYS_NO_ALIAS_1(x4, sz4)) + +#define _GET_ARRAYS_MACRO(_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,NAME,...) NAME +#define arrays_no_alias(...) \ + _GET_ARRAYS_MACRO(__VA_ARGS__, _ARRAYS_NO_ALIAS_5, _dummy, \ + _ARRAYS_NO_ALIAS_4, _dummy, _ARRAYS_NO_ALIAS_3, _dummy, \ + _ARRAYS_NO_ALIAS_2, _dummy, _ARRAYS_NO_ALIAS_1)(__VA_ARGS__) + +/* Helper to chain assigns clauses */ +#define _ASSIGNS_OBJS_1(x) assigns(memory_slice((x), sizeof(*(x)))) +#define _ASSIGNS_OBJS_2(x, y) _ASSIGNS_OBJS_1(x) _ASSIGNS_OBJS_1(y) +#define _ASSIGNS_OBJS_3(x, y, z) \ + _ASSIGNS_OBJS_2(x, y) _ASSIGNS_OBJS_1(z) +#define _ASSIGNS_OBJS_4(x, y, z, w) \ + _ASSIGNS_OBJS_3(x, y, z) _ASSIGNS_OBJS_1(w) +#define _ASSIGNS_OBJS_5(x, y, z, w, v) \ + _ASSIGNS_OBJS_4(x, y, z, w) _ASSIGNS_OBJS_1(v) +#define _ASSIGNS_OBJS_6(x, y, z, w, v, u) \ + _ASSIGNS_OBJS_5(x, y, z, w, v) _ASSIGNS_OBJS_1(u) +#define _ASSIGNS_OBJS_7(x, y, z, w, v, u, t) \ + _ASSIGNS_OBJS_6(x, y, z, w, v, u) _ASSIGNS_OBJS_1(t) +#define _ASSIGNS_OBJS_8(x, y, z, w, v, u, t, s) \ + _ASSIGNS_OBJS_7(x, y, z, w, v, u, t) _ASSIGNS_OBJS_1(s) + +#define assigns_objs(...) \ + _GET_OBJS_MACRO(__VA_ARGS__, _dummy, _dummy, _ASSIGNS_OBJS_8, \ + _ASSIGNS_OBJS_7, _ASSIGNS_OBJS_6, _ASSIGNS_OBJS_5, \ + _ASSIGNS_OBJS_4, _ASSIGNS_OBJS_3, _ASSIGNS_OBJS_2, \ + _ASSIGNS_OBJS_1)(__VA_ARGS__) + +#define _ASSIGNS_ARRS_1(x, sz) assigns(memory_slice((x), (sz))) +#define _ASSIGNS_ARRS_2(x0, sz0, x1, sz1) \ + _ASSIGNS_ARRS_1(x0, sz0) _ASSIGNS_ARRS_1(x1, sz1) +#define _ASSIGNS_ARRS_3(x0, sz0, x1, sz1, x2, sz2) \ + _ASSIGNS_ARRS_2(x0, sz0, x1, sz1) _ASSIGNS_ARRS_1(x2, sz2) +#define _ASSIGNS_ARRS_4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \ + _ASSIGNS_ARRS_3(x0, sz0, x1, sz1, x2, sz2) _ASSIGNS_ARRS_1(x3, sz3) +#define _ASSIGNS_ARRS_5(x0, sz0, x1, sz1, x2, sz2, x3, sz3, x4, sz4) \ + _ASSIGNS_ARRS_4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \ + _ASSIGNS_ARRS_1(x4, sz4) + +#define assigns_arrs(...) \ + _GET_ARRAYS_MACRO(__VA_ARGS__, _ASSIGNS_ARRS_5, _dummy, \ + _ASSIGNS_ARRS_4, _dummy, _ASSIGNS_ARRS_3, _dummy, \ + _ASSIGNS_ARRS_2, _dummy, _ASSIGNS_ARRS_1)(__VA_ARGS__) + /* * Prevent clang-format from corrupting CBMC's special ==> operator */ diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 944c9477b..74b4f5812 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -49,6 +49,8 @@ #define mld_H MLD_ADD_PARAM_SET(mld_H) #define mld_attempt_signature_generation \ MLD_ADD_PARAM_SET(mld_attempt_signature_generation) +#define mld_attempt_signature_generation_alloc \ + MLD_ADD_PARAM_SET(mld_attempt_signature_generation_alloc) #define mld_compute_t0_t1_tr_from_sk_components \ MLD_ADD_PARAM_SET(mld_compute_t0_t1_tr_from_sk_components) /* End of parameter set namespacing */ @@ -432,73 +434,34 @@ __contract__( /* @[FIPS204, Appendix C]. */ #define MLD_NONCE_UB ((UINT16_MAX - MLDSA_L) / MLDSA_L) -/************************************************* - * Name: attempt_signature_generation - * - * Description: Attempts to generate a single signature. - * - * Arguments: - uint8_t *sig: pointer to output signature - * - const uint8_t *mu: pointer to message or hash - * of exactly MLDSA_CRHBYTES bytes - * - const uint8_t *rhoprime: pointer to randomness seed - * - uint16_t nonce: current nonce value - * - const mld_polymat *mat: expanded matrix - * - const polyvecl *s1: secret vector s1 - * - const polyveck *s2: secret vector s2 - * - const polyveck *t0: vector t0 - * - * Returns: - 0: Signature generation succeeded - * - MLD_ERR_FAIL: Signature rejected (norm check failed) - * - MLD_ERR_OUT_OF_MEMORY: If MLD_CONFIG_CUSTOM_ALLOC_FREE is - * used and an allocation via MLD_CUSTOM_ALLOC returned NULL. - * - * Reference: This code differs from the reference implementation - * in that it factors out the core signature generation - * step into a distinct function here in order to improve - * efficiency of CBMC proof. - **************************************************/ + MLD_MUST_CHECK_RETURN_VALUE -static int mld_attempt_signature_generation( +static int mld_attempt_signature_generation_alloc( uint8_t sig[MLDSA_CRYPTO_BYTES], const uint8_t *mu, const uint8_t rhoprime[MLDSA_CRHBYTES], uint16_t nonce, const mld_polymat *mat, const mld_polyvecl *s1, const mld_polyveck *s2, - const mld_polyveck *t0) + const mld_polyveck *t0, uint8_t challenge_bytes[MLDSA_CTILDEBYTES], + mld_polyvecl *y, mld_polyveck *h, mld_polyvecl *z, mld_polyveck *w1, + mld_polyveck *w0, mld_poly *cp) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(mu, MLDSA_CRHBYTES)) - requires(memory_no_alias(rhoprime, MLDSA_CRHBYTES)) - requires(memory_no_alias(mat, sizeof(mld_polymat))) - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) - requires(memory_no_alias(t0, sizeof(mld_polyveck))) + requires(arrays_no_alias(sig, MLDSA_CRYPTO_BYTES, mu, MLDSA_CRHBYTES, + rhoprime, MLDSA_CRHBYTES, challenge_bytes, MLDSA_CTILDEBYTES)) + requires(objs_no_alias(mat, s1, s2, t0, h, z, w1, w0, cp)) + requires((void*) y == (void*) h) requires(nonce <= MLD_NONCE_UB) requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) requires(forall(k2, 0, MLDSA_K, array_abs_bound(t0->vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) requires(forall(k3, 0, MLDSA_L, array_abs_bound(s1->vec[k3].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) requires(forall(k4, 0, MLDSA_K, array_abs_bound(s2->vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns_arrs(sig, MLDSA_CRYPTO_BYTES, challenge_bytes, MLDSA_CTILDEBYTES) + assigns_objs(h, y, z, w1, w0, cp) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ) { unsigned int n; uint32_t z_invalid, w0_invalid, h_invalid; - int ret; - MLD_ALLOC(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES); - MLD_ALLOC(y, mld_polyvecl, 1); - MLD_ALLOC(z, mld_polyvecl, 1); - MLD_ALLOC(w1, mld_polyveck, 1); - MLD_ALLOC(w0, mld_polyveck, 1); - MLD_ALLOC(h, mld_polyveck, 1); - MLD_ALLOC(cp, mld_poly, 1); - - if (challenge_bytes == NULL || y == NULL || z == NULL || w1 == NULL || - w0 == NULL || h == NULL || cp == NULL) - { - ret = MLD_ERR_OUT_OF_MEMORY; - goto cleanup; - } /* Sample intermediate vector y */ mld_polyvecl_uniform_gamma1(y, rhoprime, nonce); @@ -540,8 +503,7 @@ __contract__( MLD_CT_TESTING_DECLASSIFY(&z_invalid, sizeof(uint32_t)); if (z_invalid) { - ret = MLD_ERR_FAIL; /* reject */ - goto cleanup; + return MLD_ERR_FAIL; /* reject */ } /* If z is valid, then its coefficients are bounded by */ @@ -562,8 +524,7 @@ __contract__( MLD_CT_TESTING_DECLASSIFY(&w0_invalid, sizeof(uint32_t)); if (w0_invalid) { - ret = MLD_ERR_FAIL; /* reject */ - goto cleanup; + return MLD_ERR_FAIL; /* reject */ } /* Compute hints for w1 */ @@ -576,8 +537,7 @@ __contract__( MLD_CT_TESTING_DECLASSIFY(&h_invalid, sizeof(uint32_t)); if (h_invalid) { - ret = MLD_ERR_FAIL; /* reject */ - goto cleanup; + return MLD_ERR_FAIL; /* reject */ } mld_polyveck_add(w0, h); @@ -595,8 +555,7 @@ __contract__( n = mld_polyveck_make_hint(h, w0, w1); if (n > MLDSA_OMEGA) { - ret = MLD_ERR_FAIL; /* reject */ - goto cleanup; + return MLD_ERR_FAIL; /* reject */ } /* All is well - write signature */ @@ -606,16 +565,88 @@ __contract__( MLD_CT_TESTING_DECLASSIFY(z, sizeof(*z)); mld_pack_sig(sig, challenge_bytes, z, h, n); - ret = 0; /* success */ + return 0; /* success */ +} + +/************************************************* + * Name: attempt_signature_generation + * + * Description: Attempts to generate a single signature. + * + * Arguments: - uint8_t *sig: pointer to output signature + * - const uint8_t *mu: pointer to message or hash + * of exactly MLDSA_CRHBYTES bytes + * - const uint8_t *rhoprime: pointer to randomness seed + * - uint16_t nonce: current nonce value + * - const mld_polymat *mat: expanded matrix + * - const polyvecl *s1: secret vector s1 + * - const polyveck *s2: secret vector s2 + * - const polyveck *t0: vector t0 + * + * Returns: - 0: Signature generation succeeded + * - MLD_ERR_FAIL: Signature rejected (norm check failed) + * - MLD_ERR_OUT_OF_MEMORY: If MLD_CONFIG_CUSTOM_ALLOC_FREE is + * used and an allocation via MLD_CUSTOM_ALLOC returned NULL. + * + * Reference: This code differs from the reference implementation + * in that it factors out the core signature generation + * step into a distinct function here in order to improve + * efficiency of CBMC proof. + **************************************************/ +MLD_MUST_CHECK_RETURN_VALUE +static int mld_attempt_signature_generation( + uint8_t sig[MLDSA_CRYPTO_BYTES], const uint8_t *mu, + const uint8_t rhoprime[MLDSA_CRHBYTES], uint16_t nonce, + const mld_polymat *mat, const mld_polyvecl *s1, const mld_polyveck *s2, + const mld_polyveck *t0) +__contract__( + requires(arrays_no_alias(sig, MLDSA_CRYPTO_BYTES, mu, MLDSA_CRHBYTES, + rhoprime, MLDSA_CRHBYTES)) + requires(objs_no_alias(mat, s1, s2, t0)) + requires(nonce <= MLD_NONCE_UB) + requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, + array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) + requires(forall(k2, 0, MLDSA_K, array_abs_bound(t0->vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + requires(forall(k3, 0, MLDSA_L, array_abs_bound(s1->vec[k3].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + requires(forall(k4, 0, MLDSA_K, array_abs_bound(s2->vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + assigns_arrs(sig, MLDSA_CRYPTO_BYTES) + ensures(return_value == 0 || return_value == MLD_ERR_FAIL || + return_value == MLD_ERR_OUT_OF_MEMORY) +) +{ + int ret; + MLD_ALLOC(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES); + typedef union + { + mld_polyvecl y; + mld_polyveck h; + } u_yh; + MLD_ALLOC(yh, u_yh, 1); + MLD_ALLOC(z, mld_polyvecl, 1); + MLD_ALLOC(w1, mld_polyveck, 1); + MLD_ALLOC(w0, mld_polyveck, 1); + MLD_ALLOC(cp, mld_poly, 1); + mld_polyvecl *y = &yh->y; + mld_polyveck *h = &yh->h; + + if (challenge_bytes == NULL || y == NULL || z == NULL || w1 == NULL || + w0 == NULL || h == NULL || cp == NULL) + { + ret = MLD_ERR_OUT_OF_MEMORY; + goto cleanup; + } + + ret = mld_attempt_signature_generation_alloc(sig, mu, rhoprime, nonce, mat, + s1, s2, t0, challenge_bytes, y, + h, z, w1, w0, cp); cleanup: /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ MLD_FREE(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES); - MLD_FREE(y, mld_polyvecl, 1); + MLD_FREE(yh, u_yh, 1); MLD_FREE(z, mld_polyvecl, 1); MLD_FREE(w1, mld_polyveck, 1); MLD_FREE(w0, mld_polyveck, 1); - MLD_FREE(h, mld_polyveck, 1); MLD_FREE(cp, mld_poly, 1); return ret; diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile index dc518af3d..4b53679b0 100644 --- a/proofs/cbmc/attempt_signature_generation/Makefile +++ b/proofs/cbmc/attempt_signature_generation/Makefile @@ -20,29 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c CHECK_FUNCTION_CONTRACTS=mld_attempt_signature_generation -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \ - $(MLD_NAMESPACE)polyvecl_ntt \ - $(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery \ - $(MLD_NAMESPACE)polyveck_reduce \ - $(MLD_NAMESPACE)polyveck_invntt_tomont \ - $(MLD_NAMESPACE)polyveck_caddq \ - $(MLD_NAMESPACE)polyveck_decompose \ - $(MLD_NAMESPACE)polyveck_pack_w1 \ - mld_H \ - $(MLD_NAMESPACE)poly_challenge \ - $(MLD_NAMESPACE)poly_ntt \ - $(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery \ - $(MLD_NAMESPACE)polyvecl_invntt_tomont \ - $(MLD_NAMESPACE)polyvecl_add \ - $(MLD_NAMESPACE)polyvecl_reduce \ - $(MLD_NAMESPACE)polyvecl_chknorm \ - $(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery \ - $(MLD_NAMESPACE)polyveck_sub \ - $(MLD_NAMESPACE)polyveck_reduce \ - $(MLD_NAMESPACE)polyveck_chknorm \ - $(MLD_NAMESPACE)polyveck_add \ - $(MLD_NAMESPACE)polyveck_make_hint \ - $(MLD_NAMESPACE)pack_sig +USE_FUNCTION_CONTRACTS=mld_attempt_signature_generation_alloc USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on diff --git a/proofs/cbmc/attempt_signature_generation_alloc/Makefile b/proofs/cbmc/attempt_signature_generation_alloc/Makefile new file mode 100644 index 000000000..6213ce3d8 --- /dev/null +++ b/proofs/cbmc/attempt_signature_generation_alloc/Makefile @@ -0,0 +1,80 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = attempt_signature_generation_alloc_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = mld_attempt_signature_generation_alloc + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c + +CHECK_FUNCTION_CONTRACTS=mld_attempt_signature_generation_alloc +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \ + $(MLD_NAMESPACE)polyvecl_ntt \ + $(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery \ + $(MLD_NAMESPACE)polyveck_reduce \ + $(MLD_NAMESPACE)polyveck_invntt_tomont \ + $(MLD_NAMESPACE)polyveck_caddq \ + $(MLD_NAMESPACE)polyveck_decompose \ + $(MLD_NAMESPACE)polyveck_pack_w1 \ + mld_H \ + $(MLD_NAMESPACE)poly_challenge \ + $(MLD_NAMESPACE)poly_ntt \ + $(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery \ + $(MLD_NAMESPACE)polyvecl_invntt_tomont \ + $(MLD_NAMESPACE)polyvecl_add \ + $(MLD_NAMESPACE)polyvecl_reduce \ + $(MLD_NAMESPACE)polyvecl_chknorm \ + $(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery \ + $(MLD_NAMESPACE)polyveck_sub \ + $(MLD_NAMESPACE)polyveck_reduce \ + $(MLD_NAMESPACE)polyveck_chknorm \ + $(MLD_NAMESPACE)polyveck_add \ + $(MLD_NAMESPACE)polyveck_make_hint \ + $(MLD_NAMESPACE)pack_sig + +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3 +CBMCFLAGS += --slice-formula +CBMCFLAGS += --no-array-field-sensitivity + +FUNCTION_NAME = mld_attempt_signature_generation_alloc + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/attempt_signature_generation_alloc/attempt_signature_generation_alloc_harness.c b/proofs/cbmc/attempt_signature_generation_alloc/attempt_signature_generation_alloc_harness.c new file mode 100644 index 000000000..5b1c73845 --- /dev/null +++ b/proofs/cbmc/attempt_signature_generation_alloc/attempt_signature_generation_alloc_harness.c @@ -0,0 +1,36 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "sign.h" + +int mld_attempt_signature_generation_alloc( + uint8_t sig[MLDSA_CRYPTO_BYTES], const uint8_t *mu, + const uint8_t rhoprime[MLDSA_CRHBYTES], uint16_t nonce, + const mld_polymat *mat, const mld_polyvecl *s1, const mld_polyveck *s2, + const mld_polyveck *t0, uint8_t challenge_bytes[MLDSA_CTILDEBYTES], + mld_polyvecl *y, mld_polyveck *h, mld_polyvecl *z, mld_polyveck *w1, + mld_polyveck *w0, mld_poly *cp); + +void harness(void) +{ + uint8_t *sig; + uint8_t *mu; + uint8_t *rhoprime; + uint16_t nonce; + mld_polymat *mat; + mld_polyvecl *s1; + mld_polyveck *s2; + mld_polyveck *t0; + uint8_t *challenge_bytes; + mld_polyvecl *y; + mld_polyveck *h; + mld_polyvecl *z; + mld_polyveck *w1; + mld_polyveck *w0; + mld_poly *cp; + + int r; + r = mld_attempt_signature_generation_alloc(sig, mu, rhoprime, nonce, mat, s1, + s2, t0, challenge_bytes, y, h, z, + w1, w0, cp); +}