Skip to content

Commit 8757192

Browse files
rishav-karanjitrishav-karanjit
committed
auto commit
1 parent 9353e17 commit 8757192

File tree

1 file changed

+42
-33
lines changed

1 file changed

+42
-33
lines changed

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

Lines changed: 42 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -95,25 +95,25 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
9595
print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
9696
}
9797

98-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
99-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
100-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
101-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
102-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
103-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
104-
var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
105-
var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors);
106-
var _ :- expect WriteManifest.Write("encrypt.json");
107-
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
108-
var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
109-
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
110-
print "\nRunning no tests\n";
111-
return;
112-
}
98+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
99+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
100+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
101+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
102+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
103+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
104+
// var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
105+
// var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors);
106+
// var _ :- expect WriteManifest.Write("encrypt.json");
107+
// var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
108+
// var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
109+
// if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
110+
// print "\nRunning no tests\n";
111+
// return;
112+
// }
113113
Validate();
114-
StringOrdering();
115-
LargeTests();
116-
PerfQueryTests();
114+
// StringOrdering();
115+
// LargeTests();
116+
// PerfQueryTests();
117117
BasicIoTest();
118118
RunIoTests();
119119
BasicQueryTest();
@@ -853,6 +853,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
853853
var exprAttrNames := map["#pk" := HashName];
854854
var exprAttrValues := map[":val" := DDB.AttributeValue.S(newValue)];
855855

856+
expect HashName in records[i].item, "`HashName` is not in records.";
857+
856858
var updateInput := DDB.UpdateItemInput(
857859
TableName := TableName,
858860
Key := map[HashName := records[i].item[HashName]],
@@ -866,7 +868,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
866868
);
867869

868870
var updateSignedItemResult := wClient.UpdateItem(updateInput);
869-
870871
expect updateSignedItemResult.Failure?, "UpdateItem should have failed for signed item.";
871872
// This error is of type DynamoDbEncryptionTransformsException
872873
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
@@ -880,19 +881,19 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
880881
method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>)
881882
{
882883
var wClient :- expect newGazelle(writeConfig);
883-
print(writeConfig.config.attributeActionsOnEncrypt);
884884
var rClient :- expect newGazelle(readConfig);
885885
DeleteTable(wClient);
886886
WriteAllRecords(wClient, records);
887-
887+
var attributeToDelete := "Two";
888+
var valueToDelete := "Dos";
888889
// Try to delete records with a condition expression with condition to
889-
// delete records if the record has an attribute "Two" with value "Dos"
890+
// delete records if the record has an attribute attributeToDelete with value valueToDelete
890891
for i := 0 to |records| {
891-
// Set up condition expression to only delete if Two = "Dos"
892+
// Set up condition expression to only delete if Two = valueToDelete
892893
var conditionExpr := "#attr = :val";
893-
var exprAttrNames := map["#attr" := "Two"];
894-
var exprAttrValues := map[":val" := DDB.AttributeValue.S("Dos")];
895-
894+
var exprAttrNames := map["#attr" := attributeToDelete];
895+
var exprAttrValues := map[":val" := DDB.AttributeValue.S(valueToDelete)];
896+
expect HashName in records[i].item, "`HashName` is not in records.";
896897
var deleteInput := DDB.DeleteItemInput(
897898
TableName := TableName,
898899
Key := map[HashName := records[i].item[HashName]],
@@ -904,13 +905,21 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
904905
// The delete operation will succeed only if the condition is met
905906
var deleteResult := wClient.DeleteItem(deleteInput);
906907

907-
expect deleteResult.Failure?, "DeleteItem should have failed.";
908-
// This error is of type DynamoDbEncryptionTransformsException
909-
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
910-
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
911-
expect deleteResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
912-
var hasDynamoDbEncryptionTransformsException? := String.HasSubString(deleteResult.error.objMessage, "Condition Expressions forbidden on encrypted attributes");
913-
expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
908+
expect attributeToDelete in writeConfig.config.attributeActionsOnEncrypt, "`attributeToDelete` not found in attributeActionsOnEncrypt of config.";
909+
if writeConfig.config.attributeActionsOnEncrypt[attributeToDelete] == SE.ENCRYPT_AND_SIGN {
910+
expect deleteResult.Failure?, "DeleteItem should have failed.";
911+
// This error is of type DynamoDbEncryptionTransformsException
912+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
913+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
914+
expect deleteResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
915+
var hasDynamoDbEncryptionTransformsException? := String.HasSubString(deleteResult.error.objMessage, "Condition Expressions forbidden on encrypted attributes");
916+
expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
917+
} else if attributeToDelete in records[i].item && records[i].item[attributeToDelete].S? && records[i].item[attributeToDelete].S == valueToDelete {
918+
expect deleteResult.Success?;
919+
} else {
920+
expect deleteResult.Failure?, "DeleteItem should have failed.";
921+
expect deleteResult.error.ConditionalCheckFailedException?;
922+
}
914923
}
915924
}
916925

0 commit comments

Comments
 (0)