Extract and TC ML-Kem #3174
Workflow file for this run
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
| name: Extract and TC ML-Kem | |
| on: | |
| pull_request: | |
| merge_group: | |
| workflow_dispatch: | |
| push: | |
| branches: [main] | |
| env: | |
| CARGO_TERM_COLOR: always | |
| jobs: | |
| extract-mlkem: | |
| if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }} | |
| runs-on: "ubuntu-latest" | |
| steps: | |
| - name: ⤵ Extract libcrux version from PR body | |
| id: extract_version | |
| uses: actions/github-script@v7 | |
| with: | |
| result-encoding: string | |
| script: | | |
| let extractLibcruxRef = body => body.match(/libcrux-ref:\s*([a-zA-Z0-9._\/-]+)/)?.[1]; | |
| const refMap = new Map(); | |
| if (context.eventName === 'pull_request') { | |
| const ref = extractLibcruxRef(context.payload.pull_request?.body || '') ?? 'main'; | |
| core.notice(`Using libcrux ref: ${resolved}`); | |
| return resolved; | |
| } else if (context.eventName === 'merge_group') { | |
| const query = 'query {repository(owner:"cryspen", name:"hax") {mergeQueue {entries(first:100) {nodes {pullRequest {body, number}}}}}}'; | |
| const result = await github.graphql(query); | |
| const mergeQueuePRs = result.repository.mergeQueue.entries.nodes; | |
| for (const entry of mergeQueuePRs) { | |
| const pr = entry.pullRequest | |
| core.notice("Found merge queue PR:", pr); | |
| const ref = extractLibcruxRef(pr.body); | |
| ref && refMap.set(pr.number, ref); | |
| } | |
| if (refMap.size === 0) { | |
| core.notice('No libcrux-ref specified, defaulting to "main"'); | |
| return 'main'; | |
| } | |
| const uniqueRefs = new Set(refMap.values()); | |
| if (uniqueRefs.size > 1) { | |
| let errorMessage = 'Error: Multiple different libcrux refs detected:\n'; | |
| for (const [prNum, ref] of refMap.entries()) | |
| errorMessage += `- PR #${prNum}: ${ref}\n`; | |
| core.setFailed(errorMessage); | |
| return; | |
| } | |
| const [ref] = uniqueRefs; | |
| core.notice(`Using libcrux ref: ${ref}`); | |
| return ref; | |
| } | |
| core.warning(`Unsupported event type: ${context.eventName}, default to main`); | |
| return 'main'; | |
| - name: ⤵ Clone Libcrux repository | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: cryspen/libcrux | |
| path: libcrux | |
| ref: ${{ steps.extract_version.outputs.result }} | |
| - uses: actions/checkout@v4 | |
| with: | |
| path: hax | |
| - name: Use local hax-lib | |
| working-directory: libcrux | |
| run: | | |
| cargo remove hax-lib -v -p libcrux-ml-kem | |
| cargo add hax-lib --path "../hax/hax-lib" -v -p libcrux-ml-kem | |
| - uses: DeterminateSystems/nix-installer-action@main | |
| - name: Set up Cachix | |
| uses: cachix/cachix-action@v15 | |
| with: | |
| name: fstar-nix-versions | |
| push: false | |
| - name: ⤵ Install hax | |
| run: | | |
| nix profile install ./hax | |
| - name: ⤵ Install FStar | |
| run: nix profile install github:FStarLang/FStar/v2025.02.17 | |
| - name: 🏃 Extract ML-KEM crate | |
| working-directory: libcrux/libcrux-ml-kem | |
| run: ./hax.py extract | |
| - name: 🏃 Lax ML-KEM crate | |
| working-directory: libcrux/libcrux-ml-kem | |
| run: | | |
| env FSTAR_HOME=${{ github.workspace }}/fstar \ | |
| HAX_HOME=${{ github.workspace }}/hax \ | |
| PATH="${PATH}:${{ github.workspace }}/fstar/bin" \ | |
| ./hax.py prove --admit |