Termination check: handle recursion through proof trees and add recursive types check

[Lysxia]

Close #1232

• Handle recursion through proof trees (the original examples of Remaining unsoundness in the termination check #1232).
• Termination checking of impl methods must happen under bounds of the original trait method declaration (see this comment from that same issue).
• Add recursive types check:
  • Types can only recurse in "strictly positive" positions.
  • Recursive associated types are rejected (this also makes use of the new support for proof trees).
  • Recursive traits are rejected (detecting additional counterexamples in Remaining unsoundness in the termination check #1232).
• New attributes
  • #[trusted(ghost)] (more fine grained than #[trusted] #[check(ghost)], i.e., it still enables Coma translation of program functions)
  • #[trusted(terminates)] (idem, and can also be used on types)
  • #[trusted(positive(T, U))] to postulate "strictly positive" type arguments (can also be used in extern_spec!)
• Guide: expanded the Termination chapter with more details, recording the counterexamples found in Remaining unsoundness in the termination check #1232.

Some related things that are not handled in this PR:

• There remains a recursion check in the translation pass, which may reject types that pass the new recursive type check (see the commented out example in the guide).
• We'd like to use the new trait solver to better handle ambiguity, but AFAICT this only happens when a bound overlaps with an impl, in which case we should be able to pick the bound and do nothing more, which happens to match the current behavior, so we don't have a pressing reason to use the more "proper" entry point to the trait solver (Use new trait solver API to avoid ambiguity errors #1671)
• We'd like to better detect empty recursive types (struct Never(Box<Never>), Reject empty types before Why3 rejects them. #881)

Finally, I put traits in the same dependency graph as types, but there are currently no edges between traits and types. When checking traits, I only find dependencies to other traits in trait bounds (for instance, trait Tr0 where T1: Tr2<T3> has an edge Tr0 -> Tr2, and T1 and T3 are ignored). And when checking types, there are no edges due to bounds (in struct T<A: Tr>(A), Tr is ignored; but we will track dependencies to trait impls whenever T is instantiated) or trait objects dyn Tr (because they are unsupported). Can you find a counterexample where that breaks soundness?

[jhjourdan]

Ok, many thanks for that!

There is a lot of things to review, and I need to think about this, because there is a lot of potential for unsoundness.

[Lysxia]

there are currently no edges between traits and types

I came up with an argument for that. You can split every trait in two: its associated types on one side, and its methods and supertrait constraints on the other side. Once associated type declarations are viewed as standalone constructs, they depend on nothing. That's why there is no need to track dependencies between ADTs and associated type declarations (which are different from associated trait instances, for which I do track dependencies).

The only remaining dependencies from types to traits are via trait objects, which are basically not supported at the moment.

[jhjourdan]

Cannot associated types depend on associated types of subtraits?

[Lysxia]

I don't see how.

Another way to think about it is that associated types are like extra type parameters (as they would actually be in Rocq), with differences only relevant to type inference.

trait Tr {
   type A;
}

struct S<T: Tr>(T::A);

// is like

trait Tr<A> {
}

struct S<A, T: Tr<A>>(A);