Explicit Unsized Metadata & Unified DST Handling - Split1

[Lin23299]

This PR is a split for #259, it contains the main part of unified DST handling and can pass the test set of current main branch.

The implementations of slice_to_array and slice_to_ref_array are not included in this PR. Since the type of Eurydice_slice is defined as a general type in Builtin.ml instead of a marco type in eurydice_glue.h. These functions using it should be implemented using the new type in split2. In this PR we shall focus on the dst handling.

[protz]

Is this intentional?

       > ERROR translating dyn_trait_struct_type::Trait::{vtable}: Not_found
-```

[Lin23299]

Is this intentional?

No... It works on my PC.

[protz]

can you either run make nix-magic or apply this patch? I do not have the issue on my machine either and I wonder if it's because we need to upgrade the dependencies

thanks

diff --git a/flake.lock b/flake.lock
index c882537..4826255 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1759502955,
-        "narHash": "sha256-DH9FwoTLY6wPBwnL/DPdSeBZnuNbGKNbA2kT6QJlfPo=",
-        "owner": "aeneasverif",
+        "lastModified": 1760451507,
+        "narHash": "sha256-i5XnhV7vohBc1Hv18p0kTGRhUgV+W8DLEWCII0yacgA=",
+        "owner": "AeneasVerif",
         "repo": "charon",
-        "rev": "b51c1fcb513d7c41a5c2a6d73b5cca4d3ad908a8",
+        "rev": "150afa5f6ba469c99c4a2fa6e1037ae5a4004c68",
         "type": "github"
       },
       "original": {
@@ -75,11 +75,11 @@
         "systems": "systems_2"
       },
       "locked": {
-        "lastModified": 1692799911,
-        "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=",
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
         "type": "github"
       },
       "original": {
@@ -93,11 +93,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1759417092,
-        "narHash": "sha256-oBt3/rriV+RNuYMnSIs9NY1QgvgGGHAxBdUS+4D02ZQ=",
+        "lastModified": 1760479652,
+        "narHash": "sha256-ML1vqrTVktUEA3JM5tAZmOcepNNrUteANz/ppuq760I=",
         "owner": "fstarlang",
         "repo": "fstar",
-        "rev": "20bfb3cbadc40c305e2fe51747f4cceeadeb58e8",
+        "rev": "91688a4e314b035c982aad4db7cf90422c86620a",
         "type": "github"
       },
       "original": {
@@ -119,11 +119,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1757448545,
-        "narHash": "sha256-oePLSANVxdqhgf3R4hpvknG0BXI9n5q+pot4vuBzYQM=",
-        "owner": "fstarlang",
+        "lastModified": 1759855638,
+        "narHash": "sha256-+ik3D77Qs4N1ZjyDMmcyZDbG+68uWWlg8Xo7/RlyxvM=",
+        "owner": "FStarLang",
         "repo": "karamel",
-        "rev": "fb36fecb552c9fb202beb38a6c5a732c3f2cd49f",
+        "rev": "254e099bd586b17461845f6b0cab44c3ef5080e9",
         "type": "github"
       },
       "original": {
@@ -149,11 +149,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1751011381,
-        "narHash": "sha256-krGXKxvkBhnrSC/kGBmg5MyupUUT5R6IBCLEzx9jhMM=",
+        "lastModified": 1759381078,
+        "narHash": "sha256-gTrEEp5gEspIcCOx9PD8kMaF1iEmfBcTbO0Jag2QhQs=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "30e2e2857ba47844aa71991daa6ed1fc678bcbb7",
+        "rev": "7df7ff7d8e00218376575f0acdcc5d66741351ee",
         "type": "github"
       },
       "original": {

[protz]

Ok, for the build failure, please run git rm -rf out/ && make test, then commit the result -- some files (like Eurydice.h) are now gone from the code generation.

For instance: git add out && git commit -am "Refresh test output"

[protz]

Perfect, thanks! Now we'll see if some of these functions you commented out in eurydice_glue.h are needed for kyber

[protz]

Warning 4: in the arguments to Eurydice.slice_subslice_from < uint8_t > < core_ops_range_RangeFrom size_t > < Eurydice_derefed_slice uint8_t > □, in the sequence statement at index 16, after the definition of uu____11398, in top-level declaration libcrux_ml_kem.polynomial.vec_from_bytes, in file libcrux_secrets_libcrux_sha3_libcrux_ml_kem: Malformed input:
       > subtype mismatch:
       >   <N:3, CGS:1> Eurydice_dst_ref 2 size_t -> core_ops_range_RangeFrom size_t -> Eurydice_dst_ref 2 size_t (a.k.a. <N:3, CGS:1> Eurydice_dst_ref 2 size_t -> core_ops_range_RangeFrom size_t -> Eurydice_dst_ref 2 size_t) vs:
       >   <N:3, CGS:0> Eurydice_dst_ref 2 size_t -> core_ops_range_RangeFrom size_t -> Eurydice_dst_ref 2 size_t (a.k.a. <N:3, CGS:0> Eurydice_dst_ref 2 size_t -> core_ops_range_RangeFrom size_t -> Eurydice_dst_ref 2 size_t)

looks like the abstract syntax for slice_subslice_from is incorrect (maybe it has an extra const generic argument?)

[protz]

Ok the error is related to slice_to_array2

[Lin23299]

It seems that kyber depends on the C macro definition of Eurydice_slice and some related stuff?

[Lin23299]

slice_to_array2

Then we need the split2 of this PR :)

[protz]

@Lin23299 CI passes here.

TODO to merge this:

1. Please describe briefly what remains on this branch (sizeof and alignof + better way of doing substitutions).
2. Please make sure there's a test for sizeof and alignof

[ssyram]

Hi, thanks for this, here's how I would respond:

1. For the remaining of this PR:
   1.1. We newly added the Eurydice::sizeof & Eurydice::alignof builtins to correspond to the NullOp::SizeOf and NullOp::AlignOf in Charon, which are used to compute the size and align fields in vtables. However, as the drop field in the vtable is not yet properly implemented, we cannot add tests for these builtins yet.
   1.2. As for the way of doing substitution, we adopted the recommended approach of using Charon.Substitute.extract_from_binder, this is required to properly handle the shifting of DeBruijn indices during substitution --- we are going to move the binded value out from its binder, hence we need to ensure that the binding indices are decremented by one accordingly. This is briefly commented also.
2. As mentioned, the test cases for Eurydice::sizeof & Eurydice::alignof cannot be added yet due to the incomplete implementation of the drop field in vtables. We will add these tests once the implementation is complete and we can handle the translation of the drop field correctly.

To summarise, I think the current one is ready to merge.

[protz]

Great thanks!