Class 12

// In the previous class, we used well-founded orders on non-negative integers and on datatypes.
// Now, we define a well-founded order on all types, see slides.
// As the slides show, we also consider compositions of well-founded orders: union, adding
// a top element, and lexicographic tuples of various lengths.
// In this class, we'll show many useful examples of how to prove termination.

// Here is an example that uses the well-founded order on Booleans, where `false` is smaller
// than `true`.

function x(c: bool): int
  decreases c
{
  if c then y(c) else 0
}

function y(c: bool): int
  decreases !c
{
  if c then 1 else x(c)
}

// The Ackermann function is a famous function that grows very quickly. Evaluating the
// function can take a long time, but it's easy to prove that it does indeed terminate.
// We do that using a lexicographic pair.

function Ack(m: nat, n: nat): nat
  decreases m, n
{
  if m == 0 then
    n + 1
  else if n == 0 then
    Ack(m - 1, 1)
  else
    Ack(m - 1, Ack(m, n - 1))
}

// The next example counts the number of integers `i`, where `0 <= i < n`, that satify `P(i)`.
// For this example, the precise definition of `P` does not matter, so we omit its body.
// Here is the straightforward way to define function `CountPs`, and proving termination of
// this function is also simple.

predicate P(x: int)

function CountPs(n: nat): int
  decreases n
{
  if n == 0 then
    0
  else if P(n - 1) then
    1 + CountPs(n - 1)
  else
    CountPs(n - 1)
}

// Suppose the recursive cases of `CountPs` were more complicated. Then, we may want to
// refactor those cases into a separate function:

function CountPs2(n: nat): int
  decreases 2 * n + 1
{
  if n == 0 then
    0
  else if P(n - 1) then
    AddAndCountTheRest(n, 1)
  else
    AddAndCountTheRest(n, 0)
}

function AddAndCountTheRest(n: nat, x: int): int
  requires n != 0
  decreases 2 * n
{
  x + CountPs2(n - 1)
}

// To prove termination of these mutually recursive functions, we can't just use
// `decreases n` for both functions, because the call from `CountPs2` to `AddAndCountTheRest`
// does not cause a decrease in parameter `n`. Instead, these two functions use the
// `decreases` clauses `2 * n + 1` and `2 * n`, respectively.

// An easier way to prove termination is to use a lexicographic pair rather than
// multiplying by 2 and adding, as shown here:

function CountPs3(n: nat): int
  decreases n, 1
{
  if n == 0 then
    0
  else if P(n - 1) then
    AddAndCountTheRest3(n, 1)
  else
    AddAndCountTheRest3(n, 0)
}

function AddAndCountTheRest3(n: nat, x: int): int
  requires n != 0
  decreases n, 0
{
  x + CountPs3(n - 1)
}

// The choice of `1` and `0` in these `decreases` clauses is arbitrary. Any two
// expressions where the former is larger than the latter would work. For example,
//     decreases n, 496
//     decreases n, 28
// would also work. Since Dafny pads `decreases` clauses with a "top" element at the
// end, we can also omit the constant in the `decreases` clause of `CountPs3`.
// Then, since "top" is larger than anything else, we can replace the constant
// in the `decreases` clause of `AddAndCountTheRest3` with any expression, for
// example, with `x`. We then get

function CountPs4(n: nat): int
  decreases n
{
  if n == 0 then
    0
  else if P(n - 1) then
    AddAndCountTheRest4(n, 1)
  else
    AddAndCountTheRest4(n, 0)
}

function AddAndCountTheRest4(n: nat, x: int): int
  requires n != 0
  decreases n, x
{
  x + CountPs4(n - 1)
}

// This choice is especially nice, because each of these `decreases` clauses
// lists the respective function's parameters, which is what Dafny's default
// `decreases` clauses do. Thus, we can omit these `decreases` clauses altogether
// and rely on the defaults.

function CountPs5(n: nat): int
{
  if n == 0 then
    0
  else if P(n - 1) then
    AddAndCountTheRest5(n, 1)
  else
    AddAndCountTheRest5(n, 0)
}

function AddAndCountTheRest5(n: nat, x: int): int
  requires n != 0
{
  x + CountPs5(n - 1)
}

// In fact, the `decreases m, n` clause that we used for the Ackermann function
// above also coincides with the default `decreases` clause for that function, so
// the verifier will prove termination of that function even if we omit an explicit
// `decreases` clause. This is often the case in practice, which is why we didn't have to
// write any `decreases` clauses in the first many weeks of this class.
// (Remember: If you want to find out what `decreases` clause Dafny uses as the default,
// look at the function's hover text in the IDE.)

// The next example is a function that illustrates what seems like a need to increment
// the termination metric. That doesn't work, of course, because then we're not proving
// termination, and such a function might not terminate at all. But if there's some
// limit on how many times such increments can happen, then we can prove termination.
// To set the stage, let's start with a function that has an easy termination proof:

