Skip to content

Commit 3a81da9

Browse files
auto commit
1 parent 0773fe8 commit 3a81da9

File tree

1 file changed

+5
-15
lines changed

1 file changed

+5
-15
lines changed

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Lines changed: 5 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -812,7 +812,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
812812
var _ :- expect wClient.CreateTable(schemaOnEncrypt);
813813

814814
// Create a PartiQL INSERT statement
815-
var insertStatement := CreateInsertStatement(TableName);
815+
// The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb.
816+
var insertStatement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'";
816817
var inputForInsertStatement := DDB.ExecuteStatementInput(
817818
Statement := insertStatement,
818819
Parameters := None,
@@ -823,9 +824,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
823824
);
824825
var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement);
825826
expect resultForInsertStatement.Failure?;
827+
print(resultForInsertStatement.error);
826828

827829
// Create a PartiQL SELECT statement
828-
var selectStatement := CreateSelectStatement(TableName);
830+
// The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb.
831+
var selectStatement := "SELECT * FROM" + TableName + "WHERE partition_key = 'a' AND sort_key = 'b'";
829832
var inputForSelectStatement := DDB.ExecuteStatementInput(
830833
Statement := selectStatement,
831834
Parameters := None,
@@ -838,19 +841,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
838841
expect resultForSelectStatement.Failure?;
839842
}
840843

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-
854844
method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
855845
{
856846
var exp := NormalizeItem(expected);

0 commit comments

Comments
 (0)