Expand some collection methods and fix algebra package hierarchy (#1418)

frontends/algebra/src/main/stainless/algebra/Ring.scala → frontends/algebra/stainless/algebra/Ring.scala

@@ -29,13 +29,13 @@ object Ring {
   import Monoid._
 
   /* FIXME TypeChecker reports an error on this example, because of type encoding:
-		[info] [ Fatal  ] Type checking failed with message:
-		[info] [ Fatal  ] An ADT (Object$0), and a function (is$anon$7) cannot be mutually recursive
-		[info] [ Fatal  ] Run has failed with error: inox.package$FatalError: Type checking failed with message:
-		[info] [ Fatal  ] An ADT (Object$0), and a function (is$anon$7) cannot be mutually recursive
-	*/
+    [info] [ Fatal  ] Type checking failed with message:
+    [info] [ Fatal  ] An ADT (Object$0), and a function (is$anon$7) cannot be mutually recursive
+    [info] [ Fatal  ] Run has failed with error: inox.package$FatalError: Type checking failed with message:
+    [info] [ Fatal  ] An ADT (Object$0), and a function (is$anon$7) cannot be mutually recursive
+  */
 
-	def ringBigInt: Ring[BigInt] = new Ring[BigInt] {
+  def ringBigInt: Ring[BigInt] = new Ring[BigInt] {
     def addition: AbelianGroup[BigInt] = additionAbelianGroup
 
     def multiplication: Monoid[BigInt] = new Monoid[BigInt] {

frontends/algebra/src/main/stainless/algebra/proofs/List.scala → frontends/algebra/stainless/algebra/proofs/List.scala

@@ -44,7 +44,7 @@ object List {
           assert(M.combine(M.combine(y1, y2), ys.foldRight(M.identity)(M.combine)) == M.combine(y1, M.combine(y2, ys.foldRight(M.identity)(M.combine))))
           assert(M.combine(y1, M.combine(y2, ys.foldRight(M.identity)(M.combine))) == M.combine(y1, (y2 :: ys).foldRight(M.identity)(M.combine)))
           assert(M.combine(y1, (y2 :: ys).foldRight(M.identity)(M.combine)) == (y1 :: y2 :: ys).foldRight(M.identity)(M.combine))
-          check((y1 :: y2 :: ys).foldLeft(M.identity)(M.combine) == (y1 :: y2 :: ys).foldRight(M.identity)(M.combine))
+          (y1 :: y2 :: ys).foldLeft(M.identity)(M.combine) == (y1 :: y2 :: ys).foldRight(M.identity)(M.combine)
       }
     }
   }.holds

frontends/benchmarks/verification/valid/CovCollection.scala

@@ -4,10 +4,10 @@ import ListOps._
 
 object CovCollection {
   def zipWith[A,B,C](f: (A,B) => C)(l1: List[A], l2: List[B]): List[C] = {
-    require(l1.length == l2.length)
+    require(l1.blength == l2.blength)
     (l1, l2) match {
       case (Nil, Nil) => Nil
-      case (a ::as, b ::bs) => f(a,b) :: zipWith(f)(as, bs)
+      case (a :: as, b :: bs) => f(a,b) :: zipWith(f)(as, bs)
     }
   }
 

frontends/common/src/it/scala/stainless/LibrarySuite.scala

@@ -47,16 +47,19 @@ abstract class AbstractLibrarySuite(opts: Seq[inox.OptionValue[_]]) extends AnyF
       val funs = exProgram.symbols.functions.values.filter(keep(exProgram.trees)).map(_.id).toSeq
       val analysis = Await.result(run.execute(funs, exProgram.symbols, ExtractionSummary.NoSummary), Duration.Inf)
       val report = analysis.toReport
+      val invalids = analysis.vrs.filter(_._2.isInvalid)
+      val inconcls = analysis.vrs.filter(_._2.isInconclusive)
       assert(report.totalConditions == report.totalValid,
         "Only " + report.totalValid + " valid out of " + report.totalConditions + "\n" +
-        "Invalids are:\n" + analysis.vrs.filter(_._2.isInvalid).mkString("\n") + "\n" +
-        "Unknowns are:\n" + analysis.vrs.filter(_._2.isInconclusive).mkString("\n"))
+        "Invalids are:\n" + invalids.map(_._1.condition.getPos).mkString("\n") + "\n" +
+        "Unknowns are:\n" + inconcls.map(_._1.condition.getPos).mkString("\n"))
     }
   }
 }
 
 class LibrarySuite extends AbstractLibrarySuite(Seq(
   termination.optInferMeasures(true),
   termination.optCheckMeasures(YesNoOnly.Yes),
+  inox.optTimeout(30.seconds),
 ))
 