function Combine(a: nat, b: nat): (c: nat)
  ensures c == 100 * a + b
  decreases a, b
{
  if a == 0 then
    b
  else if b == 0 then
    Combine(a - 1, b + 100)
  // else if 5000 <= b then
  //   Combine(a + 1, b - 100)
  else
    Combine(a, b - 1) + 1
}

// The `b == 0` branch of this function essentially trades 1 unit of `a` for 100
// units of `b`. That decreases the lexicographic pair `a, b` and maintains the
// property in the function's postcondition.
//
// Now, suppose we want to go in the other direction, as indicated by the two lines
// that are commented out above. That commented-out branch trades 100 units of `b`
// for 1 unit of `a`, provided there is an ample supply of `b` units. If we included
// those two lines, the function does not always terminate.
//
// Let's limit the number of times that we are willing to take that branch. To do so,
// we'll introduce an extra parameter that holds a "budget" for how many times we're
// willing to increment `a` in this way. Now, we can prove termination using a
// lexicographic triple.

function Combine2(a: nat, b: nat, incBudget: nat): (c: nat)
  ensures c == 100 * a + b
  decreases incBudget, a, b
{
  if a == 0 then
    b
  else if b == 0 then
    Combine2(a - 1, b + 100, incBudget)
  else if 5000 <= b && incBudget != 0 then
    Combine2(a + 1, b - 100, incBudget - 1)
  else
    Combine2(a, b - 1, incBudget) + 1
}

// In the next example, we define multiplication as a function that
// performs repeated additions and we prove that our function is commutative,
// that is, that `Mult(x, y)` is the same as `Mult(y, x)`. The proof makes
// five calls to the induction hypothesis (that is, five recursive calls to the
// lemma itself). Each of those calls show a decrease of the lexicographic
// pair `x, y`, which proves termination. Two of the recursive calls are
// creative and interesting.

function Mult(x: nat, y: nat): nat {
  if y == 0 then 0 else x + Mult(x, y - 1)
}

lemma {:induction false} MultCommutative(x: nat, y: nat)
  ensures Mult(x, y) == Mult(y, x)
  decreases x, y
{
  if x == y {
  } else if x == 0 {
    assert Mult(x, y) == Mult(x, y - 1);
    assert Mult(y, x) == 0 == Mult(y - 1, x);
    MultCommutative(x, y - 1);
  } else if y < x {
    // This is one of the two interesting uses of the induction hypothesis.
    // This recursive call takes care of all cases where `y` is less than `x`.
    // It works because the property we're trying to prove is symmetric in
    // `x` and `y` and because the recursive call terminates since we're giving
    // a first parameter that's smaller than the given `x`.
    MultCommutative(y, x);
  } else {
    calc {
      Mult(x, y);
    ==  // def. Mult
      x + Mult(x, y - 1);
    ==  { MultCommutative(x, y - 1); }
      x + Mult(y - 1, x);
    ==  // def. Mult
      x + y - 1 + Mult(y - 1, x - 1);
      // Here is the other interesting use of the induction hypothesis. Since the
      // line above has the term `Mult(y - 1, x - 1)`, our first attempt at calling
      // the lemma recursively might be `MultCommutative(y - 1, x - 1)`. However,
      // such a call may not terminate, because we can't prove that `y - 1, x - 1`
      // is below `x, y`. Luckily, because the property we're trying to prove is
      // symmetric in `x` and `y`, we can use the recursive call `MultCommutative(x - 1, y - 1)`
      // (note the order of the parameters) to obtain the information about
      // `Mult(y - 1, x - 1)` that we need. By ordering the parameters in this way,
      // we also decrease the lexicographic pair `x, y`, so we're able to prove termination.
    ==  { MultCommutative(x - 1, y - 1); }
      x + y - 1 + Mult(x - 1, y - 1);
    ==  // def. Mult
      y + Mult(x - 1, y);
    ==  { MultCommutative(x - 1, y); }
      y + Mult(y, x - 1);
    ==  // def. Mult
       Mult(y, x);
    }
  }
}

// The next example shows another common pattern of using the induction hypothesis.
// The property proved by the `DropSame` lemma is that two different ways of defining
// a "drop" function (which returns a given list, dropping its first `n` elements)
// give the same result.

datatype List<X> = Nil | Cons(head: X, tail: List<X>)

function Length(xs: List): nat {
  if xs == Nil then 0 else 1 + Length(xs.tail)
}

function Drop(xs: List, n: nat): List
  requires n <= Length(xs)
{
  if n == 0 then xs else Drop(xs.tail, n - 1)
}

