Explicit Unsized Metadata & Unified DST Handling #259

ssyram · 2025-08-09T15:59:58Z

I've implemented on the Charon side (AeneasVerif/charon#797) a functionality of making the pointer-metadata explicit in Charon. This reflects in that both RawPtr and RvRef in the rvalue type now will take an additional operand, which stores the metadata. So that, now, codes like:

let dst : &[i32] = &x.dst;

Now will have the RHS represented as:

@9 := ptr_metadata(copy (x@1))
@3 := &((*(x@1)).dst, move (@9))

This is a part of the full DST (dynamically sized types) support plan. A new type struct Eurydice::DstRef<Pointee, Meta> { Pointee *ptr, Meta meta } is also added as the ultimate representation of such types. A function mk_reference is added, this function judges if the given metadata is (), the default case indicating no metadata is required (Thin pointer), otherwise, wrap the whole value with Eurydice::DstRef.

This has 3 major implications:

The whole workflow for slices should be restructured, as a slice &[T] is now simply Eurydice::DstRef<T, usize>, we may add an abbreviation as type Eurydice::Slice<T> = Eurydice::DstRef<T, usize> for better readability, though. This involves also the casting part in AstOfLlbc and many Cleanups.
The str type should now simply Eurydice::DstRef<char, usize>.
The original mechanism for handling "generic-DST" (i.e., types of the form Type<U : ?Sized>) can be now more generally handled. This should also make the codes more structured & clean.

Let us merge #252 first to partly alleviate the situation!

Of course, if we are simply to adapt to the new AST from Charon, we can ignore the final Operand for metadata, and everything will remain exactly the same as before.

msprotz · 2025-08-11T16:39:40Z

Your plan seems good. I'm hoping to merge #252 shortly as soon as I confirm no breakages. Thanks.

ssyram · 2025-08-12T01:23:56Z

Thanks! Let us progress on this!

Lin23299 · 2025-08-13T09:28:19Z

I'm implementing the step 1, i.e. turning Slice<T> to DstRef<T,usize>. Note that the latter type is actually an instance of the generic type for fat pointer DstRef<Pointee,Meta>. This type is now added to the decls of current file similarly as the Arr<T,C> in #252 .

The problem is also similar -- the macro implementations about slices in eurydice_glue.h do not work anymore. Moreover, it is quite hard to modify them because we need to handle monomorphized DstRef types instead of a general typeEurydice_slice defined in C.

Currently we are planning to implement these functions using abstract syntax in Builtin.ml. Since a lot of them are related to arrays, I'm going to merge #252 to this branch first to avoid doing things useless. @msprotz what do you think?

msprotz · 2025-08-13T19:29:49Z

This is a good plan. I think I mentioned this earlier, but I wonder if it's worth extending the cremepat PPX rewriter to allow you to write concrete syntax for expressions (not just patterns).

The idea is that if we end up writing a lot of deeply embedded syntax, things are going to get very hard to maintain. You could image doing something like:

let slice_len = Checker.check_decl (DFunction (..., [ mk_binder "x" (mk_slice (TBound 0)) ], [%creme "let len = x.len in len"]))

What do you think? I don't have a good sense of the amount of work involved. Maybe all the functions that operate on slices are small and this won't be a problem.

Lin23299 · 2025-08-14T01:31:00Z

I shall first try to see the amount of work and do we need the cremepat PPX rewriter :)

…unsize

…en in abstract syntax when they are not needed

…unsize

…em to be useless

ssyram · 2025-10-07T13:22:12Z

Hi @msprotz , we think this PR should be quite ready and also the Charon is now ready for this. Would you please have a look on this?

Nadrieril · 2025-10-07T14:18:20Z

This appears to have conflicts with the main branch, could you resolve them first?

protz

Here's a preliminary review -- I'll do a more in-depth review once this is rebased and I have some answers to my questions.

