Translating rust array type [T;C] into struct arr { T[C] data; }

[Lin23299]

According to our discussion in #37, I've done with this prototype which can pass make test. The cases are mainly unchanged except adding some assert! to avoid unused variable warning.

I'll introduce the main changes with my thoughts on them. This version surely needs more cleanup but maybe you can take a look first and give some feedback :)

Translation

In AstOfLlbc.ml, three basic changes:

1. The types of arrays are translated into the following type:

let arr : K.lident = [ "Eurydice" ], "arr"
let mk_arr (t : K.typ) (cg: K.cg) : K.typ = K.TCgApp (K.TApp (arr, [ t ]), cg)

2. The corresponding decl_of_Arr is included in the translated program.

let decl_of_Arr =
  K.DType (Builtin.arr , [], 1, 1, Flat [(Some "data", (K.TCgArray (TBound 0,0), true))])

3. The expressions of arrays come from [x;N] or [x,y,z] and functions related to arrays are similarly translated.

Cleanup phases

In Cleanup2.ml:

1. In remove_implicit_array_copies, a recursive call for multi-demensional array is added.
2. The translation of from_fn and map functions are changed from the pass-by-ref style to directly returning the struct of array as value.
3. remove_array_repeats is changed by 1) find and translate the arr{T data[N];} pattern in expressions; 2) force visit_DGlobal to return a initializer list as macro definitions in C.

A new phase remove_builtin_decls in Cleanup3.ml is added to remove several specific monomorphized array types which are already defined in eurydice_glue.h for builtin functions (e.g. [u8;4] for core_num__u32__to_be_bytes).

External definitions

As we discussed in #37, I changed the function types in Builtin.ml to use the new struct types. box_new_array and slice_of_boxed_array are no longer needed.

Notably, most of the C macro definitions of functions for slices and arrays in eurydice_glue.h are unchanged. Because it seems that the pointer to the struct is nearly "the same" as the pointer to the array data. It works for now and I'm not sure should we keep this or add more type-polymorphic macros as @msprotz mentioned.

Others

As mentioned in FStarLang/karamel#627, I've added a new builtin function 'empty_array' to replace the empty buffer list for 0-length array. it's later implemented as follows:

#define Eurydice_empty_array(dummy, t, t_dst)                                  \
  ((t_dst) { { } })

I still need a dummy arg to pass the checker, maybe you have better idea?

[ssyram]

@msprotz Shall we merge this? What else should we do / wait for?

[msprotz]

We are still blocked on #252 (comment) -- @ssyram do you think that this issue is fixed by AeneasVerif/charon#790?

[msprotz]

If you have time, do you think you could look into this bug? It seems to be an x64-only behavior (and, specifically, on OSX): in those conditions, the function keccakf1600 is not extracted. hax also throws a lot of panics along the lines of:

thread 'rustc' panicked at compiler/rustc_middle/src/ty/context.rs:2946:9:
assertion failed: eps.array_windows().all(|[a, b]|
        a.skip_binder().stable_cmp(self, &b.skip_binder()) !=
            Ordering::Greater)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
warning: Hax panicked when translating `core::iter::traits::collect::IntoIterator`.
 --> /rustc/library/core/src/iter/traits/collect.rs:282:1

which might be related.

[msprotz]

This is tracked as AeneasVerif/charon#804 and is triggered on a much smaller example.

[ssyram]

OK, so the main problem now is the sorting issue AeneasVerif/charon#790 ? This I think has been fixed by my PR in AeneasVerif/hax#2 . Yes, I think you're right that this is the discrepancy between the architecture... This is caused by that the order hash of Rustc used to implement rustc_middle::ty::stable_cmp function in Rustc produces a contradictory (while stable) result in the orders. So I fixed this by adding a sorting operation before calling the mk_poly_existential_predicates function in Hax. Now this is waiting for the merge in Hax by @Nadrieril.

Is this the key factor that produces the issues in comment? I would suggest you simply add the sorting mechanism in the fix on your local computer so to confirm if this fixes everything or there is any other issue we need to overcome. We may work together more efficiently in this way!

