# Labs 01: Using the Stainless Verification System

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

Don't forget to bring your laptops!

### Deliverable

You are given 1 week for this assignment.

Send your solutions by mail to nicolas.voirol@epfl.ch.

### Exercise 1

Try to verify the putAside function. When a function fails to verify, Stainless will provide you with a counterexample (when it exists) to help you understand what went wrong. Look at the counterexample returned for the given implementation of putAside; what is wrong with this function?

Fix the function so that Stainless succeeds in showing the function correct.

```object Bank1 {
case class Acc(checking : BigInt, savings : BigInt)

def putAside(x: BigInt, a: Acc): Acc = {
require (notRed(a) && a.checking >= x)
Acc(a.checking - x, a.savings + x)
} ensuring {
r => notRed(r) && sameTotal(a, r)
}

def sameTotal(a1: Acc, a2: Acc): Boolean = {
a1.checking + a1.savings == a2.checking + a2.savings
}

def notRed(a: Acc) : Boolean = {
a.checking >= 0 && a.savings >= 0
}
}```

### Exercise 2

Add specifications so that the insertion sort function verifies.

Note: you will need either the Z3 or CVC4 backend solvers for this to verify. See the Inox documentation for some information about installing these.

```import stainless.annotation._
import stainless.lang._

object InsertionSort {

sealed abstract class Option[T]
case class Some[T](value: T) extends Option[T]
case class None[T]() extends Option[T]

sealed abstract class List {
def size: BigInt = (this match {
case Nil() => BigInt(0)
case Cons(_, t) => 1 + t.size
})

def content: Set[BigInt] = this match {
case Nil() => Set()
case Cons(h, t) => Set(h) ++ t.content
}

def min: Option[BigInt] = this match {
case Nil() => None()
case Cons(h, t) => t.min match {
case None() => Some(h)
case Some(m) => if(h < m) Some(h) else Some(m)
}
}

def isSorted: Boolean = this match {
case Nil() => true
case Cons(h, Nil()) => true
case Cons(h1, t1 @ Cons(h2, t2)) => h1 <= h2 && t1.isSorted
}

/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
def insert(e: BigInt): List = {
require(isSorted)
this match {
case Nil() => Cons(e, Nil())
case Cons(h, t) =>
if (h <= e) {
Cons(h, t.insert(e))
} else {
Cons(e, this)
}
}
}

/* Insertion sort yields a sorted list of same size and content as the input
* list */
def sort: List = (this match {
case Nil() => Nil()
case Cons(h, t) => t.sort.insert(h)
}) ensuring(res => res.content == this.content
&& res.isSorted
&& res.size == this.size
)

}

case class Cons(h: BigInt, t: List) extends List
case class Nil() extends List
}```

### Exercise 3

Add a post-condition to firstPosOf and see comment in function wtf.

```import stainless.lang._
import stainless.annotation._

object SearchList {
sealed abstract class List[T] {
def size: BigInt = {
this match {
case Nil() => BigInt(0)
case Cons(h, t) => BigInt(1) + t.size
}
} ensuring { _ >= 0 }

def content: Set[T] = {
this match {
case Nil() => Set()
case Cons(h, t) => Set(h) ++ t.content
}
}

def firstPosOf(v: T): BigInt = {
this match {
case Nil() => BigInt(-1)
case Cons(h, t) if h == v => BigInt(0)
case Cons(h, t) =>
val p = t.firstPosOf(v)
if (p >= 0) {
p + 1
} else {
p
}
}
} ensuring {
res => false // TODO: Ensure that if (and only if) res is non-negative, the list contains v.

}

def take(n: BigInt): List[T] = {
require(n >= 0)
this match {
case Nil() => Nil[T]()
case Cons(h, t) if n == 0 => Nil[T]()
case Cons(h, t) => Cons(h, t.take(n - 1))
}
} ensuring {
res => res.size <= n
}

def contains(v: T): Boolean = {
this match {
case Nil() => false
case Cons(h, _) if h == v => true
case Cons(_, t) => t.contains(v)
}
} ensuring {
res => res == (content contains v)
}
}

case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]

@induct
def wtf[T](l: List[T], v: T): Boolean = {
// What is this function checking? Translate to english. Can you remove the l.contains(v) part? Why?
!((l.contains(v)) && (l.take(l.firstPosOf(v)).contains(v)))
}.holds
}```

### Exercise 04

Add contracts to the following code to make sure that evaluation of the untyped lambda calculus returns either *None* (when evaluation gets stuck), or a value (defined by the *isValue* predicate).

```import stainless.lang._

object LambdaCalculus {
abstract class Term
case class Var(x: BigInt) extends Term
case class Abs(x: BigInt, body: Term) extends Term
case class App(func: Term, arg: Term) extends Term

// free variables of t
def fv(t: Term): Set[BigInt] = t match {
case Var(x) => Set(x)
case Abs(x, body) => fv(body) -- Set(x)
case App(func, arg) => fv(func) ++ fv(arg)
}

// [x->u]t
def subst(x: BigInt, u: Term, t: Term): Term = t match {
case Var(y) => if (x == y) u else t
case Abs(y, body) => if (x == y) t else Abs(y, subst(x, u, body))
case App(f, a) => App(subst(x, u, f), subst(x, u, a))
}

// big step call-by-value evaluation
def eval(t: Term): Option[Term] = t match {
case App(t1, t2) => eval(t1) match {
case Some(Abs(x, body)) => eval(t2) match {
case Some(v2) => eval(subst(x, v2, body))
case None() => None[Term]()
}
case _ => None[Term]() // stuck
}
case _ => Some(t) // Abs or Var, already a value
}

def isValue(t: Term): Boolean = t match {
case Var(x) => true
case Abs(x, body) => true
case App(f, a) => false
}
}```

But wait, something feels a little off… what about the Omega term? Remember that induction is only sound when applied on a well-founded domain. In our case, this translates to termination of recursive functions! Check termination of your program by giving the –termination argument to Stainless. What does Stainless tell you?