Minor refactoring (#111)

* Remove benchmarking of Kyber specification. * Removed unused variable in extract_to_fstar.py * Skip Kyber specification sampling tests for now.
cryspen · Oct 12, 2023 · b191a32 · b191a32
1 parent 6a133b9
commit b191a32
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 130 deletions.
diff --git a/extract_to_fstar.py b/extract_to_fstar.py
@@ -6,7 +6,7 @@
 import sys
 
 
-def shell(command, expect=0, cwd=None, format_filter_string=False):
+def shell(command, expect=0, cwd=None):
     subprocess_stdout = subprocess.DEVNULL
 
     print("Command: ", end="")
@@ -101,7 +101,6 @@ def shell(command, expect=0, cwd=None, format_filter_string=False):
             "fstar",
         ],
         cwd=options.crate_path,
-        format_filter_string=True,
     )
 elif options.kyber_reference:
     shell(
@@ -114,7 +113,6 @@ def shell(command, expect=0, cwd=None, format_filter_string=False):
             "fstar",
         ],
         cwd=".",
-        format_filter_string=True,
     )
 else:
     shell(["cargo", "hax", "into", "fstar"], cwd=options.crate_path)
diff --git a/specs/kyber/Cargo.toml b/specs/kyber/Cargo.toml
@@ -8,14 +8,9 @@ libcrux = { version = "=0.0.2-pre.1", path = "../../" }
 hacspec-lib = { version = "0.0.1", path = "../hacspec-lib" }
 
 [dev-dependencies]
-criterion = "0.5.1"
 hex = { version = "0.4.3", features = ["serde"] }
 pqcrypto-kyber = { version = "0.7.6", default-features = false }
 proptest = "1.2.0"
 rand = "0.8.5"
 serde = { version = "1.0.171", features = ["derive"] }
 serde_json = "1.0.102"
-
-[[bench]]
-name = "kem"
-harness = false
diff --git a/specs/kyber/benches/kem.rs b/specs/kyber/benches/kem.rs
diff --git a/specs/kyber/src/sampling.rs b/specs/kyber/src/sampling.rs
@@ -232,6 +232,7 @@ mod tests {
 
     proptest! {
         #[test]
+        #[ignore = "see https://github.com/cryspen/libcrux/issues/112"]
         fn uniform_sampler_mean_and_variance(randomness in vec(any::<u8>(), REJECTION_SAMPLING_ATTEMPTS * parameters::REJECTION_SAMPLING_SEED_SIZE)) {
             let mut sampled_ring_element = KyberPolynomialRingElement::ZERO;
 
@@ -277,6 +278,7 @@ mod tests {
         }
 
         #[test]
+        #[ignore = "see https://github.com/cryspen/libcrux/issues/112"]
         fn binomial_sampler_mean_and_variance(
             randomness in vec(any::<u8>(), 2 * 2 * 64)
             )