Unspecialized extern specs

[arnaudgolfouse]

In creusot_contracts, when implementing a trait that is specified with extern_spec!, the calls to the trait methods will ignore the spec of the implementation and fetch the spec of the trait instead.

Example

// in creusot_contracts

pub struct EmptyIt {}
impl ::std::iter::Iterator for EmptyIt {
    type Item = ();
    #[ensures(result == None)]
    fn next(&mut self) -> Option<()> { None }
}
impl creusot_contracts::std::iter::Iterator for EmptyIt { /* ... */ }

// in user code
let mut empty = EmptyIt {};
let x = empty.next();

Then in coma, next appears as:

let rec next'0 (self:borrowed ()) (return'  (ret:t_Option'0))= any
    [ return' (result:t_Option'0)-> {[%#siter1] match result with
        | C_None'0 -> completed'0 self
        | C_Some'0 v -> produces'0 self.current (Seq.singleton v) self.final
        end}
      (! return' {result}) ]

This is the spec of the trait, not the one we wrote on EmptyIt::next.
(Note that completed'0 and produces'0 are the correct ones, so it still works in this case)

[arnaudgolfouse]

This is mainly an issue for #[pure]/#[terminates] functions, where putting the annotation on the trait implementation does nothing.