Support for ensures in spec fns

[jonhnet]

A common pattern in our Dafny predicates is to build up a definition recursively, then use an ensures to export its meaning under a more-powerful quantifier. For example, with receipts we recursively construct a sequence of values where each is related to the one before it by some predicate; users want to know this relation is true ∀ entry pairs in the receipt.

In Dafny, a single 'ensures' line expressing the fact acts as the proof (because it's the necessary inductive property to complete the proof) as well as broadcasting the result via trigger to anyone who mentions the definition name: exactly the automation we want. The absence of this feature has led to a bunch of tedium in porting Dafny specs into Verus.

Ultimately completing the feature requires:

• The ability to use the ensures as an induction hypothesis (not yet supported in this PR)
• Appropriate interaction with recommends (which we want to just treat as requires, in practice)
• The present PR disallows return statements inside spec fns to keep the implementation easy, but that's an unnecessary restriction

[jonhnet]

This PR includes tests of stuff that works plus three ignored tests for stuff that doesn't, most conspicuously test_spec_fn_ensures_induction. Handing off to Chris for now.