chore: add new externs for file append and cpu time

AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs

@@ -130,20 +130,42 @@ pub mod DafnyLibraries {
             }
         }
 
+        pub fn INTERNAL_AppendBytesToFile(
+            path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+            bytes: &::dafny_runtime::Sequence<u8>,
+        ) -> (
+            bool,
+            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+        ) {
+            SendBytesToFile(path, bytes, true)
+        }
+
         pub fn INTERNAL_WriteBytesToFile(
             path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
             bytes: &::dafny_runtime::Sequence<u8>,
         ) -> (
             bool,
             ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+        ) {
+            SendBytesToFile(path, bytes, false)
+        }
+
+        pub fn SendBytesToFile(
+            path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+            bytes: &::dafny_runtime::Sequence<u8>,
+            append: bool
+        ) -> (
+            bool,
+            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
         ) {
             let file_name = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(path);
             let path = Path::new(&file_name);
 
             let maybe_file = std::fs::OpenOptions::new()
+                .append(append)
                 .write(true)
                 .create(true)
-                .truncate(true)
+                .truncate(!append)
                 .open(path);
             let mut file = match maybe_file {
                 Err(why) => {

AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs

@@ -7,6 +7,7 @@
 
 use crate::*;
 use std::time::SystemTime;
+use std::convert::TryFrom;
 
 impl crate::Time::_default {
     #[allow(non_snake_case)]
@@ -26,6 +27,12 @@ impl crate::Time::_default {
         }
     }
 
+    #[allow(non_snake_case)]
+    #[allow(dead_code)]
+    pub fn GetProcessCpuTimeMillis() -> i64 {
+        i64::try_from(cpu_time::ProcessTime::now().as_duration().as_millis()).expect("CPU millisecond didn't fit in an i64")
+    }
+
     #[allow(non_snake_case)]
     pub fn GetCurrentTimeStamp() -> ::std::rc::Rc<
         _Wrappers_Compile::Result<

AwsCryptographyPrimitives/runtimes/rust/Cargo.toml

@@ -13,6 +13,7 @@ aws-lc-sys = "0.22.0"
 aws-smithy-runtime-api = "1.7.3"
 aws-smithy-types = "1.2.9"
 chrono = "0.4.38"
+cpu-time = "1.0.0"
 dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"}
 dashmap = "6.1.0"
 pem = "3.0.4"

ComAmazonawsDynamodb/runtimes/rust/Cargo.toml

@@ -12,6 +12,7 @@ aws-sdk-dynamodb = "1.53.0"
 aws-smithy-runtime-api = "1.7.3"
 aws-smithy-types = "1.2.9"
 chrono = "0.4.38"
+cpu-time = "1.0.0"
 dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"}
 dashmap = "6.1.0"
 tokio = {version = "1.41.1", features = ["full"] }

ComAmazonawsKms/runtimes/rust/Cargo.toml

@@ -12,6 +12,7 @@ aws-sdk-kms = "1.50.0"
 aws-smithy-runtime-api = "1.7.3"
 aws-smithy-types = "1.2.9"
 chrono = "0.4.38"
+cpu-time = "1.0.0"
 dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"}
 dashmap = "6.1.0"
 tokio = {version = "1.41.1", features = ["full"] }

StandardLibrary/Makefile

@@ -24,6 +24,7 @@ PYTHON_MODULE_NAME=smithy_dafny_standard_library
 
 RUST_OTHER_FILES := \
         runtimes/rust/src/concurrent_call.rs \
+        runtimes/rust/src/dafny_libraries.rs \
         runtimes/rust/src/sets.rs \
         runtimes/rust/src/time.rs \
 	runtimes/rust/src/uuid.rs

StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go

@@ -14,7 +14,18 @@ var m_DafnyLibraries struct {
 }
 
 func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
-	p := _dafny.SequenceVerbatimString(path, false)
+	p := func() string {
+		var s string
+		for i := _dafny.Iterate(path); ; {
+			val, notEndOfSequence := i()
+			if notEndOfSequence {
+				s = s + string(val.(_dafny.Char))
+			} else {
+				return s
+			}
+		}
+	}()
+
 	dat, err := ioutil.ReadFile(p)
 	if err != nil {
 		errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
@@ -25,11 +36,20 @@ func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny
 }
 
 func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
-	p := _dafny.SequenceVerbatimString(path, false)
+	p := func() string {
+		var s string
+		for i := _dafny.Iterate(path); ; {
+			val, notEndOfSequence := i()
+			if notEndOfSequence {
+				s = s + string(val.(_dafny.Char))
+			} else {
+				return s
+			}
+		}
+	}()
 
 	// Create directories
 	os.MkdirAll(filepath.Dir(p), os.ModePerm)
-
 	bytesArray := _dafny.ToByteArray(bytes)
 	err := ioutil.WriteFile(p, bytesArray, 0644)
 	if err != nil {
@@ -38,3 +58,37 @@ func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny.
 	}
 	return false, _dafny.EmptySeq
 }
+
+func (_static CompanionStruct_Default___) INTERNAL_AppendBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
+	p := func() string {
+		var s string
+		for i := _dafny.Iterate(path); ; {
+			val, notEndOfSequence := i()
+			if notEndOfSequence {
+				s = s + string(val.(_dafny.Char))
+			} else {
+				return s
+			}
+		}
+	}()
+
+	// Create directories
+	os.MkdirAll(filepath.Dir(p), os.ModePerm)
+
+	bytesArray := _dafny.ToByteArray(bytes)
+
+	f, err := os.OpenFile(p, os.O_APPEND|os.O_CREATE|os.O_WRONLY, 0644)
+	if err != nil {
+		return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
+	}
+
+	if _, err := f.Write(bytesArray); err != nil {
+		return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
+	}
+
+	if err := f.Close(); err != nil {
+		return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
+	}
+
+	return false, _dafny.EmptySeq
+}

StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go

@@ -1,20 +1,44 @@
 package _Time
 
 import (
+	"syscall"
 	"time"
 
 	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
 	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
 )
 
+var m__Time = CompanionStruct_Default___{}
+
+func (CompanionStruct_Default___) CurrentRelativeTimeMilli() int64 {
+	return CurrentRelativeTimeMilli()
+}
+
+func (CompanionStruct_Default___) CurrentRelativeTime() int64 {
+	return CurrentRelativeTime()
+}
 func CurrentRelativeTime() int64 {
 	return int64(time.Now().Second())
 }
 
+func (CompanionStruct_Default___) GetCurrentTimeStamp() Wrappers.Result {
+	return GetCurrentTimeStamp()
+}
+
 func GetCurrentTimeStamp() Wrappers.Result {
 	return Wrappers.Companion_Result_.Create_Success_(dafny.SeqOfChars([]dafny.Char(time.Now().Format("2006-01-02T15:04:05.000000Z"))...))
 }
 
 func CurrentRelativeTimeMilli() int64 {
 	return time.Now().UnixMilli()
 }
+
+func (CompanionStruct_Default___) GetProcessCpuTimeMillis() int64 {
+	return GetProcessCpuTimeMillis()
+}
+
+func GetProcessCpuTimeMillis() int64 {
+	usage := new(syscall.Rusage)
+	syscall.Getrusage(syscall.RUSAGE_SELF, usage)
+	return (usage.Utime.Nano() + usage.Stime.Nano()) / 1000000
+}

StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/FileIO.java

@@ -102,6 +102,54 @@ > INTERNAL_WriteBytesToFile(
     }
   }
 
