Apply invariants on constructor-like functions

A common pattern is that we have some struct S { ... } with an invariant. Let's say we have encapsulated this into a function s.invariant().

However, if we do something like below, the invariant will be ignored unless for those functions which take self:

#[invariant(self.invariant()]
impl S {
  fn new(...) -> S { ... } // invariant will not be enforced
  fn mutate(&mut self, ...) { ... } // invariant will be enforced
}

One solution to the above is to write the following:

#[invariant(self.invariant()]
impl S {
  #[post(ret.invariant())]
  fn new(...) -> S { ... } // invariant will now be enforced

This issue is about whether the above should perhaps be default behavior. That is, the post is added automatically for all functions returning the type of impl with the invariant.