Verus feature wishlist:

- Allow a function to leave invariants open on return, and allow a function
  to close invariants that were left open, perhaps by tracking the thread's
  set of open invariants as an explicit value.

- Support --expand-errors for trait implementations.  Workaround: assert
  the expected invocation of trait implementation, which causes Verus to
  see the specialized implementation.