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 {
119
119
&& config. multi. keyFieldName in outer. attributeActionsOnEncrypt
120
120
&& outer. attributeActionsOnEncrypt[config. multi. keyFieldName] == SE. ENCRYPT_AND_SIGN
121
121
==> output. Failure?
122
+ ensures
123
+ && config. multi?
124
+ && config. multi. cache. Some?
125
+ && config. multi. cache. value. Shared?
126
+ ==> output. Failure?
127
+
122
128
{
123
129
var mplR := MaterialProviders. MaterialProviders ();
124
130
var mpl :- mplR. MapFailure (e => AwsCryptographyMaterialProviders(e));
@@ -139,7 +145,7 @@ module SearchConfigToInfo {
139
145
140
146
var cache;
141
147
if cacheType. Shared? {
142
- cache := cacheType . Shared;
148
+ return Failure (E("Scan Beacons and Searchable Encryption do NOT support Shared caches.")) ;
143
149
} else {
144
150
// = specification/searchable-encryption/search-config.md#key-store-cache
145
151
// # 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