+  /**
+   * Attempts to append {@code bytes} to the file at {@code path}, creating nonexistent parent
+   * directories as necessary, and returns a tuple of the following values:
+   *
+   * <dl>
+   *   <dt>{@code isError}
+   *   <dd>true iff an exception was thrown during path string conversion or when writing to the
+   *       file
+   *   <dt>{@code errorMsg}
+   *   <dd>the error message of the thrown exception if {@code isError} is true, or an empty
+   *       sequence otherwise
+   * </dl>
+   *
+   * <p>We return these values individually because {@code Result} is not defined in the runtime but
+   * instead in library code. It is the responsibility of library code to construct an equivalent
+   * {@code Result} value.
+   */
+  public static Tuple2<
+    Boolean,
+    DafnySequence<? extends Character>
+  > INTERNAL_AppendBytesToFile(
+    DafnySequence<? extends Character> path,
+    DafnySequence<? extends Byte> bytes
+  ) {
+    try {
+      final Path pathObj = dafnyStringToPath(path);
+      createParentDirs(pathObj);
+
+      // It's safe to cast `bytes` to `DafnySequence<Byte>` since the cast value is immediately
+      // consumed
+      @SuppressWarnings("unchecked")
+      final byte[] byteArr = DafnySequence.toByteArray(
+        (DafnySequence<Byte>) bytes
+      );
+
+      java.io.OutputStream out = Files.newOutputStream(
+        pathObj,
+        java.nio.file.StandardOpenOption.CREATE,
+        java.nio.file.StandardOpenOption.APPEND
+      );
+      out.write(byteArr);
+      out.close();
+      return Tuple2.create(false, DafnySequence.empty(TypeDescriptor.CHAR));
+    } catch (Exception ex) {
+      return Tuple2.create(true, stackTraceToDafnyString(ex));
+    }
+  }
+
   /** Returns a Path constructed from the given Dafny string. */
   private static final Path dafnyStringToPath(
     final DafnySequence<? extends Character> path

StandardLibrary/runtimes/java/src/main/java/Time/__default.java

@@ -1,7 +1,9 @@
 package Time;
 
 import Wrappers_Compile.Result;
+import com.sun.management.OperatingSystemMXBean;
 import dafny.DafnySequence;
+import java.lang.management.ManagementFactory;
 import java.text.DateFormat;
 import java.text.SimpleDateFormat;
 import java.util.Date;
@@ -17,6 +19,12 @@ public static Long CurrentRelativeTimeMilli() {
     return System.currentTimeMillis();
   }
 
+  public static Long GetProcessCpuTimeMillis() {
+    OperatingSystemMXBean bean =
+      (com.sun.management.OperatingSystemMXBean) ManagementFactory.getOperatingSystemMXBean();
+    return new Long(bean.getProcessCpuTime() / 1000000);
+  }
+
   public static Result<
     DafnySequence<? extends Character>,
     DafnySequence<? extends Character>