From 0773fe8ffbfeffb4e64d5899b7a04373be6a8c08 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 4 Jun 2025 17:27:55 -0700 Subject: [PATCH 1/9] Add test execute statement --- .../dafny/DDBEncryption/src/TestVectors.dfy | 48 +++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 8ed52309d..4088d58a4 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -382,6 +382,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestBatchWriteItem(c1, c2, globalRecords); BasicIoTestPutItem(c1, c2, globalRecords); BasicIoTestTransactWriteItems(c1, c2, globalRecords); + BasicIoTestExecuteStatement(c1, c2); } } @@ -803,6 +804,53 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestTransactGetItems(rClient, records); } + method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig) + { + var wClient :- expect newGazelle(writeConfig); + var rClient :- expect newGazelle(readConfig); + DeleteTable(wClient); + var _ :- expect wClient.CreateTable(schemaOnEncrypt); + + // Create a PartiQL INSERT statement + var insertStatement := CreateInsertStatement(TableName); + var inputForInsertStatement := DDB.ExecuteStatementInput( + Statement := insertStatement, + Parameters := None, + ConsistentRead := None, + NextToken := None, + ReturnConsumedCapacity := None, + Limit := None + ); + var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); + expect resultForInsertStatement.Failure?; + + // Create a PartiQL SELECT statement + var selectStatement := CreateSelectStatement(TableName); + var inputForSelectStatement := DDB.ExecuteStatementInput( + Statement := selectStatement, + Parameters := None, + ConsistentRead := Some(true), + NextToken := None, + ReturnConsumedCapacity := None, + Limit := None + ); + var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); + expect resultForSelectStatement.Failure?; + } + + function CreateInsertStatement(tableName : string) : string + { + // Convert DynamoDB item to PartiQL INSERT statement + "INSERT INTO \"" + tableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'" + } + + function CreateSelectStatement(tableName : string) : string + { + // Create a SELECT statement to retrieve an item by its hash key + // Example: SELECT * FROM "TableName" WHERE id = 1 + "SELECT * FROM" + tableName + "WHERE partition_key = 'a' AND sort_key = 'b'" + } + method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool) { var exp := NormalizeItem(expected); From 3a81da9933e075c3b5fa8283c7f1cdd1cba47080 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 5 Jun 2025 09:32:36 -0700 Subject: [PATCH 2/9] auto commit --- .../dafny/DDBEncryption/src/TestVectors.dfy | 20 +++++-------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 4088d58a4..6fd77c9c6 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -812,7 +812,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var _ :- expect wClient.CreateTable(schemaOnEncrypt); // Create a PartiQL INSERT statement - var insertStatement := CreateInsertStatement(TableName); + // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb. + var insertStatement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'"; var inputForInsertStatement := DDB.ExecuteStatementInput( Statement := insertStatement, Parameters := None, @@ -823,9 +824,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?; + print(resultForInsertStatement.error); // Create a PartiQL SELECT statement - var selectStatement := CreateSelectStatement(TableName); + // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb. + var selectStatement := "SELECT * FROM" + TableName + "WHERE partition_key = 'a' AND sort_key = 'b'"; var inputForSelectStatement := DDB.ExecuteStatementInput( Statement := selectStatement, Parameters := None, @@ -838,19 +841,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { expect resultForSelectStatement.Failure?; } - function CreateInsertStatement(tableName : string) : string - { - // Convert DynamoDB item to PartiQL INSERT statement - "INSERT INTO \"" + tableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'" - } - - function CreateSelectStatement(tableName : string) : string - { - // Create a SELECT statement to retrieve an item by its hash key - // Example: SELECT * FROM "TableName" WHERE id = 1 - "SELECT * FROM" + tableName + "WHERE partition_key = 'a' AND sort_key = 'b'" - } - method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool) { var exp := NormalizeItem(expected); From ec36a25556220fdc95ce81897354638c29aa3f36 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 5 Jun 2025 09:41:19 -0700 Subject: [PATCH 3/9] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 6fd77c9c6..082103e4b 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -824,7 +824,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?; - print(resultForInsertStatement.error); + print(resultForInsertStatement.error.objMessage); // Create a PartiQL SELECT statement // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb. @@ -839,6 +839,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); expect resultForSelectStatement.Failure?; + print(resultForSelectStatement.error.objMessage); } method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool) From 96b9c027ca57caf18dfc2f70586d9b82e3f7277d Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 5 Jun 2025 10:15:32 -0700 Subject: [PATCH 4/9] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index cd0fb7fe7..aa3e654dd 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -854,11 +854,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?; - print(resultForInsertStatement.error.objMessage); + expect resultForInsertStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; // Create a PartiQL SELECT statement // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb. - var selectStatement := "SELECT * FROM" + TableName + "WHERE partition_key = 'a' AND sort_key = 'b'"; + var selectStatement := "SELECT * FROM " + TableName + " WHERE partition_key = 'a' AND sort_key = 'b'"; var inputForSelectStatement := DDB.ExecuteStatementInput( Statement := selectStatement, Parameters := None, @@ -869,7 +869,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); expect resultForSelectStatement.Failure?; - print(resultForSelectStatement.error.objMessage); + expect resultForSelectStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; } method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool) From 1a4901da5153eeae597617767018584fcbac1522 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 5 Jun 2025 10:20:56 -0700 Subject: [PATCH 5/9] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 ++ 1 file changed, 2 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index aa3e654dd..45ac0d45e 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -854,6 +854,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?; + expect resultForInsertStatement.error.OpaqueWithText?; expect resultForInsertStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; // Create a PartiQL SELECT statement @@ -869,6 +870,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); expect resultForSelectStatement.Failure?; + expect resultForSelectStatement.error.OpaqueWithText?; expect resultForSelectStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; } From 1258a3b85d369577641a5c678c112895619a8a38 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 6 Jun 2025 13:21:54 -0700 Subject: [PATCH 6/9] debug code --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 3 +++ 1 file changed, 3 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 45ac0d45e..4d2c5e60b 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -855,6 +855,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?; expect resultForInsertStatement.error.OpaqueWithText?; + print("error message:"); + print(resultForInsertStatement.error.objMessage); + print("\n"); expect resultForInsertStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; // Create a PartiQL SELECT statement From 445d585142719e2c7466450a75017a9503a73bf2 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 6 Jun 2025 15:50:14 -0700 Subject: [PATCH 7/9] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 5 ----- 1 file changed, 5 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 52f7f0f83..d9c4ac0a6 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -856,10 +856,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?; expect resultForInsertStatement.error.OpaqueWithText?; - print("error message:"); - print(resultForInsertStatement.error.objMessage); - print("\n"); - expect resultForInsertStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; // Create a PartiQL SELECT statement // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb. @@ -875,7 +871,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); expect resultForSelectStatement.Failure?; expect resultForSelectStatement.error.OpaqueWithText?; - expect resultForSelectStatement.error.objMessage == "ExecuteStatement not Supported on encrypted tables."; } method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool) From 9b45469c12a933f57ff1a433621b0f193c6d8271 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 6 Jun 2025 16:13:59 -0700 Subject: [PATCH 8/9] auto commit --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index d9c4ac0a6..d37172a1b 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -854,8 +854,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { Limit := None ); var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); - expect resultForInsertStatement.Failure?; - expect resultForInsertStatement.error.OpaqueWithText?; + expect resultForInsertStatement.Failure?, "ExecuteStatement should have failed"; + expect resultForInsertStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; // Create a PartiQL SELECT statement // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb. @@ -869,8 +869,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { Limit := None ); var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); - expect resultForSelectStatement.Failure?; - expect resultForSelectStatement.error.OpaqueWithText?; + expect resultForSelectStatement.Failure?, "ExecuteStatement should have failed"; + expect resultForSelectStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; } method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool) From 06f018cd27e6b87828141c12fa7f85cf88600607 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 9 Jun 2025 09:15:05 -0700 Subject: [PATCH 9/9] Add comments --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index d37172a1b..d89a90d7a 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -855,6 +855,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement); expect resultForInsertStatement.Failure?, "ExecuteStatement should have failed"; + // This error is of type DynamoDbEncryptionTransformsException + // but AWS SDK wraps it into its own type for which customers should be unwrapping. + // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText. expect resultForInsertStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; // Create a PartiQL SELECT statement @@ -870,6 +873,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { ); var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement); expect resultForSelectStatement.Failure?, "ExecuteStatement should have failed"; + // This error is of type DynamoDbEncryptionTransformsException + // but AWS SDK wraps it into its own type for which customers should be unwrapping. + // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText. expect resultForSelectStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; }