Auto-generating well-foundedness axioms for ADT types in the ADT plugin

[marcoeilers]

This PR extends the ADT plugin to generate an additional domain TWellFoundedOrder for every ADT type T that constrains the decreasing and bounded functions used in termination checks in the obvious way, so that users can write clauses like decreases t for a parameter t of an ADT type by default.

The additional domain is generated for an ADT type T iff:

• The termination plugin is not deactivated
• The program contains a WellFoundedOrder domain, i.e., the decreasing and bounded functions are actually declared
• The program does not yet contain domain TWellFoundedOrder, i.e., there is no user-provided definition of the well-foundedness order for this type yet.

The generated domain for type T and recursive constructor C1(T) and non-recursive constructor C2(V) looks as follows:

domain TWellFoundedOrder {
  axiom {
    forall v: V :: { C2(v) } bounded(C2(v))
  }
  axiom {
    forall t: T :: { C1(t) } bounded(C1(t)) && decreasing(t, C1(t))
  }
  axiom {
    forall v1: T, v2: T, v3: T :: { decreasing(v1, v2), decreasing(v2, v3) }
      decreasing(v1, v2) && decreasing(v2, v3) ==> decreasing(v1, v3)
  }
}

[jcp19]

I have two comments about the design, one about unexpected results and the other about completeness.

1. Assuming that our ADTs define inductive types, let's consider the Stream type:

adt Stream = Stream(x: Int, s: Stream)

The existence of a value of this type implies false in this scenario. An inexperienced user may be confused that the following verifies:

decreases s
function mapPlusOne(s: Stream): Stream {
    Stream(s.x + 1, mapPlusOne(s.s))
}

The successful verification is correct, but if a user is not aware that ADTs are inductive, they may expect a termination error here. It is unclear to me what would be the best way to avoid surprising users here. At any rate, a possibility could be to extend the second axiom to sth like

axiom {
    forall t: T :: { C1(t) } (hasBaseCase() ==> bounded(C1(t))) && decreasing(t, C1(t))
  }

hasBaseCase() would be a boolean constant axiomatized to be true iff there is a non-recursive constructor. This would get rid of the surprising behaviour above, but it kind of ad hoc.

2. This approach is very incomplete for mutually recursive data-types, e.g.,

adt List1 = List1(x: Int, l: List2)
adt List2 = Empty | NonEmpty(l: List2)

decreases l
function len(l: List2): Int {
    l == Empty? 0 : 1 + len(l.l) // cannot prove that l.l < l
}

This is not such a big deal because the user can always override the termination measures, but may be a bit annoying.

[marcoeilers]

Thanks!
The second issue I think I can address relatively easily; I'll go do that.
The first issue I agree is not great, but IMO it basically exists independently of termination measures. Once someone has defined that Stream ADT, something has already gone wrong; that's just not a recursive data type. IMO that declaration should result in an error (that'd be SUPER simple to check, too) or at the very least a warning.

[jcp19]

I've come to terms with allowing the snippet I showed in Point 1 to verify. Trying to avoid this particular surprising behaviour sounds like enumerating badness. Doing so is more consistent with what we do for preconditions (we do NOT try to find out whether they are satisfiable).

Another option would be to simply not generate a well founded order for ADTs without a base case, although I would prefer some static check that rejects ADT definitions like this

[marcoeilers]

Okay, mutually recursive ADT definitions are now supported.
I would also be in favor of rejecting ADT definitions that don't have a base case, but then IMO this should be a separate PR, I'll put it on my to do list.