Support diverging functions

Currently, the presence of a Hermes annotation implies that the annotated function will return without diverging, and all `ensures` clauses provide conditions which hold *given* that the function doesn't diverge. However, users may want to annotate functions which diverge under some conditions (e.g. `Option::unwrap`) or even all conditions (e.g. `panic!`). We'll need a syntax that allows distinguishing the common case, where an `ensures` clause is implicitly prefixed with "this function returns and...", and the more general case where the user can write "raw" conditions which also specify the conditions under which a function diverges.