How do we ensure totality?

We want to be able to guarantee that "`cargo hermes verify` succeeded" implies "this program is sound". With enough Hermes features, this should be bulletproof via the following reasoning:
- [x] All unsafe operations must be inside of an `unsafe` block (already guaranteed by Rust)
- [x] All unsafe traits must be implemented by an `unsafe impl` block (already guaranteed by Rust)
- [ ] All `unsafe` and `unsafe impl` blocks must carry a safety comment (can be guaranteed by Hermes, similar to the Clippy lint)
- TODO: For `unsafe` blocks, we need a way to parse normal (non-doc) comments and to support comments which are anchored on blocks instead of on function definitions, trait definitions, or trait impl blocks
- [ ] All `unsafe impl` blocks must have a proof of correctness which depends only on left-hand-side trait bounds
- [ ] All `unsafe` blocks must have a proof of correctness which depends only on function preconditions
- Note that this naturally handles the distinction between safe and `unsafe` functions – a function which needs to be `unsafe` (because it needs safety preconditions) *cannot* be marked as `safe` because then the inline Hermes safety proof will fail to verify
- [ ] All functions which have documented `ensures` post-conditions must also prove that their pre-conditions (either `requires` for `unsafe` functions or no preconditions for safe functions) imply their post-conditions
- NOTE: Safe functions cannot have `requires` preconditions, as safe functions must assume that they can be called by any valid type-checked code with any arguments
- NOTE: By a similar token, safe traits cannot have `isSafe` invariants
- [ ] Field invariants are tricky without the "`unsafe` fields" feature. We'll somehow need to reason about the total set of code which can mutate a field. We may need Hermes annotations to live on the containing module or something.

Other considerations:
- How do we ensure that all `unsafe` and `unsafe impl` blocks are annotated? We could either rely on the Clippy lint or have Hermes do its own analysis and reject undocumented `unsafe` blocks
- How do we ensure that all safety comments/Hermes annotations behave as expected? For example, if Hermes just ensures that a block has a Hermes annotation *or* a safety comment, what if the user *intended* to write a Hermes annotation, but typo'd it, and so we treat it as an opaque safety comment and don't validate its contents? Maybe, instead, we could require users to opt *out*? E.g., the default behavior of Hermes is to require *every* `unsafe` block to be annotated with a Hermes annotation, and one of the valid annotations is "unchecked prose safety proof" or something like that. Could opt-out with `cargo hermes verify --allow-partial` or something like that.

Another thing to consider: We need to ensure that a function or `unsafe` block which calls an `unsafe` function *without* a Hermes annotation must itself either *not* have a Hermes annotation or have an `unsafe(axiom)` annotation. The reason is that an `unsafe` function *without* a Hermes annotation will appear to Lean to have no safety preconditions. For example, you could do:

```rust
unsafe fn unreachable_unchecked() {
unsafe { std::hint::unreachable_unchecked() }
}

/// ```hermes, spec
/// ensures ret = t
/// proof
/// ...
/// ```
fn identity(t: T) -> T {
unsafe { unreachable_unchecked() }
t
}
```

`identity` is actually unsound because it calls `unreachable_unchecked`, but since `unreachable_unchecked` doesn't have a Hermes annotation, the lowered Lean for `identity` won't realize that `unreachable_unchecked` has any preconditions, and so it will accept a proof of `identity`'s spec as valid.