@@ -69,7 +69,7 @@ module TestAwsKmsHierarchicalKeyring {
69
69
return encryptionMaterialsIn;
70
70
}
71
71
72
- method {:test} TestHierarchyClientESDKSuite ()
72
+ method {:test} {:vcs_split_on_every_assert} TestHierarchyClientESDKSuite ()
73
73
{
74
74
var branchKeyId := BRANCH_KEY_ID;
75
75
// TTL = 166.67 hours
@@ -84,10 +84,17 @@ module TestAwsKmsHierarchicalKeyring {
84
84
id := None,
85
85
kmsConfiguration := kmsConfig,
86
86
logicalKeyStoreName := logicalKeyStoreName,
87
- grantTokens := None,
88
- ddbTableName := branchKeyStoreName,
89
- ddbClient := Some(ddbClient),
90
- kmsClient := Some (kmsClient)
87
+ storage := Some(
88
+ KeyStoreTypes.ddb(
89
+ KeyStoreTypes.DynamoDBTable(
90
+ ddbTableName := branchKeyStoreName,
91
+ ddbClient := Some(ddbClient)
92
+ ))),
93
+ keyManagement := Some (
94
+ KeyStoreTypes.kms(
95
+ KeyStoreTypes.AwsKms(
96
+ kmsClient := Some(kmsClient)
97
+ )))
91
98
);
92
99
93
100
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
@@ -113,7 +120,7 @@ module TestAwsKmsHierarchicalKeyring {
113
120
TestRoundtrip (hierarchyKeyring, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyId);
114
121
}
115
122
116
- method {:test} TestHierarchyClientDBESuite () {
123
+ method {:test} {:vcs_split_on_every_assert} TestHierarchyClientDBESuite () {
117
124
var branchKeyId := BRANCH_KEY_ID;
118
125
// TTL = 166.67 hours
119
126
var ttl : Types. PositiveLong := (1 * 60000) * 10;
@@ -127,10 +134,17 @@ module TestAwsKmsHierarchicalKeyring {
127
134
id := None,
128
135
kmsConfiguration := kmsConfig,
129
136
logicalKeyStoreName := logicalKeyStoreName,
130
- grantTokens := None,
131
- ddbTableName := branchKeyStoreName,
132
- ddbClient := Some(ddbClient),
133
- kmsClient := Some (kmsClient)
137
+ storage := Some(
138
+ KeyStoreTypes.ddb(
139
+ KeyStoreTypes.DynamoDBTable(
140
+ ddbTableName := branchKeyStoreName,
141
+ ddbClient := Some(ddbClient)
142
+ ))),
143
+ keyManagement := Some (
144
+ KeyStoreTypes.kms(
145
+ KeyStoreTypes.AwsKms(
146
+ kmsClient := Some(kmsClient)
147
+ )))
134
148
);
135
149
136
150
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
@@ -156,7 +170,7 @@ module TestAwsKmsHierarchicalKeyring {
156
170
TestRoundtrip (hierarchyKeyring, materials, TEST_DBE_ALG_SUITE_ID, branchKeyId);
157
171
}
158
172
159
- method {:test} TestBranchKeyIdSupplier ()
173
+ method {:test} {:vcs_split_on_every_assert} TestBranchKeyIdSupplier ()
160
174
{
161
175
var branchKeyIdSupplier: Types. IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier ();
162
176
// TTL = 166.67 hours
@@ -171,10 +185,17 @@ module TestAwsKmsHierarchicalKeyring {
171
185
id := None,
172
186
kmsConfiguration := kmsConfig,
173
187
logicalKeyStoreName := logicalKeyStoreName,
174
- grantTokens := None,
175
- ddbTableName := branchKeyStoreName,
176
- ddbClient := Some(ddbClient),
177
- kmsClient := Some (kmsClient)
188
+ storage := Some(
189
+ KeyStoreTypes.ddb(
190
+ KeyStoreTypes.DynamoDBTable(
191
+ ddbTableName := branchKeyStoreName,
192
+ ddbClient := Some(ddbClient)
193
+ ))),
194
+ keyManagement := Some (
195
+ KeyStoreTypes.kms(
196
+ KeyStoreTypes.AwsKms(
197
+ kmsClient := Some(kmsClient)
198
+ )))
178
199
);
179
200
180
201
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
@@ -202,7 +223,7 @@ module TestAwsKmsHierarchicalKeyring {
202
223
TestRoundtrip (hierarchyKeyring, materials, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_B);
203
224
}
204
225
205
- method {:test} TestInvalidDataKeyError ()
226
+ method {:test} {:vcs_split_on_every_assert} TestInvalidDataKeyError ()
206
227
{
207
228
var branchKeyIdSupplier: Types. IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier ();
208
229
// TTL = 166.67 hours
@@ -215,10 +236,17 @@ module TestAwsKmsHierarchicalKeyring {
215
236
id := None,
216
237
kmsConfiguration := kmsConfig,
217
238
logicalKeyStoreName := logicalKeyStoreName,
218
- grantTokens := None,
219
- ddbTableName := branchKeyStoreName,
220
- ddbClient := Some(ddbClient),
221
- kmsClient := Some (kmsClient)
239
+ storage := Some(
240
+ KeyStoreTypes.ddb(
241
+ KeyStoreTypes.DynamoDBTable(
242
+ ddbTableName := branchKeyStoreName,
243
+ ddbClient := Some(ddbClient)
244
+ ))),
245
+ keyManagement := Some (
246
+ KeyStoreTypes.kms(
247
+ KeyStoreTypes.AwsKms(
248
+ kmsClient := Some(kmsClient)
249
+ )))
222
250
);
223
251
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
224
252
var hierarchyKeyring :- expect mpl. CreateAwsKmsHierarchicalKeyring (
@@ -341,6 +369,13 @@ module TestAwsKmsHierarchicalKeyring {
341
369
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
342
370
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
343
371
var ddbClient :- expect DDB. DynamoDBClient ();
372
+ // Recommend commenting the assume out while developing this method,
373
+ // and just ignore the modifies exeptions,
374
+ // and then re-enabling it once everything is safe
375
+ assume {:axiom} && kmsClientWest. Modifies == {}
376
+ && kmsClientEast. Modifies == {}
377
+ && ddbClient. Modifies == {};
378
+
344
379
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
345
380
346
381
// Create a Key Store with the a KMS configuration and
@@ -351,7 +386,7 @@ module TestAwsKmsHierarchicalKeyring {
351
386
kmsConfiguration := kmsConfig,
352
387
logicalKeyStoreName := logicalKeyStoreName,
353
388
grantTokens := None,
354
- ddbTableName := branchKeyStoreName,
389
+ ddbTableName := Some( branchKeyStoreName) ,
355
390
ddbClient := Some (ddbClient),
356
391
kmsClient := Some (kmsClientWest)
357
392
);
@@ -367,7 +402,7 @@ module TestAwsKmsHierarchicalKeyring {
367
402
kmsConfiguration := kmsConfig,
368
403
logicalKeyStoreName := logicalKeyStoreName,
369
404
grantTokens := None,
370
- ddbTableName := branchKeyStoreName,
405
+ ddbTableName := Some( branchKeyStoreName) ,
371
406
ddbClient := Some (ddbClient),
372
407
kmsClient := Some (kmsClientEast)
373
408
);
@@ -481,6 +516,13 @@ module TestAwsKmsHierarchicalKeyring {
481
516
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
482
517
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
483
518
var ddbClient :- expect DDB. DynamoDBClient ();
519
+ // Recommend commenting the assume out while developing this method,
520
+ // and just ignore the modifies exeptions,
521
+ // and then re-enabling it once everything is safe
522
+ assume {:axiom} && kmsClientWest. Modifies == {}
523
+ && kmsClientEast. Modifies == {}
524
+ && ddbClient. Modifies == {};
525
+
484
526
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
485
527
486
528
// Create a Key Store with the a KMS configuration and
@@ -491,7 +533,7 @@ module TestAwsKmsHierarchicalKeyring {
491
533
kmsConfiguration := kmsConfig,
492
534
logicalKeyStoreName := logicalKeyStoreName,
493
535
grantTokens := None,
494
- ddbTableName := branchKeyStoreName,
536
+ ddbTableName := Some( branchKeyStoreName) ,
495
537
ddbClient := Some (ddbClient),
496
538
kmsClient := Some (kmsClientWest)
497
539
);
@@ -507,7 +549,7 @@ module TestAwsKmsHierarchicalKeyring {
507
549
kmsConfiguration := kmsConfig,
508
550
logicalKeyStoreName := logicalKeyStoreName,
509
551
grantTokens := None,
510
- ddbTableName := branchKeyStoreName,
552
+ ddbTableName := Some( branchKeyStoreName) ,
511
553
ddbClient := Some (ddbClient),
512
554
kmsClient := Some (kmsClientEast)
513
555
);
@@ -601,6 +643,13 @@ module TestAwsKmsHierarchicalKeyring {
601
643
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
602
644
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
603
645
var ddbClient :- expect DDB. DynamoDBClient ();
646
+ // Recommend commenting the assume out while developing this method,
647
+ // and just ignore the modifies exeptions,
648
+ // and then re-enabling it once everything is safe
649
+ assume {:axiom} && kmsClientWest. Modifies == {}
650
+ && kmsClientEast. Modifies == {}
651
+ && ddbClient. Modifies == {};
652
+
604
653
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
605
654
606
655
// Create a Key Store with the a KMS configuration and
@@ -611,7 +660,7 @@ module TestAwsKmsHierarchicalKeyring {
611
660
kmsConfiguration := kmsConfig,
612
661
logicalKeyStoreName := logicalKeyStoreName,
613
662
grantTokens := None,
614
- ddbTableName := branchKeyStoreName,
663
+ ddbTableName := Some( branchKeyStoreName) ,
615
664
ddbClient := Some (ddbClient),
616
665
kmsClient := Some (kmsClientWest)
617
666
);
@@ -627,7 +676,7 @@ module TestAwsKmsHierarchicalKeyring {
627
676
kmsConfiguration := kmsConfig,
628
677
logicalKeyStoreName := logicalKeyStoreName,
629
678
grantTokens := None,
630
- ddbTableName := branchKeyStoreName,
679
+ ddbTableName := Some( branchKeyStoreName) ,
631
680
ddbClient := Some (ddbClient),
632
681
kmsClient := Some (kmsClientEast)
633
682
);
@@ -719,6 +768,13 @@ module TestAwsKmsHierarchicalKeyring {
719
768
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
720
769
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
721
770
var ddbClient :- expect DDB. DynamoDBClient ();
771
+
772
+ // Recommend commenting the assume out while developing this method,
773
+ // and just ignore the modifies exeptions,
774
+ // and then re-enabling it once everything is safe
775
+ assume {:axiom} && kmsClientWest. Modifies == {}
776
+ && kmsClientEast. Modifies == {}
777
+ && ddbClient. Modifies == {};
722
778
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
723
779
724
780
// Different logical key store names for both Key Stores
@@ -733,7 +789,7 @@ module TestAwsKmsHierarchicalKeyring {
733
789
kmsConfiguration := kmsConfig,
734
790
logicalKeyStoreName := logicalKeyStoreName,
735
791
grantTokens := None,
736
- ddbTableName := branchKeyStoreName,
792
+ ddbTableName := Some( branchKeyStoreName) ,
737
793
ddbClient := Some (ddbClient),
738
794
kmsClient := Some (kmsClientWest)
739
795
);
@@ -750,7 +806,7 @@ module TestAwsKmsHierarchicalKeyring {
750
806
kmsConfiguration := kmsConfig,
751
807
logicalKeyStoreName := logicalKeyStoreNameNew,
752
808
grantTokens := None,
753
- ddbTableName := branchKeyStoreName,
809
+ ddbTableName := Some( branchKeyStoreName) ,
754
810
ddbClient := Some (ddbClient),
755
811
kmsClient := Some (kmsClientEast)
756
812
);
0 commit comments