Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Sign up
Appearance settings

Commit 3bd48ba

Browse files
chore(dafny): Add Update and delete test (#1942)
1 parent 69c37c6 commit 3bd48ba

File tree

1 file changed

+108
-0
lines changed

1 file changed

+108
-0
lines changed

‎TestVectors/dafny/DDBEncryption/src/TestVectors.dfy‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -397,6 +397,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
397397
BasicIoTestBatchWriteItem(c1, c2, globalRecords);
398398
BasicIoTestPutItem(c1, c2, globalRecords);
399399
BasicIoTestTransactWriteItems(c1, c2, globalRecords);
400+
BasicIoTestUpdateItem(c1, c2, globalRecords, "One");
401+
BasicIoTestUpdateItem(c1, c2, globalRecords, "Two");
402+
BasicIoTestDeleteItem(c1, c2, globalRecords, "One", "Uno");
403+
BasicIoTestDeleteItem(c1, c2, globalRecords, "Two", "Dos");
404+
BasicIoTestDeleteItemWithoutConditionExpression(c1, c2, globalRecords, "One", "Uno");
405+
BasicIoTestDeleteItemWithoutConditionExpression(c1, c2, globalRecords, "Two", "Dos");
400406
BasicIoTestExecuteStatement(c1, c2);
401407
BasicIoTestExecuteTransaction(c1, c2);
402408
BasicIoTestBatchExecuteStatement(c1, c2);
@@ -844,6 +850,108 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
844850
BasicIoTestTransactGetItems(rClient, records);
845851
}
846852

853+
method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>, attributeToUpdate: DDB.AttributeName)
854+
{
855+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
856+
WriteAllRecords(wClient, records);
857+
// Update each record by appending "updated" to the partition key
858+
for i := 0 to |records| {
859+
var newValue := "updated";
860+
// Create an update expression to update the partition key
861+
var updateExpr := "SET #att = :val";
862+
expect attributeToUpdate in writeConfig.config.attributeActionsOnEncrypt, "`attributeToUpdate` not in attributeActionsOnEncrypt";
863+
var exprAttrNames := map["#att" := attributeToUpdate];
864+
var exprAttrValues := map[":val" := DDB.AttributeValue.S(newValue)];
865+
expect HashName in records[i].item, "`HashName` is not in records.";
866+
var updateInput := DDB.UpdateItemInput(
867+
TableName := TableName,
868+
Key := map[HashName := records[i].item[HashName]],
869+
UpdateExpression := Some(updateExpr),
870+
ExpressionAttributeNames := Some(exprAttrNames),
871+
ExpressionAttributeValues := Some(exprAttrValues),
872+
ReturnValues := None,
873+
ReturnConsumedCapacity := None,
874+
ReturnItemCollectionMetrics := None,
875+
ConditionExpression := None
876+
);
877+
var updateResult := wClient.UpdateItem(updateInput);
878+
if writeConfig.config.attributeActionsOnEncrypt[attributeToUpdate] == SE.ENCRYPT_AND_SIGN || writeConfig.config.attributeActionsOnEncrypt[attributeToUpdate] == SE.SIGN_ONLY {
879+
expect updateResult.Failure?, "UpdateItem should have failed for signed item.";
880+
// This error is of type DynamoDbEncryptionTransformsException
881+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
882+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
883+
expect updateResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
884+
var hasDynamoDbEncryptionTransformsException? := String.HasSubString(updateResult.error.objMessage, "Update Expressions forbidden on signed attributes");
885+
expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
886+
} else {
887+
expect updateResult.Success?;
888+
}
889+
}
890+
}
891+
892+
method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string)
893+
{
894+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
895+
WriteAllRecords(wClient, records);
896+
// Try to delete records with a condition expression with condition to
897+
// delete records if the record has an attribute attributeToDelete with value expectedAttributeValue
898+
for i := 0 to |records| {
899+
// Set up condition expression to only delete if Two = expectedAttributeValue
900+
var conditionExpr := "#attr = :val";
901+
var exprAttrNames := map["#attr" := attributeToDelete];
902+
var exprAttrValues := map[":val" := DDB.AttributeValue.S(expectedAttributeValue)];
903+
expect HashName in records[i].item, "`HashName` is not in records.";
904+
var deleteInput := DDB.DeleteItemInput(
905+
TableName := TableName,
906+
Key := map[HashName := records[i].item[HashName]],
907+
ConditionExpression := Some(conditionExpr),
908+
ExpressionAttributeNames := Some(exprAttrNames),
909+
ExpressionAttributeValues := Some(exprAttrValues),
910+
ReturnValues := Some(DDB.ReturnValue.ALL_OLD)
911+
);
912+
var deleteResult := wClient.DeleteItem(deleteInput);
913+
expect attributeToDelete in writeConfig.config.attributeActionsOnEncrypt, "`attributeToDelete` not found in attributeActionsOnEncrypt of config.";
914+
if writeConfig.config.attributeActionsOnEncrypt[attributeToDelete] == SE.ENCRYPT_AND_SIGN {
915+
expect deleteResult.Failure?, "DeleteItem should have failed.";
916+
// This error is of type DynamoDbEncryptionTransformsException
917+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
918+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
919+
expect deleteResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
920+
var hasDynamoDbEncryptionTransformsException? := String.HasSubString(deleteResult.error.objMessage, "Condition Expressions forbidden on encrypted attributes");
921+
expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
922+
} else if attributeToDelete in records[i].item && records[i].item[attributeToDelete].S? && records[i].item[attributeToDelete].S == expectedAttributeValue {
923+
expect deleteResult.Success?, "DeleteItem should have succeeded.";
924+
expect deleteResult.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput";
925+
expect HashName in deleteResult.value.Attributes.value, "Deleted item does not have right partition key:" + HashName;
926+
expect deleteResult.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted.";
927+
} else {
928+
expect deleteResult.Failure?, "DeleteItem should have failed.";
929+
expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException";
930+
}
931+
}
932+
}
933+
934+
method BasicIoTestDeleteItemWithoutConditionExpression(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string)
935+
{
936+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
937+
WriteAllRecords(wClient, records);
938+
for i := 0 to |records| {
939+
expect HashName in records[i].item, "`HashName` is not in records.";
940+
var deleteInputWithoutConditionExpression := DDB.DeleteItemInput(
941+
TableName := TableName,
942+
Key := map[HashName := records[i].item[HashName]],
943+
ReturnValues := Some(DDB.ReturnValue.ALL_OLD)
944+
);
945+
var deleteResultForWithoutConditionExpressionCase := wClient.DeleteItem(deleteInputWithoutConditionExpression);
946+
expect deleteResultForWithoutConditionExpressionCase.Success?, "DeleteItem should have succeeded.";
947+
expect deleteResultForWithoutConditionExpressionCase.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput";
948+
if attributeToDelete in records[i].item {
949+
expect HashName in deleteResultForWithoutConditionExpressionCase.value.Attributes.value, "Deleted item does not have right partition key:" + HashName;
950+
expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted.";
951+
}
952+
}
953+
}
954+
847955
method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
848956
{
849957
var wClient, rClient := SetupTestTable(writeConfig, readConfig);

0 commit comments

Comments
(0)

AltStyle によって変換されたページ (->オリジナル) /