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 (