WIP

Author: texastony

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

@@ -156,28 +156,19 @@ module {:options "/functionSyntax:4" } HierarchicalVersionUtils {
     input: Types.EncryptionContextString
   ): (output: Result<Types.EncryptionContext, string>)
     ensures output.Success? ==> |output.value| == |input| // Output map size equals input map size
-    ensures output.Failure? ==> output.error == "Unable to encode string"
   {
-    var encodedEncryptionContext
-      := set k <- input
-           ::
-             (UTF8.Encode(k), UTF8.Encode(input[k]), k);
+    var encodedInputResult: seq<(string, (UTF8.ValidUTF8Bytes, UTF8.ValidUTF8Bytes))> :- Seq.MapWithResult(
+      // Dafny requires the type of the element being mapped over, or it feaks out.
+      (strKey: string)
+      =>
+      var keyValueUtf8 :- Utf8EncodeKeyValue(strKey, input[strKey]);
+      Success(strKey, keyValueUtf8),
+        input.Keys
+      );
 
-    if (forall i <- encodedEncryptionContext
-          ::
-            && i.0.Success?
-            && i.1.Success?)
-    then
-      var resultMap := map i <- encodedEncryptionContext :: i.0.value := i.1.value;
-      if |resultMap| == |input| then
-        Success(resultMap)
-      else
-        Failure("Unable to encode string")
-    else
-      Failure("Unable to encode string")
   }
 
-  function method Utf8EncodeKeyValue(
+  function Utf8EncodeKeyValue(
     strKey: string,
     strValue: string
   ) : (res: Result<(UTF8.ValidUTF8Bytes, UTF8.ValidUTF8Bytes), Types.Error>)
@@ -199,12 +190,6 @@ module {:options "/functionSyntax:4" } HierarchicalVersionUtils {
     Success((key, value))
   }
 
-  function method WrapStringToError(e: string)
-    :(ret: Types.Error)
-  {
-    Types.KeyStoreException( message := e )
-  }
-
   // Helper function to decode encryption context from UTF8 bytes map to string map
   function DecodeEncryptionContext(
     input: Types.EncryptionContext