From dc95fdd0c95ce6af18af708109247f179e15b030 Mon Sep 17 00:00:00 2001
From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com>
Date: Fri, 24 Feb 2023 19:53:14 +0000
Subject: [PATCH] Mutable maps via Java extern (#87)

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
---
 examples/MutableMap/MutableMapDafny.dfy    | 173 +++++++++++++++++++++
 examples/MutableMap/MutableMapExamples.dfy |  66 ++++++++
 examples/MutableMap/MutableMapTrait.dfy    |  58 +++++++
 src/MutableMap/MutableMap.dfy              | 120 ++++++++++++++
 src/MutableMap/MutableMap.java             |  74 +++++++++
 src/MutableMap/README.md                   |  20 +++
 6 files changed, 511 insertions(+)
 create mode 100644 examples/MutableMap/MutableMapDafny.dfy
 create mode 100644 examples/MutableMap/MutableMapExamples.dfy
 create mode 100644 examples/MutableMap/MutableMapTrait.dfy
 create mode 100644 src/MutableMap/MutableMap.dfy
 create mode 100644 src/MutableMap/MutableMap.java
 create mode 100644 src/MutableMap/README.md

diff --git a/examples/MutableMap/MutableMapDafny.dfy b/examples/MutableMap/MutableMapDafny.dfy
new file mode 100644
index 00000000..9bf9dbcb
--- /dev/null
+++ b/examples/MutableMap/MutableMapDafny.dfy
@@ -0,0 +1,173 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %verify "%s"
+   
+/**
+  *  Implements mutable maps in Dafny to guard against inconsistent specifications.
+  *  Only exists to verify feasability; not meant for actual usage.
+  */
+module {:options "-functionSyntax:4"} MutableMapDafny {
+  /**
+    *  NOTE: Only here because of #2500; once resolved import "MutableMapTrait.dfy".
+    */
+  trait {:termination false} MutableMapTrait<K(==),V(==)> {
+    function content(): map<K, V>
+      reads this
+
+    method Put(k: K, v: V)
+      modifies this
+      ensures this.content() == old(this.content())[k := v]   
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v}
+      ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v}
+
+    function Keys(): (keys: set<K>)
+      reads this
+      ensures keys == this.content().Keys
+
+    predicate HasKey(k: K)
+      reads this
+      ensures HasKey(k) <==> k in this.content().Keys
+
+    function Values(): (values: set<V>)
+      reads this
+      ensures values == this.content().Values
+
+    function Items(): (items: set<(K,V)>)
+      reads this
+      ensures items == this.content().Items
+      ensures items == set k | k in this.content().Keys :: (k, this.content()[k])
+
+    function Select(k: K): (v: V)
+      reads this
+      requires this.HasKey(k)
+      ensures v in this.content().Values
+      ensures this.content()[k] == v
+
+    method Remove(k: K)
+      modifies this
+      ensures this.content() == old(this.content()) - {k}
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values
+ 
+    function Size(): (size: int)
+      reads this
+      ensures size == |this.content().Items|
+  }
+
+  class MutableMapDafny<K(==),V(==)> extends MutableMapTrait<K,V> {
+    var m: map<K,V>
+
+    function content(): map<K, V> 
+      reads this
+    {
+      m
+    }
+
+    constructor ()
+      ensures this.content() == map[]
+    {
+      m := map[];
+    }
+
+    method Put(k: K, v: V)
+      modifies this
+      ensures this.content() == old(this.content())[k := v]   
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v}
+      ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v}
+    {
+      m := m[k := v];
+      if k in old(m).Keys {
+        forall v' | v' in old(m).Values + {v} ensures v' in m.Values + {old(m)[k]} {
+          if v' == v || v' == old(m)[k] {
+            assert m[k] == v;
+          } else {
+            assert m.Keys == old(m).Keys + {k};
+          }
+        }
+      }
+      if k !in old(m).Keys {
+        forall v' | v' in old(m).Values + {v} ensures v' in m.Values {
+          if v' == v {
+          } else {
+            assert m.Keys == old(m).Keys + {k};
+          }
+        }
+      }
+    }
+
+    function Keys(): (keys: set<K>)
+      reads this
+      ensures keys == this.content().Keys
+    {
+      m.Keys
+    }
+
+    predicate HasKey(k: K)
+      reads this
+      ensures HasKey(k) <==> k in this.content().Keys
+    {
+      k in m.Keys
+    }
+
+    function Values(): (values: set<V>)
+      reads this
+      ensures values == this.content().Values
+    {
+      m.Values
+    }
+
+    function Items(): (items: set<(K,V)>)
+      reads this
+      ensures items == this.content().Items
+      ensures items == set k | k in this.content().Keys :: (k, this.content()[k])
+    {
+      var items := set k | k in m.Keys :: (k, m[k]);
+      assert items == m.Items by {
+        forall k | k in m.Keys ensures (k, m[k]) in m.Items {
+          assert (k, m[k]) in m.Items;
+        }
+        assert items <= m.Items;
+        forall x | x in m.Items ensures x in items {
+          assert (x.0, m[x.0]) in items;
+        }
+        assert m.Items <= items;
+      }
+      items
+    }
+
+    function Select(k: K): (v: V)
+      reads this
+      requires this.HasKey(k)
+      ensures v in this.content().Values
+      ensures this.content()[k] == v
+    {
+      m[k]
+    }
+
+    method Remove(k: K)
+      modifies this
+      ensures this.content() == old(this.content()) - {k}
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values
+    {
+      m := map k' | k' in m.Keys && k' != k :: m[k'];
+      if k in old(m).Keys {
+        var v := old(m)[k];
+        forall v' | v' in old(m).Values ensures v' in m.Values + {v} {
+          if v' == v {
+          } else {
+            assert exists k' | k' in m.Keys :: old(m)[k'] == v';
+          }
+        }
+      }
+    }
+
+    function Size(): (size: int)
+      reads this
+      ensures size == |this.content().Items|
+    {
+      |m|
+    }
+  }
+}
\ No newline at end of file
diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy
new file mode 100644
index 00000000..8b646834
--- /dev/null
+++ b/examples/MutableMap/MutableMapExamples.dfy
@@ -0,0 +1,66 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %run --target:java "%s" --input "%S/../../src/MutableMap/MutableMap.java"
+
+include "../../src/MutableMap/MutableMap.dfy"
+include "../../src/Wrappers.dfy"
+
+/**
+  *  Tests the Java interfacing implementation of mutable maps.
+  */
+module {:options "-functionSyntax:4"} MutableMapExamples {
+  import opened DafnyLibraries
+  import opened Wrappers
+
+  method AssertAndExpect(p: bool, maybeMsg: Option<string> := None) requires p {
+    match maybeMsg {
+      case None => {
+          expect p;
+      }
+      case Some(msg) => {
+          expect p, msg;
+      }
+    }
+  }
+
+  method Main() {
+    var m := new MutableMap<string,string>();
+    AssertAndExpect(m.Keys() == {});
+    AssertAndExpect(m.Values() == {});
+    AssertAndExpect(m.Items() == {});
+    AssertAndExpect(m.Size() == 0);
+
+    m.Put("testkey", "testvalue");
+    AssertAndExpect(m.Select("testkey") == "testvalue");
+    AssertAndExpect(m.Keys() == {"testkey"});
+    AssertAndExpect(m.Values() == {"testvalue"});
+    AssertAndExpect(m.Items() == {("testkey", "testvalue")});
+    print m.Select("testkey"), "\n";
+
+    AssertAndExpect(m.Size() == 1);
+    m.Put("testkey", "testvalue2");
+    AssertAndExpect(m.Keys() == {"testkey"});
+    AssertAndExpect(m.Values() == {"testvalue2"});
+    AssertAndExpect(m.Items() == {("testkey", "testvalue2")});
+
+    m.Put("testkey2", "testvalue2");
+    AssertAndExpect(m.Keys() == {"testkey", "testkey2"});
+    AssertAndExpect(m.Values() == {"testvalue2"});
+    AssertAndExpect(m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")});
+    AssertAndExpect(m.Size() == 2);
+    AssertAndExpect("testkey" in m.Keys());
+    AssertAndExpect("testkey2" in m.Keys());
+    print m.Select("testkey"), "\n";
+    print m.Select("testkey2"), "\n";
+
+    m.Remove("testkey");
+    AssertAndExpect(m.SelectOpt("testkey").None?);
+    AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2");
+    AssertAndExpect(m.Keys() == {"testkey2"});
+    AssertAndExpect(m.Values() == {"testvalue2"});
+    AssertAndExpect(m.Items() == {("testkey2", "testvalue2")});
+  }
+}
\ No newline at end of file
diff --git a/examples/MutableMap/MutableMapTrait.dfy b/examples/MutableMap/MutableMapTrait.dfy
new file mode 100644
index 00000000..80d47a31
--- /dev/null
+++ b/examples/MutableMap/MutableMapTrait.dfy
@@ -0,0 +1,58 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %verify "%s"
+
+/**
+  *  Specifications that should be satisfied by any implementation of mutable maps.
+  *  Possible instantiations are given in "MutableMapDafny.dfy" (not meant for usage, 
+  *  only exists to verify feasability) and "../../src/MutableMap/MutableMap.dfy" 
+  *  (meant for usage; interfaces with external code, e.g. "../../src/MutableMap/
+  *  MutableMap.java").
+  */
+module {:options "-functionSyntax:4"} MutableMapTrait {
+  trait {:termination false} MutableMapTrait<K(==),V(==)> {
+    function content(): map<K, V>
+      reads this
+
+    method Put(k: K, v: V)
+      modifies this
+      ensures this.content() == old(this.content())[k := v]   
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v}
+      ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v}
+
+    function Keys(): (keys: set<K>)
+      reads this
+      ensures keys == this.content().Keys
+
+    predicate HasKey(k: K)
+      reads this
+      ensures HasKey(k) <==> k in this.content().Keys
+
+    function Values(): (values: set<V>)
+      reads this
+      ensures values == this.content().Values
+
+    function Items(): (items: set<(K,V)>)
+      reads this
+      ensures items == this.content().Items
+      ensures items == set k | k in this.content().Keys :: (k, this.content()[k])
+
+    function Select(k: K): (v: V)
+      reads this
+      requires this.HasKey(k)
+      ensures v in this.content().Values
+      ensures this.content()[k] == v
+
+    method Remove(k: K)
+      modifies this
+      ensures this.content() == old(this.content()) - {k}
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values
+ 
+    function Size(): (size: int)
+      reads this
+      ensures size == |this.content().Items|
+  }
+}
\ No newline at end of file
diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
new file mode 100644
index 00000000..b0001440
--- /dev/null
+++ b/src/MutableMap/MutableMap.dfy
@@ -0,0 +1,120 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %verify "%s"
+
+include "../../src/Wrappers.dfy"
+
+/**
+  *  Implements mutable maps by interfacing with external code, e.g. "MutableMap.java".
+  */
+
+module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries {
+  import opened Wrappers
+
+  /**
+  *  NOTE: Only here because of #2500; once resolved import "../../examples/MutableMap/
+  *  MutableMapTrait.dfy".
+  */
+  trait {:termination false} MutableMapTrait<K(==),V(==)> {
+    function content(): map<K, V>
+      reads this
+
+    method Put(k: K, v: V)
+      modifies this
+      ensures this.content() == old(this.content())[k := v]   
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v}
+      ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v}
+
+    function Keys(): (keys: set<K>)
+      reads this
+      ensures keys == this.content().Keys
+
+    predicate HasKey(k: K)
+      reads this
+      ensures HasKey(k) <==> k in this.content().Keys
+
+    function Values(): (values: set<V>)
+      reads this
+      ensures values == this.content().Values
+
+    function Items(): (items: set<(K,V)>)
+      reads this
+      ensures items == this.content().Items
+      ensures items == set k | k in this.content().Keys :: (k, this.content()[k])
+
+    function Select(k: K): (v: V)
+      reads this
+      requires this.HasKey(k)
+      ensures v in this.content().Values
+      ensures this.content()[k] == v
+
+    method Remove(k: K)
+      modifies this
+      ensures this.content() == old(this.content()) - {k}
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values
+ 
+    function Size(): (size: int)
+      reads this
+      ensures size == |this.content().Items|
+  }
+
+  class {:extern} MutableMap<K(==),V(==)> extends MutableMapTrait<K,V> {
+    constructor {:extern} ()
+      ensures this.content() == map[]
+
+    function {:extern} content(): map<K, V>
+      reads this
+
+    method {:extern} Put(k: K, v: V)
+      modifies this
+      ensures this.content() == old(this.content())[k := v]   
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v}
+      ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v}
+
+    function {:extern} Keys(): (keys: set<K>)
+      reads this
+      ensures keys == this.content().Keys
+
+    predicate {:extern} HasKey(k: K)
+      reads this
+      ensures HasKey(k) <==> k in this.content().Keys
+
+    function {:extern} Values(): (values: set<V>)
+      reads this
+      ensures values == this.content().Values
+
+    function {:extern} Items(): (items: set<(K,V)>)
+      reads this
+      ensures items == this.content().Items
+      ensures items == set k | k in this.content().Keys :: (k, this.content()[k])
+
+    function {:extern} Select(k: K): (v: V)
+      reads this
+      requires this.HasKey(k)
+      ensures v in this.content().Values
+      ensures this.content()[k] == v
+    
+    function SelectOpt(k: K): (o: Option<V>)
+      reads this
+      ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) 
+      ensures o.None? ==> !this.HasKey(k)
+    {
+      if this.HasKey(k) then
+        Some(this.Select(k))
+      else
+        None
+    }
+
+    method {:extern} Remove(k: K)
+      modifies this
+      ensures this.content() == old(this.content()) - {k}
+      ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values
+
+    function {:extern} Size(): (size: int)
+      reads this
+      ensures size == |this.content().Items|
+  }
+}
diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java
new file mode 100644
index 00000000..afd8325a
--- /dev/null
+++ b/src/MutableMap/MutableMap.java
@@ -0,0 +1,74 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+package DafnyLibraries;
+
+import dafny.DafnySet;
+import dafny.DafnyMap;
+import dafny.Tuple2;
+import dafny.TypeDescriptor;
+import dafny.Helpers;
+
+import java.util.concurrent.*;
+import java.util.ArrayList;
+import java.util.Map;
+import java.math.BigInteger;
+
+public class MutableMap<K,V> extends _ExternBase_MutableMap<K,V> {
+  private ConcurrentHashMap<K,V> m;
+
+  public MutableMap(dafny.TypeDescriptor<K> _td_K, dafny.TypeDescriptor<V> _td_V) {
+    super(_td_K, _td_V);
+    m = new ConcurrentHashMap<K,V>();
+  }
+
+  @Override 
+  public DafnyMap<K,V> content() {
+    return new DafnyMap<K,V>(m);
+  }
+
+  @Override 
+  public void Put(K k, V v) {
+    m.put(k, v);
+  }
+
+  @Override 
+  public DafnySet<? extends K> Keys() {
+    return new DafnySet(m.keySet());
+  }
+
+  @Override 
+  public boolean HasKey(K k) {
+    return m.containsKey(k);
+  }
+
+  @Override 
+  public DafnySet<? extends V> Values() {
+    return new DafnySet(m.values());
+  }
+
+  @Override 
+  public DafnySet<? extends Tuple2<K,V>> Items() {
+    ArrayList<Tuple2<K, V>> list = new ArrayList<Tuple2<K, V>>();
+    for (Map.Entry<K, V> entry : m.entrySet()) {
+      list.add(new Tuple2<K, V>(entry.getKey(), entry.getValue()));
+    }
+    return new DafnySet<Tuple2<K, V>>(list);
+  }
+
+  @Override 
+  public V Select(K k) {
+    return m.get(k);
+  }
+
+  @Override 
+  public void Remove(K k) {
+    m.remove(k);
+  }
+
+  @Override 
+  public BigInteger Size() {
+    return BigInteger.valueOf(m.size());
+  }
+}
\ No newline at end of file
diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md
new file mode 100644
index 00000000..d4619fbd
--- /dev/null
+++ b/src/MutableMap/README.md
@@ -0,0 +1,20 @@
+# Mutable Map
+
+The `MutableMap` module introduces mutable maps for Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java.  For the future, we plan to extend both the functionality and the range of supported languages.
+
+To use `MutableMap` in your code, you must:
+
+1. `include` and `import` the `MutableMap` module as you would any other library module
+2. incorporate the corresponding language-specific implementation file (that is, currently, `MutableMap.java`) when building or running your program
+
+For example, to run the `MutableMapExamples.dfy` file in the `examples/MutableMap` directory that depends on the `MutableMap` module, run the following.
+
+```bash
+# Java
+$ dafny run MutableMapExamples.dfy --target:java --input ../../src/MutableMap/MutableMap.java
+```
+
+(If you aren't using `dafny run` to run your program,
+then you should instead integrate the appropriate language-specific implementation file in your build system.)
+
+The `examples/MutableMap` directory contains more detailed examples of how to use the `MutableMap` module.
\ No newline at end of file