Add getKeys operation on HashMap

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

@@ -97,9 +97,10 @@ case class ListMap[K, B](toList: List[(K, B)]) {
     ListMap(newList)
 
   }.ensuring(res =>
-    res.contains(keyValue._1) && res.get(keyValue._1) == Some[B](
-      keyValue._2
-    ) && res.toList.contains(keyValue)
+    res.contains(keyValue._1)
+    && res.get(keyValue._1) == Some[B](keyValue._2) 
+    && res.toList.contains(keyValue) 
+    && res.keys().content == this.keys().content ++ Set(keyValue._1)
   )
 
   def ++(keyValues: List[(K, B)]): ListMap[K, B] = {
@@ -406,19 +407,6 @@ 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 = {
-    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
@@ -505,6 +493,30 @@ object TupleListOpsGenK {
       case Nil() => ()
     }
   }.ensuring(_ => l1.forall(p))
+
+  @opaque 
+  @inlineOnce
+  def lemmaForallSubsetKeys[K](
+      l1: List[K],
+      l2: List[K],
+      p: K => Boolean
+  ): Unit = {
+    require(l2.forall(p))
+    require(l1.content.subsetOf(l2.content))
+    decreases(l1)
+
+    l1 match {
+      case Cons(head, tl) =>
+        ListSpecs.subsetContains(l1, l2)
+        ListSpecs.forallContained(l1, l2.contains , head)
+        ListSpecs.forallContained(l2, p, head)
+        assert(l2.contains(head))
+        lemmaForallSubsetKeys(tl, l2, p)
+        assert(tl.forall(p))
+        assert(p(head))
+      case Nil() => ()
+    }
+  }.ensuring(_ => l1.forall(p))
 
   @opaque
   @inlineOnce
@@ -1501,6 +1513,19 @@ object ListMapLemmas {
   )
 
   // Equivalence LEMMAS ----------------------------------------------------------------------------------------------------------------
+  @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)
+    TupleListOpsGenK.lemmaSubsetThenKeysSubset(lm1.toList, lm2.toList)
+    TupleListOpsGenK.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 lemmaAddToEqMapsPreservesEq[K, B](

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

@@ -40,7 +40,8 @@ object MutableHashMap {
       val underlying: Cell[LongMap[List[(K, V)]]],
       val hashF: Hashable[K],
       var _size: Int,
-      val defaultValue: K => V
+      val defaultValue: K => V,
+      var keys: List[K] = Nil[K]()
   ) extends MutableMap[K, V] {
 
     @pure
@@ -123,6 +124,7 @@ object MutableHashMap {
       require(valid)
       @ghost val oldMap = map
       @ghost val oldLongListMap = underlying.v.map
+      @ghost val oldKeyList = keys
 
       val contained = contains(key)
       val res = if (contained) {
@@ -146,9 +148,28 @@ object MutableHashMap {
             check(underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)))
             check(allKeysSameHashInMap(underlying.v.map, hashF)) 
             check(map.eq(oldMap + (key, v)))
+
+            // this.map.keys().forall(k => keysList.contains(k))
+            ListMapLemmas.lemmaEqMapSameKeysSet(oldMap + (key, v), map)
+            assert(this.map.keys().content == oldMap.keys().content + key)
+            assert(oldMap.keys().content.contains(key))
+            assert(oldMap.keys().content + key == oldMap.keys().content)
+            assert(this.map.keys().content == oldMap.keys().content)
+            val keysList = this.keys
+            TupleListOpsGenK.lemmaForallSubsetKeys(this.map.keys(), oldMap.keys(), k => keysList.contains(k))
+            assert(this.map.keys().forall(k => keysList.contains(k)))
+            ListSpecs.forallContained(this.map.keys(), k => keysList.contains(k), key)
+
+            check(keys.contains(key))
+            check(valid)
           } else {
+            // this.map.keys().forall(k => keysList.contains(k))
+            val keysList = this.keys
+            ListSpecs.forallContained(this.map.keys(), k => keysList.contains(k), key)
+            check(keys.contains(key))
             check(valid)
             check(map == oldMap)
+            check(valid)
           }
         })
         if (res && !contained) then _size += 1