frontends/library/stainless/collection/List.scala

@@ -404,7 +404,7 @@ sealed abstract class List[T] {
       case Cons(x, tail) =>
         Cons[T](x, tail.updated(i - 1, y))
     }
-  }
+  }.ensuring(res => res.size == this.size && res(i) == y)
 
   def iupdated(i: Int, y: T): List[T] = {
     require(0 <= i && i < isize)
@@ -700,6 +700,24 @@ object List {
       case Cons(a, b) => f(a) + rec(b)
     }
   }
+
+  @library
+  implicit class ListBigIntOps(l: List[BigInt]) {
+    def sum: BigInt = ListOps.sum(l)
+    def sorted: List[BigInt] = ListOps.sorted(l)
+    def isSorted: Boolean = ListOps.isSorted(l)
+  }
+
+  @library
+  implicit class FlattenableList[A](l: List[List[A]]) {
+    def flatten: List[A] = ListOps.flatten(l)
+  }
+
+  @library
+  implicit class ToMapOps[K, V](l: List[(K, V)]) {
+    def toMap: Map[K, V] = ListOps.toMap(l)
+    def toListMap: ListMap[K, V] = ListOps.toListMap(l)
+  }
 }
 
 @library
@@ -720,7 +738,7 @@ object ListOps {
   def sorted(ls: List[BigInt]): List[BigInt] = { ls match {
     case Cons(h, t) => sortedIns(sorted(t), h)
     case Nil() => Nil[BigInt]()
-  }} ensuring { isSorted _ }
+  }} ensuring(isSorted)
 
   private def sortedIns(ls: List[BigInt], v: BigInt): List[BigInt] = {
     require(isSorted(ls))
@@ -741,6 +759,10 @@ object ListOps {
     case (current, (k, v)) => current ++ Map(k -> v)
   }
 
+  def toListMap[K, V](l: List[(K, V)]): ListMap[K, V] = l.foldLeft(ListMap.empty[K, V]) {
+    case (current, (k, v)) => current + (k -> v)
+  }
+
   @tailrec
   def noDuplicate[T](l: List[T]): Boolean = l match {
     case Nil() => true

frontends/library/stainless/collection/ListMap.scala

@@ -14,6 +14,8 @@ case class ListMap[A, B](toList: List[(A, B)]) {
 
   def isEmpty: Boolean = toList.isEmpty
 
+  def nonEmpty: Boolean = !isEmpty
+
   def head: (A, B) = {
     require(!isEmpty)
     toList.head
@@ -49,7 +51,7 @@ case class ListMap[A, B](toList: List[(A, B)]) {
     assert(ListSpecs.noDuplicate(toList.filter(_._1 != keyValue._1).map(_._1)))
 
     ListMap(keyValue :: toList.filter(_._1 != keyValue._1))
-  }
+  }.ensuring(res => res.contains(keyValue._1) && res(keyValue._1) == keyValue._2)
 
   def ++(keyValues: List[(A, B)]): ListMap[A, B] = {
     decreases(keyValues)
@@ -76,6 +78,30 @@ case class ListMap[A, B](toList: List[(A, B)]) {
   def forall(p: ((A, B)) => Boolean): Boolean = {
     toList.forall(p)
   }
+
+  def updated(a: A, b: B): ListMap[A, B] = this + (a -> b)
+
+  def values: List[B] = toList.map(_._2)
+
+  def keys: List[A] = toList.map(_._1)
+
+  def map[A2, B2](f: ((A, B)) => (A2, B2)): ListMap[A2, B2] = {
+    def rec(curr: List[(A, B)], acc: ListMap[A2, B2]): ListMap[A2, B2] = curr match {
+      case Nil() => acc
+      case Cons(h, tl) => rec(tl, acc + f(h))
+    }
+    rec(toList, ListMap.empty)
+  }
+
+  def filter(p: ((A, B)) => Boolean): ListMap[A, B] = {
+    ListSpecs.filterSubseq(toList, p)
+    ListMapLemmas.noDuplicatePairs(this)
+    ListSpecs.noDuplicateSubseq(toList.filter(p), toList)
+    ListMapLemmas.noDuplicateKeysSubseq(toList.filter(p), toList)
+    ListMap(toList.filter(p))
+  }
+
+  def size: BigInt = toList.size
 }
 
 @library
@@ -87,6 +113,38 @@ object ListMap {
 object ListMapLemmas {
   import ListSpecs._
 
+  @opaque
+  def noDuplicatePairs[A, B](lm: ListMap[A, B]): Unit = {
+    lm.toList match {
+      case Nil() => ()
+      case Cons(x, xs) =>
+        noDuplicatePairs(ListMap(xs))
+        tailDoesNotContainPair(lm)
+    }
+  }.ensuring(ListOps.noDuplicate(lm.toList))
+
+  @opaque
+  def noDuplicateKeysSubseq[A, B](l1: List[(A, B)], l2: List[(A, B)]): Unit = {
+    require(ListOps.noDuplicate(l2.map(_._1)))
+    require(ListSpecs.subseq(l1, l2))
+    decreases(l2.size)
+    ((l1, l2): @unchecked) match {
+      case (Nil(), _) => ()
+      case (x :: xs, y :: ys) =>
+        if (x == y && ListSpecs.subseq(xs, ys)) {
+          noDuplicateKeysSubseq(xs, ys)
+          assert(ListOps.noDuplicate(xs.map(_._1)))
+          assert(!ys.map(_._1).contains(y._1))
+          subseqKeys(xs, ys)
+          ListSpecs.subseqNotContains(xs.map(_._1), ys.map(_._1), x._1)
+          assert(!xs.map(_._1).contains(x._1))
+        } else {
+          assert(ListSpecs.subseq(l1, ys))
+          noDuplicateKeysSubseq(l1, ys)
+        }
+    }
+  }.ensuring(ListOps.noDuplicate(l1.map(_._1)))
+
   @opaque
   def addValidProp[A, B](lm: ListMap[A, B], p: ((A, B)) => Boolean, a: A, b: B): Unit = {
     require(lm.forall(p) && p(a, b))
@@ -303,4 +361,57 @@ object ListMapLemmas {
   }.ensuring(_ =>
     lm.keysOf(value).forall(key => lm.get(key) == Some[B](value))
   )
+
+  @opaque
+  def containsByKeyEquiv[A, B](lm: ListMap[A, B], a: A): Unit = {
+    lm.toList match {
+      case Nil() => ()
+      case Cons((x, _), xs) if x == a => ()
+      case Cons(x, xs) =>
+        containsByKeyEquiv(ListMap(xs), a)
+    }
+  }.ensuring(lm.contains(a) == lm.toList.map(_._1).contains(a))
+
+  @opaque
+  def tailDoesNotContainKey[A, B](lm: ListMap[A, B]): Unit = {
+    require(lm.nonEmpty)
+    decreases(lm.size)
+    val Cons(x, xs) = lm.toList: @unchecked
+    containsByKeyEquiv(ListMap(xs), x._1)
+  }.ensuring(!lm.tail.contains(lm.head._1))
+
+  @opaque
+  def tailDoesNotContainPair[A, B](lm: ListMap[A, B]): Unit = {
+    require(lm.nonEmpty)
+    decreases(lm.size)
+
+    def rec(x: (A, B), @induct xs: List[(A, B)]): Unit = {
+      require(ListOps.noDuplicate(xs.map(_._1)))
+      require(!ListMap(xs).contains(x._1))
+    }.ensuring(!xs.contains(x))
+
+    (lm.toList: @unchecked) match {
+      case Cons(x, xs) =>
+        tailDoesNotContainKey(lm)
+        rec(x, xs)
+    }
+  }.ensuring(!lm.toList.tail.contains(lm.toList.head))
+
+  @opaque
+  def subseqKeys[A, B](l1: List[(A, B)], l2: List[(A, B)]): Unit = {
+    require(ListOps.noDuplicate(l1.map(_._1)))
+    require(ListOps.noDuplicate(l2.map(_._1)))
+    require(ListSpecs.subseq(l1, l2))
+    decreases(l2.size)
+    ((l1, l2): @unchecked) match {
+      case (Nil(), _) => ()
+      case (x :: xs, y :: ys) =>
+        if (x == y && ListSpecs.subseq(xs, ys)) {
+          subseqKeys(xs, ys)
+        } else {
+          assert(ListSpecs.subseq(l1, ys))
+          subseqKeys(l1, ys)
+        }
+    }
+  }.ensuring(ListSpecs.subseq(l1.map(_._1), l2.map(_._1)))
 }