Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 1e56fa0

Browse files
texastonyRitvikKapila
andauthoredDec 16, 2024··
Update DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
Co-authored-by: Ritvik Kapila <[email protected]>
1 parent 65c5aaf commit 1e56fa0

File tree

1 file changed

+8
-7
lines changed

1 file changed

+8
-7
lines changed
 

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff 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;

0 commit comments

Comments
 (0)
Please sign in to comment.