CI should work now?

cryspen · Nov 24, 2023 · be406dd · be406dd
1 parent 7bbb472
commit be406dd
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -74,6 +74,7 @@ jobs:
 
       - 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

diff --git a/hax-driver.py b/hax-driver.py
@@ -130,12 +130,16 @@ def shell(command, expect=0, cwd=None, env={}):
 cargo_hax_into = ["cargo", "hax", "into"]
 hax_env = {}
 
+exclude_sha3_implementations = "-libcrux::hacl::sha3::** -libcrux::jasmin::sha3::**"
+
 if options.kyber_reference:
     shell(
         cargo_hax_into
         + [
             "-i",
-            "-** +libcrux::kem::kyber::** -libcrux::hacl::sha3::** -libcrux::digest::** -libcrux::**::types::index_impls::**",
+            "-** +libcrux::kem::kyber::** {} -libcrux::digest::** -libcrux::**::types::index_impls::**".format(
+                exclude_sha3_implementations
+            ),
             "fstar",
         ],
         cwd=".",
@@ -146,7 +150,9 @@ def shell(command, expect=0, cwd=None, env={}):
         cargo_hax_into
         + [
             "-i",
-            "-** +compress::* +ind_cpa::* +hacspec_kyber::* +matrix::* +ntt::* +parameters::* +sampling::* +serialize::* -libcrux::hacl::sha3::* -libcrux::digest::*",
+            "-** +compress::* +ind_cpa::* +hacspec_kyber::* +matrix::* +ntt::* +parameters::* +sampling::* +serialize::* {} -libcrux::digest::*".format(
+                exclude_sha3_implementations
+            ),
             "fstar",
         ],
         cwd=os.path.join("specs", "kyber"),