File tree 1 file changed +28
-0
lines changed
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src
1 file changed +28
-0
lines changed Original file line number Diff line number Diff line change @@ -177,6 +177,34 @@ module {:options "/functionSyntax:4" } HierarchicalVersionUtils {
177
177
Failure ("Unable to encode string")
178
178
}
179
179
180
+ function method Utf8EncodeKeyValue (
181
+ strKey: string ,
182
+ strValue: string
183
+ ) : (res: Result< (UTF8. ValidUTF8Bytes, UTF8. ValidUTF8Bytes), Types. Error> )
184
+ ensures (UTF8.Encode(strKey). Success? && UTF8. Encode (strValue). Success?) <= => res. Success?
185
+ {
186
+ var key :- UTF8
187
+ .Encode (strKey)
188
+ .MapFailure (
189
+ (eStr: string )
190
+ =>
191
+ WrapStringToError ("Could not UTF8 Encode: " + strKey + " due to: " + eStr ));
192
+ var value :- UTF8
193
+ .Encode (strValue)
194
+ .MapFailure (
195
+ (eStr: string )
196
+ =>
197
+ WrapStringToError ("Could not UTF8 Encode: " + strValue + " due to: " + eStr ));
198
+
199
+ Success ((key, value))
200
+ }
201
+
202
+ function method WrapStringToError (e: string )
203
+ :(ret: Types. Error)
204
+ {
205
+ Types. KeyStoreException ( message := e )
206
+ }
207
+
180
208
// Helper function to decode encryption context from UTF8 bytes map to string map
181
209
function DecodeEncryptionContext (
182
210
input: Types .EncryptionContext
You can’t perform that action at this time.
0 commit comments