Impossible to override provided trait methods about aeneas HOT 5 OPEN

This comes from the fact that for now we do not allow overriding default methods in trait implementations, because it makes the code generation quite hard (and according to the failing assertion, the PartialEq implementation for Option<T> overrides at least one of those). Sebastian Ullrich had bumped into the same issue when he worked on Electrolysis several years ago (see http://kha.github.io/electrolysis/#default-methods ).
For now, our trait declarations only contain the required (i.e., non-default) methods, and we translate each default method once, by parameterizing it with a trait instance. For instance, in the case of Iterator, the trait declaration only contains the function next, and we generate generic functions for map, each, etc., which are parameterized by iterator instance. Of course, it doesn't work if you override one of the default methods.
The general solution would be to put all the methods in the trait declaration, and re-generate all the default methods for all the trait implementations, but this is very heavy especially for traits like Iterator which have > 70 default methods (in particular if you consider the fact that you would have to write lemmas for all the implementations of methods like all for instance).
I have a different solution which works for the cases where the default methods and the required methods are not mutually recursive, which seems to be the case in most situations. We would put all the methods in the trait declarations (so the Iterator trait would have > 70 fields but it is ok), and would generate one translation by default method, which would be parameterized by the other methods that it calls. For example in the case of iterators, functions like map, all, etc. would be parameterized by the next method.

from aeneas.

The following example is sufficient to produce the same crash:

fn main() {
    let _ = Some(1) == Some(1);
}

from aeneas.

I'm currently cleaning the issues and removing duplicates: I updated the name of the issue.

from aeneas.

The following code also triggers the same issue (comes from #71):

fn main() {
    let x = 1;
    let _ = &x == &1;
}

from aeneas.

We plan to solve this on the charon side: AeneasVerif/charon#180.

from aeneas.