From b6aa520048fd5e90c0600e243c72050ca9bf3bf8 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Wed, 30 Oct 2024 11:24:52 -0700
Subject: [PATCH] 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.
---
 .../DynamoDbEncryption/src/ConfigToInfo.dfy   | 21 ++++++++++++-------
 .../test/BeaconTestFixtures.dfy               |  3 +++
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
index 5a4062999..09f9393e2 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
+++ b/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."));
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy
index f4a1eadc6..6476fc10b 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy
+++ b/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 (