|
43 | 43 | # but we use this as a fast path to not even start the proofs |
44 | 44 | # if the byte code needs updating. |
45 | 45 | hol_light_bytecode: |
46 | | - name: HOL-Light bytecode check |
| 46 | + name: AArch64 HOL-Light bytecode check |
47 | 47 | runs-on: pqcp-arm64 |
48 | 48 | if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork |
49 | 49 | steps: |
|
57 | 57 | script: | |
58 | 58 | autogen --update-hol-light-bytecode --dry-run |
59 | 59 | hol_light_interactive: |
60 | | - name: HOL-Light interactive shell test |
| 60 | + name: AArch64 HOL-Light interactive shell test |
61 | 61 | runs-on: pqcp-arm64 |
62 | 62 | needs: [ hol_light_bytecode ] |
63 | 63 | if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork |
@@ -109,7 +109,7 @@ jobs: |
109 | 109 | needs: ["keccak_specs.ml"] |
110 | 110 | - name: keccak_f1600_x4_v8a_scalar |
111 | 111 | needs: ["keccak_specs.ml"] |
112 | | - name: HOL Light proof for ${{ matrix.proof.name }}.S |
| 112 | + name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S |
113 | 113 | runs-on: pqcp-arm64 |
114 | 114 | if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork |
115 | 115 | steps: |
@@ -151,7 +151,7 @@ jobs: |
151 | 151 |
|
152 | 152 | # x86_64 proofs |
153 | 153 | hol_light_bytecode_x86_64: |
154 | | - name: HOL-Light bytecode check |
| 154 | + name: x86_64 HOL-Light bytecode check |
155 | 155 | runs-on: pqcp-x64 |
156 | 156 | if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork |
157 | 157 | steps: |
@@ -194,7 +194,7 @@ jobs: |
194 | 194 | needs: ["mlkem_specs.ml"] |
195 | 195 | - name: mlkem_poly_basemul_acc_montgomery_cached_k4 |
196 | 196 | needs: ["mlkem_specs.ml"] |
197 | | - name: HOL Light proof for ${{ matrix.proof.name }}.S |
| 197 | + name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S |
198 | 198 | runs-on: pqcp-x64 |
199 | 199 | if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork |
200 | 200 | steps: |
|
0 commit comments