search

AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

Preliminary support for parent clauses #25

Closed msprotz closed 2 months ago

msprotz commented 2 months ago

This should be enough to unblock https://github.com/cryspen/libcrux/pull/308

This is not enough to make test-where_clauses go through, so I still want to leave this open until I get my testcase to work

msprotz commented 2 months ago

The next phase requires a little more work: I need to be handle trait clause bounds in trait impl methods, which is non-trivial (see test/where_clauses), so I'm going to leave it at this for now -- I cannot handle trait instances of the form Parent(Self, ...) yet.

So let's merge this since it already improves the state of things, once I get a green-light that what I'm doing vaguely makes sense.

msprotz commented 2 months ago

Thanks for the comments @Nadrieril it's good to know my assumptions are correct. I'll merge this for now, and ping me if you want to discuss this ParentClause business a little bit more (but the more I think about it, the more I think there's nothing wrong on the Charon side)