@@ -161,6 +182,10 @@ object MutableHashMap {
         val newBucket = Cons((key, v), currentBucket)
         val res = underlying.v.update(hash, newBucket)
 
+        if (res && !contained) then 
+          _size += 1
+          keys = Cons(key, keys)
+
         ghostExpr({
           if (res) {
             if (!currentBucket.isEmpty) {
@@ -176,13 +201,28 @@ object MutableHashMap {
             ListMapLemmas.lemmaEquivalentThenSameContains(map, oldMap + (key, v), key)
             check((oldMap + (key, v)).contains(key))
             check(map.contains(key))
+            check(keys.contains(key))
+            check(simpleValid)
+            val keysList = this.keys
+            ListMapLemmas.lemmaEqMapSameKeysSet(oldMap + (key, v), map)
+            assert(this.map.keys().content == oldMap.keys().content + key)
+            check(oldMap.keys().forall(k => oldKeyList.contains(k)))
+            ListSpecs.forallContainsSubset(oldMap.keys(), oldKeyList)
+            assert(oldMap.keys().content.subsetOf(oldKeyList.content))
+            assert(oldKeyList.content.subsetOf(keysList.content))
+            ListSpecs.subsetContains(oldMap.keys(), keysList)
+            check(oldMap.keys().forall(k => keysList.contains(k)))
+            assert(keysList.content == oldKeyList.content + key)
+            assert(this.map.keys().content.subsetOf(keysList.content))
+            ListSpecs.subsetContains(this.map.keys(), keysList)
+            check(this.map.keys().forall(k => keysList.contains(k)))
+            check(valid)
           } else {
             check(valid)
             check(map == oldMap)
           }
         })
 
-        if (res && !contained) then _size += 1
         res
       }
       res
@@ -218,10 +258,17 @@ object MutableHashMap {
             lemmaChangeOneBucketByAValidOnePreservesForallNoDuplicatesAndHash(oldLongListMap, hash, newBucket, hashF)
             check(underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)))
             check(allKeysSameHashInMap(underlying.v.map, hashF))
-            check(valid)
             check(oldMap.contains(key))
             lemmaChangeOneBucketToRemoveAKeyRemoveThisKeyInGenMap(oldLongListMap, hash, newBucket, key, hashF)
             check(map.eq(oldMap - key))
+            ListMapLemmas.lemmaEqMapSameKeysSet(oldMap - key, map)
+            assert(this.map.keys().content == oldMap.keys().content - key)
+            val keysList = this.keys
+            ListSpecs.forallContainsSubset(oldMap.keys(), keysList)
+            assert(this.map.keys().content.subsetOf(keysList.content))
+            ListSpecs.subsetContains(this.map.keys(), keysList)
+
+            check(valid)
           } else {
             check(valid)
             check(map == oldMap)
@@ -232,15 +279,63 @@ object MutableHashMap {
 
     }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map)))
 
+    override def getKeys(): List[K] = {
+      require(valid)
+      filterKeys(keys)
+    }.ensuring(res => valid && ListSpecs.noDuplicate(res) && res.content == map.keys().content)
+
+    @pure
+    def filterKeys(l: List[K], acc: List[K] = Nil()): List[K] = {
+      require(valid)
+      require({
+        val aMap = map
+        acc.forall(k => aMap.contains(k))
+      })
+      require({
+        val aMap = map
+        map.keys().content.subsetOf(l.content ++ acc.content)
+      })
+      decreases(l)
+      @ghost val aMap = map
+      l match {
+        case Cons(hd, tl) if this.contains(hd) && !acc.contains(hd) => 
+          val res = filterKeys(tl, Cons(hd, acc))
+          assert(ListSpecs.noDuplicate(res) )
+          assert(res.content.subsetOf(l.content) )
+          assert(res.forall(k => aMap.contains(k)))
+          res
+        case Cons(_, tl)                       => 
+          val res = filterKeys(tl, acc)
+          assert(ListSpecs.noDuplicate(res) )
+          assert(res.content.subsetOf(l.content) )
+          assert(res.forall(k => aMap.contains(k)))
+          res
+        case Nil()                            => acc
+      }
+
+    }.ensuring(res => 
+      val aMap = map
+      ListSpecs.noDuplicate(res) 
+      && res.content.subsetOf(l.content) 
+      && res.forall(k => aMap.contains(k)))
+
     @ghost
-    override  def valid: Boolean = underlying.v.valid &&
+    @inline
+    def simpleValid: Boolean = 
+      underlying.v.valid &&
       underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)) &&
       allKeysSameHashInMap(underlying.v.map, hashF)
 
+    @ghost
+    override def valid: Boolean = 
+      val keysList = this.keys
+      simpleValid &&
+      this.map.keys().forall(k => keysList.contains(k))
+
     @pure
     @ghost
     def map: ListMap[K, V] = {
-      require(valid)
+      require(simpleValid)
       extractMap(underlying.v.map.toList)
     }.ensuring(res => TupleListOpsGenK.invariantList(res.toList))
 

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

@@ -91,6 +91,7 @@ object MutableMapInterface{
 
     @pure
     def size: Int
+
     @pure
     def isEmpty: Boolean = {
       require(valid)
@@ -118,5 +119,10 @@ object MutableMapInterface{
       require(valid)
       ??? : Boolean
     }.ensuring(res => valid && (if (res) then abstractMap.eq(old(this).abstractMap - key) else abstractMap.eq(old(this).abstractMap)))
+
+    def getKeys(): List[K] = {
+      require(valid)
+      ??? : List[K]
+    }.ensuring(res => valid && ListSpecs.noDuplicate(res) && res.content == abstractMap.keys().content)
   }
 }