Lax Checking for ML-DSA

.github/workflows/hax.yml

@@ -68,4 +68,13 @@ jobs:
 
       - name: 🏃 Extract ML-DSA crate
         working-directory: libcrux-ml-dsa
-        run: cargo hax into fstar
+        run: ./hax.py extract
+
+      - name: 🏃 Lax ML-DSA crate
+        working-directory: libcrux-ml-dsa
+        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

.gitignore

@@ -2,16 +2,19 @@
 .vscode
 .DS_Store
 benches/boringssl/build
-proofs/fstar/extraction/.depend
-proofs/fstar/extraction/#*#
-proofs/fstar/extraction/.#*
 fuzz/corpus
 fuzz/artifacts
-proofs/fstar/extraction/.cache
 __pycache__
 kyber-crate/
 *.llbc
 .cargo/
 
 # When using sed
 *.bak
+
+# F*
+.fstar-cache
+.depend
+**/proofs/fstar/*/#*#
+**/proofs/fstar/*/.#*
+hax.fst.config.json

Cargo.toml

@@ -78,8 +78,8 @@ getrandom = { version = "0.2", features = ["js"], optional = true }
 # When using the hax toolchain, we have more dependencies.
 # This is only required when doing proofs.
 [target.'cfg(hax)'.dependencies]
-hax-lib-macros = { version = "0.1.0-alpha.1", git = "https://github.com/hacspec/hax", branch = "main" }
-hax-lib = { version = "0.1.0-alpha.1", git = "https://github.com/hacspec/hax/", branch = "main" }
+hax-lib-macros = { git = "https://github.com/hacspec/hax", branch = "main" }
+hax-lib = { git = "https://github.com/hacspec/hax/", branch = "fstar-proof-lib-small-additions" }
 
 [dev-dependencies]
 libcrux = { path = ".", features = ["rand", "tests"] }

benchmarks/benches/kyber768.rs

@@ -80,7 +80,7 @@ pub fn comparisons_pk_validation(c: &mut Criterion) {
         b.iter_batched(
             || libcrux_kem::deterministic::mlkem768_generate_keypair_derand(seed),
             |key_pair| {
-                let _valid = libcrux_kem::ml_kem768_validate_public_key(key_pair.into_parts().1);
+                let _valid = libcrux_kem::ml_kem768_validate_public_key(&key_pair.into_parts().1);
             },
             BatchSize::SmallInput,
         )

fstar-helpers/Makefile.base

@@ -0,0 +1,14 @@
+# Base Makefile for F* in libcrux.
+# This inherits from Makefile.generic, and adds the `specs` folder from HACL.
+
+VERIFY_SLOW_MODULES ?= no
+ifeq (${VERIFY_SLOW_MODULES},no)
+	ADMIT_MODULES += ${SLOW_MODULES}
+endif
+
+EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n";
+EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.';
+EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`';
+
+FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs
+include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic