How do we ensure totality?

[joshlf]

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:

• All unsafe operations must be inside of an unsafe block (already guaranteed by Rust)
• 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:

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

/// ```hermes, spec
/// ensures ret = t
/// proof
///     ...
/// ```
fn identity<T>(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.