Invariants on labels should be disallowed unless they form loop heads and while loops that are not loop heads should be rejected

Created by @alexanderjsummers on 2019-10-30 08:47

Because of how loops are verified, the current meaning of an “invariant” on a label varies significantly depending on whether the label represents the head of a loop or not. Since there is no motivation for “invariant”s on non-loop-head labels, we should make this an error.

It might become frustrating that one cannot manually choose a label to be a loop head, and also cannot see which labels were chosen as loop heads. We could consider providing extra feedback in the corresponding error message, and potentially (in cases for which the choice of loop head is ambiguous) allowing a user to declare that a label is supposed to be a loop head (in fact, once this issue is fixed, an invariant annotation would do just that).

Start by tracing how loop verification determines loop heads and how invariants on labels and while loops are currently validated. Inspect the relevant verification and error-reporting paths, then confirm the behavior rejects invariants on non-loop-head labels and while loops that are not loop heads, with appropriate feedback for the user.