Function resolve 

pub fn resolve<T: ?Sized>(_: T) -> bool

This logical function is assumed as soon as a value leaves its scope. It states that the propheties of every mutable borrow appearing in it parameter is eaqual to its current value.

Its body is opaque, but Creusot automatically generates an axiom stating relevant properties depending on the definition of T.

(open, prophetic, inline)

dead