Consolidation of expect/assume/ensures/assert

[davidcok]

A use case for expect is to insert runtime checks for extern functions that have no verifiable implementation.

Instead of this boilerplate:

method {:extern} Random(limit: nat) returns (n: int)

method Random’(limit: nat) returns (n: int)
  ensures 0 <= n < limit
{
  n := Random(n);
  expect 0 <= n < limit;
}

just allow writing

method {:extern} Random(limit: nat) returns (n: int)
   expect 0 <= n < limit

or

method {:extern} Random(limit: nat) returns (n: int)
   ensures {:check} 0 <= n < limit

Similarly, expect could be just assume {:check}, which gives a visual reminder that statically,
an expect is an assume and has soundness implications. As it is I think that expect is a dangerous way to insert run-time checks -- I prefer that it not have the static semantics of assume. It would be better to have a halt P statement which halts if P is true, with the static semantics of an assert: the verifier attempts to prove that the halt can never happen.

Note that the compiler warns about any assume statements that are being compiled. So it should correspondingly warn about expect statements that are being compiled -- but that is the point of an expect statement -- so... it should not have assume semantics.