Son HO
Son HO
> I discovered the `-Z mir-enable-passes=val` flag, which allows choosing exactly which mir passes to run! I'll have to experiment to see if we can get drops without other optimizations....
What do you mean by "we might be able to use a `TraitRef` there?
I think a dyn trait really existentially quantifies a type, and we need to represent that: `lambda Self -> Self: Iterator, Self::Item = u8` is a predicate over some type...
I think a first thing to do is to allow heterogeneous groups of mutually recursive definitions in Charon, and fail in Aeneas if such a group is not supported. I...
After discussion: we will add a pass to inline calls to methods when the implementation is known (i.e., it is not a trait clause). It should take care of most...
The `vec_error` has been fixed in https://github.com/AeneasVerif/charon/pull/48. For `trait_error`: there is still an issue linked to lifetimes. A fix is coming soon.
~~@Nadrieril you can merge this as soon as the problem with the Charon pin is solved on the side of Aeneas~~
Rephrasing a bit: we can extract the code above with Charon, and it's actually handled by Aeneas (which has a normalization mechanism) but the generated pure model doesn't type-check.
Yes, let's fix it on hax's side. But maybe wait for the merge of `charon_traits_merge`?
Another (simply recursive) example of a different flavour, inspired by the mutual recursion between `Iterator` and `IntoIterator`: ```rust pub trait Trait { fn f(&self, other: &T); } ```