From 482e76b2820acf1a3e49692e915121a68ea23e93 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 11 Jun 2025 13:47:39 -0700 Subject: [PATCH 01/19] Update and delete test: --- .../dafny/DDBEncryption/src/TestVectors.dfy | 104 ++++++++++++++++++ 1 file changed, 104 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index d89a90d7a..213425de0 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -384,6 +384,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestBatchWriteItem(c1, c2, globalRecords); BasicIoTestPutItem(c1, c2, globalRecords); BasicIoTestTransactWriteItems(c1, c2, globalRecords); + BasicIoTestUpdateItem(c1, c2, globalRecords); + BasicIoTestDeleteItem(c1, c2, globalRecords); BasicIoTestExecuteStatement(c1, c2); } } @@ -835,6 +837,108 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestTransactGetItems(rClient, records); } + method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq) + { + var wClient :- expect newGazelle(writeConfig); + var rClient :- expect newGazelle(readConfig); + WriteAllRecords(wClient, records); + + // Update each record by appending "-updated" to the partition key + for i := 0 to |records| { + :- expect Need(HashName in records[i].item, ""); + + // Get the current value of the partition key + var currentValue; + currentValue := records[i].item[HashName].N; + + // Append "-updated" to the current value + var newValue := currentValue + "-updated"; + + // Create an update expression to update the partition key + var updateExpr := "SET #pk = :val"; + var exprAttrNames := map["#pk" := HashName]; + var exprAttrValues := map[":val" := DDB.AttributeValue.S(newValue)]; + + 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 updateSignedItemResult := wClient.UpdateItem(updateInput); + + expect updateSignedItemResult.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 updateSignedItemResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; + var hasDynamoDbEncryptionTransformsException? := String.HasSubString(updateSignedItemResult.error.objMessage, "Update Expressions forbidden on signed attributes"); + expect hasDynamoDbEncryptionTransformsException?.Some?; + } + } + + method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq) + { + var wClient :- expect newGazelle(writeConfig); + var rClient :- expect newGazelle(readConfig); + WriteAllRecords(wClient, records); + + // Only delete half of the records to verify selective deletion + var deleteCount := |records| / 2; + + for i := 0 to deleteCount { + :- expect Need(HashName in records[i].item, ""); + + var deleteInput := DDB.DeleteItemInput( + TableName := TableName, + Key := map[HashName := records[i].item[HashName]], + Expected := None, + ReturnValues := None, + ReturnConsumedCapacity := None, + ReturnItemCollectionMetrics := None, + ConditionExpression := None, + ExpressionAttributeNames := None, + ExpressionAttributeValues := None + ); + + var _ :- expect wClient.DeleteItem(deleteInput); + } + + // Verify deletions were successful + for i := 0 to |records| { + :- expect Need(HashName in records[i].item, ""); + + var getInput := DDB.GetItemInput( + TableName := TableName, + Key := map[HashName := records[i].item[HashName]], + AttributesToGet := None, + ConsistentRead := None, + ReturnConsumedCapacity := None, + ProjectionExpression := None, + ExpressionAttributeNames := None + ); + + var out := rClient.GetItem(getInput); + + if i < deleteCount { + // Deleted items should not be found + expect out.Success?; + expect out.value.Item.None?, "Item " + String.Base10Int2String(i) + " should have been deleted"; + } else { + // Non-deleted items should still exist + expect out.Success?; + expect out.value.Item.Some?; + expect NormalizeItem(out.value.Item.value) == NormalizeItem(records[i].item); + } + } + } + method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig) { var wClient :- expect newGazelle(writeConfig); From 7210baf886797dfb18d1669114c835ef1abb20cc Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 11 Jun 2025 16:20:19 -0700 Subject: [PATCH 02/19] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 66 +++++++------------ 1 file changed, 23 insertions(+), 43 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 213425de0..e01f48be5 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -841,12 +841,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { { var wClient :- expect newGazelle(writeConfig); var rClient :- expect newGazelle(readConfig); + DeleteTable(wClient); WriteAllRecords(wClient, records); // Update each record by appending "-updated" to the partition key for i := 0 to |records| { - :- expect Need(HashName in records[i].item, ""); - // Get the current value of the partition key var currentValue; currentValue := records[i].item[HashName].N; @@ -879,7 +878,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText. expect updateSignedItemResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; var hasDynamoDbEncryptionTransformsException? := String.HasSubString(updateSignedItemResult.error.objMessage, "Update Expressions forbidden on signed attributes"); - expect hasDynamoDbEncryptionTransformsException?.Some?; + expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException"; } } @@ -887,55 +886,36 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { { var wClient :- expect newGazelle(writeConfig); var rClient :- expect newGazelle(readConfig); + DeleteTable(wClient); WriteAllRecords(wClient, records); - // Only delete half of the records to verify selective deletion - var deleteCount := |records| / 2; - - for i := 0 to deleteCount { - :- expect Need(HashName in records[i].item, ""); - - var deleteInput := DDB.DeleteItemInput( - TableName := TableName, - Key := map[HashName := records[i].item[HashName]], - Expected := None, - ReturnValues := None, - ReturnConsumedCapacity := None, - ReturnItemCollectionMetrics := None, - ConditionExpression := None, - ExpressionAttributeNames := None, - ExpressionAttributeValues := None - ); - - var _ :- expect wClient.DeleteItem(deleteInput); - } - - // Verify deletions were successful + // Try to delete records with a condition expression with condition to + // delete records if the record has an attribute "randomAttribute" with value "random" + // These are random attribute and value because we conditional expression should fail before going into dynamodb. for i := 0 to |records| { - :- expect Need(HashName in records[i].item, ""); + // Set up condition expression to only delete if randomAttribute = "random" + var conditionExpr := "#attr = :val"; + var exprAttrNames := map["#attr" := "randomAttribute"]; + var exprAttrValues := map[":val" := DDB.AttributeValue.S("random")]; - var getInput := DDB.GetItemInput( + var deleteInput := DDB.DeleteItemInput( TableName := TableName, Key := map[HashName := records[i].item[HashName]], - AttributesToGet := None, - ConsistentRead := None, - ReturnConsumedCapacity := None, - ProjectionExpression := None, - ExpressionAttributeNames := None + ConditionExpression := Some(conditionExpr), + ExpressionAttributeNames := Some(exprAttrNames), + ExpressionAttributeValues := Some(exprAttrValues) ); - var out := rClient.GetItem(getInput); + // The delete operation will succeed only if the condition is met + var deleteResult := wClient.DeleteItem(deleteInput); - if i < deleteCount { - // Deleted items should not be found - expect out.Success?; - expect out.value.Item.None?, "Item " + String.Base10Int2String(i) + " should have been deleted"; - } else { - // Non-deleted items should still exist - expect out.Success?; - expect out.value.Item.Some?; - expect NormalizeItem(out.value.Item.value) == NormalizeItem(records[i].item); - } + 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"; } } From 9353e171a38a4bf1c105f817f5812df7f449ee2c Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 11 Jun 2025 17:23:46 -0700 Subject: [PATCH 03/19] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index e01f48be5..9fc57ccc1 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -846,12 +846,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { // Update each record by appending "-updated" to the partition key for i := 0 to |records| { - // Get the current value of the partition key - var currentValue; - currentValue := records[i].item[HashName].N; - - // Append "-updated" to the current value - var newValue := currentValue + "-updated"; + var newValue := "updated"; // Create an update expression to update the partition key var updateExpr := "SET #pk = :val"; @@ -885,18 +880,18 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq) { var wClient :- expect newGazelle(writeConfig); + print(writeConfig.config.attributeActionsOnEncrypt); var rClient :- expect newGazelle(readConfig); DeleteTable(wClient); WriteAllRecords(wClient, records); // Try to delete records with a condition expression with condition to - // delete records if the record has an attribute "randomAttribute" with value "random" - // These are random attribute and value because we conditional expression should fail before going into dynamodb. + // delete records if the record has an attribute "Two" with value "Dos" for i := 0 to |records| { - // Set up condition expression to only delete if randomAttribute = "random" + // Set up condition expression to only delete if Two = "Dos" var conditionExpr := "#attr = :val"; - var exprAttrNames := map["#attr" := "randomAttribute"]; - var exprAttrValues := map[":val" := DDB.AttributeValue.S("random")]; + var exprAttrNames := map["#attr" := "Two"]; + var exprAttrValues := map[":val" := DDB.AttributeValue.S("Dos")]; var deleteInput := DDB.DeleteItemInput( TableName := TableName, From 8757192a8efee4e095f5e72ba4f71bb689d8833f Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 12 Jun 2025 10:32:03 -0700 Subject: [PATCH 04/19] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 75 +++++++++++-------- 1 file changed, 42 insertions(+), 33 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 9fc57ccc1..f36a30e6b 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -95,25 +95,25 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; } - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors); - var _ :- expect WriteManifest.Write("encrypt.json"); - var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); - var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); - if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { - print "\nRunning no tests\n"; - return; - } + // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors); + // var _ :- expect WriteManifest.Write("encrypt.json"); + // var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); + // var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); + // if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { + // print "\nRunning no tests\n"; + // return; + // } Validate(); - StringOrdering(); - LargeTests(); - PerfQueryTests(); + // StringOrdering(); + // LargeTests(); + // PerfQueryTests(); BasicIoTest(); RunIoTests(); BasicQueryTest(); @@ -853,6 +853,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var exprAttrNames := map["#pk" := HashName]; 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]], @@ -866,7 +868,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var updateSignedItemResult := wClient.UpdateItem(updateInput); - expect updateSignedItemResult.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. @@ -880,19 +881,19 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq) { var wClient :- expect newGazelle(writeConfig); - print(writeConfig.config.attributeActionsOnEncrypt); var rClient :- expect newGazelle(readConfig); DeleteTable(wClient); WriteAllRecords(wClient, records); - + var attributeToDelete := "Two"; + var valueToDelete := "Dos"; // Try to delete records with a condition expression with condition to - // delete records if the record has an attribute "Two" with value "Dos" + // delete records if the record has an attribute attributeToDelete with value valueToDelete for i := 0 to |records| { - // Set up condition expression to only delete if Two = "Dos" + // Set up condition expression to only delete if Two = valueToDelete var conditionExpr := "#attr = :val"; - var exprAttrNames := map["#attr" := "Two"]; - var exprAttrValues := map[":val" := DDB.AttributeValue.S("Dos")]; - + var exprAttrNames := map["#attr" := attributeToDelete]; + var exprAttrValues := map[":val" := DDB.AttributeValue.S(valueToDelete)]; + expect HashName in records[i].item, "`HashName` is not in records."; var deleteInput := DDB.DeleteItemInput( TableName := TableName, Key := map[HashName := records[i].item[HashName]], @@ -904,13 +905,21 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { // The delete operation will succeed only if the condition is met var deleteResult := wClient.DeleteItem(deleteInput); - 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"; + 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 == valueToDelete { + expect deleteResult.Success?; + } else { + expect deleteResult.Failure?, "DeleteItem should have failed."; + expect deleteResult.error.ConditionalCheckFailedException?; + } } } From f185c1ef46f4b78edad9a7edac449d0a30da0335 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 12 Jun 2025 15:53:45 -0700 Subject: [PATCH 05/19] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 38 +++++++++---------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index f36a30e6b..cde7419e8 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -95,25 +95,25 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; } - // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors); - // var _ :- expect WriteManifest.Write("encrypt.json"); - // var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); - // var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); - // if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { - // print "\nRunning no tests\n"; - // return; - // } + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors); + var _ :- expect WriteManifest.Write("encrypt.json"); + var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); + if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { + print "\nRunning no tests\n"; + return; + } Validate(); - // StringOrdering(); - // LargeTests(); - // PerfQueryTests(); + StringOrdering(); + LargeTests(); + PerfQueryTests(); BasicIoTest(); RunIoTests(); BasicQueryTest(); @@ -844,7 +844,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { DeleteTable(wClient); WriteAllRecords(wClient, records); - // Update each record by appending "-updated" to the partition key + // Update each record by appending "updated" to the partition key for i := 0 to |records| { var newValue := "updated"; From 958232153a723cdb96a08d5b58fbf08e844ec9a8 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 12 Jun 2025 16:24:56 -0700 Subject: [PATCH 06/19] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 34 ++++++++++--------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index cde7419e8..51cb8d0a8 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -384,7 +384,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestBatchWriteItem(c1, c2, globalRecords); BasicIoTestPutItem(c1, c2, globalRecords); BasicIoTestTransactWriteItems(c1, c2, globalRecords); - BasicIoTestUpdateItem(c1, c2, globalRecords); + BasicIoTestUpdateItem(c1, c2, globalRecords, "One"); + BasicIoTestUpdateItem(c1, c2, globalRecords, "Two"); BasicIoTestDeleteItem(c1, c2, globalRecords); BasicIoTestExecuteStatement(c1, c2); } @@ -837,7 +838,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestTransactGetItems(rClient, records); } - method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq) + method {:only} BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToUpdate: DDB.AttributeName) { var wClient :- expect newGazelle(writeConfig); var rClient :- expect newGazelle(readConfig); @@ -847,14 +848,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { // 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 #pk = :val"; - var exprAttrNames := map["#pk" := HashName]; + 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]], @@ -866,15 +865,18 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ReturnItemCollectionMetrics := None, ConditionExpression := None ); - - var updateSignedItemResult := wClient.UpdateItem(updateInput); - expect updateSignedItemResult.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 updateSignedItemResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; - var hasDynamoDbEncryptionTransformsException? := String.HasSubString(updateSignedItemResult.error.objMessage, "Update Expressions forbidden on signed attributes"); - expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException"; + 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?; + } } } From b8c918ec9eabd9d1b185bda73da024a1922e361a Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 13 Jun 2025 10:36:18 -0700 Subject: [PATCH 07/19] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 51cb8d0a8..23f74507b 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -838,7 +838,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestTransactGetItems(rClient, records); } - method {:only} BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToUpdate: DDB.AttributeName) + method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToUpdate: DDB.AttributeName) { var wClient :- expect newGazelle(writeConfig); var rClient :- expect newGazelle(readConfig); From eeee4b3479ba827d1f8c17e2d50247fbe0b7f27e Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 09:29:06 -0700 Subject: [PATCH 08/19] Add ReturnValues --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 23f74507b..b948dbd42 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -901,7 +901,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { Key := map[HashName := records[i].item[HashName]], ConditionExpression := Some(conditionExpr), ExpressionAttributeNames := Some(exprAttrNames), - ExpressionAttributeValues := Some(exprAttrValues) + ExpressionAttributeValues := Some(exprAttrValues), + ReturnValues := Some(DDB.ReturnValue.ALL_OLD) ); // The delete operation will succeed only if the condition is met @@ -918,9 +919,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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 == valueToDelete { expect deleteResult.Success?; + print("\n"); + print(deleteResult); } else { expect deleteResult.Failure?, "DeleteItem should have failed."; - expect deleteResult.error.ConditionalCheckFailedException?; + expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException"; } } } From 4a29b02ed1957d805169407f264828b33f2e6713 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 10:46:47 -0700 Subject: [PATCH 09/19] Add ReturnValues --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index b948dbd42..f676fc45c 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -918,9 +918,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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 == valueToDelete { - expect deleteResult.Success?; - print("\n"); - print(deleteResult); + expect deleteResult.Success?, "DeleteItem should have failed."; + expect deleteResult.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput"; + expect deleteResult.value.Attributes.value == records[i].item, "Wrong item was deleted."; } else { expect deleteResult.Failure?, "DeleteItem should have failed."; expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException"; From 2a9c145952b476109d76170ef3db154202702659 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 11:20:45 -0700 Subject: [PATCH 10/19] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 25 ++++++++----------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 76b0fc8c2..c4a66ed14 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -399,7 +399,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestTransactWriteItems(c1, c2, globalRecords); BasicIoTestUpdateItem(c1, c2, globalRecords, "One"); BasicIoTestUpdateItem(c1, c2, globalRecords, "Two"); - BasicIoTestDeleteItem(c1, c2, globalRecords); + BasicIoTestDeleteItem(c1, c2, globalRecords, "One", "Uno"); + BasicIoTestDeleteItem(c1, c2, globalRecords, "Two", "Dos"); BasicIoTestExecuteStatement(c1, c2); BasicIoTestExecuteTransaction(c1, c2); BasicIoTestBatchExecuteStatement(c1, c2); @@ -849,9 +850,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToUpdate: DDB.AttributeName) { - var wClient :- expect newGazelle(writeConfig); - var rClient :- expect newGazelle(readConfig); - DeleteTable(wClient); + var wClient, rClient := SetupTestTable(writeConfig, readConfig); WriteAllRecords(wClient, records); // Update each record by appending "updated" to the partition key @@ -889,21 +888,19 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } } - method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq) + method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string) { - var wClient :- expect newGazelle(writeConfig); - var rClient :- expect newGazelle(readConfig); - DeleteTable(wClient); + var wClient, rClient := SetupTestTable(writeConfig, readConfig); WriteAllRecords(wClient, records); - var attributeToDelete := "Two"; - var valueToDelete := "Dos"; + // var attributeToDelete := "Two"; + // var valueToDelete := "Dos"; // Try to delete records with a condition expression with condition to - // delete records if the record has an attribute attributeToDelete with value valueToDelete + // 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 = valueToDelete + // 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(valueToDelete)]; + 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, @@ -926,7 +923,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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 == valueToDelete { + } else if attributeToDelete in records[i].item && records[i].item[attributeToDelete].S? && records[i].item[attributeToDelete].S == expectedAttributeValue { expect deleteResult.Success?, "DeleteItem should have failed."; expect deleteResult.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput"; expect deleteResult.value.Attributes.value == records[i].item, "Wrong item was deleted."; From e7c6dd3a7255a5defc867a8b002d0f995d1faa2a Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 11:55:01 -0700 Subject: [PATCH 11/19] remove commented code --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 -- 1 file changed, 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index c4a66ed14..4ccf04e86 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -892,8 +892,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { { var wClient, rClient := SetupTestTable(writeConfig, readConfig); WriteAllRecords(wClient, records); - // var attributeToDelete := "Two"; - // var valueToDelete := "Dos"; // 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| { From cda4f5e10914129a7bf7fef55b228fa58b5a5cbf Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 11:56:20 -0700 Subject: [PATCH 12/19] formatting --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 4 ---- 1 file changed, 4 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 4ccf04e86..5491174c8 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -852,7 +852,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { { 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"; @@ -908,10 +907,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ExpressionAttributeValues := Some(exprAttrValues), ReturnValues := Some(DDB.ReturnValue.ALL_OLD) ); - - // The delete operation will succeed only if the condition is met 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."; From 956f4a861d661b2b2d2610481a1afd605adb83fd Mon Sep 17 00:00:00 2001 From: Rishav karanjit Date: Mon, 16 Jun 2025 14:13:27 -0700 Subject: [PATCH 13/19] Update TestVectors/dafny/DDBEncryption/src/TestVectors.dfy Co-authored-by: Lucas McDonald --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 5491174c8..331fdc567 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -918,7 +918,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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 failed."; + 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 deleteResult.value.Attributes.value == records[i].item, "Wrong item was deleted."; } else { From 93af3cca95bbcccb9fc5af96ae9f75593b78d1b2 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 15:31:20 -0700 Subject: [PATCH 14/19] WithoutConditionExpressionCase --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 5491174c8..8287357d3 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -925,6 +925,16 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { expect deleteResult.Failure?, "DeleteItem should have failed."; expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException"; } + + 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 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."; } } From b79963ff51af78767d38cfca8af3857fd673ad14 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 16:37:36 -0700 Subject: [PATCH 15/19] BasicIoTestDeleteItemWithoutConditionExpression --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 0c821d0bc..92a2a74cf 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -401,6 +401,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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); @@ -925,7 +927,14 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string) + { + var wClient, rClient := SetupTestTable(writeConfig, readConfig); + WriteAllRecords(wClient, records); + for i := 0 to |records| { var deleteInputWithoutConditionExpression := DDB.DeleteItemInput( TableName := TableName, Key := map[HashName := records[i].item[HashName]], From ad60db0a8d7199e0116642c99711aed402bc14d7 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 17:10:50 -0700 Subject: [PATCH 16/19] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 92a2a74cf..762d447a5 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/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."; + } } } From 13a5649fdd23dd13cf40584cd224e29afedebaa4 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 16 Jun 2025 22:32:50 -0700 Subject: [PATCH 17/19] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 762d447a5..d748a0fc8 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -922,7 +922,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } 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 deleteResult.value.Attributes.value == records[i].item, "Wrong item was deleted."; + 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"; @@ -945,7 +945,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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"; if attributeToDelete in records[i].item { - expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value == records[i].item, "Wrong item was deleted."; + expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted."; } } } From ca0b0fb6b5064c516a8a9169251ff52ee4c7f02d Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Tue, 17 Jun 2025 09:14:04 -0700 Subject: [PATCH 18/19] verify --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 ++ 1 file changed, 2 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index d748a0fc8..42a6d7617 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -922,6 +922,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } 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."; @@ -945,6 +946,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { 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"; 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."; } } From f222c89f74ee9d025613dff07554b21efe33a4fd Mon Sep 17 00:00:00 2001 From: Rishav karanjit Date: Fri, 20 Jun 2025 13:23:00 -0700 Subject: [PATCH 19/19] Update TestVectors/dafny/DDBEncryption/src/TestVectors.dfy Co-authored-by: Lucas McDonald --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 42a6d7617..9f1dd7e90 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -943,7 +943,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ReturnValues := Some(DDB.ReturnValue.ALL_OLD) ); var deleteResultForWithoutConditionExpressionCase := wClient.DeleteItem(deleteInputWithoutConditionExpression); - expect deleteResultForWithoutConditionExpressionCase.Success?, "DeleteItem should have failed."; + 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;