Skip to content

Commit fa7b783

Browse files
rishav-karanjitrishav-karanjit
committed
Merge branch 'rishav/addUpdateDeleteTest' of https://github.com/aws/aws-database-encryption-sdk-dynamodb into rishav/addUpdateDeleteTest
2 parents 4a29b02 + c578e37 commit fa7b783

File tree

1 file changed

+175
-30
lines changed

1 file changed

+175
-30
lines changed

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

Lines changed: 175 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
1919
import opened DynamoDbEncryptionUtil
2020
import opened DdbItemJson
2121
import opened JsonConfig
22+
import StandardLibrary.String
2223

2324
import WriteManifest
2425
import EncryptManifest
@@ -201,12 +202,24 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
201202
}
202203
expect !bad;
203204
}
204-
method DeleteTable(client : DDB.IDynamoDBClient)
205+
method DeleteTable(client : DDB.IDynamoDBClient, nameonly tableName: DDB.TableArn := TableName)
205206
requires client.ValidState()
206207
ensures client.ValidState()
207208
modifies client.Modifies
208209
{
209-
var res := client.DeleteTable(DDB.DeleteTableInput(TableName := TableName));
210+
var res := client.DeleteTable(DDB.DeleteTableInput(TableName := tableName));
211+
}
212+
213+
method SetupTestTable(writeConfig : TableConfig, readConfig : TableConfig, nameonly createTableInput: DDB.CreateTableInput := schemaOnEncrypt)
214+
returns (wClient : DDB.IDynamoDBClient, rClient : DDB.IDynamoDBClient)
215+
ensures wClient.ValidState() && rClient.ValidState()
216+
ensures fresh(wClient) && fresh(wClient.Modifies)
217+
ensures fresh(rClient) && fresh(rClient.Modifies)
218+
{
219+
wClient :- expect newGazelle(writeConfig);
220+
rClient :- expect newGazelle(readConfig);
221+
DeleteTable(client := wClient, tableName := createTableInput.TableName);
222+
var _ :- expect wClient.CreateTable(createTableInput);
210223
}
211224

212225
function GetUsed(q : SimpleQuery) : (DDB.ExpressionAttributeNameMap, DDB.ExpressionAttributeValueMap)
@@ -388,6 +401,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
388401
BasicIoTestUpdateItem(c1, c2, globalRecords, "Two");
389402
BasicIoTestDeleteItem(c1, c2, globalRecords);
390403
BasicIoTestExecuteStatement(c1, c2);
404+
BasicIoTestExecuteTransaction(c1, c2);
405+
BasicIoTestBatchExecuteStatement(c1, c2);
391406
}
392407
}
393408

@@ -742,10 +757,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
742757

