Merge pull request #719 from cryspen/franziskus/mldsa-samplev3

Introduce AVX2 `target_feature` boundary in x4 sampling
cryspen · Dec 19, 2024 · d45d29b · d45d29b
2 parents e7dca38 + 8c00dbf
commit d45d29b
Show file tree

Hide file tree

Showing 40 changed files with 3,284 additions and 3,418 deletions.
diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fst b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fst
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Arm64_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Arm64_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fst b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fst
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Avx2_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Avx2_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-ml-dsa/cg.yaml b/libcrux-ml-dsa/cg.yaml
@@ -53,7 +53,8 @@ files:
     include_in_h:
       - '"intrinsics/libcrux_intrinsics_avx2.h"'
     api:
-      patterns:  
+      patterns:
+        - [libcrux_ml_dsa, samplex4, avx2, "*"]
         - [libcrux_ml_dsa, simd, avx2, "*"]
         - [libcrux_ml_dsa, hash_functions, simd256, "*"]
         - [libcrux_ml_dsa, ml_dsa_65, avx2, "*"]
@@ -76,6 +77,7 @@ files:
     api:
       patterns:
         - [libcrux_ml_dsa, "*"]
+        - [libcrux_ml_dsa, samplex4, portable, "*"]
         - [libcrux_ml_dsa, simd, "*"]
         - [libcrux_ml_dsa, hash_functions, portable, "*"]
         - [libcrux_ml_dsa, ml_dsa_65, portable, "*"]

diff --git a/libcrux-ml-dsa/cg/code_gen.txt b/libcrux-ml-dsa/cg/code_gen.txt
@@ -3,4 +3,4 @@ Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
 Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
 Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
 F*: b0961063393215ca65927f017720cb365a193833-dirty
-Libcrux: d4b51bcb3af12fb1358ed37830e33cbd72d31590
+Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
diff --git a/libcrux-ml-dsa/cg/header.txt b/libcrux-ml-dsa/cg/header.txt
@@ -8,5 +8,5 @@
  * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
  * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: d4b51bcb3af12fb1358ed37830e33cbd72d31590
+ * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
  */
diff --git a/libcrux-ml-dsa/cg/libcrux_core.h b/libcrux-ml-dsa/cg/libcrux_core.h
@@ -8,7 +8,7 @@
  * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
  * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 87497297c8d9a6be6127d9daae13a942b5439e74
+ * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
  */
 
 #ifndef __libcrux_core_H
@@ -139,11 +139,11 @@ typedef struct libcrux_ml_dsa_ml_dsa_65_MLDSA65Signature_s {
 This function found in impl {libcrux_ml_dsa::types::MLDSASignature<SIZE>#4}
 */
 /**
-A monomorphic instance of libcrux_ml_dsa.types.as_raw_8f
+A monomorphic instance of libcrux_ml_dsa.types.as_ref_8f
 with const generics
 - SIZE= 3309
 */
-static inline uint8_t *libcrux_ml_dsa_types_as_raw_8f_fa(
+static inline uint8_t *libcrux_ml_dsa_types_as_ref_8f_fa(
     libcrux_ml_dsa_ml_dsa_65_MLDSA65Signature *self) {
   return self->value;
 }
@@ -216,11 +216,11 @@ This function found in impl
 {libcrux_ml_dsa::types::MLDSAVerificationKey<SIZE>#2}
 */
 /**
-A monomorphic instance of libcrux_ml_dsa.types.as_raw_66
+A monomorphic instance of libcrux_ml_dsa.types.as_ref_66
 with const generics
 - SIZE= 1952
 */
-static inline uint8_t *libcrux_ml_dsa_types_as_raw_66_97(
+static inline uint8_t *libcrux_ml_dsa_types_as_ref_66_97(
     libcrux_ml_dsa_types_MLDSAVerificationKey_ea *self) {
   return self->value;
 }
@@ -369,11 +369,11 @@ typedef struct libcrux_ml_dsa_types_MLDSASigningKey_22_s {
 This function found in impl {libcrux_ml_dsa::types::MLDSASigningKey<SIZE>}
 */
 /**
-A monomorphic instance of libcrux_ml_dsa.types.as_raw_9b
+A monomorphic instance of libcrux_ml_dsa.types.as_ref_9b
 with const generics
 - SIZE= 4032
 */
-static inline uint8_t *libcrux_ml_dsa_types_as_raw_9b_09(
+static inline uint8_t *libcrux_ml_dsa_types_as_ref_9b_09(
     libcrux_ml_dsa_types_MLDSASigningKey_22 *self) {
   return self->value;
 }