diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml index 1afcd318e..a541f8bfa 100644 --- a/.github/workflows/all.yml +++ b/.github/workflows/all.yml @@ -20,65 +20,65 @@ 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 - ci: - name: Extended - permissions: - contents: 'read' - id-token: 'write' - needs: [ base, nix ] - uses: ./.github/workflows/ci.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 ] + # uses: ./.github/workflows/ci.yml + # secrets: inherit cbmc: name: CBMC 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/dev/fips202/aarch64/src/fips202_native_aarch64.h b/dev/fips202/aarch64/src/fips202_native_aarch64.h index 20f616803..e6d524a93 100644 --- a/dev/fips202/aarch64/src/fips202_native_aarch64.h +++ b/dev/fips202/aarch64/src/fips202_native_aarch64.h @@ -18,25 +18,25 @@ extern const uint64_t mld_keccakf1600_round_constants[]; #define mld_keccak_f1600_x1_scalar_asm MLD_NAMESPACE(keccak_f1600_x1_scalar_asm) void mld_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns_slices(state, sizeof(uint64_t) * 25 * 1) ); #define mld_keccak_f1600_x1_v84a_asm MLD_NAMESPACE(keccak_f1600_x1_v84a_asm) void mld_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns_slices(state, sizeof(uint64_t) * 25 * 1) ); #define mld_keccak_f1600_x2_v84a_asm MLD_NAMESPACE(keccak_f1600_x2_v84a_asm) void mld_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 2)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2)) + assigns_slices(state, sizeof(uint64_t) * 25 * 2) ); #define mld_keccak_f1600_x4_scalar_v8a_hybrid_asm \ @@ -44,9 +44,9 @@ __contract__( void mld_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns_slices(state, sizeof(uint64_t) * 25 * 4) ); #define mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm \ @@ -54,9 +54,9 @@ __contract__( void mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns_slices(state, sizeof(uint64_t) * 25 * 4) ); #endif /* !MLD_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */ diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index b1208440b..87806067e 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -108,6 +108,84 @@ /*************************************************** * Convenience macros for common contract patterns ***************************************************/ + +/* Helper to chain conditions with && */ +#define objects_no_alias1(x) memory_no_alias((x), sizeof(*(x))) +#define objects_no_alias2(x, y) (objects_no_alias1(x) && objects_no_alias1(y)) +#define objects_no_alias3(x, y, z) \ + (objects_no_alias2(x, y) && objects_no_alias1(z)) +#define objects_no_alias4(x, y, z, w) \ + (objects_no_alias3(x, y, z) && objects_no_alias1(w)) +#define objects_no_alias5(x, y, z, w, v) \ + (objects_no_alias4(x, y, z, w) && objects_no_alias1(v)) +#define objects_no_alias6(x, y, z, w, v, u) \ + (objects_no_alias5(x, y, z, w, v) && objects_no_alias1(u)) +#define objects_no_alias7(x, y, z, w, v, u, t) \ + (objects_no_alias6(x, y, z, w, v, u) && objects_no_alias1(t)) +#define objects_no_alias8(x, y, z, w, v, u, t, s) \ + (objects_no_alias7(x, y, z, w, v, u, t) && objects_no_alias1(s)) +#define objects_no_alias9(x, y, z, w, v, u, t, s, r) \ + (objects_no_alias8(x, y, z, w, v, u, t, s) && objects_no_alias1(r)) +#define objects_no_alias10(x, y, z, w, v, u, t, s, r, q) \ + (objects_no_alias9(x, y, z, w, v, u, t, s, r) && objects_no_alias1(q)) + +#define select_macro(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, NAME, ...) NAME +#define objects_no_alias(...) \ + select_macro(__VA_ARGS__, objects_no_alias10, objects_no_alias9, \ + objects_no_alias8, objects_no_alias7, objects_no_alias6, \ + objects_no_alias5, objects_no_alias4, objects_no_alias3, \ + objects_no_alias2, objects_no_alias1)(__VA_ARGS__) + +#define slices_no_alias1(x, sz) memory_no_alias((x), (sz)) +#define slices_no_alias2(x0, sz0, x1, sz1) \ + (slices_no_alias1(x0, sz0) && slices_no_alias1(x1, sz1)) +#define slices_no_alias3(x0, sz0, x1, sz1, x2, sz2) \ + (slices_no_alias2(x0, sz0, x1, sz1) && slices_no_alias1(x2, sz2)) +#define slices_no_alias4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \ + (slices_no_alias3(x0, sz0, x1, sz1, x2, sz2) && slices_no_alias1(x3, sz3)) +#define slices_no_alias5(x0, sz0, x1, sz1, x2, sz2, x3, sz3, x4, sz4) \ + (slices_no_alias4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) && \ + slices_no_alias1(x4, sz4)) + +#define get_arrs_macro(_1, _2, _3, _4, _5, NAME, ...) NAME +#define slices_no_alias(...) \ + select_macro(__VA_ARGS__, dummy10, dummy9, dummy8, dummy7, dummy6, \ + _SLICES_NO_ALIAS_5, _SLICES_NO_ALIAS_4, _SLICES_NO_ALIAS_3, \ + _SLICES_NO_ALIAS_2, _SLICES_NO_ALIAS_1)(__VA_ARGS__) + +/* Helper to chain assigns clauses */ +#define assigns_objs1(x) assigns(memory_slice((x), sizeof(*(x)))) +#define assigns_objs2(x, y) assigns_objs1(x) assigns_objs1(y) +#define assigns_objs3(x, y, z) assigns_objs2(x, y) assigns_objs1(z) +#define assigns_objs4(x, y, z, w) assigns_objs3(x, y, z) assigns_objs1(w) +#define assigns_objs5(x, y, z, w, v) assigns_objs4(x, y, z, w) assigns_objs1(v) +#define assigns_objs6(x, y, z, w, v, u) \ + assigns_objs5(x, y, z, w, v) assigns_objs1(u) +#define assigns_objs7(x, y, z, w, v, u, t) \ + assigns_objs6(x, y, z, w, v, u) assigns_objs1(t) +#define assigns_objs8(x, y, z, w, v, u, t, s) \ + assigns_objs7(x, y, z, w, v, u, t) assigns_objs1(s) + +#define assigns_objs(...) \ + select_macro(__VA_ARGS__, dummy10, dummy9, _assigns_objs8, _assigns_objs7, \ + _assigns_objs6, _assigns_objs5, _assigns_objs4, _assigns_objs3, \ + _assigns_objs2, _assigns_objs1)(__VA_ARGS__) + +#define assigns_slices1(x, sz) assigns(memory_slice((x), (sz))) +#define assigns_slices2(x0, sz0, x1, sz1) \ + assigns_slices1(x0, sz0) assigns_slices1(x1, sz1) +#define assigns_slices3(x0, sz0, x1, sz1, x2, sz2) \ + assigns_slices2(x0, sz0, x1, sz1) assigns_slices1(x2, sz2) +#define assigns_slices4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \ + assigns_slices3(x0, sz0, x1, sz1, x2, sz2) assigns_slices1(x3, sz3) +#define assigns_slices5(x0, sz0, x1, sz1, x2, sz2, x3, sz3, x4, sz4) \ + assigns_slices4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) assigns_slices1(x4, sz4) + +#define assigns_slices(...) \ + select_macro(__VA_ARGS__, dummy10, dummy9, dummy8, dummy7, dummy6, \ + assigns_slices5, assigns_slices4, assigns_slices3, \ + assigns_slices2, assigns_slices1)(__VA_ARGS__) + /* * Prevent clang-format from corrupting CBMC's special ==> operator */ diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h index 1975ebf82..14d6035c5 100644 --- a/mldsa/src/ct.h +++ b/mldsa/src/ct.h @@ -268,8 +268,7 @@ static MLD_INLINE uint8_t mld_ct_memcmp(const void *a, const void *b, const size_t len) __contract__( requires(len <= UINT16_MAX) - requires(memory_no_alias(a, len)) - requires(memory_no_alias(b, len)) + requires(slices_no_alias(a, len, b, len)) ensures((return_value == 0) == forall(i, 0, len, (((const uint8_t *)a)[i] == ((const uint8_t *)b)[i]))) ) { @@ -307,8 +306,8 @@ __contract__( **************************************************/ static MLD_INLINE void mld_zeroize(void *ptr, size_t len) __contract__( - requires(memory_no_alias(ptr, len)) - assigns(memory_slice(ptr, len)) + requires(slices_no_alias(ptr, len)) + assigns_slices(ptr, len) ); #if defined(MLD_CONFIG_CUSTOM_ZEROIZE) diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index 1112de061..1e0aef7ab 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -49,8 +49,8 @@ **************************************************/ static void keccak_init(uint64_t s[MLD_KECCAK_LANES]) __contract__( - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES) ) { mld_memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES); @@ -76,9 +76,9 @@ __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) requires(r < sizeof(uint64_t) * MLD_KECCAK_LANES) requires(pos <= r) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(in, inlen)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES, + in, inlen)) + assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES) ensures(return_value < r)) { while (inlen >= r - pos) @@ -118,8 +118,8 @@ static void keccak_finalize(uint64_t s[MLD_KECCAK_LANES], unsigned int pos, __contract__( requires(pos <= r && r < sizeof(uint64_t) * MLD_KECCAK_LANES) requires((r / 8) >= 1) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES) ) { uint8_t b = 0x80; @@ -151,10 +151,10 @@ __contract__( (r == SHAKE256_RATE && pos <= SHAKE256_RATE) || (r == SHA3_512_RATE && pos <= SHA3_512_RATE)) requires(outlen <= 8 * r /* somewhat arbitrary bound */) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(out, outlen)) + requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES, + out, outlen)) + assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES, + out, outlen) ensures(return_value <= r)) { unsigned int i; diff --git a/mldsa/src/fips202/fips202.h b/mldsa/src/fips202/fips202.h index 9f0253cb8..b2c0076a7 100644 --- a/mldsa/src/fips202/fips202.h +++ b/mldsa/src/fips202/fips202.h @@ -41,8 +41,8 @@ typedef struct **************************************************/ void mld_shake128_init(mld_shake128ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + requires(objs_no_alias(state)) + assigns_objs(state) ensures(state->pos == 0) ); @@ -61,10 +61,10 @@ void mld_shake128_absorb(mld_shake128ctx *state, const uint8_t *in, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - requires(memory_no_alias(in, inlen)) + requires(objs_no_alias(state)) + requires(slices_no_alias(in, inlen)) requires(state->pos <= SHAKE128_RATE) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + assigns_objs(state) ensures(state->pos <= SHAKE128_RATE) ); @@ -78,9 +78,9 @@ __contract__( **************************************************/ void mld_shake128_finalize(mld_shake128ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) + requires(objs_no_alias(state)) requires(state->pos <= SHAKE128_RATE) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + assigns_objs(state) ensures(state->pos <= SHAKE128_RATE) ); @@ -99,11 +99,11 @@ __contract__( void mld_shake128_squeeze(uint8_t *out, size_t outlen, mld_shake128ctx *state) __contract__( requires(outlen <= 8 * SHAKE128_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - requires(memory_no_alias(out, outlen)) + requires(objs_no_alias(state)) + requires(slices_no_alias(out, outlen)) requires(state->pos <= SHAKE128_RATE) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) - assigns(memory_slice(out, outlen)) + assigns_objs(state) + assigns_slices(out, outlen) ensures(state->pos <= SHAKE128_RATE) ); @@ -117,8 +117,8 @@ __contract__( **************************************************/ void mld_shake128_release(mld_shake128ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + requires(objs_no_alias(state)) + assigns_objs(state) ); #define mld_shake256_init MLD_NAMESPACE(shake256_init) @@ -131,8 +131,8 @@ __contract__( **************************************************/ void mld_shake256_init(mld_shake256ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + requires(objs_no_alias(state)) + assigns_objs(state) ensures(state->pos == 0) ); @@ -151,10 +151,10 @@ void mld_shake256_absorb(mld_shake256ctx *state, const uint8_t *in, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - requires(memory_no_alias(in, inlen)) + requires(objs_no_alias(state)) + requires(slices_no_alias(in, inlen)) requires(state->pos <= SHAKE256_RATE) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + assigns_objs(state) ensures(state->pos <= SHAKE256_RATE) ); @@ -168,9 +168,9 @@ __contract__( **************************************************/ void mld_shake256_finalize(mld_shake256ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) + requires(objs_no_alias(state)) requires(state->pos <= SHAKE256_RATE) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + assigns_objs(state) ensures(state->pos <= SHAKE256_RATE) ); @@ -189,11 +189,11 @@ __contract__( void mld_shake256_squeeze(uint8_t *out, size_t outlen, mld_shake256ctx *state) __contract__( requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - requires(memory_no_alias(out, outlen)) + requires(objs_no_alias(state)) + requires(slices_no_alias(out, outlen)) requires(state->pos <= SHAKE256_RATE) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(out, outlen)) + assigns_objs(state) + assigns_slices(out, outlen) ensures(state->pos <= SHAKE256_RATE) ); @@ -207,8 +207,8 @@ __contract__( **************************************************/ void mld_shake256_release(mld_shake256ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + requires(objs_no_alias(state)) + assigns_objs(state) ); #define mld_shake256 MLD_NAMESPACE(shake256) @@ -226,9 +226,8 @@ void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(in, inlen)) - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(out, outlen)) + requires(slices_no_alias(in, inlen, out, outlen)) + assigns_slices(out, outlen) ); #endif /* !MLD_FIPS202_FIPS202_H */ diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c index 0fb5cd57c..19eec6337 100644 --- a/mldsa/src/fips202/fips202x4.c +++ b/mldsa/src/fips202/fips202x4.c @@ -28,13 +28,13 @@ static void mld_keccak_absorb_once_x4(uint64_t *s, uint32_t r, size_t inlen, uint8_t p) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) requires(r <= sizeof(uint64_t) * MLD_KECCAK_LANES) - requires(memory_no_alias(in0, inlen)) - requires(memory_no_alias(in1, inlen)) - requires(memory_no_alias(in2, inlen)) - requires(memory_no_alias(in3, inlen)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) + requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY, + in0, inlen, + in1, inlen, + in2, inlen, + in3, inlen)) + assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) { while (inlen >= r) __loop__( @@ -81,16 +81,16 @@ static void mld_keccak_squeezeblocks_x4(uint8_t *out0, uint8_t *out1, __contract__( requires(r <= sizeof(uint64_t) * MLD_KECCAK_LANES) requires(nblocks <= 8 /* somewhat arbitrary bound */) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - requires(memory_no_alias(out0, nblocks * r)) - requires(memory_no_alias(out1, nblocks * r)) - requires(memory_no_alias(out2, nblocks * r)) - requires(memory_no_alias(out3, nblocks * r)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - assigns(memory_slice(out0, nblocks * r)) - assigns(memory_slice(out1, nblocks * r)) - assigns(memory_slice(out2, nblocks * r)) - assigns(memory_slice(out3, nblocks * r))) + requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY, + out0, nblocks * r, + out1, nblocks * r, + out2, nblocks * r, + out3, nblocks * r)) + assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY, + out0, nblocks * r, + out1, nblocks * r, + out2, nblocks * r, + out3, nblocks * r)) { while (nblocks > 0) __loop__( diff --git a/mldsa/src/fips202/fips202x4.h b/mldsa/src/fips202/fips202x4.h index e7987207a..fb8a58e91 100644 --- a/mldsa/src/fips202/fips202x4.h +++ b/mldsa/src/fips202/fips202x4.h @@ -32,12 +32,9 @@ void mld_shake128x4_absorb_once(mld_shake128x4ctx *state, const uint8_t *in0, const uint8_t *in3, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake128x4ctx))) - requires(memory_no_alias(in0, inlen)) - requires(memory_no_alias(in1, inlen)) - requires(memory_no_alias(in2, inlen)) - requires(memory_no_alias(in3, inlen)) - assigns(memory_slice(state, sizeof(mld_shake128x4ctx))) + requires(objs_no_alias(state)) + requires(slices_no_alias(in0, inlen, in1, inlen, in2, inlen, in3, inlen)) + assigns_objs(state) ); #define mld_shake128x4_squeezeblocks MLD_NAMESPACE(shake128x4_squeezeblocks) @@ -46,16 +43,9 @@ void mld_shake128x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2, mld_shake128x4ctx *state) __contract__( requires(nblocks <= 8 /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake128x4ctx))) - requires(memory_no_alias(out0, nblocks * SHAKE128_RATE)) - requires(memory_no_alias(out1, nblocks * SHAKE128_RATE)) - requires(memory_no_alias(out2, nblocks * SHAKE128_RATE)) - requires(memory_no_alias(out3, nblocks * SHAKE128_RATE)) - assigns(memory_slice(out0, nblocks * SHAKE128_RATE), - memory_slice(out1, nblocks * SHAKE128_RATE), - memory_slice(out2, nblocks * SHAKE128_RATE), - memory_slice(out3, nblocks * SHAKE128_RATE), - memory_slice(state, sizeof(mld_shake128x4ctx))) + requires(objs_no_alias(state)) + requires(slices_no_alias(out0, nblocks * SHAKE128_RATE, out1, nblocks * SHAKE128_RATE, out2, nblocks * SHAKE128_RATE, out3, nblocks * SHAKE128_RATE)) + assigns_slices(out0, nblocks * SHAKE128_RATE, out1, nblocks * SHAKE128_RATE, out2, nblocks * SHAKE128_RATE, out3, nblocks * SHAKE128_RATE, state, sizeof(mld_shake128x4ctx)) ); #define mld_shake128x4_init MLD_NAMESPACE(shake128x4_init) @@ -71,12 +61,9 @@ void mld_shake256x4_absorb_once(mld_shake256x4ctx *state, const uint8_t *in0, const uint8_t *in3, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake256x4ctx))) - requires(memory_no_alias(in0, inlen)) - requires(memory_no_alias(in1, inlen)) - requires(memory_no_alias(in2, inlen)) - requires(memory_no_alias(in3, inlen)) - assigns(memory_slice(state, sizeof(mld_shake256x4ctx))) + requires(objs_no_alias(state)) + requires(slices_no_alias(in0, inlen, in1, inlen, in2, inlen, in3, inlen)) + assigns_objs(state) ); #define mld_shake256x4_squeezeblocks MLD_NAMESPACE(shake256x4_squeezeblocks) @@ -85,16 +72,9 @@ void mld_shake256x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2, mld_shake256x4ctx *state) __contract__( requires(nblocks <= 8 /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake256x4ctx))) - requires(memory_no_alias(out0, nblocks * SHAKE256_RATE)) - requires(memory_no_alias(out1, nblocks * SHAKE256_RATE)) - requires(memory_no_alias(out2, nblocks * SHAKE256_RATE)) - requires(memory_no_alias(out3, nblocks * SHAKE256_RATE)) - assigns(memory_slice(out0, nblocks * SHAKE256_RATE), - memory_slice(out1, nblocks * SHAKE256_RATE), - memory_slice(out2, nblocks * SHAKE256_RATE), - memory_slice(out3, nblocks * SHAKE256_RATE), - memory_slice(state, sizeof(mld_shake256x4ctx))) + requires(objs_no_alias(state)) + requires(slices_no_alias(out0, nblocks * SHAKE256_RATE, out1, nblocks * SHAKE256_RATE, out2, nblocks * SHAKE256_RATE, out3, nblocks * SHAKE256_RATE)) + assigns_slices(out0, nblocks * SHAKE256_RATE, out1, nblocks * SHAKE256_RATE, out2, nblocks * SHAKE256_RATE, out3, nblocks * SHAKE256_RATE, state, sizeof(mld_shake256x4ctx)) ); #define mld_shake256x4_init MLD_NAMESPACE(shake256x4_init) diff --git a/mldsa/src/fips202/keccakf1600.h b/mldsa/src/fips202/keccakf1600.h index e56adc156..a0d78d330 100644 --- a/mldsa/src/fips202/keccakf1600.h +++ b/mldsa/src/fips202/keccakf1600.h @@ -26,9 +26,9 @@ void mld_keccakf1600_extract_bytes(uint64_t *state, unsigned char *data, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(data, length)) - assigns(memory_slice(data, length)) + requires(slices_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(data, length)) + assigns_slices(data, length) ); #define mld_keccakf1600_xor_bytes MLD_NAMESPACE(keccakf1600_xor_bytes) @@ -37,9 +37,9 @@ void mld_keccakf1600_xor_bytes(uint64_t *state, const unsigned char *data, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(data, length)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(data, length)) + assigns_slices(state, sizeof(uint64_t) * MLD_KECCAK_LANES) ); #define mld_keccakf1600x4_extract_bytes \ @@ -51,15 +51,15 @@ void mld_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - requires(memory_no_alias(data0, length)) - requires(memory_no_alias(data1, length)) - requires(memory_no_alias(data2, length)) - requires(memory_no_alias(data3, length)) - assigns(memory_slice(data0, length)) - assigns(memory_slice(data1, length)) - assigns(memory_slice(data2, length)) - assigns(memory_slice(data3, length)) + requires(slices_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(data0, length)) + requires(slices_no_alias(data1, length)) + requires(slices_no_alias(data2, length)) + requires(slices_no_alias(data3, length)) + assigns_slices(data0, length) + assigns_slices(data1, length) + assigns_slices(data2, length) + assigns_slices(data3, length) ); #define mld_keccakf1600x4_xor_bytes MLD_NAMESPACE(keccakf1600x4_xor_bytes) @@ -71,30 +71,30 @@ void mld_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - requires(memory_no_alias(data0, length)) + requires(slices_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + requires(slices_no_alias(data0, length)) /* Case 1: all input buffers are distinct; Case 2: All input buffers are the same */ requires((data0 == data1 && data0 == data2 && data0 == data3) || - (memory_no_alias(data1, length) && - memory_no_alias(data2, length) && - memory_no_alias(data3, length))) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + (slices_no_alias(data1, length) && + slices_no_alias(data2, length) && + slices_no_alias(data3, length))) + assigns_slices(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY) ); #define mld_keccakf1600x4_permute MLD_NAMESPACE(keccakf1600x4_permute) void mld_keccakf1600x4_permute(uint64_t *state) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + requires(slices_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + assigns_slices(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY) ); #define mld_keccakf1600_permute MLD_NAMESPACE(keccakf1600_permute) void mld_keccakf1600_permute(uint64_t *state) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(slices_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + assigns_slices(state, sizeof(uint64_t) * MLD_KECCAK_LANES) ); #endif /* !MLD_FIPS202_KECCAKF1600_H */ diff --git a/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h b/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h index 20f616803..e6d524a93 100644 --- a/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h +++ b/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h @@ -18,25 +18,25 @@ extern const uint64_t mld_keccakf1600_round_constants[]; #define mld_keccak_f1600_x1_scalar_asm MLD_NAMESPACE(keccak_f1600_x1_scalar_asm) void mld_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns_slices(state, sizeof(uint64_t) * 25 * 1) ); #define mld_keccak_f1600_x1_v84a_asm MLD_NAMESPACE(keccak_f1600_x1_v84a_asm) void mld_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns_slices(state, sizeof(uint64_t) * 25 * 1) ); #define mld_keccak_f1600_x2_v84a_asm MLD_NAMESPACE(keccak_f1600_x2_v84a_asm) void mld_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 2)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2)) + assigns_slices(state, sizeof(uint64_t) * 25 * 2) ); #define mld_keccak_f1600_x4_scalar_v8a_hybrid_asm \ @@ -44,9 +44,9 @@ __contract__( void mld_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns_slices(state, sizeof(uint64_t) * 25 * 4) ); #define mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm \ @@ -54,9 +54,9 @@ __contract__( void mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm(uint64_t *state, uint64_t const *rc) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4)) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns_slices(state, sizeof(uint64_t) * 25 * 4) ); #endif /* !MLD_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */ diff --git a/mldsa/src/fips202/native/api.h b/mldsa/src/fips202/native/api.h index 4625c9a1a..bcfb781b3 100644 --- a/mldsa/src/fips202/native/api.h +++ b/mldsa/src/fips202/native/api.h @@ -48,8 +48,8 @@ #if defined(MLD_USE_FIPS202_X1_NATIVE) static MLD_INLINE int mld_keccak_f1600_x1_native(uint64_t *state) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1)) + assigns_slices(state, sizeof(uint64_t) * 25 * 1) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 1)) ); @@ -57,8 +57,8 @@ __contract__( #if defined(MLD_USE_FIPS202_X4_NATIVE) static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4)) + assigns_slices(state, sizeof(uint64_t) * 25 * 4) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 4)) ); diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index e210ff2a4..d0ecdb5ad 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -87,9 +87,9 @@ **************************************************/ static MLD_INLINE int mld_ntt_native(int32_t p[MLDSA_N]) __contract__( - requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(p)) requires(array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + assigns_slices(p, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLDSA_N, MLD_NTT_BOUND)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) @@ -140,9 +140,9 @@ static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]); **************************************************/ static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]) __contract__( - requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(p)) requires(array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + assigns_slices(p, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLDSA_N, MLD_INTT_BOUND)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) @@ -174,9 +174,9 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len, __contract__( requires(len <= MLDSA_N) requires(buflen <= ( 5 * 168) && buflen % 3 == 0) - requires(memory_no_alias(r, sizeof(int32_t) * len)) - requires(memory_no_alias(buf, buflen)) - assigns(memory_slice(r, sizeof(int32_t) * len)) + requires(objs_no_alias(r)) + requires(slices_no_alias(buf, buflen)) + assigns_slices(r, sizeof(int32_t) * len) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(r, 0, (unsigned) return_value, 0, MLDSA_Q)) ); @@ -206,9 +206,9 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, __contract__( requires(len <= MLDSA_N) requires(buflen <= (2 * 136)) - requires(memory_no_alias(r, sizeof(int32_t) * len)) - requires(memory_no_alias(buf, buflen)) - assigns(memory_slice(r, sizeof(int32_t) * len)) + requires(objs_no_alias(r)) + requires(slices_no_alias(buf, buflen)) + assigns_slices(r, sizeof(int32_t) * len) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))) ); @@ -238,9 +238,9 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, __contract__( requires(len <= MLDSA_N) requires(buflen <= (2 * 136)) - requires(memory_no_alias(r, sizeof(int32_t) * len)) - requires(memory_no_alias(buf, buflen)) - assigns(memory_slice(r, sizeof(int32_t) * len)) + requires(objs_no_alias(r)) + requires(slices_no_alias(buf, buflen)) + assigns_slices(r, sizeof(int32_t) * len) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))) ); @@ -265,11 +265,10 @@ __contract__( **************************************************/ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0) __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a1, a0)) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns_slices(a1, sizeof(int32_t) * MLDSA_N) + assigns_slices(a0, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a1, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(a0, 0, MLDSA_N, MLDSA_GAMMA2+1)) @@ -297,11 +296,10 @@ __contract__( **************************************************/ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0) __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a1, a0)) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns_slices(a1, sizeof(int32_t) * MLDSA_N) + assigns_slices(a0, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a1, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(a0, 0, MLDSA_N, MLDSA_GAMMA2+1)) @@ -321,9 +319,9 @@ __contract__( **************************************************/ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N]) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a)) requires(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + assigns_slices(a, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) @@ -346,12 +344,10 @@ __contract__( static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, const int32_t *h) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a, b, h)) requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) requires(array_bound(h, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N)) + assigns_slices(b, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N)) @@ -373,12 +369,10 @@ __contract__( static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, const int32_t *h) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a, b, h)) requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) requires(array_bound(h, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N)) + assigns_slices(b, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N)) @@ -400,7 +394,7 @@ __contract__( **************************************************/ static MLD_INLINE int mld_poly_chknorm_native(const int32_t *a, int32_t B) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a)) requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX) requires(array_bound(a, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) @@ -421,9 +415,9 @@ __contract__( **************************************************/ static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a) __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns_slices(r, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(r, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(r, MLDSA_N)) @@ -443,9 +437,9 @@ __contract__( **************************************************/ static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a) __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns_slices(r, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(r, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(r, MLDSA_N)) @@ -469,12 +463,10 @@ __contract__( static MLD_INLINE int mld_poly_pointwise_montgomery_native( int32_t c[MLDSA_N], const int32_t a[MLDSA_N], const int32_t b[MLDSA_N]) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) + requires(objs_no_alias(a, b, c)) requires(array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) requires(array_abs_bound(b, 0, MLDSA_N, MLD_NTT_BOUND)) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns_slices(c, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(c, 0, MLDSA_N, MLDSA_Q)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) @@ -502,14 +494,12 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native( int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N], const int32_t v[4][MLDSA_N]) __contract__( - requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(u, sizeof(int32_t) * 4 * MLDSA_N)) - requires(memory_no_alias(v, sizeof(int32_t) * 4 * MLDSA_N)) + requires(objs_no_alias(w, u, v)) requires(forall(l0, 0, 4, array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(l1, 0, 4, array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + assigns_slices(w, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) @@ -535,14 +525,12 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native( int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N], const int32_t v[5][MLDSA_N]) __contract__( - requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(u, sizeof(int32_t) * 5 * MLDSA_N)) - requires(memory_no_alias(v, sizeof(int32_t) * 5 * MLDSA_N)) + requires(objs_no_alias(w, u, v)) requires(forall(l0, 0, 5, array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(l1, 0, 5, array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + assigns_slices(w, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) @@ -568,14 +556,12 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native( int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N], const int32_t v[7][MLDSA_N]) __contract__( - requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(u, sizeof(int32_t) * 7 * MLDSA_N)) - requires(memory_no_alias(v, sizeof(int32_t) * 7 * MLDSA_N)) + requires(objs_no_alias(w, u, v)) requires(forall(l0, 0, 7, array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(l1, 0, 7, array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + assigns_slices(w, sizeof(int32_t) * MLDSA_N) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index ab08fb6ea..fe4f76a0c 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -183,9 +183,9 @@ void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES], static int mld_unpack_hints( mld_polyveck *h, const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES]) __contract__( - requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES)) - requires(memory_no_alias(h, sizeof(mld_polyveck))) - assigns(memory_slice(h, sizeof(mld_polyveck))) + requires(slices_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES)) + requires(objs_no_alias(h)) + assigns_objs(h) /* All returned coefficients are either 0 or 1 */ ensures(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index 1fdec836d..81f2ebac2 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -22,12 +22,11 @@ MLD_INTERNAL_API void mld_pack_pk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], const uint8_t rho[MLDSA_SEEDBYTES], const mld_polyveck *t1) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(t1, sizeof(mld_polyveck))) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES, rho, MLDSA_SEEDBYTES)) + requires(objs_no_alias(t1)) requires(forall(k0, 0, MLDSA_K, array_bound(t1->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10))) - assigns(memory_slice(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + assigns_slices(pk, MLDSA_CRYPTO_PUBLICKEYBYTES) ); @@ -52,20 +51,15 @@ void mld_pack_sk(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], const uint8_t key[MLDSA_SEEDBYTES], const mld_polyveck *t0, const mld_polyvecl *s1, const mld_polyveck *s2) __contract__( - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(tr, MLDSA_TRBYTES)) - requires(memory_no_alias(key, MLDSA_SEEDBYTES)) - requires(memory_no_alias(t0, sizeof(mld_polyveck))) - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) + requires(slices_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES, rho, MLDSA_SEEDBYTES, tr, MLDSA_TRBYTES, key, MLDSA_SEEDBYTES)) + requires(objs_no_alias(t0, s1, s2)) requires(forall(k0, 0, MLDSA_K, array_bound(t0->vec[k0].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))) requires(forall(k1, 0, MLDSA_L, array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) requires(forall(k2, 0, MLDSA_K, array_abs_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + assigns_slices(sk, MLDSA_CRYPTO_SECRETKEYBYTES) ); @@ -92,16 +86,14 @@ void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES], const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z, const mld_polyveck *h, const unsigned int number_of_hints) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(c, MLDSA_CTILDEBYTES)) - requires(memory_no_alias(z, sizeof(mld_polyvecl))) - requires(memory_no_alias(h, sizeof(mld_polyveck))) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, c, MLDSA_CTILDEBYTES)) + requires(objs_no_alias(z, h)) requires(forall(k0, 0, MLDSA_L, array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) requires(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) requires(number_of_hints <= MLDSA_OMEGA) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) ); #define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk) @@ -118,11 +110,10 @@ MLD_INTERNAL_API void mld_unpack_pk(uint8_t rho[MLDSA_SEEDBYTES], mld_polyveck *t1, const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(t1, sizeof(mld_polyveck))) - assigns(memory_slice(rho, MLDSA_SEEDBYTES)) - assigns(memory_slice(t1, sizeof(mld_polyveck))) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES, rho, MLDSA_SEEDBYTES)) + requires(objs_no_alias(t1)) + assigns_slices(rho, MLDSA_SEEDBYTES) + assigns_objs(t1) ensures(forall(k0, 0, MLDSA_K, array_bound(t1->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10))) ); @@ -148,19 +139,11 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES], mld_polyvecl *s1, mld_polyveck *s2, const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(tr, MLDSA_TRBYTES)) - requires(memory_no_alias(key, MLDSA_SEEDBYTES)) - requires(memory_no_alias(t0, sizeof(mld_polyveck))) - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(rho, MLDSA_SEEDBYTES)) - assigns(memory_slice(tr, MLDSA_TRBYTES)) - assigns(memory_slice(key, MLDSA_SEEDBYTES)) - assigns(memory_slice(t0, sizeof(mld_polyveck))) - assigns(memory_slice(s1, sizeof(mld_polyvecl))) - assigns(memory_slice(s2, sizeof(mld_polyveck))) + requires(slices_no_alias(rho, MLDSA_SEEDBYTES, tr, MLDSA_TRBYTES, key, MLDSA_SEEDBYTES)) + requires(objs_no_alias(t0, s1, s2)) + requires(slices_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + assigns_slices(rho, MLDSA_SEEDBYTES, tr, MLDSA_TRBYTES, key, MLDSA_SEEDBYTES) + assigns_objs(t0, s1, s2) ensures(forall(k0, 0, MLDSA_K, array_bound(t0->vec[k0].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))) ensures(forall(k1, 0, MLDSA_L, @@ -188,13 +171,10 @@ MLD_INTERNAL_API int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z, mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES]) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(c, MLDSA_CTILDEBYTES)) - requires(memory_no_alias(z, sizeof(mld_polyvecl))) - requires(memory_no_alias(h, sizeof(mld_polyveck))) - assigns(memory_slice(c, MLDSA_CTILDEBYTES)) - assigns(memory_slice(z, sizeof(mld_polyvecl))) - assigns(memory_slice(h, sizeof(mld_polyveck))) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, c, MLDSA_CTILDEBYTES)) + requires(objs_no_alias(z, h)) + assigns_slices(c, MLDSA_CTILDEBYTES) + assigns_objs(z, h) ensures(forall(k0, 0, MLDSA_L, array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ensures(forall(k1, 0, MLDSA_K, diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index a68be3a24..f2d2e8ba7 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -53,9 +53,9 @@ void mld_poly_reduce(mld_poly *a) MLD_STATIC_TESTABLE void mld_poly_caddq_c(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ) { @@ -211,10 +211,10 @@ __contract__( requires(1 <= len && len <= MLDSA_N / 2 && start + 2 * len <= MLDSA_N) requires(0 <= bound && bound < INT32_MAX - MLDSA_Q) requires(-MLDSA_Q_HALF < zeta && zeta < MLDSA_Q_HALF) - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(slices_no_alias(r, sizeof(int32_t) * MLDSA_N)) requires(array_abs_bound(r, 0, start, bound + MLDSA_Q)) requires(array_abs_bound(r, start, MLDSA_N, bound)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns_slices(r, sizeof(int32_t) * MLDSA_N) ensures(array_abs_bound(r, 0, start + 2*len, bound + MLDSA_Q)) ensures(array_abs_bound(r, start + 2 * len, MLDSA_N, bound))) { @@ -252,10 +252,10 @@ __contract__( /* Reference: Embedded in `ntt()` in the reference implementation @[REF]. */ static MLD_INLINE void mld_ntt_layer(int32_t r[MLDSA_N], const unsigned layer) __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(slices_no_alias(r, sizeof(int32_t) * MLDSA_N)) requires(1 <= layer && layer <= 8) requires(array_abs_bound(r, 0, MLDSA_N, layer * MLDSA_Q)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns_slices(r, sizeof(int32_t) * MLDSA_N) ensures(array_abs_bound(r, 0, MLDSA_N, (layer + 1) * MLDSA_Q))) { unsigned start, k, len; @@ -277,9 +277,9 @@ __contract__( MLD_STATIC_TESTABLE void mld_poly_ntt_c(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { @@ -346,10 +346,10 @@ __contract__( * @[REF] */ static MLD_INLINE void mld_invntt_layer(int32_t r[MLDSA_N], unsigned layer) __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(slices_no_alias(r, sizeof(int32_t) * MLDSA_N)) requires(1 <= layer && layer <= 8) requires(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns_slices(r, sizeof(int32_t) * MLDSA_N) ensures(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> (layer - 1)) * MLDSA_Q))) { unsigned start, k, len; @@ -383,9 +383,9 @@ __contract__( MLD_STATIC_TESTABLE void mld_poly_invntt_tomont_c(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND)) ) { @@ -445,12 +445,10 @@ MLD_STATIC_TESTABLE void mld_poly_pointwise_montgomery_c(mld_poly *c, const mld_poly *a, const mld_poly *b) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(c, sizeof(mld_poly))) + requires(objs_no_alias(a, b, c)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) requires(array_abs_bound(b->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) - assigns(memory_slice(c, sizeof(mld_poly))) + assigns_objs(c) ensures(array_abs_bound(c->coeffs, 0, MLDSA_N, MLDSA_Q)) ) { @@ -524,10 +522,10 @@ MLD_STATIC_TESTABLE unsigned int mld_rej_uniform_c(int32_t *a, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_NBLOCKS * MLD_STREAM128_BLOCKBYTES) && buflen % 3 == 0) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(slices_no_alias(a, sizeof(int32_t) * target)) + requires(slices_no_alias(buf, buflen)) requires(array_bound(a, 0, offset, 0, MLDSA_Q)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns_slices(a, sizeof(int32_t) * target) ensures(offset <= return_value && return_value <= target) ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) @@ -589,10 +587,10 @@ static unsigned int mld_rej_uniform(int32_t *a, unsigned int target, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_NBLOCKS * MLD_STREAM128_BLOCKBYTES) && buflen % 3 == 0) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(slices_no_alias(a, sizeof(int32_t) * target)) + requires(slices_no_alias(buf, buflen)) requires(array_bound(a, 0, offset, 0, MLDSA_Q)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns_slices(a, sizeof(int32_t) * target) ensures(offset <= return_value && return_value <= target) ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) @@ -878,7 +876,7 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES]) MLD_STATIC_TESTABLE uint32_t mld_poly_chknorm_c(const mld_poly *a, int32_t B) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(0 <= B && B <= MLDSA_Q - MLD_REDUCE32_RANGE_MAX) requires(array_bound(a->coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ensures(return_value == 0 || return_value == 0xFFFFFFFF) diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h index 3b6bf42a9..df65a1ed2 100644 --- a/mldsa/src/poly.h +++ b/mldsa/src/poly.h @@ -34,9 +34,9 @@ typedef struct MLD_INTERNAL_API void mld_poly_reduce(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_bound(a->coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ); @@ -52,9 +52,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_caddq(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -76,11 +76,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_add(mld_poly *r, const mld_poly *b) __contract__( - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(r, sizeof(mld_poly))) + requires(objs_no_alias(b, r)) requires(forall(k0, 0, MLDSA_N, (int64_t) r->coeffs[k0] + b->coeffs[k0] < MLD_REDUCE32_DOMAIN_MAX)) requires(forall(k1, 0, MLDSA_N, (int64_t) r->coeffs[k1] + b->coeffs[k1] >= INT32_MIN)) - assigns(memory_slice(r, sizeof(mld_poly))) + assigns_objs(r) ensures(forall(k2, 0, MLDSA_N, r->coeffs[k2] == old(*r).coeffs[k2] + b->coeffs[k2])) ensures(forall(k3, 0, MLDSA_N, r->coeffs[k3] < MLD_REDUCE32_DOMAIN_MAX)) ensures(forall(k4, 0, MLDSA_N, r->coeffs[k4] >= INT32_MIN)) @@ -104,11 +103,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_sub(mld_poly *r, const mld_poly *b) __contract__( - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(r, sizeof(mld_poly))) + requires(objs_no_alias(b, r)) requires(array_abs_bound(r->coeffs, 0, MLDSA_N, MLDSA_Q)) requires(array_abs_bound(b->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(r, sizeof(mld_poly))) + assigns_objs(r) ensures(array_bound(r->coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX)) ); @@ -124,9 +122,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_shiftl(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, 1 << 10)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -142,9 +140,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_ntt(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ); @@ -163,9 +161,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_invntt_tomont(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns_objs(a) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND)) ); @@ -185,12 +183,10 @@ MLD_INTERNAL_API void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a, const mld_poly *b) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(c, sizeof(mld_poly))) + requires(objs_no_alias(a, b, c)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) requires(array_abs_bound(b->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) - assigns(memory_slice(c, sizeof(mld_poly))) + assigns_objs(c) ensures(array_abs_bound(c->coeffs, 0, MLDSA_N, MLDSA_Q)) ); @@ -212,12 +208,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) __contract__( - requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(memory_no_alias(a1, sizeof(mld_poly))) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a0, a1, a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(mld_poly))) - assigns(memory_slice(a0, sizeof(mld_poly))) + assigns_objs(a1, a0) ensures(array_bound(a0->coeffs, 0, MLDSA_N, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1)) ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1)) ); @@ -237,9 +230,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_uniform(mld_poly *a, const uint8_t seed[MLDSA_SEEDBYTES + 2]) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_SEEDBYTES + 2)) - assigns(memory_slice(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) + requires(slices_no_alias(seed, MLDSA_SEEDBYTES + 2)) + assigns_objs(a) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -263,15 +256,9 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2, mld_poly *vec3, uint8_t seed[4][MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)]) __contract__( - requires(memory_no_alias(vec0, sizeof(mld_poly))) - requires(memory_no_alias(vec1, sizeof(mld_poly))) - requires(memory_no_alias(vec2, sizeof(mld_poly))) - requires(memory_no_alias(vec3, sizeof(mld_poly))) - requires(memory_no_alias(seed, 4 * MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2))) - assigns(memory_slice(vec0, sizeof(mld_poly))) - assigns(memory_slice(vec1, sizeof(mld_poly))) - assigns(memory_slice(vec2, sizeof(mld_poly))) - assigns(memory_slice(vec3, sizeof(mld_poly))) + requires(objs_no_alias(vec0, vec1, vec2, vec3)) + requires(slices_no_alias(seed, 4 * MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2))) + assigns_objs(vec0, vec1, vec2, vec3) ensures(array_bound(vec0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ensures(array_bound(vec1->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ensures(array_bound(vec2->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) @@ -293,10 +280,10 @@ __contract__( MLD_INTERNAL_API void mld_polyt1_pack(uint8_t r[MLDSA_POLYT1_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYT1_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(slices_no_alias(r, MLDSA_POLYT1_PACKEDBYTES)) + requires(objs_no_alias(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, 1 << 10)) - assigns(memory_slice(r, MLDSA_POLYT1_PACKEDBYTES)) + assigns_slices(r, MLDSA_POLYT1_PACKEDBYTES) ); #define mld_polyt1_unpack MLD_NAMESPACE(polyt1_unpack) @@ -312,9 +299,9 @@ __contract__( MLD_INTERNAL_API void mld_polyt1_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT1_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYT1_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYT1_PACKEDBYTES)) + assigns_objs(r) ensures(array_bound(r->coeffs, 0, MLDSA_N, 0, 1 << 10)) ); @@ -332,10 +319,10 @@ __contract__( MLD_INTERNAL_API void mld_polyt0_pack(uint8_t r[MLDSA_POLYT0_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYT0_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(slices_no_alias(r, MLDSA_POLYT0_PACKEDBYTES)) + requires(objs_no_alias(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)) - assigns(memory_slice(r, MLDSA_POLYT0_PACKEDBYTES)) + assigns_slices(r, MLDSA_POLYT0_PACKEDBYTES) ); @@ -352,9 +339,9 @@ __contract__( MLD_INTERNAL_API void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYT0_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYT0_PACKEDBYTES)) + assigns_objs(r) ensures(array_bound(r->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)) ); @@ -383,7 +370,7 @@ __contract__( MLD_INTERNAL_API uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) requires(0 <= B && B <= MLDSA_Q - MLD_REDUCE32_RANGE_MAX) requires(array_bound(a->coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ensures(return_value == 0 || return_value == 0xFFFFFFFF) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 7a319ca51..f445a73ca 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -42,11 +42,9 @@ MLD_STATIC_TESTABLE void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0) __contract__( - requires(memory_no_alias(a1, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(objs_no_alias(a1, a0)) requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(mld_poly))) - assigns(memory_slice(a0, sizeof(mld_poly))) + assigns_objs(a1, a0) ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)) ) @@ -127,12 +125,10 @@ unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a, const mld_poly *h) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(h, sizeof(mld_poly))) + requires(objs_no_alias(a, b, h)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(b, sizeof(mld_poly))) + assigns_objs(b) ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ) { @@ -229,10 +225,10 @@ MLD_STATIC_TESTABLE unsigned int mld_rej_eta_c(int32_t *a, unsigned int target, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_ETA_NBLOCKS * MLD_STREAM256_BLOCKBYTES)) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(objs_no_alias(a)) + requires(slices_no_alias(buf, buflen)) requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns_slices(a, sizeof(int32_t) * target) ensures(offset <= return_value && return_value <= target) ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) ) @@ -301,10 +297,10 @@ static unsigned int mld_rej_eta(int32_t *a, unsigned int target, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_ETA_NBLOCKS * MLD_STREAM256_BLOCKBYTES)) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(objs_no_alias(a)) + requires(slices_no_alias(buf, buflen)) requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns_slices(a, sizeof(int32_t) * target) ensures(offset <= return_value && return_value <= target) ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) ) @@ -798,9 +794,9 @@ void mld_polyz_pack(uint8_t r[MLDSA_POLYZ_PACKEDBYTES], const mld_poly *a) MLD_STATIC_TESTABLE void mld_polyz_unpack_c( mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns_objs(r) ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ) { diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h index c6aa49835..d2162ceaf 100644 --- a/mldsa/src/poly_kl.h +++ b/mldsa/src/poly_kl.h @@ -33,11 +33,9 @@ MLD_INTERNAL_API void mld_poly_decompose(mld_poly *a1, mld_poly *a0) __contract__( - requires(memory_no_alias(a1, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(objs_no_alias(a1, a0)) requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(mld_poly))) - assigns(memory_slice(a0, sizeof(mld_poly))) + assigns_objs(a1, a0) ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)) ); @@ -61,10 +59,8 @@ MLD_INTERNAL_API unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, const mld_poly *a1) __contract__( - requires(memory_no_alias(h, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(memory_no_alias(a1, sizeof(mld_poly))) - assigns(memory_slice(h, sizeof(mld_poly))) + requires(objs_no_alias(h, a0, a1)) + assigns_objs(h) ensures(return_value <= MLDSA_N) ensures(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) ); @@ -83,12 +79,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(h, sizeof(mld_poly))) + requires(objs_no_alias(a, b, h)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(b, sizeof(mld_poly))) + assigns_objs(b) ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ); @@ -118,15 +112,9 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, uint8_t nonce3) __contract__( - requires(memory_no_alias(r0, sizeof(mld_poly))) - requires(memory_no_alias(r1, sizeof(mld_poly))) - requires(memory_no_alias(r2, sizeof(mld_poly))) - requires(memory_no_alias(r3, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(r0, sizeof(mld_poly))) - assigns(memory_slice(r1, sizeof(mld_poly))) - assigns(memory_slice(r2, sizeof(mld_poly))) - assigns(memory_slice(r3, sizeof(mld_poly))) + requires(objs_no_alias(r0, r1, r2, r3)) + requires(slices_no_alias(seed, MLDSA_CRHBYTES)) + assigns_objs(r0, r1, r2, r3) ensures(array_abs_bound(r0->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ensures(array_abs_bound(r1->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ensures(array_abs_bound(r2->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) @@ -152,9 +140,9 @@ MLD_INTERNAL_API void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES], uint8_t nonce) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(objs_no_alias(r)) + requires(slices_no_alias(seed, MLDSA_CRHBYTES)) + assigns_objs(r) ensures(array_abs_bound(r->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ); #endif /* MLD_CONFIG_SERIAL_FIPS202_ONLY */ @@ -177,9 +165,9 @@ MLD_INTERNAL_API void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES], uint16_t nonce) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(a, sizeof(mld_poly))) + requires(objs_no_alias(a)) + requires(slices_no_alias(seed, MLDSA_CRHBYTES)) + assigns_objs(a) ensures(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ); #endif /* MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_SERIAL_FIPS202_ONLY */ @@ -205,15 +193,9 @@ void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, uint16_t nonce0, uint16_t nonce1, uint16_t nonce2, uint16_t nonce3) __contract__( - requires(memory_no_alias(r0, sizeof(mld_poly))) - requires(memory_no_alias(r1, sizeof(mld_poly))) - requires(memory_no_alias(r2, sizeof(mld_poly))) - requires(memory_no_alias(r3, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(r0, sizeof(mld_poly))) - assigns(memory_slice(r1, sizeof(mld_poly))) - assigns(memory_slice(r2, sizeof(mld_poly))) - assigns(memory_slice(r3, sizeof(mld_poly))) + requires(objs_no_alias(r0, r1, r2, r3)) + requires(slices_no_alias(seed, MLDSA_CRHBYTES)) + assigns_objs(r0, r1, r2, r3) ensures(array_bound(r0->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ensures(array_bound(r1->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ensures(array_bound(r2->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) @@ -236,9 +218,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) __contract__( - requires(memory_no_alias(c, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CTILDEBYTES)) - assigns(memory_slice(c, sizeof(mld_poly))) + requires(objs_no_alias(c)) + requires(slices_no_alias(seed, MLDSA_CTILDEBYTES)) + assigns_objs(c) /* All coefficients of c are -1, 0 or +1 */ ensures(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) ); @@ -256,10 +238,10 @@ __contract__( MLD_INTERNAL_API void mld_polyeta_pack(uint8_t r[MLDSA_POLYETA_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(slices_no_alias(r, MLDSA_POLYETA_PACKEDBYTES)) + requires(objs_no_alias(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) - assigns(memory_slice(r, MLDSA_POLYETA_PACKEDBYTES)) + assigns_slices(r, MLDSA_POLYETA_PACKEDBYTES) ); /* @@ -290,9 +272,9 @@ __contract__( MLD_INTERNAL_API void mld_polyeta_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYETA_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYETA_PACKEDBYTES)) + assigns_objs(r) ensures(array_bound(r->coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)) ); @@ -310,10 +292,10 @@ __contract__( MLD_INTERNAL_API void mld_polyz_pack(uint8_t r[MLDSA_POLYZ_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYZ_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(slices_no_alias(r, MLDSA_POLYZ_PACKEDBYTES)) + requires(objs_no_alias(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) - assigns(memory_slice(r, MLDSA_POLYZ_PACKEDBYTES)) + assigns_slices(r, MLDSA_POLYZ_PACKEDBYTES) ); @@ -330,9 +312,9 @@ __contract__( MLD_INTERNAL_API void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(objs_no_alias(r)) + requires(slices_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns_objs(r) ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ); @@ -350,10 +332,10 @@ __contract__( MLD_INTERNAL_API void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(slices_no_alias(r, MLDSA_POLYW1_PACKEDBYTES)) + requires(objs_no_alias(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES)) + assigns_slices(r, MLDSA_POLYW1_PACKEDBYTES) ); #endif /* !MLD_POLY_KL_H */ diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index 05c67d9ba..6a69a6998 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -39,10 +39,10 @@ __contract__( * that it does not change the bound established at the end of * mld_polyvec_matrix_expand. */ - requires(memory_no_alias(mat, sizeof(mld_polymat))) + requires(objs_no_alias(mat)) 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)))) - assigns(memory_slice(mat, sizeof(mld_polymat))) + assigns_objs(mat) ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) ) @@ -330,14 +330,12 @@ void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a, MLD_STATIC_TESTABLE void mld_polyvecl_pointwise_acc_montgomery_c( mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v) __contract__( - requires(memory_no_alias(w, sizeof(mld_poly))) - requires(memory_no_alias(u, sizeof(mld_polyvecl))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(w, u, v)) requires(forall(l0, 0, MLDSA_L, array_bound(u->vec[l0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(l1, 0, MLDSA_L, array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(w, sizeof(mld_poly))) + assigns_objs(w) ensures(array_abs_bound(w->coeffs, 0, MLDSA_N, MLDSA_Q)) ) { diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 469003488..ae9a062ca 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -45,10 +45,10 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v, const uint8_t seed[MLDSA_CRHBYTES], uint16_t nonce) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) + requires(objs_no_alias(v)) + requires(slices_no_alias(seed, MLDSA_CRHBYTES)) requires(nonce <= (UINT16_MAX - MLDSA_L) / MLDSA_L) - assigns(memory_slice(v, sizeof(mld_polyvecl))) + assigns_objs(v) ensures(forall(k0, 0, MLDSA_L, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); @@ -67,10 +67,10 @@ __contract__( MLD_INTERNAL_API void mld_polyvecl_reduce(mld_polyvecl *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_L, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_L, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) ); @@ -90,12 +90,11 @@ __contract__( MLD_INTERNAL_API void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v) __contract__( - requires(memory_no_alias(u, sizeof(mld_polyvecl))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(u, v)) requires(forall(p0, 0, MLDSA_L, array_abs_bound(u->vec[p0].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND))) requires(forall(p1, 0, MLDSA_L, array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - assigns(memory_slice(u, sizeof(mld_polyvecl))) + assigns_objs(u) ensures(forall(q2, 0, MLDSA_L, array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) ); @@ -112,9 +111,9 @@ __contract__( MLD_INTERNAL_API void mld_polyvecl_ntt(mld_polyvecl *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_L, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); @@ -132,9 +131,9 @@ __contract__( MLD_INTERNAL_API void mld_polyvecl_invntt_tomont(mld_polyvecl *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_L, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND))) ); @@ -155,12 +154,10 @@ MLD_INTERNAL_API void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a, const mld_polyvecl *v) __contract__( - requires(memory_no_alias(r, sizeof(mld_polyvecl))) - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(r, a, v)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) requires(forall(k0, 0, MLDSA_L, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(r, sizeof(mld_polyvecl))) + assigns_objs(r) ensures(forall(k1, 0, MLDSA_L, array_abs_bound(r->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q))) ); @@ -191,14 +188,12 @@ MLD_INTERNAL_API void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v) __contract__( - requires(memory_no_alias(w, sizeof(mld_poly))) - requires(memory_no_alias(u, sizeof(mld_polyvecl))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(w, u, v)) requires(forall(l0, 0, MLDSA_L, array_bound(u->vec[l0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(l1, 0, MLDSA_L, array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(w, sizeof(mld_poly))) + assigns_objs(w) ensures(array_abs_bound(w->coeffs, 0, MLDSA_N, MLDSA_Q)) ); @@ -220,7 +215,7 @@ MLD_MUST_CHECK_RETURN_VALUE MLD_INTERNAL_API uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t B) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(v)) requires(0 <= B && B <= (MLDSA_Q - 1) / 8) requires(forall(k0, 0, MLDSA_L, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) @@ -253,10 +248,10 @@ typedef struct MLD_INTERNAL_API void mld_polyveck_reduce(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) ); @@ -273,10 +268,10 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_caddq(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) ); @@ -296,12 +291,11 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v) __contract__( - requires(memory_no_alias(u, sizeof(mld_polyveck))) - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(u, v)) requires(forall(p0, 0, MLDSA_K, array_abs_bound(u->vec[p0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) requires(forall(p1, 0, MLDSA_K, array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) - assigns(memory_slice(u, sizeof(mld_polyveck))) + assigns_objs(u) ensures(forall(q2, 0, MLDSA_K, array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) ); @@ -320,11 +314,10 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_sub(mld_polyveck *u, const mld_polyveck *v) __contract__( - requires(memory_no_alias(u, sizeof(mld_polyveck))) - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(u, v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(u->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) requires(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(u, sizeof(mld_polyveck))) + assigns_objs(u) ensures(forall(k0, 0, MLDSA_K, array_bound(u->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) ); @@ -342,9 +335,9 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_shiftl(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) ); @@ -360,9 +353,9 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_ntt(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); @@ -379,9 +372,9 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_invntt_tomont(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns_objs(v) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) ); @@ -402,12 +395,10 @@ MLD_INTERNAL_API void mld_polyveck_pointwise_poly_montgomery(mld_polyveck *r, const mld_poly *a, const mld_polyveck *v) __contract__( - requires(memory_no_alias(r, sizeof(mld_polyveck))) - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(r, a, v)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(r, sizeof(mld_polyveck))) + assigns_objs(r) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(r->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q))) ); @@ -428,7 +419,7 @@ MLD_MUST_CHECK_RETURN_VALUE MLD_INTERNAL_API uint32_t mld_polyveck_chknorm(const mld_polyveck *v, int32_t B) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v)) requires(0 <= B && B <= (MLDSA_Q - 1) / 8) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, @@ -456,12 +447,9 @@ MLD_INTERNAL_API void mld_polyveck_power2round(mld_polyveck *v1, mld_polyveck *v0, const mld_polyveck *v) __contract__( - requires(memory_no_alias(v1, sizeof(mld_polyveck))) - requires(memory_no_alias(v0, sizeof(mld_polyveck))) - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(objs_no_alias(v1, v0, v)) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) - assigns(memory_slice(v1, sizeof(mld_polyveck))) - assigns(memory_slice(v0, sizeof(mld_polyveck))) + assigns_objs(v1, v0) ensures(forall(k1, 0, MLDSA_K, array_bound(v0->vec[k1].coeffs, 0, MLDSA_N, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1))) ensures(forall(k2, 0, MLDSA_K, array_bound(v1->vec[k2].coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1))) ); @@ -490,12 +478,10 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0) __contract__( - requires(memory_no_alias(v1, sizeof(mld_polyveck))) - requires(memory_no_alias(v0, sizeof(mld_polyveck))) + requires(objs_no_alias(v1, v0)) requires(forall(k0, 0, MLDSA_K, array_bound(v0->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) - assigns(memory_slice(v1, sizeof(mld_polyveck))) - assigns(memory_slice(v0, sizeof(mld_polyveck))) + assigns_objs(v1, v0) ensures(forall(k1, 0, MLDSA_K, array_bound(v1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) ensures(forall(k2, 0, MLDSA_K, @@ -519,10 +505,8 @@ MLD_INTERNAL_API unsigned int mld_polyveck_make_hint(mld_polyveck *h, const mld_polyveck *v0, const mld_polyveck *v1) __contract__( - requires(memory_no_alias(h, sizeof(mld_polyveck))) - requires(memory_no_alias(v0, sizeof(mld_polyveck))) - requires(memory_no_alias(v1, sizeof(mld_polyveck))) - assigns(memory_slice(h, sizeof(mld_polyveck))) + requires(objs_no_alias(h, v0, v1)) + assigns_objs(h) ensures(return_value <= MLDSA_N * MLDSA_K) ensures(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) ); @@ -542,14 +526,12 @@ MLD_INTERNAL_API void mld_polyveck_use_hint(mld_polyveck *w, const mld_polyveck *v, const mld_polyveck *h) __contract__( - requires(memory_no_alias(w, sizeof(mld_polyveck))) - requires(memory_no_alias(v, sizeof(mld_polyveck))) - requires(memory_no_alias(h, sizeof(mld_polyveck))) + requires(objs_no_alias(w, v, h)) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) - assigns(memory_slice(w, sizeof(mld_polyveck))) + assigns_objs(w) ensures(forall(k2, 0, MLDSA_K, array_bound(w->vec[k2].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) ); @@ -570,11 +552,11 @@ MLD_INTERNAL_API void mld_polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES], const mld_polyveck *w1) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) - requires(memory_no_alias(w1, sizeof(mld_polyveck))) + requires(slices_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) + requires(objs_no_alias(w1)) requires(forall(k1, 0, MLDSA_K, array_bound(w1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) - assigns(memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) + assigns_slices(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES) ); #define mld_polyveck_pack_eta MLD_NAMESPACE_KL(polyveck_pack_eta) @@ -592,11 +574,11 @@ MLD_INTERNAL_API void mld_polyveck_pack_eta(uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES], const mld_polyveck *p) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyveck))) + requires(slices_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) + requires(objs_no_alias(p)) requires(forall(k1, 0, MLDSA_K, array_abs_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) + assigns_slices(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES) ); #define mld_polyvecl_pack_eta MLD_NAMESPACE_KL(polyvecl_pack_eta) @@ -614,11 +596,11 @@ MLD_INTERNAL_API void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES], const mld_polyvecl *p) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyvecl))) + requires(slices_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) + requires(objs_no_alias(p)) requires(forall(k1, 0, MLDSA_L, array_abs_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) + assigns_slices(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES) ); #define mld_polyvecl_pack_z MLD_NAMESPACE_KL(polyvecl_pack_z) @@ -636,11 +618,11 @@ MLD_INTERNAL_API void mld_polyvecl_pack_z(uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES], const mld_polyvecl *p) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyvecl))) + requires(slices_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) + requires(objs_no_alias(p)) requires(forall(k1, 0, MLDSA_L, array_bound(p->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - assigns(memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) + assigns_slices(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES) ); #define mld_polyveck_pack_t0 MLD_NAMESPACE_KL(polyveck_pack_t0) @@ -658,11 +640,11 @@ MLD_INTERNAL_API void mld_polyveck_pack_t0(uint8_t r[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES], const mld_polyveck *p) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyveck))) + requires(slices_no_alias(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) + requires(objs_no_alias(p)) requires(forall(k0, 0, MLDSA_K, array_bound(p->vec[k0].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))) - assigns(memory_slice(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) + assigns_slices(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES) ); #define mld_polyvecl_unpack_eta MLD_NAMESPACE_KL(polyvecl_unpack_eta) @@ -680,9 +662,9 @@ MLD_INTERNAL_API void mld_polyvecl_unpack_eta( mld_polyvecl *p, const uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyvecl))) - assigns(memory_slice(p, sizeof(mld_polyvecl))) + requires(slices_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) + requires(objs_no_alias(p)) + assigns_objs(p) ensures(forall(k1, 0, MLDSA_L, array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); @@ -702,9 +684,9 @@ MLD_INTERNAL_API void mld_polyvecl_unpack_z(mld_polyvecl *z, const uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) - requires(memory_no_alias(z, sizeof(mld_polyvecl))) - assigns(memory_slice(z, sizeof(mld_polyvecl))) + requires(slices_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) + requires(objs_no_alias(z)) + assigns_objs(z) ensures(forall(k1, 0, MLDSA_L, array_bound(z->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); @@ -724,9 +706,9 @@ MLD_INTERNAL_API void mld_polyveck_unpack_eta( mld_polyveck *p, const uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyveck))) - assigns(memory_slice(p, sizeof(mld_polyveck))) + requires(slices_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) + requires(objs_no_alias(p)) + assigns_objs(p) ensures(forall(k1, 0, MLDSA_K, array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); @@ -746,9 +728,9 @@ MLD_INTERNAL_API void mld_polyveck_unpack_t0(mld_polyveck *p, const uint8_t r[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyveck))) - assigns(memory_slice(p, sizeof(mld_polyveck))) + requires(slices_no_alias(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) + requires(objs_no_alias(p)) + assigns_objs(p) ensures(forall(k1, 0, MLDSA_K, array_bound(p->vec[k1].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))) ); @@ -768,9 +750,9 @@ MLD_INTERNAL_API void mld_polyvec_matrix_expand(mld_polymat *mat, const uint8_t rho[MLDSA_SEEDBYTES]) __contract__( - requires(memory_no_alias(mat, sizeof(mld_polymat))) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - assigns(memory_slice(mat, sizeof(mld_polymat))) + requires(objs_no_alias(mat)) + requires(slices_no_alias(rho, MLDSA_SEEDBYTES)) + assigns_objs(mat) ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) ); @@ -803,14 +785,12 @@ void mld_polyvec_matrix_pointwise_montgomery(mld_polyveck *t, const mld_polymat *mat, const mld_polyvecl *v) __contract__( - requires(memory_no_alias(t, sizeof(mld_polyveck))) - requires(memory_no_alias(mat, sizeof(mld_polymat))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(objs_no_alias(t, mat, v)) 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(l1, 0, MLDSA_L, array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(t, sizeof(mld_polyveck))) + assigns_objs(t) ensures(forall(k0, 0, MLDSA_K, array_abs_bound(t->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) ); diff --git a/mldsa/src/randombytes.h b/mldsa/src/randombytes.h index 801bcbaa9..fbe7f1e9a 100644 --- a/mldsa/src/randombytes.h +++ b/mldsa/src/randombytes.h @@ -16,8 +16,8 @@ void randombytes(uint8_t *out, size_t outlen); static MLD_INLINE void mld_randombytes(uint8_t *out, size_t outlen) __contract__( - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(out, outlen)) + requires(slices_no_alias(out, outlen)) + assigns_slices(out, outlen) ) { randombytes(out, outlen); } #endif /* !MLD_CONFIG_CUSTOM_RANDOMBYTES */ #endif /* !MLD_CONFIG_NO_RANDOMIZED_API */ diff --git a/mldsa/src/rounding.h b/mldsa/src/rounding.h index a83562b0f..5f8156207 100644 --- a/mldsa/src/rounding.h +++ b/mldsa/src/rounding.h @@ -49,11 +49,9 @@ **************************************************/ static MLD_INLINE void mld_power2round(int32_t *a0, int32_t *a1, int32_t a) __contract__( - requires(memory_no_alias(a0, sizeof(int32_t))) - requires(memory_no_alias(a1, sizeof(int32_t))) + requires(objs_no_alias(a0, a1)) requires(a >= 0 && a < MLDSA_Q) - assigns(memory_slice(a0, sizeof(int32_t))) - assigns(memory_slice(a1, sizeof(int32_t))) + assigns_objs(a0, a1) ensures(*a0 > -(MLD_2_POW_D/2) && *a0 <= (MLD_2_POW_D/2)) ensures(*a1 >= 0 && *a1 <= (MLDSA_Q - 1) / MLD_2_POW_D) ensures((*a1 * MLD_2_POW_D + *a0 - a) % MLDSA_Q == 0) @@ -81,11 +79,9 @@ __contract__( **************************************************/ static MLD_INLINE void mld_decompose(int32_t *a0, int32_t *a1, int32_t a) __contract__( - requires(memory_no_alias(a0, sizeof(int32_t))) - requires(memory_no_alias(a1, sizeof(int32_t))) + requires(objs_no_alias(a0, a1)) requires(a >= 0 && a < MLDSA_Q) - assigns(memory_slice(a0, sizeof(int32_t))) - assigns(memory_slice(a1, sizeof(int32_t))) + assigns_objs(a0, a1) /* a0 = -MLDSA_GAMMA2 can only occur when (q-1) = a - (a mod MLDSA_GAMMA2), * then a1=1; and a0 = a - (a mod MLDSA_GAMMA2) - 1 (@[FIPS204, Algorithm 36 (Decompose)]) */ ensures(*a0 >= -MLDSA_GAMMA2 && *a0 <= MLDSA_GAMMA2) diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 4dfd19c50..1af495668 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -57,8 +57,7 @@ static int mld_check_pct(uint8_t const pk[MLDSA_CRYPTO_PUBLICKEYBYTES], uint8_t const sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) @@ -138,9 +137,8 @@ static int mld_check_pct(uint8_t const pk[MLDSA_CRYPTO_PUBLICKEYBYTES], static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2, const uint8_t seed[MLDSA_CRHBYTES]) __contract__( - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) + requires(objs_no_alias(s1, s2)) + requires(slices_no_alias(seed, MLDSA_CRHBYTES)) assigns(object_whole(s1), object_whole(s2)) ensures(forall(l0, 0, MLDSA_L, array_abs_bound(s1->vec[l0].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) ensures(forall(k0, 0, MLDSA_K, array_abs_bound(s2->vec[k0].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) @@ -210,19 +208,12 @@ static int mld_compute_t0_t1_tr_from_sk_components( uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], const uint8_t rho[MLDSA_SEEDBYTES], const mld_polyvecl *s1, const mld_polyveck *s2) __contract__( - requires(memory_no_alias(t0, sizeof(mld_polyveck))) - requires(memory_no_alias(t1, sizeof(mld_polyveck))) - requires(memory_no_alias(tr, MLDSA_TRBYTES)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) + requires(objs_no_alias(t0, t1, s1, s2)) + requires(slices_no_alias(tr, MLDSA_TRBYTES, pk, MLDSA_CRYPTO_PUBLICKEYBYTES, rho, MLDSA_SEEDBYTES)) requires(forall(l0, 0, MLDSA_L, array_bound(s1->vec[l0].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) requires(forall(k0, 0, MLDSA_K, array_bound(s2->vec[k0].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) - assigns(memory_slice(t0, sizeof(mld_polyveck))) - assigns(memory_slice(t1, sizeof(mld_polyveck))) - assigns(memory_slice(tr, MLDSA_TRBYTES)) - assigns(memory_slice(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + assigns_objs(t0, t1) + assigns_slices(tr, MLDSA_TRBYTES, pk, MLDSA_CRYPTO_PUBLICKEYBYTES) ensures(forall(k1, 0, MLDSA_K, array_bound(t0->vec[k1].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))) ensures(forall(k2, 0, MLDSA_K, array_bound(t1->vec[k2].coeffs, 0, MLDSA_N, 0, 1 << 10))) ensures(return_value == 0 || return_value == MLD_ERR_OUT_OF_MEMORY)) @@ -400,11 +391,10 @@ __contract__( requires(in2len <= MLD_MAX_BUFFER_SIZE) requires(in3len <= MLD_MAX_BUFFER_SIZE) requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(in1, in1len)) - requires(in2len == 0 || memory_no_alias(in2, in2len)) - requires(in3len == 0 || memory_no_alias(in3, in3len)) - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(out, outlen)) + requires(slices_no_alias(in1, in1len, out, outlen)) + requires(in2len == 0 || slices_no_alias(in2, in2len)) + requires(in3len == 0 || slices_no_alias(in3, in3len)) + assigns_slices(out, outlen) ) { mld_shake256ctx state; @@ -469,20 +459,15 @@ static int mld_attempt_signature_generation( const mld_polymat *mat, const mld_polyvecl *s1, const mld_polyveck *s2, const mld_polyveck *t0) __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(slices_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(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ) diff --git a/mldsa/src/sign.h b/mldsa/src/sign.h index 7c8ecc97c..7a237b45e 100644 --- a/mldsa/src/sign.h +++ b/mldsa/src/sign.h @@ -111,9 +111,7 @@ int crypto_sign_keypair_internal(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], const uint8_t seed[MLDSA_SEEDBYTES]) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - requires(memory_no_alias(seed, MLDSA_SEEDBYTES)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES, seed, MLDSA_SEEDBYTES)) assigns(object_whole(pk)) assigns(object_whole(sk)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || @@ -144,8 +142,7 @@ MLD_EXTERNAL_API int crypto_sign_keypair(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) assigns(object_whole(pk)) assigns(object_whole(sk)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || @@ -193,14 +190,11 @@ int crypto_sign_signature_internal( __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(prelen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(m, mlen)) - requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - requires((externalmu == 0 && (prelen == 0 || memory_no_alias(pre, prelen))) || + requires(objs_no_alias(siglen)) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, m, mlen, rnd, MLDSA_RNDBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires((externalmu == 0 && (prelen == 0 || slices_no_alias(pre, prelen))) || (externalmu == 1 && mlen == MLDSA_CRHBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) assigns(object_whole(siglen)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) @@ -243,13 +237,11 @@ int crypto_sign_signature(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen, const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(m, mlen)) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(objs_no_alias(siglen)) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, m, mlen, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) && *siglen == 0)) @@ -285,11 +277,9 @@ int crypto_sign_signature_extmu(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen, const uint8_t mu[MLDSA_CRHBYTES], const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(mu, MLDSA_CRHBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(objs_no_alias(siglen)) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, mu, MLDSA_CRHBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) && *siglen == 0)) @@ -324,13 +314,11 @@ int crypto_sign(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen, const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sm, MLDSA_CRYPTO_BYTES + mlen)) - requires(memory_no_alias(smlen, sizeof(size_t))) - requires(m == sm || memory_no_alias(m, mlen)) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sm, MLDSA_CRYPTO_BYTES + mlen)) + requires(objs_no_alias(smlen)) + requires(slices_no_alias(sm, MLDSA_CRYPTO_BYTES + mlen, ctx, ctxlen, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(m == sm || slices_no_alias(m, mlen)) + assigns_slices(sm, MLDSA_CRYPTO_BYTES + mlen) assigns(object_whole(smlen)) ensures((return_value == 0 && *smlen == MLDSA_CRYPTO_BYTES + mlen) || (return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY)) @@ -371,11 +359,10 @@ __contract__( requires(prelen <= MLD_MAX_BUFFER_SIZE) requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(m, mlen)) + requires(slices_no_alias(sig, siglen, m, mlen)) requires(externalmu == 0 || (externalmu == 1 && mlen == MLDSA_CRHBYTES)) - requires(externalmu == 1 || prelen == 0 || memory_no_alias(pre, prelen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(externalmu == 1 || prelen == 0 || slices_no_alias(pre, prelen)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -411,10 +398,9 @@ __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(siglen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(m, mlen)) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(slices_no_alias(sig, siglen, m, mlen)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -446,9 +432,7 @@ int crypto_sign_verify_extmu(const uint8_t *sig, size_t siglen, const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) __contract__( requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(mu, MLDSA_CRHBYTES)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(slices_no_alias(sig, siglen, mu, MLDSA_CRHBYTES, pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -480,14 +464,12 @@ int crypto_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) __contract__( requires(smlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(m, smlen)) - requires(memory_no_alias(mlen, sizeof(size_t))) - requires(m == sm || memory_no_alias(sm, smlen)) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - assigns(memory_slice(m, smlen)) - assigns(memory_slice(mlen, sizeof(size_t))) + requires(objs_no_alias(mlen)) + requires(slices_no_alias(m, smlen, ctx, ctxlen, pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(m == sm || slices_no_alias(sm, smlen)) + assigns_objs(mlen) + assigns_slices(m, smlen) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -535,13 +517,10 @@ int crypto_sign_signature_pre_hash_internal( __contract__( requires(ctxlen <= MLD_MAX_BUFFER_SIZE) requires(phlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(ph, phlen)) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(objs_no_alias(siglen)) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, ph, phlen, rnd, MLDSA_RNDBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) && *siglen == 0)) @@ -588,10 +567,9 @@ __contract__( requires(phlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77) requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(ph, phlen)) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(slices_no_alias(sig, siglen, ph, phlen)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -631,13 +609,10 @@ int crypto_sign_signature_pre_hash_shake256( __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(m, mlen)) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(objs_no_alias(siglen)) + requires(slices_no_alias(sig, MLDSA_CRYPTO_BYTES, m, mlen, rnd, MLDSA_RNDBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + assigns_slices(sig, MLDSA_CRYPTO_BYTES) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) && *siglen == 0)) @@ -677,10 +652,9 @@ __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77) requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(m, mlen)) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(slices_no_alias(sig, siglen, m, mlen)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -735,10 +709,10 @@ size_t mld_prepare_domain_separation_prefix( __contract__( requires(ctxlen <= 255) requires(phlen <= MLD_MAX_BUFFER_SIZE) - requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(hashalg == MLD_PREHASH_NONE || memory_no_alias(ph, phlen)) - requires(memory_no_alias(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES)) - assigns(memory_slice(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES)) + requires(ctxlen == 0 || slices_no_alias(ctx, ctxlen)) + requires(hashalg == MLD_PREHASH_NONE || slices_no_alias(ph, phlen)) + requires(slices_no_alias(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES)) + assigns_slices(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES) ensures(return_value <= MLD_DOMAIN_SEPARATION_MAX_BYTES) ); @@ -765,9 +739,8 @@ MLD_EXTERNAL_API int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(slices_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES, sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + assigns_slices(pk, MLDSA_CRYPTO_PUBLICKEYBYTES) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); #endif /* !MLD_SIGN_H */