chore(dafny): Add Update and delete test (#1942)

Author: rishav-karanjit

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -397,6 +397,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         BasicIoTestBatchWriteItem(c1, c2, globalRecords);
         BasicIoTestPutItem(c1, c2, globalRecords);
         BasicIoTestTransactWriteItems(c1, c2, globalRecords);
+        BasicIoTestUpdateItem(c1, c2, globalRecords, "One");
+        BasicIoTestUpdateItem(c1, c2, globalRecords, "Two");
+        BasicIoTestDeleteItem(c1, c2, globalRecords, "One", "Uno");
+        BasicIoTestDeleteItem(c1, c2, globalRecords, "Two", "Dos");
+        BasicIoTestDeleteItemWithoutConditionExpression(c1, c2, globalRecords, "One", "Uno");
+        BasicIoTestDeleteItemWithoutConditionExpression(c1, c2, globalRecords, "Two", "Dos");
         BasicIoTestExecuteStatement(c1, c2);
         BasicIoTestExecuteTransaction(c1, c2);
         BasicIoTestBatchExecuteStatement(c1, c2);
@@ -844,6 +850,108 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       BasicIoTestTransactGetItems(rClient, records);
     }
 
+    method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>, attributeToUpdate: DDB.AttributeName)
+    {
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
+      WriteAllRecords(wClient, records);
+      // Update each record by appending "updated" to the partition key
+      for i := 0 to |records| {
+        var newValue := "updated";
+        // Create an update expression to update the partition key
+        var updateExpr := "SET #att = :val";
+        expect attributeToUpdate in writeConfig.config.attributeActionsOnEncrypt, "`attributeToUpdate` not in attributeActionsOnEncrypt";
+        var exprAttrNames := map["#att" := attributeToUpdate];
+        var exprAttrValues := map[":val" := DDB.AttributeValue.S(newValue)];
+        expect HashName in records[i].item, "`HashName` is not in records.";
+        var updateInput := DDB.UpdateItemInput(
+          TableName := TableName,
+          Key := map[HashName := records[i].item[HashName]],
+          UpdateExpression := Some(updateExpr),
+          ExpressionAttributeNames := Some(exprAttrNames),
+          ExpressionAttributeValues := Some(exprAttrValues),
+          ReturnValues := None,
+          ReturnConsumedCapacity := None,
+          ReturnItemCollectionMetrics := None,
+          ConditionExpression := None
+        );
+        var updateResult := wClient.UpdateItem(updateInput);
+        if writeConfig.config.attributeActionsOnEncrypt[attributeToUpdate] == SE.ENCRYPT_AND_SIGN || writeConfig.config.attributeActionsOnEncrypt[attributeToUpdate] == SE.SIGN_ONLY {
+          expect updateResult.Failure?, "UpdateItem should have failed for signed item.";
+          // This error is of type DynamoDbEncryptionTransformsException
+          // but AWS SDK wraps it into its own type for which customers should be unwrapping.
+          // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
+          expect updateResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+          var hasDynamoDbEncryptionTransformsException? := String.HasSubString(updateResult.error.objMessage, "Update Expressions forbidden on signed attributes");
+          expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
+        } else {
+          expect updateResult.Success?;
+        }
+      }
+    }
+
+    method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string)
+    {
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
+      WriteAllRecords(wClient, records);
+      // Try to delete records with a condition expression with condition to
+      // delete records if the record has an attribute attributeToDelete with value expectedAttributeValue
+      for i := 0 to |records| {
+        // Set up condition expression to only delete if Two = expectedAttributeValue
+        var conditionExpr := "#attr = :val";
+        var exprAttrNames := map["#attr" := attributeToDelete];
+        var exprAttrValues := map[":val" := DDB.AttributeValue.S(expectedAttributeValue)];
+        expect HashName in records[i].item, "`HashName` is not in records.";
+        var deleteInput := DDB.DeleteItemInput(
+          TableName := TableName,
+          Key := map[HashName := records[i].item[HashName]],
+          ConditionExpression := Some(conditionExpr),
+          ExpressionAttributeNames := Some(exprAttrNames),
+          ExpressionAttributeValues := Some(exprAttrValues),
+          ReturnValues := Some(DDB.ReturnValue.ALL_OLD)
+        );
+        var deleteResult := wClient.DeleteItem(deleteInput);
+        expect attributeToDelete in writeConfig.config.attributeActionsOnEncrypt, "`attributeToDelete` not found in attributeActionsOnEncrypt of config.";
+        if writeConfig.config.attributeActionsOnEncrypt[attributeToDelete] == SE.ENCRYPT_AND_SIGN {
+          expect deleteResult.Failure?, "DeleteItem should have failed.";
+          // This error is of type DynamoDbEncryptionTransformsException
+          // but AWS SDK wraps it into its own type for which customers should be unwrapping.
+          // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
+          expect deleteResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+          var hasDynamoDbEncryptionTransformsException? := String.HasSubString(deleteResult.error.objMessage, "Condition Expressions forbidden on encrypted attributes");
+          expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
+        } else if attributeToDelete in records[i].item && records[i].item[attributeToDelete].S? && records[i].item[attributeToDelete].S == expectedAttributeValue {
+          expect deleteResult.Success?, "DeleteItem should have succeeded.";
+          expect deleteResult.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput";
+          expect HashName in deleteResult.value.Attributes.value, "Deleted item does not have right partition key:" + HashName;
+          expect deleteResult.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted.";
+        } else {
+          expect deleteResult.Failure?, "DeleteItem should have failed.";
+          expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException";
+        }
+      }
+    }
+
+    method BasicIoTestDeleteItemWithoutConditionExpression(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string)
+    {
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
+      WriteAllRecords(wClient, 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]],
+          ReturnValues := Some(DDB.ReturnValue.ALL_OLD)
+        );
+        var deleteResultForWithoutConditionExpressionCase := wClient.DeleteItem(deleteInputWithoutConditionExpression);
+        expect deleteResultForWithoutConditionExpressionCase.Success?, "DeleteItem should have succeeded.";
+        expect deleteResultForWithoutConditionExpressionCase.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput";
+        if attributeToDelete in records[i].item {
+          expect HashName in deleteResultForWithoutConditionExpressionCase.value.Attributes.value, "Deleted item does not have right partition key:" + HashName;
+          expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted.";
+        }
+      }
+    }
+
     method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
     {
       var wClient, rClient := SetupTestTable(writeConfig, readConfig);