fix: remove usage of :| (#1320)

aws · Aug 28, 2024 · eeb3f51 · eeb3f51
1 parent 6128a39
commit eeb3f51
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 16 deletions.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy
@@ -11,6 +11,7 @@ module BatchGetItemTransform {
   import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
   import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
   import Seq
+  import SortedSets
 
   method Input(config: Config, input: BatchGetItemInputTransformInput)
     returns (output: Result<BatchGetItemInputTransformOutput, Error>)
@@ -34,14 +35,15 @@ module BatchGetItemTransform {
       return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
     }
     var tableNames := input.sdkOutput.Responses.value.Keys;
+    var tableNamesSeq := SortedSets.ComputeSetToSequence(tableNames);
+    ghost var tableNamesSet' := tableNames;
+    var i := 0;
     var result := map[];
-    while tableNames != {}
-      decreases |tableNames|
-      invariant tableNames <= input.sdkOutput.Responses.value.Keys
+    while i < |tableNamesSeq|
+      invariant tableNamesSet' <= input.sdkOutput.Responses.value.Keys
       // true but expensive -- invariant result.Keys + tableNames == input.sdkOutput.Responses.value.Keys
     {
-      var tableName :| tableName in tableNames;
-      tableNames := tableNames - { tableName };
+      var tableName := tableNamesSeq[i];
       var responses := input.sdkOutput.Responses.value[tableName];
       if tableName in config.tableEncryptionConfigs {
         var tableConfig := config.tableEncryptionConfigs[tableName];
@@ -74,6 +76,7 @@ module BatchGetItemTransform {
       } else {
         result := result + map[tableName := responses];
       }
+      i := i + 1;
     }
     return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Responses := Some(result))));
   }

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy
@@ -11,22 +11,27 @@ module BatchWriteItemTransform {
   import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
   import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
   import Seq
+  import SortedSets
   import Util = DynamoDbEncryptionUtil
 
-  method Input(config: Config, input: BatchWriteItemInputTransformInput)
+  method {:vcs_split_on_every_assert} Input(config: Config, input: BatchWriteItemInputTransformInput)
     returns (output: Result<BatchWriteItemInputTransformOutput, Error>)
     requires ValidConfig?(config)
     ensures ValidConfig?(config)
     modifies ModifiesConfig(config)
   {
     var tableNames := input.sdkInput.RequestItems.Keys;
     var result : map<DDB.TableName, DDB.WriteRequests> := map[];
-    while tableNames != {}
-      decreases |tableNames|
-      invariant tableNames <= input.sdkInput.RequestItems.Keys
+    var tableNamesSeq := SortedSets.ComputeSetToSequence(tableNames);
+    ghost var tableNamesSet' := tableNames;
+    var i := 0;
+    while i < |tableNamesSeq|
+      invariant Seq.HasNoDuplicates(tableNamesSeq)
+      invariant forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet'
+      invariant |tableNamesSet'| == |tableNamesSeq| - i
+      invariant tableNamesSet' <= input.sdkInput.RequestItems.Keys
     {
-      var tableName :| tableName in tableNames;
-      tableNames := tableNames - { tableName };
+      var tableName := tableNamesSeq[i];
 
       var writeRequests : DDB.WriteRequests := input.sdkInput.RequestItems[tableName];
       //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-batchwriteitem
@@ -64,6 +69,11 @@ module BatchWriteItemTransform {
         }
         writeRequests := encryptedItems;
       }
+      tableNamesSet' := tableNamesSet' - {tableName};
+      i := i + 1;
+      assert forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' by {
+        reveal Seq.HasNoDuplicates();
+      }
       result := result[tableName := writeRequests];
     }
     :- Need(|result| ==  |input.sdkInput.RequestItems|, E("Internal Error")); // Dafny gets too confused

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
@@ -16,6 +16,7 @@ module
   import DynamoDbItemEncryptor
   import SearchConfigToInfo
   import Seq
+  import SortedSets
   import ET = AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import DDB = ComAmazonawsDynamodbTypes
@@ -119,6 +120,9 @@ module
     //# [DynamoDb Item Encryptor](./ddb-table-encryption-config.md)
     //# per configured table, using these table encryption configs.
     var m' := config.tableEncryptionConfigs;
+    var mKeys := m'.Keys;
+    var tableNamesSeq := SortedSets.ComputeSetToSequence(mKeys);
+    ghost var mKeysSet := mKeys;
 
     ghost var inputConfigsModifies: set<object> := set
       tableConfig <- config.tableEncryptionConfigs.Values,
@@ -130,8 +134,9 @@ module
       :: o;
 
     var allLogicalTableNames := {};
+    var i := 0;
 
-    while m'.Keys != {}
+    while i < |tableNamesSeq|
       invariant m'.Keys <= config.tableEncryptionConfigs.Keys
       invariant forall k <- m' :: m'[k] == config.tableEncryptionConfigs[k]
       invariant forall internalConfig <- internalConfigs.Values :: internalConfig.logicalTableName in allLogicalTableNames
@@ -140,10 +145,10 @@ module
       invariant AllTableConfigsValid?(internalConfigs)
       invariant ValidConfig?(Config(internalConfigs))
 
-      decreases m'.Keys
       modifies inputConfigsModifies
     {
-      var tableName: string :| tableName in m';
+      var tableName: string := tableNamesSeq[i];
+
       var inputConfig := config.tableEncryptionConfigs[tableName];
       :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table maped to multipule physical tables: " + inputConfig.logicalTableName));
 
@@ -223,8 +228,7 @@ module
         assert ConfigsMatch(tableName, internalConfig, inputConfig);
       }
 
-      // Pop 'tableName' off the map, so that we may continue iterating
-      m' := map k' | k' in m' && k' != tableName :: m'[k'];
+      i := i + 1;
     }
     assert SearchValidState(DdbMiddlewareConfig.Config(tableEncryptionConfigs := internalConfigs));