Why are some functions eliminated from the glue, and why are some other functions still written using macros? (like slice_split_at_mut?) -- I expected all of these to be in abstract syntax now. Is there a reason for that?
Can you please write high-level summaries of the new functions? What does vtable_typ_of_dyn_pred do? Do I understand correctly that this PR now generates struct declarations for vtables? (If so, that's great!)
As always, commented-out code should go, since we can see quite well in the diff what went away (I'm thinking of eurydice_glue.h right now)

I feel like I'm seeing changes related to the array PR in there, too, so I'm going to stop for now until you merge main into this branch. Overall, it looks quite good, and I'm very pleased with the amount of ad-hoc code for DST support that is going away. Good work!

edit: also please make sure that you have good test coverage -- does test-unsize also cover vtable metadata?

protz · 2025-10-07T18:22:25Z

lib/AstOfLlbc.ml

+          match List.rev @@ ty_decl_ref.generics.types with
+          (* This is `()`, which has metadata `()` *)
+          | [] -> None
+          (* For tuple, the type of metadata is the last element *)


can you say more about that? this seems weird

This is written by me. For a tuple type (X, Y, Z), the ptr-metadata is the same as Z as the last field, but if the tuple is empty, which means it is the unit type (), then there is surely no ptr-metadata.

protz · 2025-10-07T18:22:46Z

lib/AstOfLlbc.ml

+            decl.item_meta.lang_item = Some "sized"
+      in
+      let var_is_sized =
+        true


I presume this is work in progress?

OK, this is a tough issue. If we use the correct impl (which is a line below), it causes many errors in the tests -- this suggests that the original treatments to the references are not correct, especially when handling std libraries like the call_mut functions. To get this truly right, we will need a monomorphization procedure that supports the PtrMetadata-type-level computation, but this is not that realistic especially considering that we are now migrating to mono LLBC, which should resolve the problem. So we simply leave a true here to restore the current behavior.

In a more precise tone, in those cases (like call_mut's assoc-types), the generic params can actually be substituted by some non-sized types. As we are working with the references, so there will be a need to compute PtrMetadata(T) from the type parameter T.

lib/AstOfLlbc.ml

protz · 2025-10-07T18:27:11Z

lib/AstOfLlbc.ml

            match !*sub_e.K.typ with
-            | TBuf (t_pointee, _) | TArray (t_pointee, _) ->
-                Krml.Helpers.(mk_deref t_pointee !*sub_e.K.node)
+            | TArray (_, _) -> assert false


if there's no comment explaining why, I usually like to put failwith followed by a reason why this shouldn't happen

I've removed this line cuz it can be covered by the following case for error info. Actually this is a cleanup for the array PR we missed before.

protz · 2025-10-07T18:27:38Z

lib/AstOfLlbc.ml

-            mk_deep_copy e (expression_of_const_generic env cg)
-        | _ -> e
-      end
+  | Copy p -> expression_of_place env p


ok this should have been in the array PR already, no?

protz · 2025-10-07T18:28:31Z

lib/AstOfLlbc.ml

  | C.TAdt { id = TBuiltin TBox; _ } -> true
  | _ -> false

+let mk_reference (e : K.expr) (metadata : K.expr) : K.expr =


also a comment like "returns either a regular naked C pointer, or a fat pointer in the case of DSTs" would help here I think

Updated the comments for this function :)

protz · 2025-10-07T18:29:24Z

lib/AstOfLlbc.ml

+                (K.ETApp (Builtin.(expr_of_builtin empty_array), [], [], [ ty ]))
+            in
+            K.with_type typ_arr (K.EApp (empty_array, [ K.with_type ty K.EAny ]))
+            (* a dummy arg is needed to pass the checker *)


can you remind me about the empty array issue? was the upstream bug ever fixed?

The previous discussion of empty array ended here: #252 (comment). The current situation is that we use a builtin function to initialize the empty array as (t_dst) {.data = {}}. The existence of empty array is still an open issue i think.

protz · 2025-10-07T18:29:44Z

lib/AstOfLlbc.ml

+                (TArray (typ_of_ty env t, constant_of_scalar_value (assert_cg_scalar cg)))
+                (K.EBufCreateL (Stack, List.map (expression_of_operand env) ops))
+            in
+            K.with_type typ_arr (expression_of_struct_Arr array_expr)


nit -- this function does not follow the naming convention... maybe mk_arr_struct?

…-better-unsize

protz

Ok I read the rest (thanks for merging main in!) and it looks like this all makes sense. Some general comments:

I need a few more high-level explanations to finish the review (see detailed remarks)
let's try to understand why you need to reimplement a reachability analysis
I think some cleanup phases from Cleanup3 should no longer be necessary, correct? like add_extra_type_to_slice_index

protz · 2025-10-08T17:37:35Z

lib/PreCleanup.ml

+      | _ -> super#visit_expr env e
+  end
+
+(** Comes from [drop_unused] in Inlining.ml, we use it to remove the builtin function defined using


why do you not do what was done before, and mark these as private, so that they are automatically eliminated by the reachability analysis?

These functions are marked as private. This is kind of a quick fix cuz we need to remove these functions in precleanup to pass the following check while directly using Krml.Inlining.drop_unused after precleanup causes some other errors. I will try to directly reuse it by looking further into these errors.

protz · 2025-10-08T17:39:10Z

lib/PreCleanup.ml

+  | CgConst n -> Krml.Helpers.mk_sizet (int_of_string (snd n))
+  | CgVar _ -> failwith "non-const length in the Arr<T,C>"
+
+let expand_slice_to_array =


can you describe what this function does, to help me understand a little bit better?

First of all, this should be a part of the array PR. But try_into() was not included in the test cases. Now it is added in slice_array.rs.

The difference is that the previous implementation of slice_to_array and slice_to_ref_array are based on that array was transalted into pointer T*. So we basically just do the memcpy. However, now arrays are translated into structs, so we need to first allocate the array struct and do the memcpy to its data field.

This is exactly what this function does for slice_to_array (the first case). For slice_to_ref_array, it allocates the struct and call slice_to_ref_array2 defiend in glue.h to finish the possible core_result_Err . See slice_array_f3 in out/test-slice_array/slice_array.c for the translation result.

Can you split this into a separate PR? That would make it much easier to review. Thanks.

Lin23299 · 2025-10-09T06:02:06Z

Why are some functions eliminated from the glue, and why are some other functions still written using macros? (like slice_split_at_mut?) -- I expected all of these to be in abstract syntax now. Is there a reason for that?

No special reason. I just found that some macros can still work after a little bit changes (e.g. from s.len to s.meta). Thus I do not have to implement them using abstract syntax.

Lin23299 · 2025-10-09T07:34:33Z

As always, commented-out code should go, since we can see quite well in the diff what went away (I'm thinking of eurydice_glue.h right now)

I've removed some of these code in eurydice_glue.h. I'm not sure about the Eurydice_chunks and Eurydice_slice_iterator which depended on the old Eurydice_slice defiend using macro. They are not used in the test cases and just commented-out for now. Maybe we need to implement them in abstract syntax.

let's try to understand why you need to reimplement a reachability analysis

As mentioned in the reply, I'll try to reuse the drop_unused pass.

Edit: I've found that applying a general drop_unused at precleanup stage will eliminate some private definitions we introduced for later passes. For example, the Eurydice_assert defined in Builtin.ml is unused in the program until recognize_assert from Cleanup2. The translation will crush after that without the private definition of Eurydice_assert.

On the other hand, why we need to eliminate these new builtin functions early? Because they are functions with implementation and actually use the range types in code. If the program does not use and include the range type, the existence of these functions will fail the check after precleanup.

It seems quite tricky for me. Maybe we have to reimplement and “fine-tune” this reachability analysis to eliminate some of the unused functions.

I think some cleanup phases from Cleanup3 should no longer be necessary, correct? like add_extra_type_to_slice_index

Yes! After the array PR and the implementation of other builtin functions, I've removed it successfully.

ssyram · 2025-10-09T08:00:20Z

Thank @Lin23299 for helping refining the PR! I'm mainly working on adapting the vtable support in Eurydice. For the vtable, now charon should be quite ready for that with some minor issues:

The vtable instances have some opaque fields (which is going to be partly alleviated by my next PR Vtable Metadata charon#840), so translating the actual instance may not be smooth in Eurydice now.
The vtable is not yet supporting closures (and hence no &dyn Fn series support), this should also be fixed later when splitting the Supporting dyn Trait charon#762 further.
The vtable is not yet supported by monomorphization of Charon. This is a tough case.

Yet, there is still a bug in the vtable support in Charon. Now the stuff has been fixed in AeneasVerif/charon#842 . After merging that, we will have pretty nice vtable support:

typedef struct dyn_trait_struct_type_Trait__vtable__s
{
  size_t size;
  size_t align;
  void (*drop)(Eurydice_dst_ref_06 x0);
  void (*method_method)(Eurydice_dst_ref_06 x0);
  core_marker_MetaSized__vtable_ *super_trait_0;
}
dyn_trait_struct_type_Trait__vtable_;

typedef struct Eurydice_dst_ref_06_s
{
  Eurydice_c_void_t *ptr;
  dyn_trait_struct_type_Trait__vtable_ *meta;
}
Eurydice_dst_ref_06;

void dyn_trait_struct_type_use_trait(Eurydice_dst_ref_06 t)
{
  Eurydice_dst_ref_06 uu____0 = t;
  uu____0.meta->method_method(uu____0);
}

For the Rust code:

trait Trait {
  fn method(&self);
}
fn use_trait(t: &dyn Trait) {
  t.method();
}

1. metadata of dyn from struct to pointer; 2. new example added; 3. Eurydice_c_void_t defined;

protz · 2025-10-09T23:47:34Z

Ok I am traveling for a couple conferences right now, so the best way to get this moving is to split the changes that are only about arrays into a separate PR, merge that, and come back to this one. I think it'll make the process easier for all of us... thanks!

(And very excited about vtable support -- this is great!)

protz · 2025-10-09T23:49:27Z

It seems quite tricky for me. Maybe we have to reimplement and “fine-tune” this reachability analysis to eliminate some of the unused functions.

Yes, maybe some functions can only be eliminated later. I agree that it is tricky and I've had similar issues in the past. Let me think about this...

protz · 2025-10-25T21:16:07Z

@Lin23299 can you merge main into this branch to make sure we don't have any commits left behind? thank you!

protz · 2025-10-27T04:13:52Z

Ok there's only this one left -- please merge main into this branch to make sure there's nothing important left on this branch.

@Lin23299 congratulations on a super nice piece of work!

…-better-unsize

Lin23299 · 2025-10-27T08:38:07Z

@protz I've merged main into this by simply taking every change from main. We do have a missing cleanup in main.ml and everything else is fine.

Btw, I have no idea why the output of libcrux is slightly different while the source code of Eurydice is almost the same (and the CI failure). Shall I do the setup-libcrux or manually pull it before running test-libcrux? Shall I admit the modification of libcrux-Cargo.lock done by the test? Or in a summerized way, how could I make sure the local test-libcrux reflects the online CI, maybe using some nix command I guess?

protz · 2025-10-27T14:28:25Z

@Lin23299: @Nadrieril updated the README.md so perhaps there is some useful information in there. In the meanwhile:

run make check-dependencies: if it returns any output, then one of your subprojects is not at the correct revision; please git pull that subproject, or whatever else is needed
run make clean-llbc to be on the safe side
run make test

Please note that the Cargo.lock file should not be modified (insofar as I understand); you may want to do git reset origin/main libcrux-Cargo.lock && git commit -m "Revert Cargo.lock for libcrux"

Let me know how it goes!

protz · 2025-10-27T16:50:10Z

(I did this for you in the interest of cleaning up PRs.)

Lin23299 · 2025-10-28T03:09:43Z

Thank you very much! These instructions works for me and everything is pretty clean now. :)

ssyram added 2 commits August 9, 2025 23:14

draft support of rvalue with metadata

ff29fdd

unop for ptr-metadata

616877b

ssyram changed the title ~~Charon update: Better Unsized Type~~ Explicit Unsized Metadata & Unified DST Handling Aug 9, 2025

error for fetching meta from generics

7d31e84

Lin23299 added 2 commits August 13, 2025 14:44

unchanged builtin type of slice

81bb856

updated [typ_of_ty] for fat pointer

70db499

Lin23299 added 5 commits August 14, 2025 10:34

Merge branch 'array_handling' into c-better-unsize

35e19f3

rename c_char_t and c_void_t

56811ee

defined array_to_subslice_to using abs syntax

fff533c

Merge branch 'main' of github.com:AeneasVerif/eurydice into c-better-…

ed85c63

…unsize

added [remove_unused_builtin] in PreCleanup to remove the funcs writt…

71f392a

…en in abstract syntax when they are not needed

msprotz mentioned this pull request Aug 19, 2025

Generate const qualifiers #262

Closed

Lin23299 and others added 13 commits August 20, 2025 11:27

updated abstract syntan defs

8056259

added other builtin funcs for slice<T>, not tested

8583acd

Added simple case for PtrMetadata inheritance

e03ab05

removed dst_def, cleanup and special treatment of dst fields

4ed93f7

Merge branch 'main' of github.com:AeneasVerif/eurydice into c-better-…

c6cd0e2

…unsize

more cleanup about dst

b9a9190

updated str, using c_star_t instead of prims_string

03167e8

updated glue.h, test cases passed

480f94a

removed special case for non-dst field, leaving the [slice_of_dst] case

e4b1af2

Merge branch 'AeneasVerif:main' into c-better-unsize

01429aa

removed the macro def of slice, replaced slice_of_dst into ECast

767bbe1

updated testcases following changes in krml

13b8de2

simplified taking dst field, removed special cases for Slice which se…

2875732

…em to be useless

ssyram marked this pull request as ready for review October 7, 2025 13:21

protz reviewed Oct 7, 2025

View reviewed changes

Merge branch 'main' of https://github.com/AeneasVerif/eurydice into c…

aeeb403

…-better-unsize

protz reviewed Oct 8, 2025

View reviewed changes

Lin23299 added 3 commits October 9, 2025 11:02

Merge branch 'AeneasVerif:main' into c-better-unsize

54b3558

minors

ce512e4

removed commented-out code in glue.h

639dedd

removed add_extra_type_to_slice_index

807c3c4

correct vtable

21b08bd

ssyram added 2 commits October 9, 2025 17:11

fixing vtables

23c81e8

1. metadata of dyn from struct to pointer; 2. new example added; 3. Eurydice_c_void_t defined;

cleanup

2a7726e

Lin23299 mentioned this pull request Oct 14, 2025

Explicit Unsized Metadata & Unified DST Handling - Split1 #298

Merged

Merge branch 'main' of https://github.com/AeneasVerif/eurydice into c…

becfd61

…-better-unsize

ssyram mentioned this pull request Oct 27, 2025

Vtable Instance Support #308

Draft

Refresh

c209ff9

protz merged commit 47bb02a into AeneasVerif:main Oct 27, 2025
3 checks passed

ssyram deleted the c-better-unsize branch October 28, 2025 01:14

Explicit Unsized Metadata & Unified DST Handling #259

Explicit Unsized Metadata & Unified DST Handling #259

Uh oh!

Conversation

ssyram commented Aug 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

msprotz commented Aug 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ssyram commented Aug 12, 2025

Uh oh!

Lin23299 commented Aug 13, 2025

Uh oh!

msprotz commented Aug 13, 2025

Uh oh!

Lin23299 commented Aug 14, 2025

Uh oh!

ssyram commented Oct 7, 2025

Uh oh!

Nadrieril commented Oct 7, 2025

Uh oh!

protz left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ssyram Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

protz left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Lin23299 commented Oct 9, 2025

Uh oh!

Lin23299 commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ssyram commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

protz commented Oct 9, 2025

ssyram commented Aug 9, 2025 •

edited

Loading

msprotz commented Aug 11, 2025 •

edited

Loading

protz left a comment •

edited

Loading

ssyram Oct 9, 2025 •

edited

Loading

protz left a comment •

edited

Loading

Lin23299 commented Oct 9, 2025 •

edited

Loading

ssyram commented Oct 9, 2025 •

edited

Loading

protz commented Oct 27, 2025 •

edited

Loading