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