PYTHON PASSING

Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py

@@ -1,5 +1,37 @@
 # Module: DafnyStdLibs_FileIOInternalExterns
 
-@staticmethod
-def INTERNAL_ReadBytesFromFile(i):
-  return i * i
+import traceback
+import os
+import os.path
+import _dafny
+
+class default__:
+  @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, None)
+    except:
+      exc_str = traceback.format_exc()
+      exc_seq = _dafny.Seq(exc_str)
+      return (True, None, exc_seq)
+
+  @staticmethod
+  def INTERNAL__WriteBytesToFile(path, contents):
+    path_str = path.VerbatimString(False)
+    contents_bytes = bytes(contents)
+
+    try:
+      os.makedirs(os.path.basename(path_str), exist_ok=True)
+
+      with open(path_str, mode="wb") as file:
+          contents = file.write(contents_bytes)
+          return (False, None)
+    except:
+      exc_str = traceback.format_exc()
+      exc_seq = _dafny.Seq(exc_str)
+      return (True, exc_seq)
+