From 36891fa8f4bb503f69cd6c4ba8964866c2543872 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Fri, 15 Aug 2025 10:06:27 -0700
Subject: [PATCH 1/6] auto commit

---
 src/MutableMap/MutableMap.dfy | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
index 94487a13..6ac68a4d 100644
--- a/src/MutableMap/MutableMap.dfy
+++ b/src/MutableMap/MutableMap.dfy
@@ -62,8 +62,12 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
   }
 
   class {:extern} MutableMap<K(==),V(==)> extends MutableMapTrait<K,V> {
-    constructor {:extern} ()
-      ensures this.content() == map[]
+
+    // Invariant on key-value pairs this map may hold
+    ghost const inv: (K, V) -> bool
+
+    constructor {:extern} (ghost inv: (K, V) -> bool, bytesKeys: bool := false)
+      ensures this.inv == inv
 
     function {:extern} content(): map<K, V>
       reads this

From 4420de04ee1779debf0b8482c6ed56faa57dd0ce Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Sat, 16 Aug 2025 22:14:04 -0700
Subject: [PATCH 2/6] auto commit

---
 src/MutableMap/MutableMap.dfy | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
index 6ac68a4d..c2aab154 100644
--- a/src/MutableMap/MutableMap.dfy
+++ b/src/MutableMap/MutableMap.dfy
@@ -67,6 +67,7 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
     ghost const inv: (K, V) -> bool
 
     constructor {:extern} (ghost inv: (K, V) -> bool, bytesKeys: bool := false)
+      ensures 0 == |this.content().Items| 
       ensures this.inv == inv
 
     function {:extern} content(): map<K, V>

From 72ba9eaa2719d024974fb600029aadcc684057fe Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Mon, 18 Aug 2025 09:05:56 -0700
Subject: [PATCH 3/6] auto commit

---
 examples/MutableMap/MutableMapExamples.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy
index 99f590a5..d0e35c70 100644
--- a/examples/MutableMap/MutableMapExamples.dfy
+++ b/examples/MutableMap/MutableMapExamples.dfy
@@ -27,7 +27,7 @@ module {:options "-functionSyntax:4"} MutableMapExamples {
   }
 
   method Main() {
-    var m := new MutableMap<string,string>();
+    var m := new MutableMap((k: string, v: string) => true, false);
     AssertAndExpect(m.Keys() == {});
     AssertAndExpect(m.Values() == {});
     AssertAndExpect(m.Items() == {});

From dfa203647a0618ef56a2700abcd97360d4a28455 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Mon, 18 Aug 2025 09:13:52 -0700
Subject: [PATCH 4/6] auto commit

---
 src/MutableMap/MutableMap.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
index c2aab154..b23f86bd 100644
--- a/src/MutableMap/MutableMap.dfy
+++ b/src/MutableMap/MutableMap.dfy
@@ -67,7 +67,7 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
     ghost const inv: (K, V) -> bool
 
     constructor {:extern} (ghost inv: (K, V) -> bool, bytesKeys: bool := false)
-      ensures 0 == |this.content().Items| 
+      ensures 0 == |this.content().Items|
       ensures this.inv == inv
 
     function {:extern} content(): map<K, V>

From 449228e28d4308f62f83e302767b63dadda41cd1 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Mon, 18 Aug 2025 09:34:05 -0700
Subject: [PATCH 5/6] auto commit

---
 src/MutableMap/MutableMap.java | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java
index 9a3e06be..ff49a44b 100644
--- a/src/MutableMap/MutableMap.java
+++ b/src/MutableMap/MutableMap.java
@@ -18,10 +18,16 @@
 public class MutableMap<K, V> implements DafnyLibraries.MutableMapTrait<K, V> {
   private ConcurrentHashMap<K,V> m;
 
-  public MutableMap(dafny.TypeDescriptor<K> _td_K, dafny.TypeDescriptor<V> _td_V) {
+  // TODO: remove bytesKeys boolean https://github.com/dafny-lang/dafny/issues/6333
+  public MutableMap(
+    dafny.TypeDescriptor<K> _td_K, 
+    dafny.TypeDescriptor<V> _td_V,
+    boolean bytesKeys) {
     m = new ConcurrentHashMap<K,V>();
   }
 
+  public void __ctor(boolean bytesKeys) {}
+
   @Override 
   public DafnyMap<K,V> content() {
     return new DafnyMap<K,V>(m);

From 214b085d9896a0a735b10fd02970945836d3a0e7 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 19 Aug 2025 12:57:29 -0700
Subject: [PATCH 6/6] auto commit

---
 src/MutableMap/MutableMap.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
index b23f86bd..3233c35d 100644
--- a/src/MutableMap/MutableMap.dfy
+++ b/src/MutableMap/MutableMap.dfy
@@ -67,7 +67,7 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
     ghost const inv: (K, V) -> bool
 
     constructor {:extern} (ghost inv: (K, V) -> bool, bytesKeys: bool := false)
-      ensures 0 == |this.content().Items|
+      ensures this.content() == map[]
       ensures this.inv == inv
 
     function {:extern} content(): map<K, V>