[protz]

Thanks for bringing this to my attention, I was not aware of this PR. I've asked @W95Psp to take a look if he can while we wait for @Nadrieril to come back online. It would be good to merge this to unblock.

[ssyram]

OK, thanks!

[ssyram]

Thanks for merging AeneasVerif/hax#2, so is the problem fixed? Btw, the merge may not take effect immediately as Charon seems to fix a specific commit hash code in Cargo.lock.

[protz]

Do you see hax in Cargo.lock for Charon?

jonathan@MacBookPro:~/Code/charon (main) $ nix flake update hax --extra-experimental-features nix-command --extra-experimental-features flakes --override-input hax "github:aeneasverif/hax/f6ef814"
warning: input '' has an override for a non-existent input 'hax'
warning: the flag '--override-input hax github:aeneasverif/hax/f6ef814' does not match any input
warning: 'hax' does not match any input of this flake

this is the error I got

[ssyram]

I think simply cargo update is OK? As now it should be the latest version of the Aeneas-version of Hax? In the Cargo.lock, hax is provided as three crates: hax-frontend-exporter, hax-adt-into & hax-frontend-exporter-options. If you are to change the hash codes there, simply change the source field should suffice. See, e.g., AeneasVerif/charon@b4061c4 for this.

[protz]

AeneasVerif/charon#808

but it looks like CI is down so maybe that'll have to wait until Monday

[protz]

Happy to confirm that AeneasVerif/hax#2 fixes the intel libcrux extraction issue. Now I need to make sure the tests still pass and we should be good.

[protz]

This needs to be fixed here:

@@ -163,8 +163,8 @@ typedef struct {
   KRML_CLITERAL(Eurydice_slice) { ptr_, len_ }

 #define core_array__core__clone__Clone_for__Array_T__N___clone( \
-    len, src, dst, elem_type, _ret_t)                           \
-  (memcpy(dst, src, len * sizeof(elem_type)))
+    len, src, elem_type, _ret_t)                                \
+  (*(src))
 #define TryFromSliceError uint8_t
 #define core_array_TryFromSliceError uint8_t

[protz]

Ok there is a bunch of stuff to fix on the test side for libcrux but at least the code compiles without errors.

Everything is on branch protz/ci-arr.

@keks @franziskuskiefer should we work together to fix those tests for this upcoming PR? That way this doesn't come as a surprise for libcrux.

[franziskuskiefer]

@keks @franziskuskiefer should we work together to fix those tests for this upcoming PR? That way this doesn't come as a surprise for libcrux.

Do you have a branch somewhere with the extraction? Then we could take a first look to see what it takes to fix it up.

[msprotz]

Here: https://github.com/cryspen/libcrux/tree/protz/ci-arr

With this branch, ./c.sh still works and the generated C compiles (modulo the mini-fix above) except for the tests where I was only able to fix partially. It's just mechanical.

[franziskuskiefer]

Here: https://github.com/cryspen/libcrux/tree/protz/ci-arr

The c directory on that branch doesn't build for me unfortunately because there appear to be neon types in the core.

Trying to extract (boring.sh) I'm seeing a couple cycles such as the following. This means we have to explicitly put all array types into the config? Since there are platform specific pieces here I don't think we can use globs.

Eurydice.arr_51 (found in file libcrux_mlkem_core) mentions libcrux_ml_kem.vector.avx2.SIMD256Vector (found in file libcrux_mlkem768_avx2)

[protz]

Ok I need to debug the build on ARM too. Let me take a look.

[protz]

I was able to confirm that this does not break libcrux (see my latest commit on protz/ci-arr branch of libcrux). I'm going to try to figure out the CI issues and then merge this.

[ssyram]

OK, I tried to merge the latest into the PR. But kyber seems to report the same error as before.

[protz]

Congratulations! This has now been merged as part of #283. I will review the metadata PR tomorrow.

Thanks for all the good work and sorry it took so long to merge -- I wanted to be absolutely sure that nothing was broken.