Merge branch 'main' into sam/regexZippers

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala

@@ -232,6 +232,11 @@ object MutableHashMap {
 
     }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map)))
 
+    def repack(): Boolean = {
+      require(valid)
+      this.underlying.v.repack()
+    }.ensuring (res => res == false || map == old(this).map)
+
     @ghost
     override  def valid: Boolean = underlying.v.valid &&
       underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)) &&

data-structures/uarray/UArrayExample.scala

@@ -88,20 +88,16 @@ object UArrayExample:
   end UArray
 
   object UArray:
-    @extern @ignore // used because `new Array[T]` leaks out of @extern due to some compiler magic
-    def _ofSize[T: ClassTag](size: Int): UArray[T] = {
+    @extern
+    def ofSize[T: ClassTag](size: Int): UArray[T] = {
+      require(0 <= size)
       @ghost val definedNot = Array.fill(size)(false)
       given ct: realClassTag[T] = summon[ClassTag[T]].real
       val content = new Array[T](size)
       UArray[T](content, size, definedNot)
-    }
-
-    @extern
-    def ofSize[T: ClassTag](size: Int): UArray[T] = {
-      require(0 <= size)
-      _ofSize[T](size)
     }.ensuring(res => res.size == size)
 
+
   end UArray
 
   def arr3[T: ClassTag](mk: Int => T): Array[T] =

tctests.txt

@@ -24,6 +24,7 @@ lexers/regex/verifiedlexer
 software-foundations
 system-f
 tutorials/add-digits
+tutorials/binary-search
 tutorials/const-fold
 tutorials/dispenser
 tutorials/krakow2020/working

tutorials/binary-search/search-question.txt

@@ -0,0 +1,79 @@
+import stainless.lang.*
+object Find {
+
+  // 0. Download stainless release from
+  //     https://github.com/epfl-lara/stainless/releases/tag/v0.9.9.0
+
+  // 1. Recall the example find from the lecture that does linear search:
+
+  // abbreviation expanded by the compiler
+  inline def interval(a: Array[Int], lo: Int, hi: Int): Boolean = 
+    0 <= lo && lo <= hi && hi <= a.size
+
+  def existsIn(a: Array[Int], lo: Int, hi: Int, x: Int): Boolean = 
+    require(interval(a, lo, hi))
+    decreases(hi - lo)
+    !(lo == hi) &&
+    ((a(hi - 1) == x) || existsIn(a, lo, hi - 1, x))
+
+  def find(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi))
+    var i = lo
+    (while i < hi && a(i) != x do    
+      decreases(hi - i)
+      i = i + 1
+    ).invariant(lo <= i && i <= hi && !existsIn(a, lo, i, x))
+    if i < hi then i
+    else -1
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    (res == -1 && !existsIn(a, lo, hi, x)))
+
+  // 2. Consider binary search algorithm to whom you should give sorted array.
+  // Let us for now assume we are happy with require and ensuring as is.
+  // The body of search1 has multiple errors. Fix them so that stainless verifies it.
+
+  def search1(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi))
+    if lo < hi then
+      val i = (lo + hi) / 2
+      val seeing = a(i)
+      if x == seeing then i
+      else if x < seeing then search1(a, lo, i, x)
+      else search1(a, i, hi, x)
+    else 
+      -1
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    (res == -1)
+  )
+
+  // 3. Once fixed, convert search1 to use a while loop, specifying the body (???), 
+  // the decreases and the invariant, so that new function verifies with the given
+  // require and ensuring. Compare your specification to one for search1.
+
+  def search2(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi))
+    var lo0 = lo
+    var hi0 = hi
+    var res = -1
+    (while res == -1 && lo0 < hi0 do
+      (??? : Unit)
+    ).invariant(true)
+    res
+    if res == -1 then
+      assert(lo0 == hi0)
+    else
+      assert(a(res) == x)
+    res
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    (res == -1)
+  )
+
+  // 4. (Open Ended). Suppose we wish to extend the ensuring of search1 with
+  // the specification (res == -1 && !existsIn(a, lo, hi, x))) as for find.
+  // How would you need to modify require?
+  // Do you expect that you would need any lemmas?  
+
+}

tutorials/binary-search/search.scala

