File tree Expand file tree Collapse file tree 1 file changed +8
-7
lines changed
DynamoDbEncryption/dafny/DynamoDbEncryption/src Expand file tree Collapse file tree 1 file changed +8
-7
lines changed Original file line number Diff line number Diff line change @@ -120,16 +120,17 @@ module SearchConfigToInfo {
120120 && outer. attributeActionsOnEncrypt[config. multi. keyFieldName] == SE. ENCRYPT_AND_SIGN
121121 ==> output. Failure?
122122 // Not in Spec, but for now, SE does not support the Shared Cache Type
123- ensures
123+ ensures
124124 && config. multi?
125125 && config. multi. cache. Some?
126126 && config. multi. cache. value. Shared?
127- && output. Failure?
128- // If the failure was NOT caused by booting up the MPL
129- && ! output. error. AwsCryptographyMaterialProviders?
130- ==>
131- && output. error. DynamoDbEncryptionException?
132- && output. error. message == "Searchable Encryption does not support the Shared Cache type at this time. "
127+ ==>
128+ && output. Failure?
129+ // If the failure was NOT caused by booting up the MPL
130+ && ! output. error. AwsCryptographyMaterialProviders?
131+ ==>
132+ && output. error. DynamoDbEncryptionException?
133+ && output. error. message == "Searchable Encryption does not support the Shared Cache type at this time. "
133134 {
134135 // TODO-FutureCleanUp : https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1510
135136 // It is not-good that the MPL is initialized here;
You can’t perform that action at this time.
0 commit comments