Skip to content

Coq small fixes

Coq small fixes #1130

Workflow file for this run

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: ⤵ Clone Libcrux repository
uses: actions/checkout@v4
with:
repository: cryspen/libcrux
- uses: actions/checkout@v4
with:
path: hax
- uses: DeterminateSystems/nix-installer-action@main
- uses: DeterminateSystems/magic-nix-cache-action@main
- name: ⤵ Install hax
run: |
nix profile install ./hax
- name: ⤵ Install FStar
run: nix profile install github:FStarLang/FStar/v2024.01.13
- name: ⤵ Clone HACL-star repository
uses: actions/checkout@v4
with:
repository: hacl-star/hacl-star
path: hacl-star
- name: 🏃 Extract ML-KEM crate
working-directory: libcrux-ml-kem
run: ./hax.py extract
- name: 🏃 Lax ML-KEM crate
working-directory: libcrux-ml-kem
run: |
env FSTAR_HOME=${{ github.workspace }}/fstar \
HACL_HOME=${{ github.workspace }}/hacl-star \
HAX_HOME=${{ github.workspace }}/hax \
PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
./hax.py prove --admit