SparsePostQuantumRatchet/.github/workflows/hax.yml
2025-10-02 09:29:32 -07:00

27 lines
540 B
YAML

name: hax
on:
push:
jobs:
fstar-type-checking:
runs-on: "ubuntu-latest"
steps:
- uses: actions/checkout@v4
- name: โคต Install and configure hax
uses: hacspec/hax-actions@main
with:
fstar: v2025.02.17
hax_reference: hax-lib-v0.3.5
- run: sudo apt-get install protobuf-compiler
- name: ๐Ÿƒ Extract F*
run: |
rm -f proofs/fstar/extraction/*.fst*
./hax.py extract
- name: ๐Ÿƒ Type-check extracted F*
run: ./hax.py prove