Add a verified HashSet implementation + refactor package name of map …

…+ add script (#106)

* renaming of package in the maps

* add mutable sets project and start working on the implementation

* working on hashset

* add new lemmas about getKeysList to reuse in the set

* working on listmap to use it for hashset

* finished the Set

* add a few properties

* remove benchmark results

* restore deleted file

* change name package in lexers

* rename map package in caching functions

* finish renaming map package to map

* Add script that runs all verify.sh scripts

* scala version 3.5.0 for sbt projects

* fail if one fails

* config + remove useless file

* add main class + method to get an empty set

* filter hashset to not verify the maps

* make it compile with SBT and add a Main

* rename interfaces to avoid confusion with immutable structures

* remove benchmark result files

* add $1 at the end of verify.sh scripts to be able to pass --compact when running tests

* add a success message in run-tests so that we can export the log to PR as long as the CI is dead

* add unfold to make ConstFold verify

* message out of the loop

* typo in script

* add mutablesets in the tests nightly

* error in verify script for set + error in run-test scripts making all passing

* run all tests once

* run on laraquad2

* remove laraquad2 requirement

* with VCs admit back

* remove cache

WIP/Terverak/verify.sh

@@ -1,3 +1,3 @@
 #!/bin/bash
 
-stainless-dotty src/main/scala/terverak/**/*.scala "$@"
+stainless-dotty src/main/scala/terverak/**/*.scala "$@" $1

caching/CachedFunction.scala

@@ -1,4 +1,4 @@
-import ch.epfl.chassot.*
+import ch.epfl.map.*
 import stainless.lang.StaticChecks.*
 import stainless.annotation.*
 import stainless.lang.{ghost => ghostExpr, _}

caching/verify.sh

@@ -1,8 +1,9 @@
 stainless-dotty\
  CachedFunction.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableHashMap.scala \
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/iMutableMaps.scala\
- --config-file=stainless.conf --functions=CachedFunction._    
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala\
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala\
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala \
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala\
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/iMutableMaps.scala\
+ --config-file=stainless.conf --functions=CachedFunction._\
+  $1

data-structures/bitstream_esa/verify.sh

@@ -4,4 +4,5 @@ asn1jvm_Verification.scala  \
 asn1jvm_Helper.scala \
 asn1jvm_Bitstream.scala \
 --config-file=stainless.conf \
--D-parallel=5
+-D-parallel=5 \
+$1

data-structures/maps/mutablemaps/README.md

@@ -58,4 +58,4 @@ The SMT queries generated by Stainless during the verification of the `MutableLo
 
 To run the main class, run in `sbt`
 
-```$ runMain ch.epfl.chassot.Main```
+```$ runMain ch.epfl.map.Main```

data-structures/maps/mutablemaps/build.sbt

@@ -1,6 +1,6 @@
 name := "MutableMaps"
 version := "0.1.0-SNAPSHOT"
-scalaVersion :="3.3.3" 
+scalaVersion :="3.5.0" 
 
 run / fork := true
 

data-structures/maps/mutablemaps/generate_smt_queries.py

@@ -72,7 +72,7 @@ def main():
         shutil.rmtree("./smt-sessions")
     except OSError as e:
         print("Error: %s - %s." % (e.filename, e.strerror))
-    files = ["./src/main/scala/ch/epfl/chassot/ListLongMap.scala", "./src/main/scala/ch/epfl/chassot/MutableLongMap.scala"]
+    files = ["./src/main/scala/ch/epfl/map/ListLongMap.scala", "./src/main/scala/ch/epfl/map/MutableLongMap.scala"]
     res = verify(files)
     table = extract_table_from_res(res)
     today_date = time.strftime("%Y-%m-%d--%H-%M-%S")

data-structures/maps/mutablemaps/src/main/scala/benchmark/HashMapBenchmark.scala

@@ -5,15 +5,15 @@ import org.openjdk.jmh.annotations.*
 import scala.collection.mutable.LongMap
 import scala.collection.mutable.HashMap
 import scala.util.Random
-import ch.epfl.chassot.MutableLongMap
+import ch.epfl.map.MutableLongMap
 import stainless.collection.{List => StainlessList}
 import scala.collection.immutable
-import ch.epfl.chassot.EfficientFill
-import ch.epfl.chassot.MutableHashMap
-import ch.epfl.chassot.MutableLongMap
-import ch.epfl.chassot.Hashable
-import ch.epfl.chassot.ListMap
-import ch.epfl.chassot.Ordering
+import ch.epfl.map.EfficientFill
+import ch.epfl.map.MutableHashMap
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.Hashable
+import ch.epfl.map.ListMap
+import ch.epfl.map.Ordering
 
 
 @State(Scope.Benchmark)

data-structures/maps/mutablemaps/src/main/scala/benchmark/VerifiedMapBenchmark.scala

@@ -5,14 +5,14 @@ import org.openjdk.jmh.annotations.*
 import scala.collection.mutable.LongMap
 import scala.collection.mutable.HashMap
 import scala.util.Random
-import ch.epfl.chassot.MutableLongMap
-import ch.epfl.chassot.MutableLongMapOpti
-import ch.epfl.chassot.ListLongMap
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.MutableLongMapOpti
+import ch.epfl.map.ListLongMap
 import stainless.collection.{List => StainlessList}
 import scala.collection.immutable
-import ch.epfl.chassot.MutableLongMapOpti.LongMapOpti
+import ch.epfl.map.MutableLongMapOpti.LongMapOpti
 import benchmark.BenchmarkUtil.getHashMapEmptyBuffer
-import ch.epfl.chassot.EfficientFill
+import ch.epfl.map.EfficientFill
 
 @State(Scope.Benchmark)
 class ArrayFillBenchmark {

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/EfficientFill.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/EfficientFill.scala

@@ -1,7 +1,7 @@
 /** This file contains implementations of a "fill" function for Array, used as benchmark.
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import MutableLongMap.*
 

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap-onlyCode.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap-onlyCode.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot Contains only the code of the ListLongMap, without specification nor proof, for line counting purposes.
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -19,7 +19,9 @@ import scala.collection.mutable
 case class ListMap[K, B](toList: List[(K, B)]) {
   require(TupleListOpsGenK.invariantList(toList))
 
-  def isEmpty: Boolean = toList.isEmpty
+  def isEmpty: Boolean = {
+    toList.isEmpty
+  }.ensuring(res => toList.size >= Int.MaxValue || res == (size == 0))
 
   def eq(other: ListMap[K, B]): Boolean = toList.content == other.toList.content
 
@@ -48,10 +50,16 @@ case class ListMap[K, B](toList: List[(K, B)]) {
     val res = TupleListOpsGenK.containsKey(toList, key)
     if (res) {
       TupleListOpsGenK.lemmaContainsKeyImpliesGetValueByKeyDefined(toList, key)
+      TupleListOpsGenK.lemmaInListThenGetKeysListContains(toList, key)
+    } else {
+      if(this.keys().contains(key)){
+        TupleListOpsGenK.lemmaInGetKeysListThenContainsKey(toList, key)
+        check(false)
+      }
     }
     res
 
-  }.ensuring(res => !res || this.get(key).isDefined)
+  }.ensuring(res => (!res && !this.keys().contains(key)) || (this.get(key).isDefined && this.keys().contains(key)))
 
   @inline
   def get(key: K): Option[B] = {
@@ -65,7 +73,12 @@ case class ListMap[K, B](toList: List[(K, B)]) {
 
   def keys(): List[K] = {
     TupleListOpsGenK.getKeysList(toList)
-  }
+  }.ensuring(res => 
+    noDuplicate(res) 
+    && res.length == this.toList.length 
+    && res.forall(k => TupleListOpsGenK.containsKey(this.toList, k)) 
+    && res.content == this.toList.map(_._1).content
+    )
 
   def apply(key: K): B = {
     require(contains(key))
@@ -98,7 +111,9 @@ case class ListMap[K, B](toList: List[(K, B)]) {
   }
   def -(key: K): ListMap[K, B] = {
     ListMap(TupleListOpsGenK.removePresrvNoDuplicatedKeys(toList, key))
-  }.ensuring(res => !res.contains(key))
+  }.ensuring(res => 
+    !res.contains(key)
+    && this.keys().content - key == res.keys().content )
 
   def --(keys: List[K]): ListMap[K, B] = {
     decreases(keys)
@@ -141,7 +156,12 @@ object TupleListOpsGenK {
         Cons(head._1, getKeysList(tl))
       case Nil() => Nil[K]()
     }
-  }.ensuring(res => noDuplicate(res) && res.length == l.length && res.forall(k => containsKey(l, k)))
+  }.ensuring(res => 
+    noDuplicate(res) 
+    && res.length == l.length 
+    && res.forall(k => containsKey(l, k)) 
+    && res.content == l.map(_._1).content
+    )
 
   @pure
   def intSizeKeys[K](l: List[K]): Int = {
@@ -162,13 +182,13 @@ object TupleListOpsGenK {
         if (s1 < Integer.MAX_VALUE) {
           1 + s1
         } else {
-          0
+          Integer.MAX_VALUE
         }
       }
 
       case Nil() => 0
     }
-  }.ensuring(res => res >= 0)
+  }.ensuring(res => res >= 0 && (l.isEmpty == (res == 0)))
 
   def getKeysOf[K, B](l: List[(K, B)], value: B): List[K] = {
     require(invariantList(l))
@@ -349,6 +369,96 @@ object TupleListOpsGenK {
 
   // ----------- LEMMAS -----------------------------------------------------
 
+  /**
+   * Wow this one was generated by copilot, I just had to adjust the postcondition as it wrote it in the wrong
+   * direction.
+   * But Impressive!
+   **/
+  @opaque
+  @inlineOnce 
+  def lemmaRemoveFromListThenKeysSetRemove[K, B](l: List[(K, B)], key: K): Unit = {
+    require(invariantList(l))
+    decreases(l)
+    l match {
+      case Cons(head, tl) if (head._1 == key) => 
+        if(containsKey(l, key)){
+          val h = (key, getValueByKey(l, key).get)
+          assert(l.head == (key, getValueByKey(l, key).get))
+          if(tl.contains(h)){
+            lemmaContainsTupleThenContainsKey(tl, h._1, h._2)
+            check(false)
+          }
+          assert(!tl.contains(head))
+          check(tl.content == l.content - (key, getValueByKey(l, key).get))
+        } else {
+          check(tl.content == l.content)
+        }
+      case Cons(head, tl) if (head._1 != key) =>
+        lemmaRemoveFromListThenKeysSetRemove(tl, key)
+        if(getKeysList(tl).contains(head._1)){
+          lemmaInGetKeysListThenContainsKey(tl, head._1) 
+          check(false)
+        }
+        if(containsKey(removePresrvNoDuplicatedKeys(tl, key), head._1)){
+          lemmaInListThenGetKeysListContains(removePresrvNoDuplicatedKeys(tl, key), head._1)
+          check(false)
+        }
+      case Nil() => ()
+    }
+  }.ensuring(_ => getKeysList(l).content - key == getKeysList(removePresrvNoDuplicatedKeys(l, key)).content)
+
+  @opaque 
+  @inlineOnce
+  def lemmaEqMapSameKeysSet[K, B](lm1: ListMap[K, B], lm2: ListMap[K, B]): Unit = {
+    require(lm1.eq(lm2))
+    assert(lm1.toList.content == lm2.toList.content)
+    ListSpecs.subsetRefl(lm1.toList)
+    ListSpecs.subsetRefl(lm2.toList)
+    lemmaSubsetThenKeysSubset(lm1.toList, lm2.toList)
+    lemmaSubsetThenKeysSubset(lm2.toList, lm1.toList)
+    assert(lm1.keys().content.subsetOf(lm2.keys().content))
+    assert(lm2.keys().content.subsetOf(lm1.keys().content))
+  }.ensuring(_ => lm1.keys().content == lm2.keys().content)
+
+  @opaque
+  @inlineOnce
+  def lemmaSubsetThenKeysSubset[K, B](l1: List[(K, B)], l2: List[(K, B)]): Unit = {
+    require(invariantList(l1))
+    require(invariantList(l2))
+    require(l1.content.subsetOf(l2.content))
+    decreases(l1)
+    l1 match
+      case Cons(hd, tl) => 
+        lemmaSubsetThenKeysSubset(tl, l2)
+        assert(getKeysList(tl).content.subsetOf(getKeysList(l2).content))
+        assert(l2.contains(hd))
+        lemmaMapFirstElmtContains(l2, hd)
+        assert(l2.map(_._1).contains(hd._1))
+        assert(getKeysList(l2).contains(hd._1))
+        assert(!containsKey(tl, hd._1))
+        if(getKeysList(tl).contains(hd._1)){
+          lemmaInGetKeysListThenContainsKey(tl, hd._1)
+          check(false)
+        }
+        assert(!getKeysList(tl).contains(hd._1))
+      case Nil() => ()
+
+
+  }.ensuring(_ => getKeysList(l1).content.subsetOf(getKeysList(l2).content))
+
+  @opaque
+  @inlineOnce
+  def lemmaMapFirstElmtContains[K, B](l: List[(K, B)], p: (K, B)): Unit = {
+      require(invariantList(l))
+      require(l.contains(p))
+      decreases(l)
+      l match {
+        case Cons(head, tl) if (head != p) =>
+          lemmaMapFirstElmtContains(tl, p)
+        case _ => ()
+      }
+    }.ensuring(_ => l.map(_._1).contains(p._1))
+
   @opaque
   @inlineOnce
   def lemmainsertNoDuplicatedKeysPreservesForall[K, B](

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/Main.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/Main.scala

@@ -1,13 +1,13 @@
-package ch.epfl.chassot
+package ch.epfl.map
 
-import ch.epfl.chassot.MutableLongMap
-import ch.epfl.chassot.ListLongMap
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.ListLongMap
 import stainless.collection.List
 import benchmark.BenchmarkUtil.*
 import benchmark.Key
-import ch.epfl.chassot.MutableHashMap.*
-import ch.epfl.chassot.MutableLongMap.ValueCellFull
-import ch.epfl.chassot.MutableLongMap.EmptyCell
+import ch.epfl.map.MutableHashMap.*
+import ch.epfl.map.MutableLongMap.ValueCellFull
+import ch.epfl.map.MutableLongMap.EmptyCell
 import scala.collection.mutable.HashMap
 object Main {
   def main(args: Array[String]): Unit = {

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

@@ -1,6 +1,6 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection.{ListMap => ListMapStainless, ListMapLemmas => ListMapLemmasStainless, _}
@@ -15,7 +15,7 @@ import LongMapFixedSize.validMask
 import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
 // import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
 
-import MutableMapInterface.iMHashMap
+import MutableMapInterface.MutableMap
 
 trait Hashable[K] {
   @pure
@@ -41,7 +41,7 @@ object MutableHashMap {
       val hashF: Hashable[K],
       var _size: Int,
       val defaultValue: K => V
-  ) extends iMHashMap[K, V] {
+  ) extends MutableMap[K, V] {
 
     @pure
     override def defaultEntry: K => V = this.defaultValue

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala

@@ -1,6 +1,6 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -13,7 +13,7 @@ import stainless.lang.Cell
 import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
 // import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
 
-import MutableMapInterface.iMLongMap
+import MutableMapInterface.MutLongMap
 
 object MutableLongMap {
   import LongMapFixedSize.validMask
@@ -44,7 +44,7 @@ object MutableLongMap {
   @mutable
   final case class LongMap[V](
       val underlying: Cell[LongMapFixedSize[V]]
-  ) extends iMLongMap[V] {
+  ) extends MutLongMap[V] {
 
     @pure
     override def defaultEntry: Long => V = underlying.v.defaultEntry

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMapOpti.scala → data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMapOpti.scala

@@ -4,7 +4,7 @@
   *
   * It comes without proof or specification, and is used for benchmarking purposes.
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._