Adding Zippers implementation and verification, and some benchmarks

.github/workflows/bolts-CI.yml

@@ -24,6 +24,8 @@ jobs:
         temp-dir: "/tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}"
     - name: Bolts admit VCs tests
       run: ./run-tests.sh --admit-vcs
+    - name: Clean up
+      run: rm -rf $JAVA_OPTS_TMP_DIR
   fail_if_pull_request_is_draft:
     if: github.event.pull_request.draft == true
     runs-on: [self-hosted, linux]

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

@@ -9,7 +9,6 @@ import stainless.equations._
 import stainless.lang._
 import stainless.proof.check
 import scala.annotation.tailrec
-import scala.collection.immutable
 
 // Uncomment the following import to run benchmarks
 // import OptimisedChecks.*

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

@@ -9,9 +9,7 @@ import stainless.equations._
 import stainless.lang._
 import stainless.proof.check
 import scala.annotation.tailrec
-import scala.collection.immutable
 import stainless.collection.ListOps.noDuplicate
-import scala.collection.mutable
 
 // Uncomment the following import to run benchmarks
 // import OptimisedChecks.*
@@ -406,7 +404,7 @@ object TupleListOpsGenK {
       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 = {
@@ -459,28 +457,6 @@ object TupleListOpsGenK {
       }
     }.ensuring(_ => l.map(_._1).contains(p._1))
 
-  @opaque
-  @inlineOnce
-  def lemmainsertNoDuplicatedKeysPreservesForall[K, B](
-      l: List[(K, B)],
-      key: K,
-      value: B,
-      p: ((K, B)) => Boolean
-  ): Unit = {
-    require(invariantList(l))
-    require(l.forall(p))
-    require(p((key, value)))
-    decreases(l)
-
-    l match {
-      case Cons(head, tl) if (head._1 != key) =>
-        lemmainsertNoDuplicatedKeysPreservesForall(tl, key, value, p)
-      case _ => ()
-    }
-
-  }.ensuring(_ => insertNoDuplicatedKeys(l, key, value).forall(p))
-
-
   @opaque 
   @inlineOnce
   def lemmaForallSubset[K, B](

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

@@ -4,7 +4,7 @@
 package ch.epfl.map
 
 object OptimisedChecks {
-  extension [T](inline value: T) inline def.ensuring(condition: T => Boolean): T = value
+  extension [T](inline value: T) inline def ensuring(condition: T => Boolean): T = value
   inline def require(inline condition: Boolean): Unit = ()
   inline def assert(inline condition: Boolean): Unit = ()
 }