Dependencies update #719
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Copyright (c) The mlkem-native project authors | |
| # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT | |
| name: HOL-Light | |
| permissions: | |
| contents: read | |
| on: | |
| push: | |
| branches: ["main"] | |
| paths: | |
| - '.github/workflows/hol_light.yml' | |
| - 'proofs/hol_light/arm/Makefile' | |
| - 'proofs/hol_light/arm/**/*.S' | |
| - 'proofs/hol_light/arm/**/*.ml' | |
| - 'proofs/hol_light/x86/Makefile' | |
| - 'proofs/hol_light/x86/**/*.S' | |
| - 'proofs/hol_light/x86/**/*.ml' | |
| - 'flake.nix' | |
| - 'flake.lock' | |
| - 'nix/hol_light/*' | |
| - 'nix/s2n_bignum/*' | |
| pull_request: | |
| branches: ["main"] | |
| paths: | |
| - '.github/workflows/hol_light.yml' | |
| - 'proofs/hol_light/arm/Makefile' | |
| - 'proofs/hol_light/arm/**/*.S' | |
| - 'proofs/hol_light/arm/**/*.ml' | |
| - 'proofs/hol_light/x86/Makefile' | |
| - 'proofs/hol_light/x86/**/*.S' | |
| - 'proofs/hol_light/x86/**/*.ml' | |
| - 'flake.nix' | |
| - 'flake.lock' | |
| - 'nix/hol_light/*' | |
| - 'nix/s2n_bignum/*' | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| # The proofs also check that the byte code is up to date, | |
| # but we use this as a fast path to not even start the proofs | |
| # if the byte code needs updating. | |
| hol_light_bytecode: | |
| name: AArch64 HOL-Light bytecode check | |
| runs-on: pqcp-arm64 | |
| if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork | |
| steps: | |
| - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| 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: | |
| 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@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| 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/arm mlkem/mlkem_poly_tobytes.o | |
| echo 'needs "arm/proofs/mlkem_poly_tobytes.ml";;' | hol.sh | |
| hol_light_proofs: | |
| needs: [ hol_light_bytecode ] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| proof: | |
| # Dependencies on {name}.{S,ml} are implicit | |
| - name: mlkem_ntt | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] | |
| - name: mlkem_intt | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] | |
| - name: mlkem_poly_tomont | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml"] | |
| - name: mlkem_poly_mulcache_compute | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"] | |
| - name: mlkem_poly_reduce | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml"] | |
| - name: mlkem_poly_basemul_acc_montgomery_cached_k2 | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml"] | |
| - name: mlkem_poly_basemul_acc_montgomery_cached_k3 | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml"] | |
| - name: mlkem_poly_basemul_acc_montgomery_cached_k4 | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml"] | |
| - name: mlkem_poly_tobytes | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml" ] | |
| - name: mlkem_rej_uniform | |
| needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_rej_uniform_table.ml"] | |
| - name: keccak_f1600_x1_scalar | |
| needs: ["keccak_specs.ml"] | |
| - name: keccak_f1600_x1_v84a | |
| needs: ["keccak_specs.ml"] | |
| - name: keccak_f1600_x2_v84a | |
| needs: ["keccak_specs.ml"] | |
| - name: keccak_f1600_x4_v8a_v84a_scalar | |
| needs: ["keccak_specs.ml"] | |
| - name: keccak_f1600_x4_v8a_scalar | |
| 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@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Get changed files | |
| id: changed-files | |
| uses: tj-actions/changed-files@e0021407031f5be11a464abee9a0776171c79891 # v47.0.1 | |
| - 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/arm/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 | |
| # 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@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| 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@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| 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 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o | |
| echo 'needs "x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.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: mlkem_ntt | |
| needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] | |
| - name: mlkem_intt | |
| needs: ["mlkem_specs.ml", "mlkem_zetas.ml"] | |
| - name: mlkem_poly_basemul_acc_montgomery_cached_k2 | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_poly_basemul_acc_montgomery_cached_k3 | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_poly_basemul_acc_montgomery_cached_k4 | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_reduce | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_tobytes | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_rej_uniform | |
| needs: ["mlkem_specs.ml", "mlkem_rej_uniform_table.ml"] | |
| - name: mlkem_frombytes | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_tomont | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_unpack | |
| needs: ["mlkem_specs.ml"] | |
| - name: mlkem_mulcache_compute | |
| needs: ["mlkem_specs.ml", "mlkem_zetas.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@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Get changed files | |
| id: changed-files | |
| uses: tj-actions/changed-files@e0021407031f5be11a464abee9a0776171c79891 # v47.0.1 | |
| - 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/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 |