Subtype mismatch

[franziskuskiefer]

Dropping the cloop, which rewrite the iterator into a C loop, gives the following error.

Warning 4: in the arguments to core.slice.iter.{(core::iter::traits::iterator::Iterator␣for␣core::slice::iter::Iter<'a,␣T>[TraitClause@0])#182}.next < libcrux_ml_dsa_polynomial_PolynomialRingElement_9b > □, in the definition of uu____5867, in the sequence statement at index 0, after the definition of iter, in the last element of the sequence, after the definition of uu____5850, in the last element of the sequence, after the definition of verification_key_hash, in the last element of the sequence, after the definition of offset, in top-level declaration libcrux_ml_dsa.encoding.signing_key.generate_serialized_d2, in file libcrux_mldsa65_portable: Malformed input:
subtype mismatch:
   core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_9b* -> core_option_Option  libcrux_ml_dsa_polynomial_PolynomialRingElement_9b* (a.k.a.  core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_9b* -> core_option_Option  libcrux_ml_dsa_polynomial_PolynomialRingElement_9b*) vs:
   core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_9b* -> core_option_Option_dc (a.k.a.  core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_9b* -> core_option_Option_dc)
--------------------------------------------------------------------------------

Cannot re-check libcrux_ml_dsa.encoding.signing_key.generate_serialized_a9 as valid Low* and will not extract it.  If libcrux_ml_dsa.encoding.signing_key.generate_serialized_a9 is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.

Warning 4: in the arguments to core.slice.iter.{(core::iter::traits::iterator::Iterator␣for␣core::slice::iter::Iter<'a,␣T>[TraitClause@0])#182}.next < libcrux_ml_dsa_polynomial_PolynomialRingElement_24 > □, in the definition of uu____5867, in the sequence statement at index 0, after the definition of iter, in the last element of the sequence, after the definition of uu____5850, in the last element of the sequence, after the definition of verification_key_hash, in the last element of the sequence, after the definition of offset, in top-level declaration libcrux_ml_dsa.encoding.signing_key.generate_serialized_a9, in file libcrux_mldsa65_avx2: Malformed input:
subtype mismatch:
   core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_24* -> core_option_Option  libcrux_ml_dsa_polynomial_PolynomialRingElement_24* (a.k.a.  core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_24* -> core_option_Option  libcrux_ml_dsa_polynomial_PolynomialRingElement_24*) vs:
   core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_24* -> core_option_Option_c4 (a.k.a.  core_slice_iter_Iter libcrux_ml_dsa_polynomial_PolynomialRingElement_24* -> core_option_Option_c4)

To reproduce, comment out the cloop (use only the code inside), and run the following inside the libcrux-ml-dsa directory.

cargo clean
./c.sh --config cg.yaml --out cg --no-glue --no-unrolling --no-karamel_include --no-karamel_include --mldsa65

[msprotz]

@franziskuskiefer this generates more monomorphizations, so you will need the following patch to libcrux (as tested on your franziskus/mldsa-c-ci branch):

diff --git a/libcrux-ml-dsa/cg.yaml b/libcrux-ml-dsa/cg.yaml
index 5ea47625..a7d0f286 100644
--- a/libcrux-ml-dsa/cg.yaml
+++ b/libcrux-ml-dsa/cg.yaml
@@ -69,7 +69,9 @@ files:
       monomorphizations_using:
         - [libcrux_ml_dsa, simd, avx2, "*"]
         - [libcrux_ml_dsa, hash_functions, simd256, "*"]
-      # monomorphizations_exact:
+      monomorphizations_exact:
+        - ["libcrux_ml_dsa_polynomial_PolynomialRingElement libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit_x4"]
+        - ["libcrux_ml_dsa_polynomial_PolynomialRingElement libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit[6size_t]_x2"]
       #   - [core, option, Option_c4]

   - name: libcrux_mldsa65_portable

the names are for some reason not using the short suffix feature, but maybe it's because you're using function types somewhere? not sure -- need to investigate, please file a bug if the long names are bothersome

if you uncomment the cloop! you get further bundling issues, which I'm working on right now, but at least the patch above should restore things back to normal for ml-dsa

[msprotz]

@franziskuskiefer should you disable one of those cloop! macros, you will need the following change to cg.yaml:

diff --git a/libcrux-ml-dsa/cg.yaml b/libcrux-ml-dsa/cg.yaml
index 5ea47625..191e60bb 100644
--- a/libcrux-ml-dsa/cg.yaml
+++ b/libcrux-ml-dsa/cg.yaml
@@ -69,8 +69,11 @@ files:
       monomorphizations_using:
         - [libcrux_ml_dsa, simd, avx2, "*"]
         - [libcrux_ml_dsa, hash_functions, simd256, "*"]
-      # monomorphizations_exact:
-      #   - [core, option, Option_c4]
+      monomorphizations_exact:
+        - ["libcrux_ml_dsa_polynomial_PolynomialRingElement libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit_x4"]
+        - ["libcrux_ml_dsa_polynomial_PolynomialRingElement libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit[6size_t]_x2"]
+        - [core, result, Result_ef0]
+        - [core, option, Option_c4]

   - name: libcrux_mldsa65_portable
     inline_static: true
@@ -101,6 +104,7 @@ files:
       monomorphizations_exact:
         - [libcrux_ml_dsa, pre_hash, PreHashResult]
         - [core, result, Result_a8]
+        - [core, result, Result_ef]
         - [core, option, Option_84]

furthermore, the C code will now change as follows:

-  for (size_t i = (size_t)0U;
-       i < Eurydice_slice_len(
-               Eurydice_array_to_slice(
-                   (size_t)5U, s1,
-                   libcrux_ml_dsa_polynomial_PolynomialRingElement_24),
-               libcrux_ml_dsa_polynomial_PolynomialRingElement_24);
-       i++) {
-    size_t _cloop_j = i;
-    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 *ring_element =
-        &s1[_cloop_j];
-    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 uu____1 =
-        ring_element[0U];
-    libcrux_ml_dsa_encoding_error_serialize_a8(
-        uu____1, Eurydice_array_to_subslice2(signing_key_serialized, offset,
-                                             offset + (size_t)128U, uint8_t));
-    offset = offset + (size_t)128U;
+  core_slice_iter_Iter iter =
+      core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I__1__into_iter(
+          core_slice___Slice_T___iter(
+              Eurydice_array_to_slice(
+                  (size_t)5U, s1,
+                  libcrux_ml_dsa_polynomial_PolynomialRingElement_24),
+              libcrux_ml_dsa_polynomial_PolynomialRingElement_24,
+              core_slice_iter_Iter),
+          core_slice_iter_Iter, core_slice_iter_Iter);
+  while (true) {
+    Option_c4 uu____1 =
+        core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Iter__a__T__TraitClause_0___182__next(
+            &iter, libcrux_ml_dsa_polynomial_PolynomialRingElement_24,
+            Option_c4);
+    if (uu____1.tag == None) {
+      break;
+    } else {
+      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 *ring_element =
+          uu____1.f0;
+      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 uu____2 =
+          ring_element[0U];
+      libcrux_ml_dsa_encoding_error_serialize_a8(
+          uu____2, Eurydice_array_to_subslice2(signing_key_serialized, offset,
+                                               offset + (size_t)128U, uint8_t));
+      offset = offset + (size_t)128U;
+    }

I could conceivably add peephole optimizations to "recognize" such trivial iterators on ranges (I thought I had them -- maybe they broke), if needed, please file followup issue. Thanks!