Skip to content

Commit c578e37

Browse files
rishav-karanjitrishav-karanjit
authored
Merge branch 'main' into rishav/addUpdateDeleteTest
2 parents b8c918e + 69c37c6 commit c578e37

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;
@@ -927,46 +936,182 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
927936

928937
method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
929938
{
930-
var wClient :- expect newGazelle(writeConfig);
931-
var rClient :- expect newGazelle(readConfig);
932-
DeleteTable(wClient);
933-
var _ :- expect wClient.CreateTable(schemaOnEncrypt);
939+
var wClient, rClient := SetupTestTable(writeConfig, readConfig);
934940

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

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

9721117
method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
@@ -1223,11 +1368,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
12231368
)
12241369
}
12251370

1226-
function MakeCreateTableInput() : DDB.CreateTableInput
1371+
function MakeCreateTableInput(nameonly tableName: DDB.TableName := TableName) : DDB.CreateTableInput
12271372
{
12281373
DDB.CreateTableInput (
12291374
AttributeDefinitions := [DDB.AttributeDefinition(AttributeName := HashName, AttributeType := DDB.ScalarAttributeType.N)],
1230-
TableName := TableName,
1375+
TableName := tableName,
12311376
KeySchema := [DDB.KeySchemaElement(AttributeName := HashName, KeyType := DDB.HASH)],
12321377
LocalSecondaryIndexes := None,
12331378
GlobalSecondaryIndexes := None,

0 commit comments

Comments
 (0)