# Labs 01: Scala, Stainless, and State Machines

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

**Don't forget to bring your laptops!**

### Preparation

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).

#### Stainless SBT plugin

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**.

#### Stainless Command-Line

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`.

#### Summary

To summarize, here are the things you should prepare:

##### For usage with sbt

- Install Z3: https://github.com/Z3Prover/z3/releases
- Create a blank project using `sbt new epfl-lara/stainless-project.g8`

##### For usage via the command-line

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

##### For editing Scala files

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

#### Verifying your code

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.

#### Note for Windows users

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.

### Deliverable

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

### Problem 1: BigInt

**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.

### Problem 2: Int

**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) }

### Problem 3: Preconditions

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)) }

### Problem 4: Binary Search

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 } } }

### Problem 5: Balanced Tree

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: Finite State Machines

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) }