Revert config change

aws · Mar 9, 2024 · a87c15e · a87c15e
1 parent a2ef35c
commit a87c15e
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -97,7 +97,7 @@ module SearchConfigToInfo {
     outer : DynamoDbTableEncryptionConfig,
     keyStore : I.ValidStore,
     config : BeaconKeySource,
-    client: PT.IAwsCryptographicPrimitivesClient
+    client: Primitives.AtomicPrimitivesClient
   )
     returns (output : Result<I.KeySource, Error>)
     modifies client.Modifies
@@ -179,7 +179,9 @@ module SearchConfigToInfo {
     :- Need(0 < |config.standardBeacons|, E("At least one standard beacon must be configured."));
 
     var maybePrimitives := Primitives.AtomicPrimitives();
-    var primitives :- maybePrimitives.MapFailure(e => AwsCryptographyPrimitives(e));
+    var primitivesX: PT.IAwsCryptographicPrimitivesClient :- maybePrimitives.MapFailure(e => AwsCryptographyPrimitives(e));
+    assert primitivesX is Primitives.AtomicPrimitivesClient;
+    var primitives := primitivesX as Primitives.AtomicPrimitivesClient;
     var source :- MakeKeySource(outer, config.keyStore, config.keySource, primitives);
     output := ConvertVersionWithSource(outer, config, source);
   }