auto commit

Author: rishav-karanjit

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -934,7 +934,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
     {
       var wClient, rClient := SetupTestTable(writeConfig, readConfig);
       WriteAllRecords(wClient, records);
-      for i := 0 to |records| {      
+      for i := 0 to |records| {
+        expect HashName in records[i].item, "`HashName` is not in records.";
         var deleteInputWithoutConditionExpression := DDB.DeleteItemInput(
           TableName := TableName,
           Key := map[HashName := records[i].item[HashName]],
@@ -943,7 +944,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         var deleteResultForWithoutConditionExpressionCase := wClient.DeleteItem(deleteInputWithoutConditionExpression);
         expect deleteResultForWithoutConditionExpressionCase.Success?, "DeleteItem should have failed.";
         expect deleteResultForWithoutConditionExpressionCase.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput";
-        expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value == records[i].item, "Wrong item was deleted.";
+        if attributeToDelete in records[i].item {
+          expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value == records[i].item, "Wrong item was deleted.";
+        }
       }
     }