refine the cache

Use the provided cache.

Calling `mpl.CreateCryptographicMaterialsCache`
with a `Shared` cache will result in an error.

Update the testing to
ensure that no shared cache is passed.

Author: seebees

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -137,14 +137,19 @@ module SearchConfigToInfo {
       else
         MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
 
-    //= specification/searchable-encryption/search-config.md#key-store-cache
-    //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
-    //# MUST be created.
-    var input := MPT.CreateCryptographicMaterialsCacheInput(
-      cache := cacheType
-    );
-    var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
-    var cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
+    var cache;
+    if cacheType.Shared? {
+      cache := cacheType.Shared;
+    } else {
+      //= specification/searchable-encryption/search-config.md#key-store-cache
+      //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
+      //# MUST be created.
+      var input := MPT.CreateCryptographicMaterialsCacheInput(
+        cache := cacheType
+      );
+      var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
+      cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
+    }
 
     if config.multi? {
       :- Need(0 < config.multi.cacheTTL, E("Beacon Cache TTL must be at least 1."));

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -181,6 +181,9 @@ module BeaconTestFixtures {
     ensures output.keyStore.ValidState()
     ensures fresh(output.keyStore.Modifies)
     ensures output.version == 1
+    ensures
+    && output.keySource.multi?
+    && output.keySource.multi.cache.None?
   {
     var store := GetKeyStore();
     return BeaconVersion (