From bf5b5af99f8bbc74354ac7a652950f23029616f9 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Mon, 11 May 2026 20:22:17 -0400 Subject: [PATCH 1/7] Avoid mismatched comparison (suggested code improvement, not a bug!) Signed-off-by: Nicky Mouha --- mlkem/src/verify.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h index 600afa44a..0911a46b8 100644 --- a/mlkem/src/verify.h +++ b/mlkem/src/verify.h @@ -333,7 +333,7 @@ __contract__( ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i])))) { uint8_t r = 0, s = 0; - unsigned i; + size_t i; for (i = 0; i < len; i++) __loop__( From 82e4dc9425bb4521649f4fc777081fae5c0ba33b Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 12:24:21 -0400 Subject: [PATCH 2/7] cbmc.h: fix forall/exists to quantize over all indices Signed-off-by: Nicky Mouha --- mlkem/src/cbmc.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mlkem/src/cbmc.h b/mlkem/src/cbmc.h index 80e1a36fc..07fcf13de 100644 --- a/mlkem/src/cbmc.h +++ b/mlkem/src/cbmc.h @@ -89,14 +89,14 @@ #define forall(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_forall \ { \ - unsigned qvar; \ + size_t qvar; \ ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \ } #define exists(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_exists \ { \ - unsigned qvar; \ + size_t qvar; \ ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \ } /* clang-format on */ From 1229cc13f4e0f3bfcc8392b36c259cf6705591bc Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 12:25:31 -0400 Subject: [PATCH 3/7] verify.h: relax bound on len Signed-off-by: Nicky Mouha --- mlkem/src/verify.h | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h index 0911a46b8..d8fbf30f6 100644 --- a/mlkem/src/verify.h +++ b/mlkem/src/verify.h @@ -317,8 +317,7 @@ __contract__(ensures(return_value == (cond ? a : b))) * * @param[in] a First byte array. * @param[in] b Second byte array. - * @param len Length of the byte arrays, upper-bounded to UINT16_MAX to - * control proof complexity only. + * @param len Length of the byte arrays. * * @retval 0 The byte arrays are equal. * @retval 0xFF The byte arrays are not equal. @@ -326,7 +325,7 @@ __contract__(ensures(return_value == (cond ? a : b))) static MLK_INLINE uint8_t mlk_ct_memcmp(const uint8_t *a, const uint8_t *b, const size_t len) __contract__( - requires(len <= UINT16_MAX) + requires(len <= MLK_MAX_BUFFER_SIZE) requires(memory_no_alias(a, len)) requires(memory_no_alias(b, len)) ensures((return_value == 0) || (return_value == 0xFF)) From 7a03a4d43ce7843a7ece01bda04ae1e18191d3a4 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 12:35:30 -0400 Subject: [PATCH 4/7] cbmc.h: fix spaces Signed-off-by: Nicky Mouha --- mlkem/src/cbmc.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mlkem/src/cbmc.h b/mlkem/src/cbmc.h index 07fcf13de..4d5b7c700 100644 --- a/mlkem/src/cbmc.h +++ b/mlkem/src/cbmc.h @@ -96,7 +96,7 @@ #define exists(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_exists \ { \ - size_t qvar; \ + size_t qvar; \ ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \ } /* clang-format on */ From 0bc7711a9cc1d9d28102207edb13713ceebd8985 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 17:02:52 -0400 Subject: [PATCH 5/7] proofs/cbmc/ct_memcmp/Makefile: use cvc5 instead of bitwuzla Signed-off-by: Nicky Mouha --- proofs/cbmc/ct_memcmp/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/cbmc/ct_memcmp/Makefile b/proofs/cbmc/ct_memcmp/Makefile index 7b7c1ce1f..51c060096 100644 --- a/proofs/cbmc/ct_memcmp/Makefile +++ b/proofs/cbmc/ct_memcmp/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--cvc5 FUNCTION_NAME = mlk_ct_memcmp From 3eda479f8004cebc6b99cb3e3912cafecd8c2c77 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 20:13:47 -0400 Subject: [PATCH 6/7] add cvc5 to Nix config, fix all timeouts Signed-off-by: Nicky Mouha --- flake.nix | 4 ++-- nix/cbmc/default.nix | 2 ++ nix/util.nix | 4 ++-- proofs/cbmc/indcpa_dec/Makefile | 2 +- proofs/cbmc/indcpa_enc/Makefile | 2 +- proofs/cbmc/indcpa_keypair_derand/Makefile | 2 +- proofs/cbmc/keccak_squeeze_once/Makefile | 2 +- proofs/cbmc/nttunpack_native_x86_64/Makefile | 2 +- proofs/cbmc/poly_ntt_native/Makefile | 2 +- proofs/cbmc/poly_reduce_native/Makefile | 2 +- 10 files changed, 13 insertions(+), 11 deletions(-) diff --git a/flake.nix b/flake.nix index 31483560a..be16a6adf 100644 --- a/flake.nix +++ b/flake.nix @@ -25,7 +25,7 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system}; pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system}; util = pkgs.callPackage ./nix/util.nix { - inherit (pkgs) bitwuzla z3; + inherit (pkgs) bitwuzla cvc5 z3; inherit (pkgs-unstable) cbmc; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; @@ -237,7 +237,7 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux; util = pkgs.callPackage ./nix/util.nix { inherit pkgs; - inherit (pkgs) bitwuzla z3; + inherit (pkgs) bitwuzla cvc5 z3; inherit (pkgs-unstable) cbmc; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index 58e21c796..e33f885f0 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -3,6 +3,7 @@ # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT { buildEnv , cbmc +, cvc5 , fetchFromGitHub , callPackage , bitwuzla @@ -37,6 +38,7 @@ buildEnv { inherit bitwuzla# 0.8.2 + cvc5# 1.3.2 ninja; # 1.13.2 }; } diff --git a/nix/util.nix b/nix/util.nix index c63835721..c67116933 100644 --- a/nix/util.nix +++ b/nix/util.nix @@ -2,7 +2,7 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -{ pkgs, cbmc, bitwuzla, z3, python3-for-slothy }: +{ pkgs, cbmc, bitwuzla, cvc5, z3, python3-for-slothy }: rec { glibc-join = p: p.buildPackages.symlinkJoin { name = "glibc-join"; @@ -96,7 +96,7 @@ rec { }; }; - cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla z3; }; + cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla cvc5 z3; }; valgrind_varlat = pkgs.callPackage ./valgrind { }; hol_light' = pkgs.callPackage ./hol_light { }; diff --git a/proofs/cbmc/indcpa_dec/Makefile b/proofs/cbmc/indcpa_dec/Makefile index 0233f0b81..27c8af140 100644 --- a/proofs/cbmc/indcpa_dec/Makefile +++ b/proofs/cbmc/indcpa_dec/Makefile @@ -37,7 +37,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_indcpa_dec diff --git a/proofs/cbmc/indcpa_enc/Makefile b/proofs/cbmc/indcpa_enc/Makefile index e9ac63b84..ddc2a955c 100644 --- a/proofs/cbmc/indcpa_enc/Makefile +++ b/proofs/cbmc/indcpa_enc/Makefile @@ -43,7 +43,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_indcpa_enc diff --git a/proofs/cbmc/indcpa_keypair_derand/Makefile b/proofs/cbmc/indcpa_keypair_derand/Makefile index 115e78769..51bd35025 100644 --- a/proofs/cbmc/indcpa_keypair_derand/Makefile +++ b/proofs/cbmc/indcpa_keypair_derand/Makefile @@ -36,7 +36,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_indcpa_keypair_derand diff --git a/proofs/cbmc/keccak_squeeze_once/Makefile b/proofs/cbmc/keccak_squeeze_once/Makefile index afa7ade38..90cf523f3 100644 --- a/proofs/cbmc/keccak_squeeze_once/Makefile +++ b/proofs/cbmc/keccak_squeeze_once/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--z3 FUNCTION_NAME = mlk_keccak_squeeze_once diff --git a/proofs/cbmc/nttunpack_native_x86_64/Makefile b/proofs/cbmc/nttunpack_native_x86_64/Makefile index f54a2ce0b..d865e27a7 100644 --- a/proofs/cbmc/nttunpack_native_x86_64/Makefile +++ b/proofs/cbmc/nttunpack_native_x86_64/Makefile @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = nttunpack_native_x86_64 diff --git a/proofs/cbmc/poly_ntt_native/Makefile b/proofs/cbmc/poly_ntt_native/Makefile index fb2924e5f..50981df71 100644 --- a/proofs/cbmc/poly_ntt_native/Makefile +++ b/proofs/cbmc/poly_ntt_native/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_poly_ntt diff --git a/proofs/cbmc/poly_reduce_native/Makefile b/proofs/cbmc/poly_reduce_native/Makefile index 8a1202b90..e85b86916 100644 --- a/proofs/cbmc/poly_reduce_native/Makefile +++ b/proofs/cbmc/poly_reduce_native/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_poly_reduce_native From dbe8a5d981581e0438d57bde824e8f5180084e2c Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Fri, 15 May 2026 05:19:51 +0100 Subject: [PATCH 7/7] [TEST] Reduce CI Signed-off-by: Hanno Becker --- .github/workflows/all.yml | 116 ++++----- .github/workflows/hol_light.yml | 414 ++++++++++++++++---------------- 2 files changed, 265 insertions(+), 265 deletions(-) diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml index 6eed804b2..7bedfae86 100644 --- a/.github/workflows/all.yml +++ b/.github/workflows/all.yml @@ -34,14 +34,14 @@ jobs: 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 + # ci: + # name: Extended + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base, nix ] + # uses: ./.github/workflows/ci.yml + # secrets: inherit cbmc: name: CBMC permissions: @@ -51,53 +51,53 @@ jobs: 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 - opentitan_integration: - name: OpenTitan - permissions: - contents: 'read' - id-token: 'write' - needs: [ base ] - uses: ./.github/workflows/integration-opentitan.yml - secrets: inherit - awslc_integration: - name: AWS-LC - permissions: - contents: 'read' - id-token: 'write' - needs: [ base ] - uses: ./.github/workflows/integration-awslc.yml - with: - commit: v1.72.0 - 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 + # opentitan_integration: + # name: OpenTitan + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base ] + # uses: ./.github/workflows/integration-opentitan.yml + # secrets: inherit + # awslc_integration: + # name: AWS-LC + # permissions: + # contents: 'read' + # id-token: 'write' + # needs: [ base ] + # uses: ./.github/workflows/integration-awslc.yml + # with: + # commit: v1.72.0 + # 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/hol_light.yml b/.github/workflows/hol_light.yml index 74860405d..84b29e164 100644 --- a/.github/workflows/hol_light.yml +++ b/.github/workflows/hol_light.yml @@ -56,215 +56,215 @@ jobs: nix-shell: 'hol_light' script: | autogen --update-hol-light-bytecode --dry-run - hol_light_interactive: - name: AArch64 HOL-Light interactive shell test - runs-on: pqcp-arm64 - needs: [ hol_light_bytecode ] - if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - fetch-depth: 0 - - uses: ./.github/actions/setup-shell - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - nix-shell: 'hol_light' - script: | - make -C proofs/hol_light/aarch64 mlkem/poly_tobytes_aarch64_asm.o - echo 'needs "mlkem_native/aarch64/proofs/poly_tobytes_aarch64_asm.ml";;' | hol.sh - hol_light_proofs: - needs: [ hol_light_bytecode ] - strategy: - fail-fast: false - matrix: - proof: - # Dependencies on {name}.{S,ml} are implicit - - name: ntt_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] - - name: intt_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] - - name: poly_tomont_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml"] - - name: poly_mulcache_compute_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] - - name: poly_reduce_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml"] - - name: polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml"] - - name: polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml"] - - name: polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml"] - - name: poly_tobytes_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml" ] - - name: rej_uniform_aarch64_asm - needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_rej_uniform_table.ml"] - - name: keccak_f1600_x1_scalar_aarch64_asm - needs: ["keccak_specs.ml"] - - name: keccak_f1600_x1_v84a_aarch64_asm - needs: ["keccak_specs.ml"] - - name: keccak_f1600_x2_v84a_aarch64_asm - needs: ["keccak_specs.ml"] - - name: keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm - needs: ["keccak_specs.ml"] - - name: keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm - needs: ["keccak_specs.ml"] - name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S - runs-on: pqcp-arm64 - if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - fetch-depth: 0 - - name: Get changed files - id: changed-files - uses: tj-actions/changed-files@9426d40962ed5378910ee2e21d5f8c6fcbf2dd96 # v47.0.6 - - name: Check if dependencies changed - id: check_run - shell: bash - run: | - run_needed=0 - changed_files="${{ steps.changed-files.outputs.all_changed_files }}" - dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}" - for changed in $changed_files; do - for needs in $dependencies; do - if [[ "$changed" == *"$needs" ]]; then - run_needed=1 - fi - done - done + # hol_light_interactive: + # name: AArch64 HOL-Light interactive shell test + # runs-on: pqcp-arm64 + # needs: [ hol_light_bytecode ] + # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork + # steps: + # - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + # with: + # fetch-depth: 0 + # - uses: ./.github/actions/setup-shell + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # nix-shell: 'hol_light' + # script: | + # make -C proofs/hol_light/aarch64 mlkem/poly_tobytes_aarch64_asm.o + # echo 'needs "mlkem_native/aarch64/proofs/poly_tobytes_aarch64_asm.ml";;' | hol.sh + # hol_light_proofs: + # needs: [ hol_light_bytecode ] + # strategy: + # fail-fast: false + # matrix: + # proof: + # # Dependencies on {name}.{S,ml} are implicit + # - name: ntt_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] + # - name: intt_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] + # - name: poly_tomont_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml"] + # - name: poly_mulcache_compute_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] + # - name: poly_reduce_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml"] + # - name: polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml"] + # - name: polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml"] + # - name: polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml"] + # - name: poly_tobytes_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml" ] + # - name: rej_uniform_aarch64_asm + # needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_rej_uniform_table.ml"] + # - name: keccak_f1600_x1_scalar_aarch64_asm + # needs: ["keccak_specs.ml"] + # - name: keccak_f1600_x1_v84a_aarch64_asm + # needs: ["keccak_specs.ml"] + # - name: keccak_f1600_x2_v84a_aarch64_asm + # needs: ["keccak_specs.ml"] + # - name: keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm + # needs: ["keccak_specs.ml"] + # - name: keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm + # needs: ["keccak_specs.ml"] + # name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S + # runs-on: pqcp-arm64 + # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork + # steps: + # - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + # with: + # fetch-depth: 0 + # - name: Get changed files + # id: changed-files + # uses: tj-actions/changed-files@9426d40962ed5378910ee2e21d5f8c6fcbf2dd96 # v47.0.6 + # - name: Check if dependencies changed + # id: check_run + # shell: bash + # run: | + # run_needed=0 + # changed_files="${{ steps.changed-files.outputs.all_changed_files }}" + # dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}" + # for changed in $changed_files; do + # for needs in $dependencies; do + # if [[ "$changed" == *"$needs" ]]; then + # run_needed=1 + # fi + # done + # done - # Always re-run upon change to nix files for HOL-Light - if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/aarch64/Makefile"* ]]; then - run_needed=1 - fi + # # Always re-run upon change to nix files for HOL-Light + # if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/aarch64/Makefile"* ]]; then + # run_needed=1 + # fi - echo "run_needed=${run_needed}" >> "$GITHUB_OUTPUT" - - uses: ./.github/actions/setup-shell - if: | - steps.check_run.outputs.run_needed == '1' - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - nix-shell: 'hol_light' - script: | - tests hol_light -p ${{ matrix.proof.name }} --verbose + # echo "run_needed=${run_needed}" >> "$GITHUB_OUTPUT" + # - uses: ./.github/actions/setup-shell + # if: | + # steps.check_run.outputs.run_needed == '1' + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # nix-shell: 'hol_light' + # script: | + # tests hol_light -p ${{ matrix.proof.name }} --verbose - # x86_64 proofs - hol_light_bytecode_x86_64: - name: x86_64 HOL-Light bytecode check - runs-on: pqcp-x64 - if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - fetch-depth: 0 - - uses: ./.github/actions/setup-shell - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - nix-shell: 'hol_light' - script: | - autogen --update-hol-light-bytecode --dry-run - hol_light_interactive_x86_64: - name: x86_64 HOL-Light interactive shell test - runs-on: pqcp-x64 - needs: [ hol_light_bytecode_x86_64 ] - if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - fetch-depth: 0 - - uses: ./.github/actions/setup-shell - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - nix-shell: 'hol_light' - script: | - make -C proofs/hol_light/x86_64 mlkem/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.o - echo 'needs "mlkem_native/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml";;' | hol.sh - hol_light_proofs_x86_64: - needs: [ hol_light_bytecode_x86_64 ] - strategy: - fail-fast: false - matrix: - proof: - # Dependencies on {name}.{S,ml} are implicit - - name: ntt_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] - - name: intt_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] - - name: polyvec_basemul_acc_montgomery_cached_k2_avx2_asm - needs: ["mlkem_specs.ml"] - - name: polyvec_basemul_acc_montgomery_cached_k3_avx2_asm - needs: ["mlkem_specs.ml"] - - name: polyvec_basemul_acc_montgomery_cached_k4_avx2_asm - needs: ["mlkem_specs.ml"] - - name: reduce_avx2_asm - needs: ["mlkem_specs.ml"] - - name: ntttobytes_avx2_asm - needs: ["mlkem_specs.ml"] - - name: rej_uniform_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_rej_uniform_table.ml"] - - name: nttfrombytes_avx2_asm - needs: ["mlkem_specs.ml"] - - name: tomont_avx2_asm - needs: ["mlkem_specs.ml"] - - name: nttunpack_avx2_asm - needs: ["mlkem_specs.ml"] - - name: poly_mulcache_compute_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] - - name: poly_compress_d4_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_decompress_d4_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_compress_d5_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_decompress_d5_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_compress_d10_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_decompress_d10_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_compress_d11_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: poly_decompress_d11_avx2_asm - needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] - - name: keccak_f1600_x4_avx2_asm - needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"] - name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S - runs-on: pqcp-x64 - if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - fetch-depth: 0 - - name: Get changed files - id: changed-files - uses: tj-actions/changed-files@9426d40962ed5378910ee2e21d5f8c6fcbf2dd96 # v47.0.6 - - name: Check if dependencies changed - id: check_run - shell: bash - run: | - run_needed=0 - changed_files="${{ steps.changed-files.outputs.all_changed_files }}" - dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}" - for changed in $changed_files; do - for needs in $dependencies; do - if [[ "$changed" == *"$needs" ]]; then - run_needed=1 - fi - done - done + # # x86_64 proofs + # hol_light_bytecode_x86_64: + # name: x86_64 HOL-Light bytecode check + # runs-on: pqcp-x64 + # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork + # steps: + # - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + # with: + # fetch-depth: 0 + # - uses: ./.github/actions/setup-shell + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # nix-shell: 'hol_light' + # script: | + # autogen --update-hol-light-bytecode --dry-run + # hol_light_interactive_x86_64: + # name: x86_64 HOL-Light interactive shell test + # runs-on: pqcp-x64 + # needs: [ hol_light_bytecode_x86_64 ] + # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork + # steps: + # - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + # with: + # fetch-depth: 0 + # - uses: ./.github/actions/setup-shell + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # nix-shell: 'hol_light' + # script: | + # make -C proofs/hol_light/x86_64 mlkem/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.o + # echo 'needs "mlkem_native/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml";;' | hol.sh + # hol_light_proofs_x86_64: + # needs: [ hol_light_bytecode_x86_64 ] + # strategy: + # fail-fast: false + # matrix: + # proof: + # # Dependencies on {name}.{S,ml} are implicit + # - name: ntt_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] + # - name: intt_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] + # - name: polyvec_basemul_acc_montgomery_cached_k2_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: polyvec_basemul_acc_montgomery_cached_k3_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: polyvec_basemul_acc_montgomery_cached_k4_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: reduce_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: ntttobytes_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: rej_uniform_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_rej_uniform_table.ml"] + # - name: nttfrombytes_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: tomont_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: nttunpack_avx2_asm + # needs: ["mlkem_specs.ml"] + # - name: poly_mulcache_compute_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] + # - name: poly_compress_d4_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_decompress_d4_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_compress_d5_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_decompress_d5_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_compress_d10_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_decompress_d10_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_compress_d11_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: poly_decompress_d11_avx2_asm + # needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"] + # - name: keccak_f1600_x4_avx2_asm + # needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"] + # name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S + # runs-on: pqcp-x64 + # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork + # steps: + # - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + # with: + # fetch-depth: 0 + # - name: Get changed files + # id: changed-files + # uses: tj-actions/changed-files@9426d40962ed5378910ee2e21d5f8c6fcbf2dd96 # v47.0.6 + # - name: Check if dependencies changed + # id: check_run + # shell: bash + # run: | + # run_needed=0 + # changed_files="${{ steps.changed-files.outputs.all_changed_files }}" + # dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}" + # for changed in $changed_files; do + # for needs in $dependencies; do + # if [[ "$changed" == *"$needs" ]]; then + # run_needed=1 + # fi + # done + # done - # Always re-run upon change to nix files for HOL-Light - if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]]; then - run_needed=1 - fi + # # Always re-run upon change to nix files for HOL-Light + # if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]]; then + # run_needed=1 + # fi - echo "run_needed=${run_needed}" >> "$GITHUB_OUTPUT" - - uses: ./.github/actions/setup-shell - if: | - steps.check_run.outputs.run_needed == '1' - with: - gh_token: ${{ secrets.GITHUB_TOKEN }} - nix-shell: 'hol_light' - script: | - tests hol_light -p ${{ matrix.proof.name }} --verbose + # echo "run_needed=${run_needed}" >> "$GITHUB_OUTPUT" + # - uses: ./.github/actions/setup-shell + # if: | + # steps.check_run.outputs.run_needed == '1' + # with: + # gh_token: ${{ secrets.GITHUB_TOKEN }} + # nix-shell: 'hol_light' + # script: | + # tests hol_light -p ${{ matrix.proof.name }} --verbose