Overhaul named/unnamed propositions, type invariants

*See also: https://github.com/google/zerocopy/issues/3107*

Currently, on function definitions, we support:
- Named propositions (e.g. `requires (foo): x > 0`, which introduces `foo` as a proposition)
- Anonymous propositions (e.g., `requires: x > 0`, which introduces an anonymously-named proposition)
- Implicitly-named propositions for type invariants, e.g.:
- `h_x_is_valid` for argument `x`
- `h_x'_is_valid` for the post-state of argument `x: &mut _`
- `h_ret_is_valid` for the return value

Though we don't have well-thought-out handling of it right now, we *may* need to also support similar propositions for unsafe traits (i.e., `isSafe`).

This makes it awkward to support anonymous propositions. If we need to write a proof about "what would happen *if I were to call* this function", we need to provide proofs of all pre-conditions as arguments to the function call. This requires the user to *name* the anonymous pre-conditions, e.g. via `{ h_unnamed: ..., h_foo: ... }` etc. The name `h_unnamed` is implicit and the user just has to magically know what to type (albeit possibly aided by helpful error messages).

However, this problem is made significantly better if we can do away with type invariants entirely. Then we can say that a set of propositions (pre-conditions or post-conditions) is *either* a single anonymous proposition *or* a set of named propositions. This means that the user *either* writes `...` for the single anonymous pre-condition *or* writes `{ h_foo: ..., h_bar: ...}` etc for named pre-conditions. The problem is that, if type invariants are expressed as function pre- and post-conditions, then the vast majority of functions have named pre- and post-conditions, and so anonymous pre- and post-conditions are mostly useless (or are frequently hard to hold correctly).

---

This dovetails with a more philosophical question: *Where* should type invariants be enforced? Currently, they're enforced at function call boundaries (arguments, return values, or the post-states of the referents of mutable references). But what if we could change this? E.g., consider:

```rust
fn foo() -> Even {
Even { val: 2 }
}
```

Do we enforce that `Even`'s invariants are upheld when it is *returned* from `foo` or when it is *constructed* inside of `foo`? The latter is reasonable, especially combined with `unsafe` fields, which would require us to construct `Even` in an `unsafe` block which would be a natural place to annotate with a Hermes proof:

```rust
fn foo() -> Even {
// SAFETY: ```hermes
// ...
// ```
unsafe { Even { val: 2 } }
}
```

This is made somewhat more complicated by the fact that programmers do sometimes want to *temporarily* violate invariants, and the function call boundary is a natural place to draw the line – ie, the point by which you must have "restored" the invariants.