File tree Expand file tree Collapse file tree 1 file changed +7
-1
lines changed
DynamoDbEncryption/dafny/DynamoDbEncryption/src Expand file tree Collapse file tree 1 file changed +7
-1
lines changed Original file line number Diff line number Diff line change @@ -119,6 +119,12 @@ module SearchConfigToInfo {
119119 && config. multi. keyFieldName in outer. attributeActionsOnEncrypt
120120 && outer. attributeActionsOnEncrypt[config. multi. keyFieldName] == SE. ENCRYPT_AND_SIGN
121121 ==> output. Failure?
122+ ensures
123+ && config. multi?
124+ && config. multi. cache. Some?
125+ && config. multi. cache. value. Shared?
126+ ==> output. Failure?
127+
122128 {
123129 var mplR := MaterialProviders. MaterialProviders ();
124130 var mpl :- mplR. MapFailure (e => AwsCryptographyMaterialProviders(e));
@@ -139,7 +145,7 @@ module SearchConfigToInfo {
139145
140146 var cache;
141147 if cacheType. Shared? {
142- cache := cacheType . Shared;
148+ return Failure (E("Scan Beacons and Searchable Encryption do NOT support Shared caches.")) ;
143149 } else {
144150 // = specification/searchable-encryption/search-config.md#key-store-cache
145151 // # For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
You can’t perform that action at this time.
0 commit comments