@@ -0,0 +1,150 @@
+/*
+    Verify this file using --solvers=smt-cvc5 v 1.0.8 or similar.
+ */
+
+import stainless.lang.*
+object Find {
+  // abbreviation expanded by the compiler
+  inline def interval(a: Array[Int], lo: Int, hi: Int): Boolean = 
+    0 <= lo && lo <= hi && hi <= a.size
+
+  def existsIn(a: Array[Int], lo: Int, hi: Int, x: Int): Boolean = 
+    require(interval(a, lo, hi))
+    decreases(hi - lo)
+    !(lo == hi) &&
+    ((a(hi - 1) == x) || existsIn(a, lo, hi - 1, x))
+
+  def existsInCombinedInterval(a: Array[Int], lo: Int, mid: Int, hi: Int, x: Int): Unit = {
+    require(interval(a, lo, mid) && interval(a, mid, hi))
+    decreases(hi - mid)
+    if mid < hi then
+      existsInCombinedInterval(a, lo, mid, hi - 1, x)
+  }.ensuring(res => 
+    (existsIn(a, lo, hi, x) == (existsIn(a, lo, mid, x) || existsIn(a, mid, hi, x))))
+
+  def find(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi))
+    var i = lo
+    (while i < hi && a(i) != x do    
+      decreases(hi - i)
+      i = i + 1
+    ).invariant(lo <= i && i <= hi && !existsIn(a, lo, i, x))
+    if i < hi then i
+    else -1
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    (res == -1 && !existsIn(a, lo, hi, x)))
+
+  // 2. fixed code that verifies:
+
+  def search1(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi))
+    decreases(hi - lo)
+    if lo < hi then
+      val i = lo + (hi - lo) / 2
+      val seeing = a(i)
+      if x == seeing then i
+      else if x < seeing then search1(a, lo, i, x)
+      else search1(a, i+1, hi, x)
+    else 
+      -1
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    (res == -1)
+  )
+
+  // 3. version using a while loop
+
+  def search2(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi))
+    var lo0 = lo
+    var hi0 = hi
+    var res = -1
+    (while res == -1 && lo0 < hi0 do
+      decreases(hi0 - lo0)
+      val i = lo0 + (hi0 - lo0) / 2
+      val seeing = a(i)
+      if x == seeing then 
+        res = i
+      else if x < seeing then 
+        hi0 = i
+      else 
+        lo0 = i+1
+    ).invariant(lo <= lo0 && lo0 <= hi0 && hi0 <= hi &&
+                ((lo <= res && res < hi && a(res) == x) || res == -1))
+    if res == -1 then
+      assert(lo0 == hi0)
+    else
+      assert(a(res) == x)
+    res
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    (res == -1))  
+
+  // 4. proving absence when element is not found, assuming the array is sorted
+
+  def isSorted(a: Array[Int], lo: Int, hi: Int): Boolean =
+    require(interval(a, lo, hi))
+    decreases(hi - lo)
+    (lo == hi) || (lo + 1 == hi) ||
+    (a(lo) <= a(lo + 1) && isSorted(a, lo + 1, hi))
+
+  def isSortedAt(a: Array[Int], lo: Int, hi: Int, i: Int): Unit = {
+    require(interval(a, lo, hi) && lo <= i && i < hi && i + 1 < hi && isSorted(a, lo, hi))
+    decreases(i - lo)
+    if lo < i then
+      isSortedAt(a, lo + 1, hi, i)
+  }.ensuring(a(i) <= a(i+1))
+
+
+  def isSortedSubinterval(a: Array[Int], lo: Int, lo1: Int, hi1: Int, hi: Int): Unit = {
+    require(interval(a, lo, hi) && isSorted(a, lo, hi) && interval(a, lo1, hi1) && lo <= lo1 && hi1 <= hi)
+    decreases(hi1 - lo1)
+    if lo1 < hi1 then
+      isSortedSubinterval(a, lo, lo1 + 1, hi1, hi)
+      if lo1 < hi && lo1 + 1 < hi then
+        isSortedAt(a, lo, hi, lo1)
+  }.ensuring(isSorted(a, lo1, hi1))
+
+  def lessWhenSorted(a: Array[Int], lo: Int, i: Int, hi: Int, x: Int): Unit = {
+    require(interval(a, lo, hi) && isSorted(a, lo, hi) && lo <= i && i < hi && x < a(i))
+    decreases(hi - i)
+    if i + 1 < hi then
+      isSortedAt(a, lo, hi, i)
+      lessWhenSorted(a, lo, i + 1, hi, x)
+      existsInCombinedInterval(a, i, i + 1, hi, x)
+  }.ensuring(!existsIn(a, i, hi, x))
+
+  def moreWhenSorted(a: Array[Int], lo: Int, i: Int, hi: Int, x: Int): Unit = {
+    require(interval(a, lo, hi) && isSorted(a, lo, hi) && lo <= i && i < hi && a(i) < x)
+    decreases(i - lo)
+    if lo < i then
+      isSortedAt(a, lo, hi, i - 1)
+      moreWhenSorted(a, lo, i - 1, hi, x)
+      existsInCombinedInterval(a, i - 1, i, hi, x)
+  }.ensuring(!existsIn(a, lo, i + 1, x))
+
+  def search4(a: Array[Int], lo: Int, hi: Int, x: Int): Int = {
+    require(interval(a, lo, hi) && isSorted(a, lo, hi))
+    decreases(hi-lo)
+    if lo < hi then
+      val i = lo + (hi - lo) / 2
+      assert(i <= hi)
+      val seeing = a(i)
+      if x == seeing then i
+      else if x < seeing then 
+        isSortedSubinterval(a, lo, lo, i, hi)
+        lessWhenSorted(a, lo, i, hi, x)
+        existsInCombinedInterval(a, lo, i, hi, x)
+        search4(a, lo, i, x)
+      else 
+        isSortedSubinterval(a, lo, i + 1, hi, hi)
+        moreWhenSorted(a, lo, i, hi, x)
+        existsInCombinedInterval(a, lo, i + 1, hi, x)
+        search4(a, i+1, hi, x)
+    else
+      -1
+  }.ensuring(res =>
+    (lo <= res && res < hi && a(res) == x) ||
+    ((res == -1) && !existsIn(a, lo, hi, x)))
+}

tutorials/binary-search/stainless.conf

@@ -0,0 +1,7 @@
+vc-cache = false
+timeout = 10
+fail-early = true
+strict-arithmetic = false
+solvers="smt-cvc5"
+no-colors=true
+