In this first lab, you will use the web-interface of leon to try to verify programs. You will use an experimental version of the Leon interface available at: http://laraquad1.epfl.ch:9000/sav15

You should also install Leon locally, on your (preferably linux) machine. Please follow the instructions on https://github.com/epfl-lara/leon#building-leon and tell us if something fails.

The web interface for the SAV labs will be directly linked to a git repository. It will allow you to run tests, submit deliverables, receive feedback, etc..

The web interface is located at http://larasrv09.epfl.ch:9000/sav15 (Tequila authentication required.)

Labs will be done in groups of at most 2. Try to form groups of two as much as possible. You will have the choice of either creating a new group or joining an existing group.

1. Go to http://larasrv09.epfl.ch:9000/sav15 and authenticate yourself
2. The first time you go there, you can either create a group or wait until somebody created a group with you.
3. Once you are within a group, go to the YourName > SSH Keys tab, and register your Public SSH key. Make sure you copy your entire key, including the `ssh-rsa` prefix and the key identifier at the end.

You are given 1 week for this assignment.

Deadline: Sunday, Mar. 1, 25:59.

You must use the interface on http://larasrv09.epfl.ch:9000/sav15/repository as follows:

1. Click on the “Deliverables” tab
2. Click “Deliver this version” on the commit corresponding to the version of your code you want to submit

Try to verify the putAside function. When a function fails to verify, you can explore the counter-example by clicking on various relevant parts of the invalid functions. You can also click on the red X-mark to open the verification result details. Look at the counter-example returned; what is wrong with this function?

Fix the function so that Leon 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
  }
}

Implement isNNF so that it returns true on NNF formulas, and false otherwise. A correct implementation of isNNF should allow vars to verify.

object PropositionalLogic {
 
  sealed abstract class Formula
  case class And(lhs: Formula, rhs: Formula) extends Formula
  case class Or(lhs: Formula, rhs: Formula) extends Formula
  case class Implies(lhs: Formula, rhs: Formula) extends Formula
  case class Not(f: Formula) extends Formula
  case class Literal(id: BigInt) extends Formula  
 
 
  def nnf(formula: Formula): Formula = (formula match {
    case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
    case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
    case Implies(lhs, rhs) => nnf(Or(Not(lhs), rhs))
    case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
    case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
    case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
    case Not(Not(f)) => nnf(f)
    case Not(Literal(_)) => formula
    case Literal(_) => formula
  }) ensuring(isNNF(_))
 
  def isNNF(f: Formula): Boolean = f match {
    /* TODO: Implement isNNF */
  }
 
  // Note that matching should be exhaustive due to precondition.
  def vars(f: Formula): Set[BigInt] = {
    require(isNNF(f))
    f match {
      case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
      case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
      case Not(Literal(i)) => Set[BigInt](i)
      case Literal(i) => Set[BigInt](i)
    }
  }
}

1. Add pre- and postconditions, or fix the code such that the following functions verify: zip, sizesAreEquiv, reverse. The postconditions on these functions give what should be checked, i.e. they should not be changed.
2. find out what the function drunk does, and provide a correct postcondition that relates the sizes of the input list with the output list
3. the function appendAssoc is meant to prove that the appending lists is associative. Formulate this predicate and make sure Leon can verify it.

import leon.lang._
import leon.annotation._
 
object ListWithSize {
    sealed abstract class List[T] {
      def size: BigInt = {
        this match {
          case Cons(h, t) => 1 + t.size
          case Nil() => 0
        }
      } // TODO: Add appropriate post-condition
 
      def sizeTailRec: BigInt = sizeTailRec0(0)
 
      def sizeTailRec0(acc: BigInt): BigInt = {
        require(acc >= 0)
        this match {
          case Cons(h, t) => t.sizeTailRec0(acc + 1)
          case Nil() => acc
        }
      }  // TODO: Add appropriate post-condition
 
      // Verify
      def zip[U](that: List[U]): List[(T, U)] = {
        // TODO: Add appropriate pre-condition
        this match {
          case Nil() => Nil()
          case Cons(h1, t1) => that match {
            case Cons(h2, t2) => Cons((h1, h2), t1.zip(t2))
          }
        }
      } ensuring(_.size == this.size)
 
 
      def content: Set[T] = this match {
        case Nil() => Set()
        case Cons(h, t) => Set(h) ++ t.content
      }
 
      // Verify
      def reverse: List[T] = {
        reverse0(Nil())
      } ensuring(_.content == this.content)
 
      def reverse0(acc: List[T]): List[T] = (this match {
        case Nil() => acc
        case Cons(h, t) => t.reverse0(Cons(h, acc))
      }) // TODO: Add appropriate post-condition
 
 
      def append(that: List[T]): List[T] = (this match {
        case Nil() => that
        case Cons(h, t) => Cons(h, t.append(that))
      }) ensuring(_.content == this.content ++ that.content)
 
 
    }
    case class Cons[T](head: T, tail: List[T]) extends List[T]
    case class Nil[T]() extends List[T]
 
 
    // Verify
    def sizesAreEquiv[T](l: List[T]): Boolean = {
      l.size == l.sizeTailRec
    }.holds
 
 
    def sizeAndContent[T](l: List[T]): Boolean = {
      l.size == 0 || l.content != Set[T]()
    }.holds
 
    def drunk[T](l: List[T]): List[T] = (l match {
      case Nil() => Nil()
      case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
    }) ensuring {
      res => true // TODO: find postcondition
    }
 
 
    def funnyCons[T](x: T, l: List[T]): List[T] = (l match {
        case Nil() => Cons(x, Nil())
        case c @ Cons(_,_) => Cons(x, c)
    }) ensuring(_.size > 0)
 
 
    @induct
    def nilAppend[T](l: List[T]): Boolean = {
      l.append(Nil()) == l
    }.holds
 
    @induct
    def appendAssoc[T](xs: List[T], ys: List[T], zs: List[T]) : Boolean = {
      false  // find predicate
    }.holds
 
    @induct
    def sizeAppend[T](l1: List[T], l2 : List[T]) : Boolean = {
      (l1.append(l2).size == l1.size + l2.size)
    }.holds
}

Add specifications so that sort verifies.

import leon.annotation._
import leon.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() => 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 leon.lang._
import leon.annotation._
 
object SearchList {
  sealed abstract class List[T] {
    def size: BigInt = {
      this match {
        case Nil() => 0
        case Cons(h, t) => 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() => -1
        case Cons(h, t) if h == v => 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()
        case Cons(h, t) if n == 0 => Nil()
        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 = { 
    !((l.contains(v)) && (l.take(l.firstPosOf(v)).contains(v))) // What is this function checking? Translate to english. Can you remove the l.contains(v) part? Why?
  }.holds
}