function Drop'(xs: List, n: nat): (r: List)
  requires n <= Length(xs)
  ensures Length(r) == Length(xs) - n
{
  // To take the `.tail` of `Drop'(xs, n - 1)` in the following line, we need
  // to know that this call returns a nonempty list. To obtain that piece of
  // information, we add a postcondition of `Drop'` that speaks about the length
  // of its result.
  if n == 0 then xs else Drop'(xs, n - 1).tail
}

lemma DropSame(xs: List, n: nat)
  requires n <= Length(xs)
  ensures Drop(xs, n) == Drop'(xs, n)
{
  if n < 2 {
    // easy
  } else {
    calc {
      Drop(xs, n);
    ==  // def. Drop
      Drop(xs.tail, n - 1);
    ==  { DropSame(xs.tail, n - 1); } // I.H.
      Drop'(xs.tail, n - 1);
    ==  // def. Drop'
      Drop'(xs.tail, n - 2).tail;
    ==  { DropSame(xs.tail, n - 2); } // I.H.
      Drop(xs.tail, n - 2).tail;
    ==  // def. Drop
      Drop(xs, n - 1).tail;
    ==  { DropSame(xs, n - 1); } // I.H.
      Drop'(xs, n - 1).tail;
    ==  // def. Drop'
      Drop'(xs, n);
    }
  }
}

// An interesting aspect of this proof is that it makes three calls to the induction hypothesis.
// Since one of those calls passes the argument `n - 2`, the `calc` statement in the proof
// requires `2 <= n`. So, both `n == 0` and `n == 1` are handled separately (and both are
// proved automatically, so we just need to spell out the `if n < 2` branch of the proof).

// Problem set 4 did some optimization of queries. We had included a precondition `arg < p`
// in one of the mutually recursive functions. It states that `arg` is structurally included
// in `p`. This is needed in the termination proof, and we can now explain why:

module QueryOptimization {
  type Name = string

  type Row = map<Name, int>

  datatype Expr =
    | Const(value: int)
    | Var(name: Name)
    | Plus(0: Expr, 1: Expr)
  datatype Pred =
    | Equal(e0: Expr, e1: Expr)
    | Leq(e0: Expr, e1: Expr)
    | And(p0: Pred, p1: Pred)

  datatype List<X> = Nil | Cons(head: X, tail: List<X>)
  type Table = List<Row>

  datatype Query =
    | Source(rows: Table)
    | Union(q0: Query, q1: Query)
    | Project(names: set<Name>, q: Query)
    | Select(cond: Pred, q: Query)

  function ProjectUnionOptimization(query: Query): Query
    decreases query
  {
    match query
    case Source(_) =>
      query
    case Union(q0, q1) =>
      Union(ProjectUnionOptimization(q0), ProjectUnionOptimization(q1))
    case Project(_, q) =>
      MoveProjectionInward(query, q)
    case Select(cond, q) =>
      Select(cond, ProjectUnionOptimization(q))
  }

  function MoveProjectionInward(p: Query, arg: Query): Query
    requires p.Project? && arg < p // the second conjunct says that `arg` is structurally included in `p`
    decreases p, arg
  {
    match arg
    case Union(q0, q1) =>
      // The proofs of termination for these calls just need the facts that q0 and q1
      // are structurally included in `arg.`
      var opt0 := MoveProjectionInward(p, q0);
      var opt1 := MoveProjectionInward(p, q1);
      Union(opt0, opt1)
    case _ =>
      // To prove termination of the call `ProjectUnionOptimization(arg)`, we need to show that `arg` is
      // below the lexicographic pair `p, arg`. That's why we need `arg < p`.
      Project(p.names, ProjectUnionOptimization(arg))
  }

  // If you were writing the two functions above without having to prove termination, then perhaps
  // you would have chosen to let `MoveProjectionInward` take `names: set<Name>` as its first parameter
  // instead of `p: Query`, which in our code above just acts like a wrapper around `p.names`. If you do
  // want the `set<Name>` parameter to be what's used at run time, then you can mark the `p` parameter
  // as `ghost`, that is, as specification-only. This gives us access to `p` so we can prove termination,
  // but `p` is then erased by the compiler and will not be part of the running program.

