Support for Generic Associated Types

[R1kM]

E.g.

trait LendingIterator {
    type Item<'a>
    where
        Self: 'a;

    fn next<'a>(&'a mut self) -> Option<Self::Item<'a>>;
}

[sonmarcho]

Where did you encounter GATs? On code you analysed with Charon or on code you want to verify?

[Nadrieril]

There's a common trait in the rust-crypto ecosystem that has GATs. But this was just an issue to track known unsupported features.

[Nadrieril]

https://github.com/AeneasVerif/charon/pull/816 implements support for GATs. We may not yet support all possible GATs but the feature is basically implemented; we can track the reamining bugs in individual issues as we find them.