743758
method BasicIoTestBatchWriteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>)
744759
{
745-
var wClient :- expect newGazelle(writeConfig);
746-
var rClient :- expect newGazelle(readConfig);
747-
DeleteTable(wClient);
748-
var _ :- expect wClient.CreateTable(schemaOnEncrypt);
760+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
749761
var i := 0;
750762
while i < |records| {
751763
var count := 10;
@@ -781,10 +793,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
781793

782794
method BasicIoTestTransactWriteItems(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>)
783795
{
784-
var wClient :- expect newGazelle(writeConfig);
785-
var rClient :- expect newGazelle(readConfig);
786-
DeleteTable(wClient);
787-
var _ :- expect wClient.CreateTable(schemaOnEncrypt);
796+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
788797
var i := 0;
789798
while i < |records| {
790799
var count := 10;
@@ -930,46 +939,182 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
930939

931940
method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
932941
{
933-
var wClient :- expect newGazelle(writeConfig);
934-
var rClient :- expect newGazelle(readConfig);
935-
DeleteTable(wClient);
936-
var _ :- expect wClient.CreateTable(schemaOnEncrypt);
942+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
937943

938944
// Create a PartiQL INSERT statement
939945
// The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb.
940-
var insertStatement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'";
946+
var insertStatement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'}";
941947
var inputForInsertStatement := DDB.ExecuteStatementInput(
942-
Statement := insertStatement,
943-
Parameters := None,
944-
ConsistentRead := None,
945-
NextToken := None,
946-
ReturnConsumedCapacity := None,
947-
Limit := None
948+
Statement := insertStatement
948949
);
949950
var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement);
950951
expect resultForInsertStatement.Failure?, "ExecuteStatement should have failed";
951952
// This error is of type DynamoDbEncryptionTransformsException
952953
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
953954
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
954955
expect resultForInsertStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
956+
var hasDynamoDbEncryptionTransformsExceptionForInsertStatement? := String.HasSubString(resultForInsertStatement.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
957+
expect hasDynamoDbEncryptionTransformsExceptionForInsertStatement?.Some?;
955958

956959
// Create a PartiQL SELECT statement
957960
// The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb.
958-
var selectStatement := "SELECT * FROM " + TableName + " WHERE partition_key = 'a' AND sort_key = 'b'";
961+
var selectStatement := "SELECT * FROM \"" + TableName + "\" WHERE partition_key = 'a' AND sort_key = 'b'}";
959962
var inputForSelectStatement := DDB.ExecuteStatementInput(
960-
Statement := selectStatement,
961-
Parameters := None,
962-
ConsistentRead := Some(true),
963-
NextToken := None,
964-
ReturnConsumedCapacity := None,
965-
Limit := None
963+
Statement := selectStatement
966964
);
967965
var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement);
968966
expect resultForSelectStatement.Failure?, "ExecuteStatement should have failed";
969967
// This error is of type DynamoDbEncryptionTransformsException
970968
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
971969
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
972970
expect resultForSelectStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
971+
var hasDynamoDbEncryptionTransformsExceptionForSelectStatement? := String.HasSubString(resultForSelectStatement.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
972+
expect hasDynamoDbEncryptionTransformsExceptionForSelectStatement?.Some?;
973+
974+
// Test for unconfigured Table
975+
var unConfiguredTable := "unConfiguredTable";
976+
var _, _ := SetupTestTable(writeConfig, readConfig, createTableInput := MakeCreateTableInput(tableName := unConfiguredTable));
977+
var insertStatementForUnconfiguredTable := "INSERT INTO \"" + unConfiguredTable + "\" VALUE {'" + HashName + "': 0, 'attribute1': 'a'}";
978+
var limit : DDB.PositiveIntegerObject := 5;
979+
var inputInsertStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
980+
Statement := insertStatementForUnconfiguredTable,
981+
Parameters := None,
982+
ConsistentRead := None,
983+
NextToken := None,
984+
ReturnConsumedCapacity := None,
985+
Limit := Some(limit),
986+
ReturnValuesOnConditionCheckFailure := None
987+
);
988+
var insertResultUnconfiguredTable := wClient.ExecuteStatement(inputInsertStatementForUnconfiguredTable);
989+
expect insertResultUnconfiguredTable.Success?;
990+
991+
var selectStatementForUnconfiguredTable := "SELECT * FROM \"" + unConfiguredTable + "\" WHERE " + HashName + " = 0";
992+
var inputSelectStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
993+
Statement := selectStatementForUnconfiguredTable,
994+
Parameters := None,
995+
ConsistentRead := None,
996+
NextToken := None,
997+
ReturnConsumedCapacity := None,
998+
Limit := Some(limit),
999+
ReturnValuesOnConditionCheckFailure := None
1000+
);
1001+
var selectResultUnconfiguredTable := rClient.ExecuteStatement(inputSelectStatementForUnconfiguredTable);
1002+
expect selectResultUnconfiguredTable.Success?;
1003+
1004+
DeleteTable(client := wClient, tableName := unConfiguredTable);
1005+
}
1006+
1007+
method BasicIoTestExecuteTransaction(writeConfig : TableConfig, readConfig : TableConfig)
1008+
{
1009+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
1010+
1011+
// Create a PartiQL transaction with INSERT and SELECT statements
1012+
// The dynamodb attributes are random and non-existent because ExecuteTransaction is supposed to fail before going to dynamodb
1013+
var statements := [
1014+
DDB.ParameterizedStatement(
1015+
Statement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'value1'}",
1016+
Parameters := None
1017+
),
1018+
DDB.ParameterizedStatement(
1019+
Statement := "SELECT * FROM " + TableName + " WHERE partition_key = 'a' AND sort_key = 'b'",
1020+
Parameters := None
1021+
)
1022+
];
1023+
1024+
var inputForTransaction := DDB.ExecuteTransactionInput(
1025+
TransactStatements := statements,
1026+
ClientRequestToken := None
1027+
);
1028+
1029+
// Test with write client
1030+
var resultForWriteTransaction := wClient.ExecuteTransaction(inputForTransaction);
1031+
expect resultForWriteTransaction.Failure?, "ExecuteTransaction should have failed";
1032+
// This error is of type DynamoDbEncryptionTransformsException
1033+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
1034+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
1035+
expect resultForWriteTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
1036+
var hasDynamoDbEncryptionTransformsExceptionForWriteTransaction? := String.HasSubString(resultForWriteTransaction.error.objMessage, "ExecuteTransaction not Supported on encrypted tables.");
1037+
expect hasDynamoDbEncryptionTransformsExceptionForWriteTransaction?.Some?;
1038+
1039+
// Test with read client
1040+
var resultForReadTransaction := rClient.ExecuteTransaction(inputForTransaction);
1041+
expect resultForReadTransaction.Failure?, "ExecuteTransaction should have failed";
1042+
// This error is of type DynamoDbEncryptionTransformsException
1043+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
1044+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
1045+
expect resultForReadTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
1046+
var hasDynamoDbEncryptionTransformsExceptionForReadTransaction? := String.HasSubString(resultForReadTransaction.error.objMessage, "ExecuteTransaction not Supported on encrypted tables.");
1047+
expect hasDynamoDbEncryptionTransformsExceptionForReadTransaction?.Some?;
1048+
}
1049+
1050+
method BasicIoTestBatchExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
1051+
{
1052+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
1053+
1054+
// Create a batch of PartiQL statements
1055+
// The dynamodb attributes are random and non-existent because BatchExecuteStatement is supposed to fail before going into dynamodb
1056+
var statements := [
1057+
DDB.BatchStatementRequest(
1058+
Statement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'value1'}",
1059+
Parameters := None,
1060+
ConsistentRead := None
1061+
),
1062+
DDB.BatchStatementRequest(
1063+
Statement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'c', 'sort_key': 'd', 'attribute1': 'value2'}",
1064+
Parameters := None,
1065+
ConsistentRead := None
1066+
),
1067+
DDB.BatchStatementRequest(
1068+
Statement := "SELECT * FROM " + TableName + " WHERE partition_key = 'a' AND sort_key = 'b'",
1069+
Parameters := None,
1070+
ConsistentRead := Some(true)
1071+
)
1072+
];
1073+
1074+
// Test with write client for batch insert
1075+
var inputForBatchInsert := DDB.BatchExecuteStatementInput(
1076+
Statements := statements[..2], // Just the INSERT statements
1077+
ReturnConsumedCapacity := None
1078+
);
1079+
1080+
var resultForBatchInsert := wClient.BatchExecuteStatement(inputForBatchInsert);
1081+
expect resultForBatchInsert.Failure?, "BatchExecuteStatement for inserts should have failed";
1082+
// This error is of type DynamoDbEncryptionTransformsException
1083+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
1084+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
1085+
expect resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
1086+
var hasDynamoDbEncryptionTransformsExceptionForBatchInsert? := String.HasSubString(resultForBatchInsert.error.objMessage, "BatchExecuteStatement not Supported on encrypted tables.");
1087+
expect hasDynamoDbEncryptionTransformsExceptionForBatchInsert?.Some?;
1088+
1089+
// Test with read client for batch select
1090+
var inputForBatchSelect := DDB.BatchExecuteStatementInput(
1091+
Statements := statements[2..], // Just the SELECT statement
1092+
ReturnConsumedCapacity := None
1093+
);
1094+
1095+
var resultForBatchSelect := rClient.BatchExecuteStatement(inputForBatchSelect);
1096+
expect resultForBatchSelect.Failure?, "BatchExecuteStatement for selects should have failed";
1097+
// This error is of type DynamoDbEncryptionTransformsException
1098+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
1099+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
1100+
expect resultForBatchSelect.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
1101+
var hasDynamoDbEncryptionTransformsExceptionForBatchSelect? := String.HasSubString(resultForBatchSelect.error.objMessage, "BatchExecuteStatement not Supported on encrypted tables.");
1102+
expect hasDynamoDbEncryptionTransformsExceptionForBatchSelect?.Some?;
1103+
1104+
// Test with mixed batch (both inserts and selects)
1105+
var inputForMixedBatch := DDB.BatchExecuteStatementInput(
1106+
Statements := statements, // All statements
1107+
ReturnConsumedCapacity := None
1108+
);
1109+
1110+
var resultForMixedBatch := wClient.BatchExecuteStatement(inputForMixedBatch);
1111+
expect resultForMixedBatch.Failure?, "BatchExecuteStatement for mixed batch should have failed";
1112+
// This error is of type DynamoDbEncryptionTransformsException
1113+
// but AWS SDK wraps it into its own type for which customers should be unwrapping.
1114+
// In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText.
1115+
expect resultForMixedBatch.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
1116+
var hasDynamoDbEncryptionTransformsExceptionForMixedBatch? := String.HasSubString(resultForMixedBatch.error.objMessage, "BatchExecuteStatement not Supported on encrypted tables.");
1117+
expect hasDynamoDbEncryptionTransformsExceptionForMixedBatch?.Some?;
9731118
}
9741119

9751120
method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
@@ -1226,11 +1371,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
12261371
)
12271372
}
12281373

1229-
function MakeCreateTableInput() : DDB.CreateTableInput
1374+
function MakeCreateTableInput(nameonly tableName: DDB.TableName := TableName) : DDB.CreateTableInput
12301375
{
12311376
DDB.CreateTableInput (
12321377
AttributeDefinitions := [DDB.AttributeDefinition(AttributeName := HashName, AttributeType := DDB.ScalarAttributeType.N)],
1233-
TableName := TableName,
1378+
TableName := tableName,
12341379
KeySchema := [DDB.KeySchemaElement(AttributeName := HashName, KeyType := DDB.HASH)],
12351380
LocalSecondaryIndexes := None,
12361381
GlobalSecondaryIndexes := None,

0 commit comments

Comments
 (0)