From 1ff326092bb704b9ae248fc4d98ca25c5c91fb2b Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Fri, 9 Aug 2024 10:04:02 -0700
Subject: [PATCH] fix: GetCurrentTimeStamp returns ISO8601 format (#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.
---
 .../src/AwsCryptographyKeyStoreOperations.dfy |  6 ++--
 .../java/src/main/java/Time/__default.java    |  2 +-
 StandardLibrary/src/Time.dfy                  | 11 ++++++-
 StandardLibrary/test/Time.dfy                 | 30 ++++++++++++++++++-
 4 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy
index b6ca63010..71bbd1360 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy
+++ b/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();
diff --git a/StandardLibrary/runtimes/java/src/main/java/Time/__default.java b/StandardLibrary/runtimes/java/src/main/java/Time/__default.java
index 0074d8f3a..ecd63f45c 100644
--- a/StandardLibrary/runtimes/java/src/main/java/Time/__default.java
+++ b/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(
diff --git a/StandardLibrary/src/Time.dfy b/StandardLibrary/src/Time.dfy
index 2c7da906e..d91a95243 100644
--- a/StandardLibrary/src/Time.dfy
+++ b/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
diff --git a/StandardLibrary/test/Time.dfy b/StandardLibrary/test/Time.dfy
index e9d4e86a5..c02b71aa4 100644
--- a/StandardLibrary/test/Time.dfy
+++ b/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'
+  }
+
 }