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!

You should start by downloading and installing Stainless locally on your (preferably linux) machine. Please follow the instructions in the Stainless README and tell us if something fails.

You are given 1 week for this assignment.

Deadline: Sunday, Feb. 26, 25:59.

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

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

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
}

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
}

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?