hax.yml

name: hax

on:
  pull_request:
  push:

jobs:
  hax:
    runs-on: "ubuntu-latest"

    steps:
      - uses: actions/checkout@v4

      - name: ⤵ Install and configure hax
        uses: hacspec/hax-actions@main
        with:
          # pin hax to known-working
          hax_reference: cc29a3f8c0eee80a1682be78cb3b0447a0257d5b

      - name: 🏃 Extract `riot-rs-runqueue`
        working-directory: ./src/riot-rs-runqueue
        run: |
          rm -f proofs/fstar/extraction/*.fst*
          cargo hax into fstar

      - name: 🏃 Lax check `riot-rs-runqueue`
        working-directory: ./src/riot-rs-runqueue/proofs/fstar/extraction
        run: OTHERFLAGS="--lax" make