Fix hax extraction and run hax on CI for Kyber reference implementati…

…on . (#83)

.github/workflows/hax.yml

@@ -0,0 +1,45 @@
+name: hax
+
+on:
+  push:
+    branches: ["dev"]
+  pull_request:
+    branches: ["dev"]
+  workflow_dispatch:
+
+env:
+  CARGO_TERM_COLOR: always
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  hax:
+    runs-on: "ubuntu-latest"
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: 🔨 OCaml Setup
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: 4.14.1
+
+      - name: ⤵ Clone hax repository
+        uses: actions/checkout@v4
+        with:
+          repository: hacspec/hacspec-v2
+          path: hax
+
+      - name: 🔨 Setup hax
+        working-directory: hax
+        run: |
+          sudo apt-get update
+          sudo apt-get install --yes nodejs
+          ./setup.sh
+
+      - name: 🏃🏻‍♀️ Run hax
+        run: |
+          eval $(opam env)
+          cargo hax into -i '-** +kem::kyber768::** -kem::kyber768::arithmetic::mutable_operations::**' fstar

src/kem/kyber768.rs

@@ -1,10 +1,18 @@
+// This module is declared here since otherwise, hax reports the following error:
+//
+// The THIR body of item
+// DefId(0:986 ~ libcrux[92b3]::kem::kyber768::parameters::COEFFICIENTS_IN_RING_ELEMENT)
+// was stolen.
+//
+// This is being tracked in https://github.com/hacspec/hacspec-v2/issues/27
+mod parameters;
+
 mod arithmetic;
 mod compress;
 mod constant_time_ops;
 mod conversions;
 mod ind_cpa;
 mod ntt;
-mod parameters;
 mod sampling;
 mod serialize;