Open franziskuskiefer opened 3 months ago
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
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: https://github.com/AeneasVerif/charon/issues/214.
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