In this first lab, you will use Stainless (https://github.com/epfl-lara/stainless) to verify programs.

Don't forget to bring your laptops!

There are two main options to use Stainless. We recommend having both available. In both cases, you will need the SMT solvers https://github.com/Z3Prover/z3/releases and https://cvc4.cs.stanford.edu/web/2018/06/25/cvc4-1-6-released/. Install them so that they are available in your path (z3 and cvc4 should be recognized as commands in your console).

The first one is through the Stainless plugin for sbt. You can get started by running:

sbt new epfl-lara/stainless-project.g8

Type in a project name (don't worry if the characters you type don't show up), and press enter. Stainless version remains 0.5.1 by default. This command creates a folder containing an sbt project. To try it, go to the new folder and start the sbt console by typing sbt.

The project has two parts, one in the verified folder which goes through Stainless and thus must use Stainless library and respect the language of Stainless. And one in core which can be arbitrary Scala code, and which can depend on the verified code. Type verified/compile to verify the file in verified/src/main/scala/*.scala, and type core/run to run the code in core/src/main/scala/*.scala.

In build.sbt, you can set the option stainlessEnabled to false in order to compile and run the code without verifying it. When changing the option, you need to reload the sbt console by typing reload.

The second option for using Stainless is by downloading the latest release from: https://github.com/epfl-lara/stainless/releases. Unzip the archive, and you will get an executable file called stainless that you can use to verify Scala files.

When using Stainless via this executable, you do not need to put files within an sbt project, but can instead just invoke Stainless on the Scala file, eg. `/path/to/stainless Problem1.scala`.

To summarize, here are the things you should prepare:

• sbt: https://github.com/sbt/sbt/releases
• Install Z3: https://github.com/Z3Prover/z3/releases
• Install CVC4: https://cvc4.cs.stanford.edu/web/2018/06/25/cvc4-1-6-released
• Create a blank project using `sbt new epfl-lara/stainless-project.g8`

• Install Stainless: https://github.com/epfl-lara/stainless/releases

• VSCode + Metals extension (or another editor of your choosing): https://code.visualstudio.com/Download

When solving exercises, you can copy the code to the verified.scala file (or to another file in the same folder), and see Stainless output using the verified/compile sbt command or using the stainless executable. Remember that you can also debug your code using normal Scala println statements in the code and running core/run. If you use println in Stainless code, please use stainless.io.StdOut.println (which can only be used on Int, String, and Char).

Please tell us if something doesn't work as expected.

As Stainless currently does not work out of the box on Windows, we advise you to run it with either the Windows Subsystem for Linux (https://docs.microsoft.com/en-us/windows/wsl/install-win10) or a virtual machine running Linux. It may also work with something like Cygwin (https://www.cygwin.com) but this has not been tested yet.

Upload your solutions on Moodle by Monday 30th September at 23:59.

BigInt represents in Stainless the types of integers. In the code below, the ensuring clause says that, for every input x to the function double, the result res should be greater than x. The ensuring clause is called the postcondition of the function.

object Problem1 {
  def double(x: BigInt): BigInt = {
    2 * x
  } ensuring(res => res >= x)
}

In that case, this specification is wrong. Running Stainless on this example should get you a counter-example. By using boolean connectives such as && or ||, modify the ensuring clause res >= x with a (non-trivial) property which is true, and make sure that it is verified by Stainless.

Int is the type of signed integers on 32 bits. Run Stainless on the following example, read the counter-example which is given, and explain in English (using comments in your submitted code) what is wrong with the specification as written. Again, modify the ensuring into a (non-trivial) property which is true and which is verified by Stainless.

object Problem2 {
  def increment(x: Int): Int = {
    x + 1
  } ensuring(res => res > x)
}

To specify properties on functions, so far we have used postconditions using the ensuring clause. We can also specify preconditions using a require clause, as follows.

def positiveAdd(a: BigInt, b: BigInt): BigInt = {
  require(a >= 0 && b >= 0)
  a + b
} ensuring(res =>
  res >= 0
)

The specification of positiveAdd says that it may only be called with arguments a and b satisfying the require clause, i.e. arguments which are non-negative. Moreover, it says that under these conditions, the result is also non-negative. Try to call positiveAdd with negative arguments, and see what Stainless tells you. Note the text and the line number of the reported error.

This explanation about positiveAdd is there to introduce the concept of preconditions which is useful for the following exercise (Problem 3). Consider the insert function, which inserts an element in a list of integers, and ensures that the resulting list is sorted. Observe the output of Stainless on this program and fix it by adding a precondition to insert.

import stainless.collection._
 
object Problem3 {
  def isSorted(l: List[BigInt]): Boolean = {
    l match {
      case Nil() => true
      case Cons(x, Nil()) => true
      case Cons(x, xs @ Cons(y, ys)) => x <= y && isSorted(xs)
    }
  }
 
  def insert(x: BigInt, l: List[BigInt]): List[BigInt] = {
    l match {
      case Nil() => Cons(x, Nil())
      case Cons(y, ys) =>
        if (x < y) Cons(x, l)
        else Cons(y, insert(x, ys))
    }
  } ensuring(res => isSorted(res))
}

This search function operates on a sorted array, and is supposed to return true when there exists an index i between lo and hi such that arr(i) = x. The function is left a bit unspecified, as we don't specify that arr should be sorted, and we could return as an option the index i instead of a boolean, but we will not worry about these aspects in this exercise.

Run Stainless on the example, and observe how it complains about the array index i in arr(i) being out of bounds, and about the precondition of search not being respected in the recursive calls. Fix the line starting with val i to have a correct code.

import stainless.lang._
 
object Problem4 {
  def search(arr: Array[Int], x: Int, lo: Int, hi: Int): Boolean = {
    require(0 <= lo && lo <= hi+1 && hi < arr.length)
    if (lo <= hi) {
      val i = (lo + hi) / 2
      val y = arr(i)
      if (x == y) true
      else if (x < y) search(arr, x, lo, i-1)
      else search(arr, x, i+1, hi)
    } else {
      false
    }
  }
}

In forallAfterInsert, we proved (by induction on the tree) that if a function p returns true on all elements of a tree t, and it returns true on an element x, then p returns true on all elements of the tree insert(t, x).

In balancedAfterInsert, our goal is to prove that if we insert an element in a balanced tree, the resulting tree is still balanced. Run Stainless (with a timeout of 10 seconds) on this code and observe that it times out on the two assertions assert(isBalanced(insert(t, x))).

For the first assertion, if we unroll the definition of insert once, we get that insert(t , x) equals Node(root, insert(left, x), right). Then, observe that four conditions need to be verified so that isBalanced returns true on that tree. For each condition, write an assertion (above the assert(isBalanced(insert(t, x))) of the first branch) stating that the condition is true.

Run Stainless (again with a timeout of 10 seconds) and by reading the line numbers in the report, see for which of the four conditions (which of the four new assertions) Stainless times out. In order to have Stainless verify this code, you need to use the previous lemma (forallAfterInsert) by calling it with the right arguments on the line above the assertion that times out.

Do the same thing for the second branch.

import stainless.lang._
import stainless.proof._
 
object Problem5 {
  sealed abstract class Tree[T]
  case class Leaf[T]() extends Tree[T]
  case class Node[T](root: T, left: Tree[T], right: Tree[T]) extends Tree[T]
 
  def forall[T](t: Tree[T], p: T => Boolean): Boolean = {
    decreases(t)
    t match {
      case Leaf() => true
      case Node(root, left, right) => p(root) && forall(left, p) && forall(right, p)
    }
  }
 
  def isBalanced(t: Tree[BigInt]): Boolean = {
    decreases(t)
    t match {
      case Leaf() => true
      case Node(root, left, right) =>
        forall(left, (node: BigInt) => node <= root) &&
        forall(right, (node: BigInt) => node >= root) &&
        isBalanced(left) &&
        isBalanced(right)
    }
  }
 
  def insert(t: Tree[BigInt], x: BigInt): Tree[BigInt] = {
    require(isBalanced((t)))
    t match {
      case Leaf() => Node(x, Leaf(), Leaf())
      case Node(root, left, right) if (root > x) => Node(root, insert(left, x), right)
      case Node(root, left, right) if (x > root) => Node(root, left, insert(right, x))
      case _ => t // case where root == x
    }
  }
 
  def forallAfterInsert(t: Tree[BigInt], x: BigInt, p: BigInt => Boolean): Unit = {
    require(isBalanced(t) && forall(t, p) && p(x))
    t match {
      case Leaf() => ()
      case Node(root, left, right) if (root > x) => forallAfterInsert(left, x, p)
      case Node(root, left, right) if (x > root) => forallAfterInsert(right, x, p)
      case _ => ()
    }
  } ensuring(_ => forall(insert(t, x), p))
 
  def balancedAfterInsert(t: Tree[BigInt], x: BigInt): Unit = {
    require(isBalanced(t))
    t match {
      case Leaf() => ()
      case Node(root, left, right) if (root > x) =>
        balancedAfterInsert(left, x) // thanks to this recursive call, we know: isBalanced(insert(left, x)))
        // ???
        assert(isBalanced(insert(t, x)))
      case Node(root, left, right) if (x > root) =>
        balancedAfterInsert(right, x) // thanks to this recursive call, we know: isBalanced(insert(right, x)))
        // ???
        assert(isBalanced(insert(t, x)))
      case _ => ()
    }
  } ensuring(_ => isBalanced(insert(t, x)))
}

Problem 6 is a bit longer, but each function it features is short and simple. We start by defining FSM, which is a class of non-deterministic finite state machines. It has a finite number of states and a transition function, which given a state and an input, give all the possible successors.

The function isRunFrom returns true when the arguments represent a valid run in the finite-state machine fsm.

The function isRunFromAllContained doesn't compute anything (the return type is Unit), but is a lemma stating that when isRunFrom holds, then all states that appear in the run belong to fsm.states.

The function isAcyclic returns true when a run has no cycle, i.e. it does not go through the same state twice.

lengthRemoveNothing is a lemma stating that the length of a list does not change if we remove an element which was not contained in it (note the @induct notation which asks Stainless to prove the lemma by induction on l).

lengthRemoveOne is a lemma stating that the length of a list decreases strictly when we remove an element contained in the list. Note the call to lengthRemoveNothing. This is how we invoke a previous lemma in Stainless. Also note the recursive call to lengthRemoveOne. This corresponds again by a proof by induction on l, but this time it is done explicitly and thus the @induct notation should not be used.

forallContained is a lemma stating that if all elements of a list l2 are contained in a list l1, and l2 does not contain x, then all elements of l2 are also in l1 - x.

largerLength is a lemma that builds upon the previous ones to show that if all elements of a list l2 are in a list l1, and that l2 has no duplicates, then the length of l2 is smaller than the length of l1.

Finally, shortAcyclicRuns is a lemma stating than the length of an acyclic run is strictly less the number of states (if we don't count the initial state). As presented, Stainless does not have enough information to verify this property and would timeout. The goal is to understand which lemmas (from the previous ones) you need in order to establish that shortAcyclicRuns holds. Replace the two commented lines ??? with the correct calls to two of the previous lemmas so that Stainless verifies.

Edit: Some solutions require more than two lemmas, this is fine as well. However, you should not make a recursive call to shortAcyclicRuns.

import stainless.collection._
import stainless.annotation._
 
object Problem6 {
 
  case class FSM[State, Input](states: List[State], transition: (State, Input) => List[State])
 
  def isRunFrom[State,Input](
    fsm: FSM[State, Input],
    run: List[(Input, State)],
    initial: State
  ): Boolean = {
    fsm.states.contains(initial) &&
    (run match {
      case Nil() => true
      case Cons((l,q), ps) =>
        fsm.transition(initial, l).contains(q) &&
        isRunFrom(fsm, ps, q)
    })
  }
 
  def isRunFromAllContained[State, Input](
    fsm: FSM[State, Input],
    run: List[(Input, State)],
    initial: State
  ): Unit = {
    require(isRunFrom(fsm, run, initial))
 
    if (!run.isEmpty) isRunFromAllContained(fsm, run.tail, run.head._2)
 
  } ensuring(_ =>
    fsm.states.contains(initial) &&
    run.map(_._2).forall(fsm.states.contains)
  )
 
  def noDuplicate[T](l: List[T]): Boolean = l match {
    case Nil() => true
    case Cons(x, xs) => !xs.contains(x) && noDuplicate(xs)
  }
 
  def isAcyclic[State,Input](run: List[(Input, State)], initial: State): Boolean = {
    val states = run.map(_._2)
    noDuplicate(Cons(initial, states))
  }
 
  def lengthRemoveNothing[T](@induct l: List[T], x: T): Unit = {
    require(!l.contains(x))
 
    ()
 
  } ensuring(_ => l.length == (l-x).length)
 
  def lengthRemoveOne[T](l: List[T], x: T): Unit = {
    require(l.contains(x))
 
    if (l.tail.contains(x)) {
      lengthRemoveOne(l.tail, x)
    } else {
      lengthRemoveNothing(l.tail, x)
    }
 
  } ensuring(_ => l.length > (l-x).length)
 
  def forallContained[T](l1: List[T], @induct l2: List[T], x: T): Unit = {
    require(l2.forall(l1.contains) && !l2.contains(x))
 
    ()
  } ensuring { _ =>
    val nl1 = l1 - x
    l2.forall(nl1.contains)
  }
 
  def largerLength[T](l1: List[T],l2: List[T]): Unit = {
    require(noDuplicate(l2) && l2.forall(l1.contains))
 
    if (!l2.isEmpty) {
      val nl1 = l1 - l2.head
      lengthRemoveOne(l1, l2.head)          // l1.length > nl1.length
      forallContained(l1, l2.tail, l2.head) // l2.tail.forall(nl1.contains)
      assert(noDuplicate(l2.tail))
      assert(l2.tail.forall(nl1.contains))
      largerLength(nl1, l2.tail)
    }
 
  } ensuring(_ => l1.length >= l2.length)
 
  def shortAcyclicRuns[State, Input](
    fsm: FSM[State, Input],
    run: List[(Input, State)],
    initial: State
  ): Unit = {
    require(isRunFrom(fsm, run, initial) && isAcyclic(run, initial))
 
    // ???
    // ???
 
  } ensuring(_ => run.length < fsm.states.length)
 
}