Missing Into implementations

[franziskuskiefer]

Into trait implementations are missing.

I manually defined it in core.h

https://github.com/cryspen/hacl-packages/blob/4bfd52161096a8b6882c910327c4023f28be54f5/libcrux/include/eurydice_glue.h#L57C9-L57C43

with custom implementations

https://github.com/cryspen/hacl-packages/blob/3113bd081da3c9f330711744e045f2847f819988/libcrux/include/libcrux_ml_kem.h#L2200-L2249

[msprotz]

I did some some investigations here. With the following revisions:

libcrux: af4e0cf4fdc40b5aca4cebe317747ff17310e983 (on lucas/extract-intrinsics)
charon: c7b2396375cec464fb1e1f27477890681697e3ad (on fix-203)
everest/karamel: 04cb86b94f57c495b715d6e9f98e29352d72d5f3 (on protz_trait_methods)
eurydice: 7d1f0f0985482600ae879a86479c47399de9e856 (on protz_trait_clauses)

I do see the from traits (passing --log Phase1 to eurydice):

  libcrux_ml_kem_types_{(core::convert::From<&0 (@Array<u8, SIZE>)> for libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#3}_from
  <cg: 1><0>(
    mutable
    SIZE(Mark.Present,(Mark.AtMost 1), ): size_t,
    mutable
    value(Mark.Present,(Mark.AtMost 1), ):  uint8_t*
  ):
  libcrux_ml_kem_types_MlKemCiphertext[[$0]]
  {
    {
      value
      =
      core.array.{(core::clone::Clone␣for␣@Array<T,␣N>)#20}.clone < uint8_t > [[@1]] @0;
    }:
    libcrux_ml_kem_types_MlKemCiphertext[[$0]]
  }

but there is no definition for the Into trait!

  external core_convert_Into_into <2>:<cg: 0> 1 -> 0
  external core_convert_{(core::convert::Into<U> for T)#3}_into <2>:<cg: 0> 1 -> 0

because there is no definition for into (the second one), I don't know that into can be implemented as a symmetrical call to from, which is why your functions end up being undefined

@Nadrieril is there any prospect of extracting the definition of cover::convert::into that relies on From?

the workaround for now will be to use from

[Nadrieril]

The implementation of Into is foreign code: it's an impl defined in the standard library. You can therefore pass --extract-opaque-bodies to charon to extract its code.

The drawback is that this flag generates a lot more code, which will likely hit unsupported features in Charon and/or Eurydice. It would make sense to add a flag to Charon to list specific foreign items to extract. I opened an issue for that: AeneasVerif/charon#214.