Making ML-KEM Extract Again

.github/workflows/hax.yml

@@ -52,70 +52,12 @@ jobs:
         run: |
           nix profile install ./hax
 
-      - name: 🏃 Extract the Kyber reference code
-        run: |
-          eval $(opam env)
-          (cd proofs/fstar/extraction/ && ./clean.sh)
-          rm -f sys/platform/proofs/fstar/extraction/*.fst*
-          ./hax-driver.py --kyber-reference
-
-      - name: 🏃 Regenerate `extraction-*` folders
-        run: ./proofs/fstar/patches.sh apply
-
-      - name: 🏃 Make sure snapshots are up-to-date
-        run: git diff --exit-code
-
-      - name: 🏃 Verify the Kyber reference code
-        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-driver.py --verify-extraction
-
-      - name: 🏃 Verify Kyber `extraction-edited` F* code
-        run: |
-          env FSTAR_HOME=${{ github.workspace }}/fstar \
-              HACL_HOME=${{ github.workspace }}/hacl-star \
-              HAX_HOME=${{ github.workspace }}/hax \
-              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
-              make -C proofs/fstar/extraction-edited
-
-      - name: 🏃 Verify Kyber `extraction-secret-independent` F* code
-        run: |
-          env FSTAR_HOME=${{ github.workspace }}/fstar \
-              HACL_HOME=${{ github.workspace }}/hacl-star \
-              HAX_HOME=${{ github.workspace }}/hax \
-              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
-              make -C proofs/fstar/extraction-secret-independent
-
-      - name: 🏃 Extract & Verify ML-KEM crate (lax)
+      - name: 🏃 Extract ML-KEM crate
         run: |
           cd libcrux-ml-kem
-          # ./hax.py extract
+          ./hax.py extract
           # 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
-
-      - name: 🏃 Extract the Kyber specification
-        run: |
-          eval $(opam env)
-          # Extract the functions in the compress module individually to test
-            # the function-extraction code.
-          # Extract functions from the remaining modules to test the
-          # module-extraction code.
-          ./hax-driver.py --crate-path specs/kyber \
-            --functions hacspec_kyber::compress::compress \
-                        hacspec_kyber::compress::decompress \
-                        hacspec_kyber::compress::compress_d \
-                        hacspec::kyber::compress::decompress_d \
-            --modules ind_cpa \
-                      hacspec_kyber \
-                      matrix \
-                      ntt \
-                      parameters \
-                      sampling \
-                      serialize \
-            --exclude-modules libcrux::hacl::sha3 libcrux::digest

Cargo.toml

@@ -8,7 +8,6 @@ members = [
     "benchmarks",
     "fuzz",
     "libcrux-ml-kem",
-    "libcrux-simd",
     "libcrux-sha3",
     "libcrux-ml-dsa",
     "libcrux-intrinsics",