user-defined type invariants (Part I)

[tjhance]

This adds the ability to specify 'type invariants' on structs & enums. A type invariant is a boolean predicate that is enforced for every exec-mode and tracked-mode instantiation of the datatype. There are 3 parts to this feature, and this PR implements 2 of them:

• Ability to specify a type invariant
• Add assertions that the type invariant is maintained on every update and Ctor node
• Allow the user to assume the type invariant holds true anywhere they want

Despite the feature being incomplete (and therefore useless) this PR is ready for review. Inserting the assertions is the most important part from a soundness perspective, and this aspect should be completely handled by this PR.

This PR introduces a new pass, defined in user_defined_type_invariants.rs which adds assertions for every relevant Ctor node and assignment operation. The assertions are added as AssertAssumeUserDefinedTypeInvariant nodes. This transformation uses information from the mode-checking pass, and it is called directly from modes.rs.

I originally intended to insert these obligations at a much lower level, but since it uses information from mode-checking, I think keeping it near the mode-checking is a good idea. Also, putting this information into the AST early helps for recursion checking and pruning, which we can handle easily by adding edges that point from the AssertAssumeUserDefinedTypeInvariant nodes to the invariant predicate fn.

A user-defined type invariant is required to have the same generic args and trait bounds as the type it applies to. In recursion-checking, we also add edges from the AssertAssumeUserDefinedTypeInvariant to the relevant trait bounds.