error[E9999]: Cannot handle error `Unimplemented`

[msprotz]

This is the branch I'm using:

jonathan@verveine:~/Code/libcrux/libcrux-ml-kem (franziskus/platform-independent-mlkem-c) $ git rev-parse head
d82403eb07853eb3c7edf1e9bcf749f3e9f44e4c

After I started using the "newtype" pattern in a couple places, I started triggering bugs in hax-frontend:

error[E9999]: Cannot handle error `Unimplemented` selecting `Binder { value: <libcrux_intrinsics::arm64_extract::_uint64x2_t as core::clone::Clone>, bound_vars: [] }`
  |
  = note: ⚠️ This is a bug in Hax's frontend.
          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!

error: Thread panicked when extracting item `libcrux_sha3::simd::arm64::{impl#0}`.
   --> libcrux-sha3/src/simd/arm64.rs:140:1
    |
140 | impl KeccakItem<2> for uint64x2_t {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Ignoring the following item due to an error: libcrux_sha3::simd::arm64::{impl#0}
   --> libcrux-sha3/src/simd/arm64.rs:140:1
    |
140 | impl KeccakItem<2> for uint64x2_t {
    | ^^^^

Thanks

[Nadrieril]

Do you happen to have a small diff that caused the error? Otherwise, do you think you could come up with a small version of a newtype that triggers this bug?

cc @W95Psp since this is a hax error.

[W95Psp]

That's similar to https://github.com/hacspec/hax/issues/310.

Running cargo hax json or cargo hax into fstar on libcrux at commit d82403eb07853eb3c7edf1e9bcf749f3e9f44e4c in directory libcrux-ml-kem gives me no error. (cargo hax json -k mir-built gives me a stealing error though :scream:, see https://github.com/hacspec/hax/issues/27, we should try to minimize this...)

Thus it seems like it's a query that hax doesn't do but that charon does, so it's harder to reproduce on my side :thinking:

[msprotz]

Yes the diff that caused the error was this:

diff --git a/libcrux-intrinsics/src/arm64_extract.rs b/libcrux-intrinsics/src/arm64_extract.rs
index e43abc8f..184f0141 100644
--- a/libcrux-intrinsics/src/arm64_extract.rs
+++ b/libcrux-intrinsics/src/arm64_extract.rs
@@ -3,15 +3,15 @@

 #![allow(non_camel_case_types, unsafe_code, unused_variables)]

-pub type _uint16x4_t = u8;
-pub type _int16x4_t = u8;
-pub type _int16x8_t = u8;
-pub type _uint8x16_t = u8;
-pub type _uint16x8_t = u8;
-pub type _uint32x4_t = u8;
-pub type _int32x4_t = u8;
-pub type _uint64x2_t = u8;
-pub type _int64x2_t = u8;
+pub struct _uint16x4_t(u8);
+pub struct _int16x4_t(u8);
+pub struct _int16x8_t(u8);
+pub struct _uint8x16_t(u8);
+pub struct _uint16x8_t(u8);
+pub struct _uint32x4_t(u8);
+pub struct _int32x4_t(u8);
+pub struct _uint64x2_t(u8);
+pub struct _int64x2_t(u8);

I tried to minimize but it's not obvious how to reproduce this since of course a single "newtype" pattern in isolation does not cause issues.

@W95Psp are you able to run charon to witness the issue on your end?

[Nadrieril]

Oh, I think the error here is that the code is not valid rust: you're missing the #[derive(Clone)] on your newtypes, but you're trying to clone them somewhere. Try to compile it with cargo normally?

If that's the issue, it's a know issue (https://github.com/AeneasVerif/charon/issues/306): sometimes we try to process code before rustc has fully checked it, which triggers errors like that. I have plans for that but that's not straightforward.

[msprotz]

You are absolutely correct. My bad -- I thought that running charon was the same as running cargo build, and it didn't cross my mind that the panic I was seeing was caused by a legitimate error.

[Nadrieril]

Your expectation is entirely legitimate, hopefully we'll get there soon enough