@@ -11,22 +11,27 @@ module BatchWriteItemTransform {
11
11
import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
12
12
import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
13
13
import Seq
14
+ import SortedSets
14
15
import Util = DynamoDbEncryptionUtil
15
16
16
- method Input (config: Config , input: BatchWriteItemInputTransformInput )
17
+ method {:vcs_split_on_every_assert} Input (config: Config , input: BatchWriteItemInputTransformInput )
17
18
returns (output: Result< BatchWriteItemInputTransformOutput, Error> )
18
19
requires ValidConfig?(config)
19
20
ensures ValidConfig?(config)
20
21
modifies ModifiesConfig (config)
21
22
{
22
23
var tableNames := input. sdkInput. RequestItems. Keys;
23
24
var result : map < DDB. TableName, DDB. WriteRequests> := map [];
24
- while tableNames != {}
25
- decreases |tableNames|
26
- invariant tableNames <= input. sdkInput. RequestItems. Keys
25
+ var tableNamesSeq := SortedSets. ComputeSetToSequence (tableNames);
26
+ ghost var tableNamesSet' := tableNames;
27
+ var i := 0;
28
+ while i < |tableNamesSeq|
29
+ invariant Seq. HasNoDuplicates (tableNamesSeq)
30
+ invariant forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet'
31
+ invariant |tableNamesSet'| == |tableNamesSeq| - i
32
+ invariant tableNamesSet' <= input. sdkInput. RequestItems. Keys
27
33
{
28
- var tableName :| tableName in tableNames;
29
- tableNames := tableNames - { tableName };
34
+ var tableName := tableNamesSeq[i];
30
35
31
36
var writeRequests : DDB. WriteRequests := input. sdkInput. RequestItems[tableName];
32
37
// = specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-batchwriteitem
@@ -64,6 +69,11 @@ module BatchWriteItemTransform {
64
69
}
65
70
writeRequests := encryptedItems;
66
71
}
72
+ tableNamesSet' := tableNamesSet' - {tableName};
73
+ i := i + 1;
74
+ assert forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' by {
75
+ reveal Seq. HasNoDuplicates ();
76
+ }
67
77
result := result[tableName := writeRequests];
68
78
}
69
79
:- Need (|result| == |input.sdkInput.RequestItems|, E("Internal Error")); // Dafny gets too confused
0 commit comments