  function ProjectUnionOptimization'(query: Query): Query
    decreases query
  {
    match query
    case Source(_) =>
      query
    case Union(q0, q1) =>
      Union(ProjectUnionOptimization'(q0), ProjectUnionOptimization'(q1))
    case Project(_, q) =>
      MoveProjectionInward'(query, query.names, q)
    case Select(cond, q) =>
      Select(cond, ProjectUnionOptimization'(q))
  }

  function MoveProjectionInward'(ghost p: Query, names: set<Name>, arg: Query): Query
    requires p.Project? && arg < p
    decreases p, arg
  {
    match arg
    case Union(q0, q1) =>
      var opt0 := MoveProjectionInward'(p, names, q0);
      var opt1 := MoveProjectionInward'(p, names, q1);
      Union(opt0, opt1)
    case _ =>
      Project(names, ProjectUnionOptimization'(arg))
  }
}

// Here is a final example that illustrates another useful pattern of writing termination
// specifications. It uses a variation of the constants we've seen above.
// The `Flatten` function takes a list of lists and puts their elements into a sequence.
//
// A straightforward way of doing that is to use two functions, one for converting
// a list into a sequence and another for repeatedly calling the first and concatenating
// the results. Each of those functions would be recursive, but the two functions are
// not mutually recursive.
//
// The version we write here is different. It uses two mutually recursive functions and
// passes a "continuation" from one to the other. This continuation says what to do
// when the inner function has exhausted the given list `xs`.

function Flatten(xss: List<List<int>>): seq<int>
  decreases xss, 0
{
  match xss
  case Nil => []
  case Cons(s, tail) => FlattenInner(s, tail)
}

function FlattenInner(xs: List<int>, continuation: List<List<int>>): seq<int>
  decreases continuation, 1, xs
{
  match xs
  case Nil => Flatten(continuation)
  case Cons(x, xs') => [x] + FlattenInner(xs', continuation)
}

// The last piece of material in this class is an explanation of how all
// functions/lemmas/methods, not just recursive ones, make use of one and the
// same well-founded order. This is necessary to argue that an entire program
// terminates, even though we're only proving that its recursive (and mutually
// recursive) functions/lemmas/methods terminate.
//
// Consider a recursive function `Fib` for computing Fibonacci numbers and a
// function `SumOfFibs` that calls `Fib` on each element of a list and adds up
// the results. Termination of the recursive calls in these functions is
// easy to prove, as we've seen before. But let's try to write `decreases` clauses
// that could be used to show a decrease with every call, not just the recursive
// ones. Here's a way to do that:

function SumOfFibs(xs: List<nat>): nat
  decreases 1, xs
{
  if xs == Nil then 0 else Fib(xs.head) + SumOfFibs(xs.tail)
}

function Fib(n: nat): nat
  decreases 0, n
{
  if n < 2 then n else Fib(n-2) + Fib(n-1)
}

// The use of the constants 1 and 0 can be thought of as indicating how many
// non-recursive calls can still be done. That is, you can think of functions
// as being placed into strata, where a non-recursive call is one that goes from
// one stratum to a lower stratum. This is illustrated using colors in this
// class's slides.
//
// It would be tedious for a programmer to have to maintain these strata manually.
// For example, if a helper function were added between `SumOfFibs` and `Fib`, then
// the strata in the example would have to be renumbered. Dafny does this automatically
// and completely hides this bookkeeping from the user. This is done by computing
// a call graph for every module, grouping each _strongly connected component_ of
// that call graph into a stratum of its own.
//
// Again, this explains why an entire program terminates, even though we're just
// proving termination of recursive (and mutually recursive) functions/lemmas/methods.
// You do not need to encode these strata yourself---just write `decreases` clauses
// as we've seen (and you can omit those, too, when the default `decreases` clauses
// fit the bill).

function Mult(x: nat, y: nat): nat {
  if y == 0 then 0 else x + Mult(x, y - 1)
}

// Fill in the two missing cases of this fairly manual proof by induction.
lemma {:induction false} MultCommutative(x: nat, y: nat)
  ensures Mult(x, y) == Mult(y, x)
  decreases x, y
{
  if x == y {
  } else if x == 0 {
    assert Mult(x, y) == Mult(x, y - 1);
    assert Mult(y, x) == 0 == Mult(y - 1, x);
    MultCommutative(x, y - 1);
  } else if y < x {
    // Our proof invokes the induction hypothesis *once* here.
  } else {
    // Our proof invokes the induction hypothesis *three times* here.
    // (Weird, right?)
  }
}

lemma DropSame(xs: List, n: nat)
  requires n <= Length(xs)
  ensures Drop(xs, n) == Drop'(xs, n)
{
  if n < 2 {
    // easy
  } else {

  }
}

// Here are the definitions lifted from the code we just went through.
  
datatype List<X> = Nil | Cons(head: X, tail: List<X>)

function Length(xs: List): nat {
  if xs == Nil then 0 else 1 + Length(xs.tail)
}

function Drop(xs: List, n: nat): List
  requires n <= Length(xs)
{
  if n == 0 then xs else Drop(xs.tail, n - 1)
}

function Drop'(xs: List, n: nat): (r: List)
  requires n <= Length(xs)
  ensures Length(r) == Length(xs) - n
{
  // To take the `.tail` of `Drop'(xs, n - 1)` in the following line, we need
  // to know that this call returns a nonempty list. To obtain that piece of
  // information, we add a postcondition of `Drop'` that speaks about the length
  // of its result.
  if n == 0 then xs else Drop'(xs, n - 1).tail
}