Missing features of the termination check

[arnaudgolfouse]

Things missing from #999:

• A way to use structurally decreasing types. E.g.

  enum List<T> {
    Nil,
    Cons(T, Box<List<T>>),
  }
  
  impl<T> List<T> {
    #[terminates]
    fn length(&self) -> usize {
        match self {
            Nil => 0,
            Cons(_, tail) => 1 + tail.length(),
        }
    }
  }

  This can probably be resolved already, by using a correct #[variant]. For example for List<T>, the variant would be the (logical) length of the list.

• Defer more things to why3, especially for logical functions.

  Since logical functions are fully inlined at their call site, it seems we could just put them all in a big function f1 ... with f2 ... block, and let why3 prove that they terminate. But this might be complicated by some functions (like Vec::deep_model) having no body.

[xldenis]

This can probably be resolved already, by using a correct #[variant]. For example for List, the variant would be the (logical) length of the list.

How do you define the logical length of the list if not with a structural variant though?

[jhjourdan]

Structural invariants are supported for logical functions by simply translating to a Why3 logical function, which supports structural invariants.

The problem is that our encoding of MIR to WhyML/MLCFG/Coma breaks structural variants by making the syntactic tracking of subvalues impossible.

[xldenis]

Since logical functions are fully inlined at their call site, it seems we could just put them all in a big function f1 ... with f2 ... block, and let why3 prove that they terminate.

There's a corollary issue: we don't want to duplicate proofs, and termination proofs are indissociable from the rest of the correctness proof for a logical function. The bodies we clone for logical functions do not generate proof obligations (which is on purpose), if a logical function has a variant we will not generate its body in the module which makes use of it, instead we will provide a defining axiom which accounts for the variant.

Something which could potentially help here is if we could tell why3 to assume the termination of a function (since we have externally proved it). This sounds wildly unsound though.

[xldenis]

Structural invariants are supported for logical functions by simply translating to a Why3 logical function, which supports structural invariants.

The problem is that our encoding of MIR to WhyML/MLCFG/Coma breaks structural variants by making the syntactic tracking of subvalues impossible.

I understand that this is now broken but it wasn't before: I have been using structural variants for years. Again, I am not saying to stop the merge #999 but this wasn't a problem before. Clearly the syntactic tracking used to work.

[jhjourdan]

By default, we were not tracking termination for program functions.

[xldenis]

By default, we were not tracking termination for program functions.

Right! I feel like variants have sort of worked for program functions in the past though, but I'm much less confident there.

[jhjourdan]

They did, but not structural variants.