Class/Trait Invariants

[ssomayyajula]

What was changed?

This PR introduces class and trait invariants as described in the updated reference manual (in this PR).

How has this been tested?

Tests in Source/IntegrationTests/TestFiles/LitTests/LitTest/invariants.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[ssomayyajula]

Do we want to mention this as a new feature in the release notes for 4.11.0?

[robin-aws]

Do we want to mention this as a new feature in the release notes for 4.11.0?

Absolutely at least add a docs/dev/news/*.feat note! Whether this makes it into 4.11 is a separate question (although I'm inclined towards yes - I think since we delayed it enough I'd rather start the code freeze over from master)

[MikaelMayer]

I will comment only the error messages, but otherwise it looks great !

[robin-aws]

Just some initial comments on the reference manual for now

[keyboardDrummer]

I think it would be good to have a performance related test.

Something like:

class HasInvariant {
  var valid: boolean
  invariant valid
}
class HasNoInvariant {
  var valid: boolean
}

method processHasInvariant(h: HasInvariant) {
  useInvariant(h);
}

method useInvariant(h: HasInvariant) {
  assert h.valid;
}

method processHasNoInvariant(h: HasNoInvariant) {
  useHasNoInvariant(h);
}

method useHasNoInvariant(h: HasNoInvariant) {}

and then verify that the resource usage of processHasInvariant and processHasNoInvariant are equal: that processHasInvariant is agnostic to the existence of the invariant.

[MikaelMayer]

Initial comments as I'm not done but it can still help

[MikaelMayer]

Finished commenting

[ssomayyajula]

Note for myself: don't delete the branch after merging.

[keyboardDrummer]

Without a test that proves that code that does not use a type invariant, but does use the type, does not have its verification performance affected by the invariant's existence, I don't think we should merge this.