ci(hax): update the hax setup (#404)

.github/workflows/hax.yml

@@ -15,14 +15,14 @@ jobs:
         uses: hacspec/hax-actions@main
         with:
           # pin hax to known-working
-          hax_reference: 533f87048f68705e8884ff9516db1371e8a2773d
+          hax_reference: 5e3e6d2028db0ca8f583b427f770bbb7c26c7bed
 
       - name: 🏃 Extract `riot-rs-runqueue`
         working-directory: ./src/riot-rs-runqueue
         run: |
           rm -f proofs/fstar/extraction/*.fst*
           cargo hax into fstar
 
-      - name: 🏃 Verify `riot-rs-runqueue`
+      - name: 🏃 Lax check `riot-rs-runqueue`
         working-directory: ./src/riot-rs-runqueue/proofs/fstar/extraction
-        run: make
+        run: OTHERFLAGS="--lax" make

_typos.toml

@@ -10,4 +10,5 @@ celcius = "celcius" # Until embedded-aht20 is fixed
 extend-exclude = [
   "doc/*.svg",
   "src/riot-rs-embassy/src/wifi/cyw43/firmware/README.md",
+  "src/riot-rs-runqueue/proofs/fstar/extraction/Makefile",
 ]

deny.toml

@@ -47,6 +47,7 @@ unknown-registry = "deny"
 unknown-git = "deny"
 # List of URLs for allowed Git repositories
 allow-git = [
+  "https://github.com/hacspec/hax",
   "https://github.com/smoltcp-rs/smoltcp",
   "https://github.com/twitchyliquid64/usbd-hid",
   "https://gitlab.com/oscore/liboscore",

src/riot-rs-runqueue/Cargo.toml

@@ -11,3 +11,9 @@ workspace = true
 
 [dependencies]
 defmt = { workspace = true, optional = true }
+
+# This is required so that F* can find the required F* model of the Rust core
+# lib, as documented in the hax documentation:
+# https://hacspec.org/book/quick_start/intro.html#setup-the-crate-you-want-to-verify
+[target.'cfg(hax)'.dependencies]
+hax-lib = { git = "https://github.com/hacspec/hax", rev = "5e3e6d2028db0ca8f583b427f770bbb7c26c7bed" }