Integrate esdk with mpl (#45)

These are the changes to the ESDK to integrate with the MPL
smithy-lang · Feb 2, 2023 · 8cec193 · 8cec193
1 parent b98df44
commit 8cec193
Showing 1 changed file with 10 additions and 2 deletions.
diff --git a/AwsCryptographyPrimitives/src/AwsCryptographyPrimitivesOperations.dfy b/AwsCryptographyPrimitives/src/AwsCryptographyPrimitivesOperations.dfy
@@ -65,7 +65,11 @@ module AwsCryptographyPrimitivesOperations refines AbstractAwsCryptographyPrimit
   }
 
   predicate HkdfExpandEnsuresPublicly(input: HkdfExpandInput, output: Result<seq<uint8>, Error>)
-  {true}
+  {
+      output.Success?
+    ==>
+      && |output.value| == input.expectedLength as nat
+  }
 
   method HkdfExpand ( config: InternalConfig,  input: HkdfExpandInput )
     returns (output: Result<seq<uint8>, Error>)
@@ -74,7 +78,11 @@ module AwsCryptographyPrimitivesOperations refines AbstractAwsCryptographyPrimit
   }
 
   predicate HkdfEnsuresPublicly(input: HkdfInput, output: Result<seq<uint8>, Error>)
-  {true}
+  {
+      output.Success?
+    ==>
+      && |output.value| == input.expectedLength as nat
+  }
 
   method Hkdf ( config: InternalConfig,  input: HkdfInput )
     returns (output: Result<seq<uint8>, Error>)