feat: Storm cache supports millisecond resolution

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy

@@ -1623,12 +1623,16 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly graceInterval: CountingNumber ,
     nameonly fanOut: CountingNumber ,
     nameonly inFlightTTL: CountingNumber ,
-    nameonly sleepMilli: CountingNumber
+    nameonly sleepMilli: CountingNumber ,
+    nameonly timeUnits: Option<TimeUnits> := Option.None
   )
   datatype SymmetricSignatureAlgorithm =
     | HMAC(HMAC: AwsCryptographyPrimitivesTypes.DigestAlgorithm)
     | None(None: None)
   type SymmetricSigningKeyList = seq<Secret>
+  datatype TimeUnits =
+    | Seconds
+    | Milliseconds
   datatype UpdateUsageMetadataInput = | UpdateUsageMetadataInput (
     nameonly identifier: seq<uint8> ,
     nameonly bytesUsed: PositiveInteger
@@ -1661,6 +1665,9 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     | EntryDoesNotExist (
         nameonly message: string
       )
+    | InFlightTTLExceeded (
+        nameonly message: string
+      )
     | InvalidAlgorithmSuiteInfo (
         nameonly message: string
       )

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/cryptographic-materials-cache.smithy

@@ -126,6 +126,12 @@ structure EntryAlreadyExists {
   message: String,
 }
 
+@error("client")
+structure InFlightTTLExceeded {
+  @required
+  message: String,
+}
+
 // Materials Cache Constructors
 
 @positional
@@ -190,26 +196,43 @@ structure StormTrackingCache {
   entryPruningTailSize: CountingNumber,
 
   @required
-  @javadoc("How many seconds before expiration should an attempt be made to refresh the materials.
+  @javadoc("How much time before expiration should an attempt be made to refresh the materials.
   If zero, use a simple cache with no storm tracking.")
   gracePeriod: CountingNumber,
 
   @required
-  @javadoc("How many seconds between attempts to refresh the materials.")
+  @javadoc("How much time between attempts to refresh the materials.")
   graceInterval: CountingNumber,
 
   @required
   @javadoc("How many simultaneous attempts to refresh the materials.")
   fanOut: CountingNumber,
 
   @required
-  @javadoc("How many seconds until an attempt to refresh the materials should be forgotten.")
+  @javadoc("How much time until an attempt to refresh the materials should be forgotten.")
   inFlightTTL: CountingNumber,
 
   @required
   @javadoc("How many milliseconds should a thread sleep if fanOut is exceeded.")
   sleepMilli: CountingNumber,
-}
+
+  @javadoc("The time unit for gracePeriod, graceInterval, and inFlightTTL.
+  The default is seconds.
+  If this is set to milliseconds, then these values will be treated as milliseconds.")
+  timeUnits: TimeUnits
+}
+
+@enum([
+  {
+    name: "Seconds",
+    value: "Seconds",
+  },
+  {
+    name: "Milliseconds",
+    value: "Milliseconds",
+  },
+])
+string TimeUnits
 
 union CacheType {
   Default : DefaultCache,

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy

@@ -269,11 +269,15 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
   method CheckCache(cache : CacheType, ttlSeconds: PositiveLong) returns (output : Outcome<Error>)
   {
     if cache.StormTracking? {
+      var gracePeriod := if cache.StormTracking.timeUnits.UnwrapOr(Types.Seconds).Seconds? then
+        cache.StormTracking.gracePeriod as PositiveLong
+      else
+        cache.StormTracking.gracePeriod as PositiveLong / 1000;
       var storm := cache.StormTracking;
-      if ttlSeconds <= storm.gracePeriod as PositiveLong {
+      if ttlSeconds <= gracePeriod {
         var msg := "When creating an AwsKmsHierarchicalKeyring with a StormCache, " +
         "the ttlSeconds of the KeyRing must be greater than the gracePeriod of the StormCache " +
-        "yet the ttlSeconds is " + N(ttlSeconds) + " and the gracePeriod is " + N(storm.gracePeriod as PositiveLong) + ".";
+        "yet the ttlSeconds is " + N(ttlSeconds) + " and the gracePeriod is " + N(gracePeriod) + ".";
         return Fail(Types.AwsCryptographicMaterialProvidersException(message := msg));
       }
       return Pass;
@@ -819,6 +823,8 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
       case StormTracking(c) =>
         var cache := c.( entryPruningTailSize := OptionalCountingNumber(c.entryPruningTailSize));
         :- StormTracker.CheckSettings(cache);
+
+
         var cmc := new StormTracker.StormTracker(cache);
         var synCmc := new StormTrackingCMC.StormTrackingCMC(cmc);
         return Success(synCmc);

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy

@@ -429,6 +429,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
       ensures GetCacheEntryEnsuresPublicly(input, output)
       ensures unchanged(History)
       ensures InternalModifies <= old(InternalModifies)
+      ensures output.Success? ==> now <= output.value.expiryTime
     {
       if cache.HasKey(input.identifier) {
         var entry := cache.Select(input.identifier);