Add more specs to List functions using bitvector indexing (#1541)

epfl-lara · Jul 22, 2024 · a38d80a · a38d80a
1 parent 1fcab3f
commit a38d80a
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 3 deletions.
diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala
@@ -67,6 +67,7 @@ sealed abstract class List[T] {
   @isabelle.fullBody
   def apply(index: BigInt): T = {
     require(0 <= index && index < size)
+    decreases(index)
     if (index == BigInt(0)) {
       head
     } else {
@@ -76,6 +77,7 @@ sealed abstract class List[T] {
 
   def iapply(index: Int): T = {
     require(0 <= index && index < isize)
+    decreases(index)
     if (index == 0) {
       head
     } else {
@@ -92,15 +94,15 @@ sealed abstract class List[T] {
       case Nil() => Cons(t, this)
       case Cons(x, xs) => Cons(x, xs :+ (t))
     }
-  } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)) && res == this ++ Cons(t, Nil[T]()))
+  } ensuring(res => (res.size == size + 1) && (if (isize < Int.MaxValue) res.isize == isize + 1 else res.isize == isize) && (res.content == content ++ Set(t)) && res == this ++ Cons(t, Nil[T]()))
 
   @isabelle.function(term = "List.rev")
   def reverse: List[T] = {
     this match {
       case Nil() => this
       case Cons(x,xs) => xs.reverse :+ x
     }
-  } ensuring (res => (res.size == size) && (res.content == content))
+  } ensuring (res => (res.size == size) && (res.isize == isize) && (res.content == content))
 
   def take(i: BigInt): List[T] = { (this, i) match {
     case (Nil(), _) => Nil[T]()
@@ -412,7 +414,7 @@ sealed abstract class List[T] {
       case Cons(x, tail) =>
         Cons[T](x, tail.iupdated(i - 1, y))
     }
-  }
+  }.ensuring(res => res.isize == this.isize && res.iapply(i) == y)
 
   private def insertAtImpl(pos: BigInt, l: List[T]): List[T] = {
     require(0 <= pos && pos <= size)
@@ -672,11 +674,20 @@ object List {
 
   @library
   def fill[T](n: BigInt)(x: T) : List[T] = {
+    decreases(if (n <= BigInt(0)) BigInt(0) else n)
     if (n <= 0) Nil[T]()
     else Cons[T](x, fill[T](n-1)(x))
   } ensuring(res => (res.content == (if (n <= BigInt(0)) Set.empty[T] else Set(x))) &&
                     res.size == (if (n <= BigInt(0)) BigInt(0) else n))
 
+  @library
+  def ifill[T](n: Int)(x: T) : List[T] = {
+    decreases(if (n <= 0) 0 else n)
+    if (n <= 0) Nil[T]()
+    else Cons[T](x, ifill[T](n - 1)(x))
+  } ensuring(res => (res.content == (if (n <= 0) Set.empty[T] else Set(x))) &&
+                    res.isize == (if (n <= 0) 0 else n))
+
   /* Range from start (inclusive) to until (exclusive) */
   @library
   def range(start: BigInt, until: BigInt): List[BigInt] = {

diff --git a/frontends/library/stainless/collection/ListSpecs.scala b/frontends/library/stainless/collection/ListSpecs.scala
@@ -21,6 +21,17 @@ object ListSpecs {
     ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
   }.holds
 
+  def isnocIndex[T](l: List[T], t: T, i: Int): Boolean = {
+    require(l.isize < Int.MaxValue)
+    require(0 <= i && i < l.isize + 1)
+    decreases(l)
+    l match {
+      case Nil() => true
+      case Cons(x, xs) => if (i > 0) isnocIndex[T](xs, t, i - 1) else true
+    }
+    ((l :+ t).iapply(i) == (if (i < l.isize) l.iapply(i) else t))
+  }.holds
+
   @isabelle.lemma(about = "stainless.collection.List.apply")
   def consIndex[T](h: T, t: List[T], i: BigInt): Boolean = {
     require(0 <= i && i < t.size + 1)