Python: StandardLibrary Externs (#418)

StandardLibrary/runtimes/python/src/standard_library/internaldafny/extern/ConcurrentCall.py

@@ -0,0 +1,25 @@
+import standard_library.internaldafny.generated.ConcurrentCall
+
+from threading import Thread
+
+class default__:
+    @staticmethod
+    def ConcurrentCall(callee, serial_iters, concurrent_iters):
+        thread_list = []
+        for i in range(0, concurrent_iters):
+            local_num = i
+            thread_list.append(
+                Thread(target=default__._executor_call, args=(callee, serial_iters, local_num))
+            )
+
+        for i in range(0, concurrent_iters):
+            thread_list[i].start()
+
+        for i in range(0, concurrent_iters):
+            thread_list[i].join()
+
+    def _executor_call(callee, serial_iters, local_num):
+        for j in range(0, serial_iters):
+            callee.call(j, local_num)
+
+standard_library.internaldafny.generated.ConcurrentCall.default__ = default__

StandardLibrary/runtimes/python/src/standard_library/internaldafny/extern/DafnyLibraries.py

@@ -0,0 +1,132 @@
+import _dafny
+from pathlib import Path
+import threading
+
+import standard_library.internaldafny.generated.DafnyLibraries
+from standard_library.internaldafny.generated.DafnyLibraries import *
+import standard_library.internaldafny.generated.Wrappers as Wrappers
+
+# This is copy-pasted from DafnyStandardLibraries:
+# https://github.com/dafny-lang/dafny/blob/f01af4a4e86a038ed4ea9f81464b2c9bca1955e4/Source/DafnyStandardLibraries/src/Std_Concurrent.py
+
+class Lock:
+    def ctor__(self):
+        pass
+
+    def __init__(self) -> None:
+        self.lock = threading.Lock()
+
+    def Lock__(self):
+        self.lock.acquire()
+
+    def Unlock(self):
+        self.lock.release()
+
+
+class MutableMap(standard_library.internaldafny.generated.DafnyLibraries.MutableMap):
+    def ctor__(self):
+        pass
+
+    def __init__(self) -> None:
+        self.map = dict()
+        self.lock = Lock()
+
+    def Keys(self):
+        self.lock.Lock__()
+        s = self.map.keys()
+        self.lock.Unlock()
+        return _dafny.Set(s)
+
+    def HasKey(self, k):
+        self.lock.Lock__()
+        b = k in self.map
+        self.lock.Unlock()
+        return b
+
+    def Values(self):
+        self.lock.Lock__()
+        s = self.map.values()
+        self.lock.Unlock()
+        return _dafny.Set(s)
+
+    def Items(self):
+        self.lock.Lock__()
+        s = self.map.items()
+        self.lock.Unlock()
+        return _dafny.Set(s)
+
+    def Put(self, k, v):
+        self.lock.Lock__()
+        self.map[k] = v
+        self.lock.Unlock()
+
+    def Get(self, k):
+        self.lock.Lock__()
+        try:
+            v = self.map.get(k)
+        except KeyError:
+            self.lock.Unlock()
+            return Wrappers.Option_None()
+        self.lock.Unlock()
+        return Wrappers.Option_Some(v)
+
+    def Remove(self, k):
+        self.lock.Lock__()
+        self.map.pop(k, None)
+        self.lock.Unlock()
+
+    def Size(self):
+        self.lock.Lock__()
+        l = len(self.map)
+        self.lock.Unlock()
+        return l
+
+    # Added by Crypto Tools.
+    # Crypto Tools externs refer a `Select` method
+    # that does not exist on the Dafny implementation.
+    def Select(self, k):
+        return self.Get(k).value
+
+# This is copy-pasted from DafnyStandardLibraries:
+# https://github.com/dafny-lang/dafny/blob/f01af4a4e86a038ed4ea9f81464b2c9bca1955e4/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns.py
+
+import traceback
+import os.path
+import pathlib
+
+class FileIO:
+    @staticmethod
+    def INTERNAL_WriteBytesToFile(path, contents):
+        path_str = path.VerbatimString(False)
+        contents_bytes = bytes(contents)
+
+        try:
+            pathlib.Path(path_str).parent.mkdir(parents=True, exist_ok=True)
+
+            with open(path_str, mode="wb") as file:
+                contents = file.write(contents_bytes)
+                return (False, _dafny.Seq())
+        except:
+            exc_str = traceback.format_exc()
+            exc_seq = _dafny.Seq(exc_str)
+            return (True, exc_seq)
+
+    @staticmethod
+    def INTERNAL_ReadBytesFromFile(path):
+        path_str = path.VerbatimString(False)
+        try:
+            with open(path_str, mode="rb") as file:
+                contents = file.read()
+                contents_seq = _dafny.Seq(contents)
+                return (False, contents_seq, _dafny.Seq())
+        except:
+            exc_str = traceback.format_exc()
+            exc_seq = _dafny.Seq(exc_str)
+            return (True, _dafny.Seq(), exc_seq)
+
+# Export externs
+standard_library.internaldafny.generated.DafnyLibraries.FileIO = FileIO
+standard_library.internaldafny.generated.DafnyLibraries.MutableMap = MutableMap
+
+import standard_library.internaldafny.generated.FileIO
+standard_library.internaldafny.generated.FileIO.DafnyLibraries = standard_library.internaldafny.generated.DafnyLibraries

StandardLibrary/runtimes/python/src/standard_library/internaldafny/extern/SortedSets.py

@@ -0,0 +1,64 @@
+from standard_library.internaldafny.generated.SortedSets import *
+import standard_library.internaldafny.generated.SortedSets
+import _dafny
+
+class default__:
+
+  @staticmethod
+  def SetToSequence(input_set):
+    return _dafny.Seq(input_set.Elements)
+
+  @staticmethod
+  def SetToOrderedSequence(input_set, is_less_than):
+    seq_as_list = list(_dafny.Seq(input_set.Elements).Elements)
+    comparer = Comparer(is_less_than)
+    from functools import cmp_to_key
+    sorted_list = sorted(seq_as_list, key=cmp_to_key(comparer.compare))
+    return _dafny.Seq(sorted_list)
+
+  @staticmethod
+  def SetToOrderedSequence2(input_set, is_less_than):
+    return default__.SetToOrderedSequence(input_set, is_less_than)
+
+class Comparer:
+  is_less_than: Any
+
+  def __init__(self, is_less_than):
+    self.is_less_than = is_less_than
+
+  def compare(self, x, y):
+    x_list = list(x.Elements)
+    y_list = list(y.Elements)
+
+    for i in range(len(x_list)):
+      x_element = x_list[i]
+      try:
+        x_element_encoded = x_element.encode("utf-16-be")
+        x_list[i] = x_element_encoded
+      except AttributeError:
+        pass # non-chars don't have an encode attribute
+
+    for i in range(len(y_list)):
+      y_element = y_list[i]
+      try:
+        y_element_encoded = y_element.encode("utf-16-be")
+        y_list[i] = y_element_encoded
+      except AttributeError:
+        pass # non-chars don't have an encode attribute
+
+    for i in range(0, min(len(x_list), len(y_list))):
+      if (self.is_less_than(x_list[i], y_list[i])):
+        return -1
+      if (self.is_less_than(y_list[i], x_list[i])):
+        return 1
+    # Reached the end of one array. Either they are equal, or the
+    # one which is shorter should be considered "less than"
+    if len(x_list) < len(y_list):
+      return -1
+    elif len(x_list) == len(y_list):
+      return 0
+    elif len(x_list) > len(y_list):
+      return 1
+
+# Export extern
+standard_library.internaldafny.generated.SortedSets.default__ = default__

StandardLibrary/runtimes/python/src/standard_library/internaldafny/extern/Time.py

@@ -0,0 +1,21 @@
+import datetime
+import pytz
+import _dafny
+
+import standard_library.internaldafny.generated.Time
+import standard_library.internaldafny.generated.Wrappers as Wrappers
+
+class default__:
+    def CurrentRelativeTime():
+        return datetime.datetime.now(tz = pytz.UTC).timestamp() * 1000
+
+    def GetCurrentTimeStamp():
+        try:
+            d = datetime.datetime.now(tz = pytz.UTC).strftime("%Y-%m-%dT%H:%M:%S:%fZ")
+            return Wrappers.Result_Success(_dafny.Seq(_dafny.string_of(d)))
+        except Exception as e:
+            return Wrappers.Result_Failure(_dafny.string_of("Could not generate a timestamp in ISO8601: " + e))
+
+
+# Export externs
+standard_library.internaldafny.generated.Time.default__ = default__

StandardLibrary/runtimes/python/src/standard_library/internaldafny/extern/UTF8.py

@@ -0,0 +1,103 @@
+"""
+Extern UTF8 encode and decode methods.
+
+Note:
+Python's `.encode()`/`.decode()` handle surrogates with 'surrogatepass'.
+However, the results of 'surrogatepass' does not comply with Dafny's expectations.
+Dafny expects a strict interpretation of Python's Unicode handling.
+Python represents Unicode characters based on their presence in the Basic Multilingual Plane (BMP).
+The BMP includes characters from U+0000 to U+FFFF (or, 0 <= ord(chr) < 65535).
+
+If a character is inside the BMP, Python internally represents it as a single UTF-16-encoded code unit.
+ex.
+"\u2386" == '⎆' --> ord('⎆') == 9094 --> 9094 < 65535 --> in BMP
+Since "\u2386" is in the BMP, Python internally represents it as '⎆':
+
+```
+>>> s = "\u2386"
+>>> s
+'⎆'
+```
+
+In contrast, if a character is outside the BMP, Python internally represents it
+as a unicode-escaped string using surrogate pairs.
+ex.
+"\uD808\uDC00" == '𒀀' --> ord('𒀀') == 73728 --> 73728 > 65535 --> outside BMP
+Since "\uD808\uDC00" is outside the BMP, Python internally represents it as "\uD808\uDC00":
+
+```
+>>> s = "\uD808\uDC00"
+>>> s
+'\ud808\udc00'
+```
+
+However, the `.decode()` method with 'surrogatepass' leaves '\ud808\udc00' as '𒀀',
+which does not match Dafny's expectation of the literal interpretation of this field.
+To correct this, the Decode extern implementation
+re-encodes any characters outside the BMP,
+then decodes them under the expected decoding.
+"""
+import _dafny
+import struct
+
+import standard_library.internaldafny.generated.UTF8
+from standard_library.internaldafny.generated.UTF8 import *
+
+def _convert_char_outside_bmp_to_unicode_escaped_string(char_outside_bmp):
+  # Re-encode the character to UTF-16. This is necessary to get the surrogate pairs.
+  utf16_encoded_char = char_outside_bmp.encode('utf-16')
+  # Define the size of the Byte Order Mark (BOM). UTF-16 encoding includes a BOM at the start.
+  bom_size = 2
+  # Extract and decode the high surrogate pair. The high surrogate is the first 2 bytes after the BOM.
+  high_surrogate = utf16_encoded_char[bom_size:bom_size+2].decode('utf-16', 'surrogatepass')
+  # Extract and decode the low surrogate pair. The low surrogate is the next 2 bytes after the high surrogate.
+  low_surrogate = utf16_encoded_char[bom_size+2:bom_size+4].decode('utf-16', 'surrogatepass')
+  # Return the high and low surrogate pairs as a tuple so they can be appended individually.
+  return (high_surrogate, low_surrogate)
+
+def _is_outside_bmp(native_char):
+  # Any char greater than 0xFFFF is outside the BMP.
+  return ord(native_char) > 0xFFFF
+
+# Extend the Dafny-generated class with our extern methods
+class default__(standard_library.internaldafny.generated.UTF8.default__):
+
+  @staticmethod
+  def Encode(s):
+    try:
+      return Wrappers.Result_Success(_dafny.Seq(
+          s.VerbatimString(False).encode('utf-16', 'surrogatepass').decode('utf-16').encode('utf-8')
+      ))
+    # Catch both UnicodeEncodeError and UnicodeDecodeError.
+    # The `try` block involves both encoding and decoding.
+    # OverflowError is possibly raised at `_strict_tostring`'s `ord(c).to_bytes`
+    # if the char `c` is not valid.
+    except (UnicodeDecodeError, UnicodeEncodeError, OverflowError):
+      return Wrappers.Result_Failure(_dafny.Seq("Could not encode input to Dafny Bytes."))
+
+  @staticmethod
+  def Decode(s):
+    try:
+      first_pass_decoded = bytes(s).decode('utf-8')
+      decoded = []
+      for i in range(len(first_pass_decoded)):
+        char = first_pass_decoded[i]
+        # Dafny-generated code expects any characters outside the BMP
+        # to be rendered as unicode-escaped strings.
+        if _is_outside_bmp(char):
+          # Any char outside the BMP needs to be re-encoded,
+          # then decoded as separate bytes.
+          high_surrogate, low_surrogate = _convert_char_outside_bmp_to_unicode_escaped_string(char)
+          decoded.append(high_surrogate)
+          decoded.append(low_surrogate)
+        else:
+          decoded.append(char)
+      return Wrappers.Result_Success(_dafny.Seq(
+        decoded
+      ))
+    except (UnicodeDecodeError, UnicodeEncodeError, ValueError, TypeError, struct.error):
+      return Wrappers.Result_Failure(_dafny.Seq("Could not decode input from Dafny Bytes."))
+
+
+# Export externs
+standard_library.internaldafny.generated.UTF8.default__ = default__

StandardLibrary/runtimes/python/src/standard_library/internaldafny/extern/UUID.py

@@ -0,0 +1,39 @@
+import _dafny
+import uuid
+
+import standard_library.internaldafny.generated.Wrappers as Wrappers
+from standard_library.internaldafny.generated.UUID import *
+import standard_library.internaldafny.generated.UUID
+
+class default__:
+    @staticmethod
+    def ToByteArray(dafny_str):
+        try:
+            uuid_from_str = uuid.UUID(''.join(dafny_str.Elements))
+            return Wrappers.Result_Success(_dafny.Seq(uuid_from_str.bytes))
+        except Exception as e:
+            return Wrappers.Result_Failure(_dafny.string_of(
+                "Could not convert UUID to byte array: " + str(e)
+            ))
+
+    @staticmethod
+    def FromByteArray(dafny_b):
+        try:
+            native_bytes = bytes(dafny_b.Elements)
+            uuid_from_bytes = uuid.UUID(bytes=native_bytes)
+            return Wrappers.Result_Success(_dafny.Seq(str(uuid_from_bytes)))
+        except Exception as e:
+            return Wrappers.Result_Failure(_dafny.string_of(
+                "Could not convert byte array to UUID: " + str(e)
+            ))
+
+    @staticmethod
+    def GenerateUUID():
+        try:
+            generated_uuid = uuid.uuid4()
+            return Wrappers.Result_Success(_dafny.Seq(str(generated_uuid)))
+        except Exception as e:
+            return Wrappers.Result_Failure(_dafny.Seq("Could not generate a UUID: " + str(e)))
+
+# Export externs
+standard_library.internaldafny.generated.UUID.default__ = default__