Skip to content

Commit 0773fe8

Browse files
Add test execute statement
1 parent 97fe459 commit 0773fe8

File tree

1 file changed

+48
-0
lines changed

1 file changed

+48
-0
lines changed

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -382,6 +382,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
382382
BasicIoTestBatchWriteItem(c1, c2, globalRecords);
383383
BasicIoTestPutItem(c1, c2, globalRecords);
384384
BasicIoTestTransactWriteItems(c1, c2, globalRecords);
385+
BasicIoTestExecuteStatement(c1, c2);
385386
}
386387
}
387388

@@ -803,6 +804,53 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
803804
BasicIoTestTransactGetItems(rClient, records);
804805
}
805806

807+
method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
808+
{
809+
var wClient :- expect newGazelle(writeConfig);
810+
var rClient :- expect newGazelle(readConfig);
811+
DeleteTable(wClient);
812+
var _ :- expect wClient.CreateTable(schemaOnEncrypt);
813+
814+
// Create a PartiQL INSERT statement
815+
var insertStatement := CreateInsertStatement(TableName);
816+
var inputForInsertStatement := DDB.ExecuteStatementInput(
817+
Statement := insertStatement,
818+
Parameters := None,
819+
ConsistentRead := None,
820+
NextToken := None,
821+
ReturnConsumedCapacity := None,
822+
Limit := None
823+
);
824+
var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement);
825+
expect resultForInsertStatement.Failure?;
826+
827+
// Create a PartiQL SELECT statement
828+
var selectStatement := CreateSelectStatement(TableName);
829+
var inputForSelectStatement := DDB.ExecuteStatementInput(
830+
Statement := selectStatement,
831+
Parameters := None,
832+
ConsistentRead := Some(true),
833+
NextToken := None,
834+
ReturnConsumedCapacity := None,
835+
Limit := None
836+
);
837+
var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement);
838+
expect resultForSelectStatement.Failure?;
839+
}
840+
841+
function CreateInsertStatement(tableName : string) : string
842+
{
843+
// Convert DynamoDB item to PartiQL INSERT statement
844+
"INSERT INTO \"" + tableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'"
845+
}
846+
847+
function CreateSelectStatement(tableName : string) : string
848+
{
849+
// Create a SELECT statement to retrieve an item by its hash key
850+
// Example: SELECT * FROM "TableName" WHERE id = 1
851+
"SELECT * FROM" + tableName + "WHERE partition_key = 'a' AND sort_key = 'b'"
852+
}
853+
806854
method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
807855
{
808856
var exp := NormalizeItem(expected);

0 commit comments

Comments
 (0)