@@ -81,7 +81,7 @@ module TestAwsKmsHierarchicalKeyring {
81
81
return encryptionMaterialsIn;
82
82
}
83
83
84
- method {:test} TestHierarchyClientESDKSuite ()
84
+ method {:test} {:vcs_split_on_every_assert} TestHierarchyClientESDKSuite ()
85
85
{
86
86
var branchKeyId := BRANCH_KEY_ID;
87
87
// TTL = 166.67 hours
@@ -96,10 +96,17 @@ module TestAwsKmsHierarchicalKeyring {
96
96
id := None,
97
97
kmsConfiguration := kmsConfig,
98
98
logicalKeyStoreName := logicalKeyStoreName,
99
- grantTokens := None,
100
- ddbTableName := branchKeyStoreName,
101
- ddbClient := Some(ddbClient),
102
- kmsClient := Some (kmsClient)
99
+ storage := Some(
100
+ KeyStoreTypes.ddb(
101
+ KeyStoreTypes.DynamoDBTable(
102
+ ddbTableName := branchKeyStoreName,
103
+ ddbClient := Some(ddbClient)
104
+ ))),
105
+ keyManagement := Some (
106
+ KeyStoreTypes.kms(
107
+ KeyStoreTypes.AwsKms(
108
+ kmsClient := Some(kmsClient)
109
+ )))
103
110
);
104
111
105
112
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
@@ -125,7 +132,7 @@ module TestAwsKmsHierarchicalKeyring {
125
132
TestRoundtrip (hierarchyKeyring, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyId);
126
133
}
127
134
128
- method {:test} TestHierarchyClientDBESuite () {
135
+ method {:test} {:vcs_split_on_every_assert} TestHierarchyClientDBESuite () {
129
136
var branchKeyId := BRANCH_KEY_ID;
130
137
// TTL = 166.67 hours
131
138
var ttl : Types. PositiveLong := (1 * 60000) * 10;
@@ -139,10 +146,17 @@ module TestAwsKmsHierarchicalKeyring {
139
146
id := None,
140
147
kmsConfiguration := kmsConfig,
141
148
logicalKeyStoreName := logicalKeyStoreName,
142
- grantTokens := None,
143
- ddbTableName := branchKeyStoreName,
144
- ddbClient := Some(ddbClient),
145
- kmsClient := Some (kmsClient)
149
+ storage := Some(
150
+ KeyStoreTypes.ddb(
151
+ KeyStoreTypes.DynamoDBTable(
152
+ ddbTableName := branchKeyStoreName,
153
+ ddbClient := Some(ddbClient)
154
+ ))),
155
+ keyManagement := Some (
156
+ KeyStoreTypes.kms(
157
+ KeyStoreTypes.AwsKms(
158
+ kmsClient := Some(kmsClient)
159
+ )))
146
160
);
147
161
148
162
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
@@ -168,7 +182,7 @@ module TestAwsKmsHierarchicalKeyring {
168
182
TestRoundtrip (hierarchyKeyring, materials, TEST_DBE_ALG_SUITE_ID, branchKeyId);
169
183
}
170
184
171
- method {:test} TestBranchKeyIdSupplier ()
185
+ method {:test} {:vcs_split_on_every_assert} TestBranchKeyIdSupplier ()
172
186
{
173
187
var branchKeyIdSupplier: Types. IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier ();
174
188
// TTL = 166.67 hours
@@ -183,10 +197,17 @@ module TestAwsKmsHierarchicalKeyring {
183
197
id := None,
184
198
kmsConfiguration := kmsConfig,
185
199
logicalKeyStoreName := logicalKeyStoreName,
186
- grantTokens := None,
187
- ddbTableName := branchKeyStoreName,
188
- ddbClient := Some(ddbClient),
189
- kmsClient := Some (kmsClient)
200
+ storage := Some(
201
+ KeyStoreTypes.ddb(
202
+ KeyStoreTypes.DynamoDBTable(
203
+ ddbTableName := branchKeyStoreName,
204
+ ddbClient := Some(ddbClient)
205
+ ))),
206
+ keyManagement := Some (
207
+ KeyStoreTypes.kms(
208
+ KeyStoreTypes.AwsKms(
209
+ kmsClient := Some(kmsClient)
210
+ )))
190
211
);
191
212
192
213
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
@@ -214,7 +235,7 @@ module TestAwsKmsHierarchicalKeyring {
214
235
TestRoundtrip (hierarchyKeyring, materials, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_B);
215
236
}
216
237
217
- method {:test} TestInvalidDataKeyError ()
238
+ method {:test} {:vcs_split_on_every_assert} TestInvalidDataKeyError ()
218
239
{
219
240
var branchKeyIdSupplier: Types. IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier ();
220
241
// TTL = 166.67 hours
@@ -227,10 +248,17 @@ module TestAwsKmsHierarchicalKeyring {
227
248
id := None,
228
249
kmsConfiguration := kmsConfig,
229
250
logicalKeyStoreName := logicalKeyStoreName,
230
- grantTokens := None,
231
- ddbTableName := branchKeyStoreName,
232
- ddbClient := Some(ddbClient),
233
- kmsClient := Some (kmsClient)
251
+ storage := Some(
252
+ KeyStoreTypes.ddb(
253
+ KeyStoreTypes.DynamoDBTable(
254
+ ddbTableName := branchKeyStoreName,
255
+ ddbClient := Some(ddbClient)
256
+ ))),
257
+ keyManagement := Some (
258
+ KeyStoreTypes.kms(
259
+ KeyStoreTypes.AwsKms(
260
+ kmsClient := Some(kmsClient)
261
+ )))
234
262
);
235
263
var keyStore :- expect KeyStore. KeyStore (keyStoreConfig);
236
264
var hierarchyKeyring :- expect mpl. CreateAwsKmsHierarchicalKeyring (
@@ -353,6 +381,13 @@ module TestAwsKmsHierarchicalKeyring {
353
381
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
354
382
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
355
383
var ddbClient :- expect DDB. DynamoDBClient ();
384
+ // Recommend commenting the assume out while developing this method,
385
+ // and just ignore the modifies exeptions,
386
+ // and then re-enabling it once everything is safe
387
+ assume {:axiom} && kmsClientWest. Modifies == {}
388
+ && kmsClientEast. Modifies == {}
389
+ && ddbClient. Modifies == {};
390
+
356
391
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
357
392
358
393
// Create a Key Store with the a KMS configuration and
@@ -363,7 +398,7 @@ module TestAwsKmsHierarchicalKeyring {
363
398
kmsConfiguration := kmsConfig,
364
399
logicalKeyStoreName := logicalKeyStoreName,
365
400
grantTokens := None,
366
- ddbTableName := branchKeyStoreName,
401
+ ddbTableName := Some( branchKeyStoreName) ,
367
402
ddbClient := Some (ddbClient),
368
403
kmsClient := Some (kmsClientWest)
369
404
);
@@ -379,7 +414,7 @@ module TestAwsKmsHierarchicalKeyring {
379
414
kmsConfiguration := kmsConfig,
380
415
logicalKeyStoreName := logicalKeyStoreName,
381
416
grantTokens := None,
382
- ddbTableName := branchKeyStoreName,
417
+ ddbTableName := Some( branchKeyStoreName) ,
383
418
ddbClient := Some (ddbClient),
384
419
kmsClient := Some (kmsClientEast)
385
420
);
@@ -493,6 +528,13 @@ module TestAwsKmsHierarchicalKeyring {
493
528
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
494
529
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
495
530
var ddbClient :- expect DDB. DynamoDBClient ();
531
+ // Recommend commenting the assume out while developing this method,
532
+ // and just ignore the modifies exeptions,
533
+ // and then re-enabling it once everything is safe
534
+ assume {:axiom} && kmsClientWest. Modifies == {}
535
+ && kmsClientEast. Modifies == {}
536
+ && ddbClient. Modifies == {};
537
+
496
538
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
497
539
498
540
// Create a Key Store with the a KMS configuration and
@@ -503,7 +545,7 @@ module TestAwsKmsHierarchicalKeyring {
503
545
kmsConfiguration := kmsConfig,
504
546
logicalKeyStoreName := logicalKeyStoreName,
505
547
grantTokens := None,
506
- ddbTableName := branchKeyStoreName,
548
+ ddbTableName := Some( branchKeyStoreName) ,
507
549
ddbClient := Some (ddbClient),
508
550
kmsClient := Some (kmsClientWest)
509
551
);
@@ -519,7 +561,7 @@ module TestAwsKmsHierarchicalKeyring {
519
561
kmsConfiguration := kmsConfig,
520
562
logicalKeyStoreName := logicalKeyStoreName,
521
563
grantTokens := None,
522
- ddbTableName := branchKeyStoreName,
564
+ ddbTableName := Some( branchKeyStoreName) ,
523
565
ddbClient := Some (ddbClient),
524
566
kmsClient := Some (kmsClientEast)
525
567
);
@@ -613,6 +655,13 @@ module TestAwsKmsHierarchicalKeyring {
613
655
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
614
656
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
615
657
var ddbClient :- expect DDB. DynamoDBClient ();
658
+ // Recommend commenting the assume out while developing this method,
659
+ // and just ignore the modifies exeptions,
660
+ // and then re-enabling it once everything is safe
661
+ assume {:axiom} && kmsClientWest. Modifies == {}
662
+ && kmsClientEast. Modifies == {}
663
+ && ddbClient. Modifies == {};
664
+
616
665
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
617
666
618
667
// Create a Key Store with the a KMS configuration and
@@ -623,7 +672,7 @@ module TestAwsKmsHierarchicalKeyring {
623
672
kmsConfiguration := kmsConfig,
624
673
logicalKeyStoreName := logicalKeyStoreName,
625
674
grantTokens := None,
626
- ddbTableName := branchKeyStoreName,
675
+ ddbTableName := Some( branchKeyStoreName) ,
627
676
ddbClient := Some (ddbClient),
628
677
kmsClient := Some (kmsClientWest)
629
678
);
@@ -639,7 +688,7 @@ module TestAwsKmsHierarchicalKeyring {
639
688
kmsConfiguration := kmsConfig,
640
689
logicalKeyStoreName := logicalKeyStoreName,
641
690
grantTokens := None,
642
- ddbTableName := branchKeyStoreName,
691
+ ddbTableName := Some( branchKeyStoreName) ,
643
692
ddbClient := Some (ddbClient),
644
693
kmsClient := Some (kmsClientEast)
645
694
);
@@ -731,6 +780,13 @@ module TestAwsKmsHierarchicalKeyring {
731
780
var kmsClientWest :- expect KMS. KMSClientForRegion (regionWest);
732
781
var kmsClientEast :- expect KMS. KMSClientForRegion (regionEast);
733
782
var ddbClient :- expect DDB. DynamoDBClient ();
783
+
784
+ // Recommend commenting the assume out while developing this method,
785
+ // and just ignore the modifies exeptions,
786
+ // and then re-enabling it once everything is safe
787
+ assume {:axiom} && kmsClientWest. Modifies == {}
788
+ && kmsClientEast. Modifies == {}
789
+ && ddbClient. Modifies == {};
734
790
var kmsConfig := KeyStoreTypes. KMSConfiguration. kmsKeyArn (keyArn);
735
791
736
792
// Different logical key store names for both Key Stores
@@ -745,7 +801,7 @@ module TestAwsKmsHierarchicalKeyring {
745
801
kmsConfiguration := kmsConfig,
746
802
logicalKeyStoreName := logicalKeyStoreName,
747
803
grantTokens := None,
748
- ddbTableName := branchKeyStoreName,
804
+ ddbTableName := Some( branchKeyStoreName) ,
749
805
ddbClient := Some (ddbClient),
750
806
kmsClient := Some (kmsClientWest)
751
807
);
@@ -762,7 +818,7 @@ module TestAwsKmsHierarchicalKeyring {
762
818
kmsConfiguration := kmsConfig,
763
819
logicalKeyStoreName := logicalKeyStoreNameNew,
764
820
grantTokens := None,
765
- ddbTableName := branchKeyStoreName,
821
+ ddbTableName := Some( branchKeyStoreName) ,
766
822
ddbClient := Some (ddbClient),
767
823
kmsClient := Some (kmsClientEast)
768
824
);
0 commit comments