Function body needs to be asserted manually

[dnezam]

Consider the following Viper program:

domain Unit {
  function unit(): Unit
}

function Asserting(b: Bool): Unit
  requires b
{ unit() }

function Flatten(xs: Seq[Seq[Int]]): Seq[Int]
  decreases xs
{
  (|xs| == 0 ?
    Seq[Int]() :
    xs[0] ++ Flatten(xs[1..]))
}

function FlattenSingleton(xs: Seq[Int]): Unit
  ensures Flatten(Seq(xs)) == xs
{
  // Does not work:
  // unit()
  
  // Does not work:
  // Asserting(|Seq(xs)| != 0)

  // Does not work:
  // let _ == (Flatten(Seq(xs))) in unit()

  // This works:
  Asserting(Flatten(Seq(xs)) == (|Seq(xs)| == 0 ?
    Seq[Int]() :
    Seq(xs)[0] ++ Flatten(Seq(xs)[1..])))
}

Why does this only verify if the body of Flatten is manually asserted? Shouldn't it already be available from Flatten(Seq(xs)) in the postcondition?

[marcoeilers]

This is not the function body being unavailable but the (intended!) incompleteness of recursive functions. Flatten's definition is unfolded once for every argument for which you use it.
So by default, when you talk about Flatten(Seq(xs)), the verifier knows that it is equal to its body, but it does not unfold the recursive call Flatten(Seq(xs)[1..]). If you mention that call manually, its definition will be unfolded and you can prove your postcondition:

method m(xs: Seq[Int]) {
  assert Flatten(Seq(xs)[1..]) == Seq()  // this line is needed to make the next one pass
  assert Flatten(Seq(xs)) == xs
}

[dnezam]

That completely slipped my mind. Thank you for the clarification!