From 3fadc8188a783fa8276cde322b3aa11f980b8060 Mon Sep 17 00:00:00 2001 From: Matt Bovel Date: Mon, 16 Dec 2024 11:28:21 +0100 Subject: [PATCH 1/3] Revert "Hide ofSize even more from scala3 when using tasty" (#119) This reverts commit 3138763f33435bd6747a67e5a30010ff7f89a04e. Co-authored-by: Samuel Chassot <14821693+samuelchassot@users.noreply.github.com> --- data-structures/uarray/UArrayExample.scala | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/data-structures/uarray/UArrayExample.scala b/data-structures/uarray/UArrayExample.scala index 82709a41..27ea4322 100644 --- a/data-structures/uarray/UArrayExample.scala +++ b/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] = From 156890f267643a53812a3ca096e6ee6f89d8fc23 Mon Sep 17 00:00:00 2001 From: Samuel Chassot <14821693+samuelchassot@users.noreply.github.com> Date: Mon, 16 Dec 2024 14:30:13 +0100 Subject: [PATCH 2/3] Add repack to hashmap (#117) * add repack on hashmap * ci update --- .../src/main/scala/ch/epfl/map/MutableHashMap.scala | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala index 4ec56b9c..98f178f0 100644 --- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala +++ b/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)) && From 13a8ad77cb037d885672982ea4038d2d81a8df81 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Viktor=20Kun=C4=8Dak?= Date: Wed, 18 Dec 2024 23:13:18 +0100 Subject: [PATCH 3/3] binary search in sorted array example used in 2nd year course lecture (#121) * binary search * add tutorials/binary-search that seems to need cvc5 --- tctests.txt | 1 + tutorials/binary-search/search-question.txt | 79 +++++++++++ tutorials/binary-search/search.scala | 150 ++++++++++++++++++++ tutorials/binary-search/stainless.conf | 7 + 4 files changed, 237 insertions(+) create mode 100644 tutorials/binary-search/search-question.txt create mode 100644 tutorials/binary-search/search.scala create mode 100644 tutorials/binary-search/stainless.conf diff --git a/tctests.txt b/tctests.txt index 62668e31..63fb9757 100644 --- a/tctests.txt +++ b/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 diff --git a/tutorials/binary-search/search-question.txt b/tutorials/binary-search/search-question.txt new file mode 100644 index 00000000..f7e115f0 --- /dev/null +++ b/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? + +} diff --git a/tutorials/binary-search/search.scala b/tutorials/binary-search/search.scala new file mode 100644 index 00000000..d3132135 --- /dev/null +++ b/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))) +} diff --git a/tutorials/binary-search/stainless.conf b/tutorials/binary-search/stainless.conf new file mode 100644 index 00000000..73db64d5 --- /dev/null +++ b/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 +