Support invariants on data structures

[romac]

Implement support for invariants on data structures.

Example

#[invariant(amount >= 0)]
pub struct Account {
  pub amount: u64
}

impl Account {
  #[pre(amount >= 0)] // needed for VC yielded at (1) to pass
  fn new(amount: u64) -> Account {
    Account { amount } // (1)
  }
}

The invariant is extracted as a method annotated with the Invariant flag:

case class Account(amount: UInt64) {
  @invariant
  def inv: Boolean = amount >= 0
}

Caveats:

• epfl-lara/stainless#559
• epfl-lara/stainless#309

Alternative designs:

• Invariant attribute on methods and/or impl block: https://docs.rs/contracts/0.6.0/contracts/attr.invariant.html