fix: GetCurrentTimeStamp returns ISO8601 format (aws#575)

The Java extern returned `YYYY-MM-DDTHH:mm:ss:ssssssZ`
This is not ISO8601.

Also, time is non-deterministic,
therefore this MUST be a method.

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy

@@ -155,7 +155,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore
     //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
     //# - `timestamp`: a timestamp for the current time.
     //# This timestamp MUST be in ISO8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
-    var timestamp :- Time.GetCurrentTimeStamp()
+    var timestamp? := Time.GetCurrentTimeStamp();
+    var timestamp :- timestamp?
     .MapFailure(e => Types.KeyStoreException(message := e));
 
     var maybeBranchKeyVersion := UUID.GenerateUUID();
@@ -225,7 +226,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore
 
     :- Need(0 < |input.branchKeyIdentifier|, Types.KeyStoreException(message := ErrorMessages.BRANCH_KEY_ID_NEEDED));
 
-    var timestamp :- Time.GetCurrentTimeStamp()
+    var timestamp? := Time.GetCurrentTimeStamp();
+    var timestamp :- timestamp?
     .MapFailure(e => Types.KeyStoreException(message := e));
 
     var maybeBranchKeyVersion := UUID.GenerateUUID();

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

@@ -19,7 +19,7 @@ public static Long CurrentRelativeTime() {
   > GetCurrentTimeStamp() {
     try {
       TimeZone tz = TimeZone.getTimeZone("UTC");
-      DateFormat df = new SimpleDateFormat("yyyy-MM-dd'T'HH:mm:ss:SSSSSS'Z'"); // Quoted "Z" to indicate UTC, no timezone offset
+      DateFormat df = new SimpleDateFormat("yyyy-MM-dd'T'HH:mm:ss.SSSSSS'Z'"); // Quoted "Z" to indicate UTC, no timezone offset
       df.setTimeZone(tz);
       return CreateGetCurrentTimeStampSuccess(
         software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(

StandardLibrary/src/Time.dfy

@@ -9,6 +9,15 @@ module {:extern "Time"} Time {
   import opened Wrappers
   import opened UInt = StandardLibrary.UInt
 
+  // Time is non-deterministic.
+  // In this way it is similar to random number.
+  // As such it MUST NOT be a Dafny function.
+  // Dafny functions MUST be deterministic.
+  // var t1 :- GetCurrentTimeStamp();
+  // wait
+  // var t2 :- GetCurrentTimeStamp();
+  // assert t1 == t2; // this will be true if GetCurrentTimeStamp is a function.
+
   // Returns the number of seconds since some fixed-as-long-as-this-program-is-running moment in the past
   // Time is represented as signed over unsigned because java does not do unsigned
   // values - net can do both so we are able to change the representation to signed.
@@ -19,7 +28,7 @@ module {:extern "Time"} Time {
 
   // Returns a timestamp for the current time in ISO8601 format in UTC
   // to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
-  function method {:extern "GetCurrentTimeStamp"} GetCurrentTimeStamp(): (res: Result<string, string>)
+  method {:extern "GetCurrentTimeStamp"} GetCurrentTimeStamp() returns (res: Result<string, string>)
 
   // The next two functions are for the benefit of the extern implementation to call,
   // avoiding direct references to generic datatype constructors

StandardLibrary/test/Time.dfy

@@ -4,7 +4,7 @@
 include "../src/StandardLibrary.dfy"
 include "../src/Time.dfy"
 
-module TestTime {
+module {:options "/functionSyntax:4" } TestTime {
   import Time
 
   method {:test} TestNonDecreasing() {
@@ -18,4 +18,32 @@ module TestTime {
     var t2 := Time.GetCurrent();
     expect t2 - t1 >= 0;
   }
+
+  method {:test} TestGetCurrentTimeStamp()
+  {
+    var CurrentTime :- expect Time.GetCurrentTimeStamp();
+    expect ISO8601?(CurrentTime);
+  }
+
+  lemma ISO8601Test()
+  {
+    assert ISO8601?("YYYY-MM-DDTHH:mm:ss.ssssssZ");
+    assert ISO8601?("2024-08-06T17:23:25.000874Z");
+  }
+
+  predicate ISO8601?(
+    CreateTime: string
+  )
+  {
+    // “YYYY-MM-DDTHH:mm:ss.ssssssZ“
+    && |CreateTime| == 27
+    && CreateTime[4] == '-'
+    && CreateTime[7] == '-'
+    && CreateTime[10] == 'T'
+    && CreateTime[13] == ':'
+    && CreateTime[16] == ':'
+    && CreateTime[19] == '.'
+    && CreateTime[26] == 'Z'
+  }
+
 }