1
1
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2
2
// SPDX-License-Identifier: Apache-2.0
3
3
include ".. / src/ Index. dfy"
4
+ include ".. / .. / DynamoDbEncryption/ test/ BeaconTestFixtures. dfy"
4
5
5
6
module TestFixtures {
6
7
import opened Wrappers
@@ -9,6 +10,7 @@ module TestFixtures {
9
10
import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
10
11
import opened AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
11
12
import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes
13
+ import opened BeaconTestFixtures
12
14
import DynamoDbEncryptionTransforms
13
15
import DynamoDbItemEncryptor
14
16
import AwsCryptographyMaterialProvidersTypes
@@ -122,11 +124,7 @@ module TestFixtures {
122
124
attributeActionsOnEncrypt := config.attributeActionsOnEncrypt,
123
125
allowedUnsignedAttributes := config.allowedUnsignedAttributes,
124
126
allowedUnsignedAttributePrefix := config.allowedUnsignedAttributePrefix,
125
- keyring := Some(keyring),
126
- cmm := None (),
127
- algorithmSuiteId := None (),
128
- legacyOverride := None (),
129
- plaintextOverride := None ()
127
+ keyring := Some(keyring)
130
128
);
131
129
var encryptor2 : IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor. DynamoDbItemEncryptor (encryptorConfig);
132
130
assert encryptor2 is DynamoDbItemEncryptor. DynamoDbItemEncryptorClient;
@@ -184,10 +182,7 @@ module TestFixtures {
184
182
{
185
183
var matProv :- expect MaterialProviders. MaterialProviders (MaterialProviders.DefaultMaterialProvidersConfig());
186
184
var keyringInput := AwsCryptographyMaterialProvidersTypes. CreateAwsKmsMultiKeyringInput (
187
- generator := Some(PUBLIC_US_WEST_2_KMS_TEST_KEY),
188
- kmsKeyIds := None (),
189
- clientSupplier := None (),
190
- grantTokens := None ()
185
+ generator := Some(PUBLIC_US_WEST_2_KMS_TEST_KEY)
191
186
);
192
187
keyring :- expect matProv. CreateAwsKmsMultiKeyring (keyringInput);
193
188
}
@@ -216,7 +211,7 @@ module TestFixtures {
216
211
ensures fresh (encryption. Modifies)
217
212
{
218
213
var keyring := GetKmsKeyring ();
219
- var encryption2 : IDynamoDbEncryptionTransformsClient :- expect DynamoDbEncryptionTransforms. DynamoDbEncryptionTransforms (
214
+ encryption :- expect DynamoDbEncryptionTransforms. DynamoDbEncryptionTransforms (
220
215
DynamoDbTablesEncryptionConfig(
221
216
tableEncryptionConfigs := map[
222
217
"foo" := DynamoDbTableEncryptionConfig(
@@ -232,17 +227,59 @@ module TestFixtures {
232
227
allowedUnsignedAttributes := Some (["plain"]),
233
228
allowedUnsignedAttributePrefix := None (),
234
229
algorithmSuiteId := None (),
230
+ keyring := Some (keyring)
231
+ )
232
+ ]
233
+ )
234
+ );
235
+ assume {:axiom} fresh (encryption. Modifies);
236
+ }
237
+
238
+ // type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
239
+
240
+ const MultiActions : AttributeActions :=
241
+ map [
242
+ "bar" := SE. SIGN_ONLY,
243
+ "std2" := SE. ENCRYPT_AND_SIGN,
244
+ "std4" := SE. ENCRYPT_AND_SIGN,
245
+ "std6" := SE. ENCRYPT_AND_SIGN,
246
+ "Name" := SE. ENCRYPT_AND_SIGN,
247
+ "Title" := SE. ENCRYPT_AND_SIGN,
248
+ "TooBad" := SE. ENCRYPT_AND_SIGN,
249
+ "Year" := SE. SIGN_ONLY,
250
+ "Date" := SE. SIGN_ONLY,
251
+ "TheKeyField" := SE. SIGN_ONLY
252
+ ]
253
+
254
+ method GetDynamoDbEncryptionTransformsMutli (plaintextOverride : Option <AwsCryptographyDbEncryptionSdkDynamoDbTypes .PlaintextOverride>)
255
+ returns (encryption: DynamoDbEncryptionTransforms. DynamoDbEncryptionTransformsClient)
256
+ ensures encryption. ValidState ()
257
+ ensures fresh (encryption)
258
+ ensures fresh (encryption. Modifies)
259
+ {
260
+ var keyring := GetKmsKeyring ();
261
+ var beacons := GetLotsaBeaconsMulti ();
262
+ var search := SearchConfig (
263
+ versions := [beacons],
264
+ writeVersion := 1
265
+ );
266
+ encryption :- expect DynamoDbEncryptionTransforms. DynamoDbEncryptionTransforms (
267
+ DynamoDbTablesEncryptionConfig(
268
+ tableEncryptionConfigs := map[
269
+ "foo" := DynamoDbTableEncryptionConfig(
270
+ logicalTableName := "foo",
271
+ partitionKeyName := "bar",
272
+ sortKeyName := None(),
273
+ attributeActionsOnEncrypt := MultiActions,
274
+ allowedUnsignedAttributes := Some (["plain"]),
235
275
keyring := Some (keyring),
236
- cmm := None (),
237
- search := None,
238
- legacyOverride := None,
239
- plaintextOverride := None
276
+ search := Some (search),
277
+ plaintextOverride := plaintextOverride
240
278
)
241
279
]
242
280
)
243
281
);
244
- assert encryption2 is DynamoDbEncryptionTransforms. DynamoDbEncryptionTransformsClient;
245
- encryption := encryption2 as DynamoDbEncryptionTransforms. DynamoDbEncryptionTransformsClient;
246
282
assume {:axiom} fresh (encryption. Modifies);
247
283
}
284
+
248
285
}
0 commit comments