From 0ef416abdd47df610b42030f94f9ecd7fb4f70eb Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 12:14:00 -0700
Subject: [PATCH 01/18] auto commit

---
 .../dafny/DDBEncryption/src/TestVectors.dfy   | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index d89a90d7a..a40c85e54 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -385,6 +385,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         BasicIoTestPutItem(c1, c2, globalRecords);
         BasicIoTestTransactWriteItems(c1, c2, globalRecords);
         BasicIoTestExecuteStatement(c1, c2);
+        BasicIoTestExecuteTransaction(c1, c2);
       }
     }
 
@@ -879,6 +880,47 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       expect resultForSelectStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
     }
 
+    method BasicIoTestExecuteTransaction(writeConfig : TableConfig, readConfig : TableConfig)
+    {
+      var wClient :- expect newGazelle(writeConfig);
+      var rClient :- expect newGazelle(readConfig);
+      DeleteTable(wClient);
+      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+
+      // Create a PartiQL transaction with INSERT and SELECT statements
+      // The dynamodb attributes are random and non-existent because ExecuteTransaction is supposed to fail before going to dynamodb
+      var statements := [
+        DDB.ParameterizedStatement(
+          Statement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'value1'}",
+          Parameters := None
+        ),
+        DDB.ParameterizedStatement(
+          Statement := "SELECT * FROM " + TableName + " WHERE partition_key = 'a' AND sort_key = 'b'",
+          Parameters := None
+        )
+      ];
+
+      var inputForTransaction := DDB.ExecuteTransactionInput(
+        TransactStatements := statements,
+        ClientRequestToken := None
+      );
+
+      // Test with write client
+      var resultForWriteTransaction := wClient.ExecuteTransaction(inputForTransaction);
+      expect resultForWriteTransaction.Failure?, "ExecuteTransaction 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.
+      print(resultForWriteTransaction);
+      expect resultForWriteTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+
+      // Test with read client
+      var resultForReadTransaction := rClient.ExecuteTransaction(inputForTransaction);
+      expect resultForReadTransaction.Failure?, "ExecuteTransaction should have failed";
+      print(resultForReadTransaction);
+      expect resultForReadTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+    }
+
     method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
     {
       var exp := NormalizeItem(expected);

From e3e628067252d59b2cfd2abeb32488b891bdca46 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 12:40:44 -0700
Subject: [PATCH 02/18] Add BasicIoTestBatchExecuteStatement

---
 .../dafny/DDBEncryption/src/TestVectors.dfy   | 68 ++++++++++++++++++-
 1 file changed, 66 insertions(+), 2 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index a40c85e54..6e4de0a3d 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -386,6 +386,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         BasicIoTestTransactWriteItems(c1, c2, globalRecords);
         BasicIoTestExecuteStatement(c1, c2);
         BasicIoTestExecuteTransaction(c1, c2);
+        BasicIoTestBatchExecuteStatement(c1, c2);
       }
     }
 
@@ -911,16 +912,79 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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.
-      print(resultForWriteTransaction);
       expect resultForWriteTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
 
       // Test with read client
       var resultForReadTransaction := rClient.ExecuteTransaction(inputForTransaction);
       expect resultForReadTransaction.Failure?, "ExecuteTransaction should have failed";
-      print(resultForReadTransaction);
+      // 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 resultForReadTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
     }
 
+    method BasicIoTestBatchExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
+    {
+      var wClient :- expect newGazelle(writeConfig);
+      var rClient :- expect newGazelle(readConfig);
+      DeleteTable(wClient);
+      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+
+      // Create a batch of PartiQL statements
+      // The dynamodb attributes are random and non-existent because BatchExecuteStatement is supposed to fail before going into dynamodb
+      var statements := [
+        DDB.BatchStatementRequest(
+          Statement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'value1'}",
+          Parameters := None,
+          ConsistentRead := None
+        ),
+        DDB.BatchStatementRequest(
+          Statement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'c', 'sort_key': 'd', 'attribute1': 'value2'}",
+          Parameters := None,
+          ConsistentRead := None
+        ),
+        DDB.BatchStatementRequest(
+          Statement := "SELECT * FROM " + TableName + " WHERE partition_key = 'a' AND sort_key = 'b'",
+          Parameters := None,
+          ConsistentRead := Some(true)
+        )
+      ];
+
+      // Test with write client for batch insert
+      var inputForBatchInsert := DDB.BatchExecuteStatementInput(
+        Statements := statements[..2],  // Just the INSERT statements
+        ReturnConsumedCapacity := None
+      );
+
+      var resultForBatchInsert := wClient.BatchExecuteStatement(inputForBatchInsert);
+      expect resultForBatchInsert.Failure?, "BatchExecuteStatement for inserts 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 resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+
+      // Test with read client for batch select
+      var inputForBatchSelect := DDB.BatchExecuteStatementInput(
+        Statements := statements[2..],  // Just the SELECT statement
+        ReturnConsumedCapacity := None
+      );
+
+      var resultForBatchSelect := rClient.BatchExecuteStatement(inputForBatchSelect);
+      expect resultForBatchSelect.Failure?, "BatchExecuteStatement for selects should have failed";
+      expect resultForBatchSelect.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+
+      // Test with mixed batch (both inserts and selects)
+      var inputForMixedBatch := DDB.BatchExecuteStatementInput(
+        Statements := statements,  // All statements
+        ReturnConsumedCapacity := None
+      );
+
+      var resultForMixedBatch := wClient.BatchExecuteStatement(inputForMixedBatch);
+      expect resultForMixedBatch.Failure?, "BatchExecuteStatement for mixed batch should have failed";
+      expect resultForMixedBatch.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+    }
+
+
     method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
     {
       var exp := NormalizeItem(expected);

From f47c0bed936f96bfbb042b9b8e148a4c2b6e4892 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 12:42:59 -0700
Subject: [PATCH 03/18] print resultForBatchInsert

---
 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 6e4de0a3d..7ca23f7a4 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -961,6 +961,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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.
+      print("\n resultForBatchInsert: \n");
+      print(resultForBatchInsert);
       expect resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
 
       // Test with read client for batch select

From 9829af564d44ced1783b6aaf07a230c949fc7d3c Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 12:43:23 -0700
Subject: [PATCH 04/18] don't print

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 --
 1 file changed, 2 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 7ca23f7a4..6e4de0a3d 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -961,8 +961,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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.
-      print("\n resultForBatchInsert: \n");
-      print(resultForBatchInsert);
       expect resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
 
       // Test with read client for batch select

From 67ae3caca079727886f44f9c65b405b161726252 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 12:44:06 -0700
Subject: [PATCH 05/18] Revert "don't print"

This reverts commit 9829af564d44ced1783b6aaf07a230c949fc7d3c.
---
 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 6e4de0a3d..7ca23f7a4 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -961,6 +961,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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.
+      print("\n resultForBatchInsert: \n");
+      print(resultForBatchInsert);
       expect resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
 
       // Test with read client for batch select

From bde2f78928d02e278bc0499ec5d48bf81a725a3f Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 12:44:39 -0700
Subject: [PATCH 06/18] Revert "Revert "don't print""

This reverts commit 67ae3caca079727886f44f9c65b405b161726252.
---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 --
 1 file changed, 2 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 7ca23f7a4..6e4de0a3d 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -961,8 +961,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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.
-      print("\n resultForBatchInsert: \n");
-      print(resultForBatchInsert);
       expect resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
 
       // Test with read client for batch select

From a8442bf373654598f7970c79c5541d4915440544 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 13:11:57 -0700
Subject: [PATCH 07/18] auto commit

---
 .../dafny/DDBEncryption/src/TestVectors.dfy   | 37 +++++++++----------
 1 file changed, 17 insertions(+), 20 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 6e4de0a3d..d32799327 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -209,6 +209,18 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       var res := client.DeleteTable(DDB.DeleteTableInput(TableName := TableName));
     }
 
+    method SetupTestTable(writeConfig : TableConfig, readConfig : TableConfig)
+      returns (wClient : DDB.IDynamoDBClient, rClient : DDB.IDynamoDBClient)
+      ensures wClient.ValidState() && rClient.ValidState()
+      ensures fresh(wClient) && fresh(wClient.Modifies)
+      ensures fresh(rClient) && fresh(rClient.Modifies)
+    {
+      wClient :- expect newGazelle(writeConfig);
+      rClient :- expect newGazelle(readConfig);
+      DeleteTable(wClient);
+      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+    }
+
     function GetUsed(q : SimpleQuery) : (DDB.ExpressionAttributeNameMap, DDB.ExpressionAttributeValueMap)
     {
       TrimMaps(q.keyExpr.UnwrapOr(""), q.filterExpr.UnwrapOr(""), names, values)
@@ -741,10 +753,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
     method BasicIoTestBatchWriteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>)
     {
-      var wClient :- expect newGazelle(writeConfig);
-      var rClient :- expect newGazelle(readConfig);
-      DeleteTable(wClient);
-      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
       var i := 0;
       while i < |records| {
         var count := 10;
@@ -780,10 +789,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
     method BasicIoTestTransactWriteItems(writeConfig : TableConfig, readConfig : TableConfig, records : seq<Record>)
     {
-      var wClient :- expect newGazelle(writeConfig);
-      var rClient :- expect newGazelle(readConfig);
-      DeleteTable(wClient);
-      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
       var i := 0;
       while i < |records| {
         var count := 10;
@@ -839,10 +845,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
     method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
     {
-      var wClient :- expect newGazelle(writeConfig);
-      var rClient :- expect newGazelle(readConfig);
-      DeleteTable(wClient);
-      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
 
       // Create a PartiQL INSERT statement
       // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb.
@@ -883,10 +886,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
     method BasicIoTestExecuteTransaction(writeConfig : TableConfig, readConfig : TableConfig)
     {
-      var wClient :- expect newGazelle(writeConfig);
-      var rClient :- expect newGazelle(readConfig);
-      DeleteTable(wClient);
-      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
 
       // Create a PartiQL transaction with INSERT and SELECT statements
       // The dynamodb attributes are random and non-existent because ExecuteTransaction is supposed to fail before going to dynamodb
@@ -925,10 +925,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
     method BasicIoTestBatchExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
     {
-      var wClient :- expect newGazelle(writeConfig);
-      var rClient :- expect newGazelle(readConfig);
-      DeleteTable(wClient);
-      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+      var wClient, rClient := SetupTestTable(writeConfig, readConfig);
 
       // Create a batch of PartiQL statements
       // The dynamodb attributes are random and non-existent because BatchExecuteStatement is supposed to fail before going into dynamodb

From 6719ef13cc98b2257b9dede657f9f095c0a5a34f Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 13:19:11 -0700
Subject: [PATCH 08/18] auto commit

---
 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 d32799327..1687a1f96 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -968,6 +968,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
       var resultForBatchSelect := rClient.BatchExecuteStatement(inputForBatchSelect);
       expect resultForBatchSelect.Failure?, "BatchExecuteStatement for selects 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 resultForBatchSelect.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
 
       // Test with mixed batch (both inserts and selects)
@@ -978,6 +981,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
       var resultForMixedBatch := wClient.BatchExecuteStatement(inputForMixedBatch);
       expect resultForMixedBatch.Failure?, "BatchExecuteStatement for mixed batch 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 resultForMixedBatch.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
     }
 

From 1f0c6bc089d359c4ee06960998791c3e3338527a Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 13:37:13 -0700
Subject: [PATCH 09/18] check substring

---
 .../dafny/DDBEncryption/src/TestVectors.dfy       | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 1687a1f96..453854f97 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -19,6 +19,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import opened DynamoDbEncryptionUtil
   import opened DdbItemJson
   import opened JsonConfig
+  import StandardLibrary.String
 
   import WriteManifest
   import EncryptManifest
@@ -864,6 +865,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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";
+      var hasDynamoDbEncryptionTransformsExceptionForInsertStatement? := String.HasSubString(resultForInsertStatement.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForInsertStatement?.Some?;
 
       // Create a PartiQL SELECT statement
       // The dynamodb attributes are random and non-existent because ExecuteStatement is supposed to be failed before going into dynamodb.
@@ -882,6 +885,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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";
+      var hasDynamoDbEncryptionTransformsExceptionForSelectStatement? := String.HasSubString(resultForSelectStatement.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForSelectStatement?.Some?;
     }
 
     method BasicIoTestExecuteTransaction(writeConfig : TableConfig, readConfig : TableConfig)
@@ -913,6 +918,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForWriteTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+      var hasDynamoDbEncryptionTransformsExceptionForWriteTransaction? := String.HasSubString(resultForWriteTransaction.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForWriteTransaction?.Some?;
 
       // Test with read client
       var resultForReadTransaction := rClient.ExecuteTransaction(inputForTransaction);
@@ -921,6 +928,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForReadTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+      var hasDynamoDbEncryptionTransformsExceptionForReadTransaction? := String.HasSubString(resultForReadTransaction.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForReadTransaction?.Some?;
     }
 
     method BasicIoTestBatchExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig)
@@ -959,6 +968,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+      var hasDynamoDbEncryptionTransformsExceptionForBatchInsert? := String.HasSubString(resultForBatchInsert.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForBatchInsert?.Some?;
 
       // Test with read client for batch select
       var inputForBatchSelect := DDB.BatchExecuteStatementInput(
@@ -972,6 +983,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForBatchSelect.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+      var hasDynamoDbEncryptionTransformsExceptionForBatchSelect? := String.HasSubString(resultForBatchSelect.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForBatchSelect?.Some?;
 
       // Test with mixed batch (both inserts and selects)
       var inputForMixedBatch := DDB.BatchExecuteStatementInput(
@@ -985,6 +998,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForMixedBatch.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
+      var hasDynamoDbEncryptionTransformsExceptionForMixedBatch? := String.HasSubString(resultForMixedBatch.error.objMessage, "DynamoDbEncryptionTransformsException");
+      expect hasDynamoDbEncryptionTransformsExceptionForMixedBatch?.Some?;
     }
 
 

From 711dac5e91fd52ffc447f754826aaeab4ba3fb6e Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 14:06:41 -0700
Subject: [PATCH 10/18] auto commit

---
 .../dafny/DDBEncryption/src/TestVectors.dfy        | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 453854f97..be3ade5c2 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -865,7 +865,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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";
-      var hasDynamoDbEncryptionTransformsExceptionForInsertStatement? := String.HasSubString(resultForInsertStatement.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForInsertStatement? := String.HasSubString(resultForInsertStatement.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForInsertStatement?.Some?;
 
       // Create a PartiQL SELECT statement
@@ -885,7 +885,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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";
-      var hasDynamoDbEncryptionTransformsExceptionForSelectStatement? := String.HasSubString(resultForSelectStatement.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForSelectStatement? := String.HasSubString(resultForSelectStatement.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForSelectStatement?.Some?;
     }
 
@@ -918,7 +918,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForWriteTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForWriteTransaction? := String.HasSubString(resultForWriteTransaction.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForWriteTransaction? := String.HasSubString(resultForWriteTransaction.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForWriteTransaction?.Some?;
 
       // Test with read client
@@ -928,7 +928,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForReadTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForReadTransaction? := String.HasSubString(resultForReadTransaction.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForReadTransaction? := String.HasSubString(resultForReadTransaction.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForReadTransaction?.Some?;
     }
 
@@ -968,7 +968,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForBatchInsert? := String.HasSubString(resultForBatchInsert.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForBatchInsert? := String.HasSubString(resultForBatchInsert.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForBatchInsert?.Some?;
 
       // Test with read client for batch select
@@ -983,7 +983,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForBatchSelect.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForBatchSelect? := String.HasSubString(resultForBatchSelect.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForBatchSelect? := String.HasSubString(resultForBatchSelect.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForBatchSelect?.Some?;
 
       // Test with mixed batch (both inserts and selects)
@@ -998,7 +998,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForMixedBatch.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForMixedBatch? := String.HasSubString(resultForMixedBatch.error.objMessage, "DynamoDbEncryptionTransformsException");
+      var hasDynamoDbEncryptionTransformsExceptionForMixedBatch? := String.HasSubString(resultForMixedBatch.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForMixedBatch?.Some?;
     }
 

From 093085baaaf24a06f92f849ea563484ab14358ed Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Tue, 10 Jun 2025 17:37:50 -0700
Subject: [PATCH 11/18] fix error substring check

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index be3ade5c2..795f0806b 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -918,7 +918,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForWriteTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForWriteTransaction? := String.HasSubString(resultForWriteTransaction.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
+      var hasDynamoDbEncryptionTransformsExceptionForWriteTransaction? := String.HasSubString(resultForWriteTransaction.error.objMessage, "ExecuteTransaction not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForWriteTransaction?.Some?;
 
       // Test with read client
@@ -928,7 +928,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForReadTransaction.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForReadTransaction? := String.HasSubString(resultForReadTransaction.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
+      var hasDynamoDbEncryptionTransformsExceptionForReadTransaction? := String.HasSubString(resultForReadTransaction.error.objMessage, "ExecuteTransaction not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForReadTransaction?.Some?;
     }
 
@@ -968,7 +968,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForBatchInsert.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForBatchInsert? := String.HasSubString(resultForBatchInsert.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
+      var hasDynamoDbEncryptionTransformsExceptionForBatchInsert? := String.HasSubString(resultForBatchInsert.error.objMessage, "BatchExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForBatchInsert?.Some?;
 
       // Test with read client for batch select
@@ -983,7 +983,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForBatchSelect.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForBatchSelect? := String.HasSubString(resultForBatchSelect.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
+      var hasDynamoDbEncryptionTransformsExceptionForBatchSelect? := String.HasSubString(resultForBatchSelect.error.objMessage, "BatchExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForBatchSelect?.Some?;
 
       // Test with mixed batch (both inserts and selects)
@@ -998,7 +998,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       // 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 resultForMixedBatch.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
-      var hasDynamoDbEncryptionTransformsExceptionForMixedBatch? := String.HasSubString(resultForMixedBatch.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
+      var hasDynamoDbEncryptionTransformsExceptionForMixedBatch? := String.HasSubString(resultForMixedBatch.error.objMessage, "BatchExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForMixedBatch?.Some?;
     }
 

From 295e8fd2aa213e1777b92ab7d03dd8445b8651b8 Mon Sep 17 00:00:00 2001
From: Rishav karanjit <karanjitrishav4@gmail.com>
Date: Tue, 10 Jun 2025 21:07:08 -0700
Subject: [PATCH 12/18] Remove extra line

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 1 -
 1 file changed, 1 deletion(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 795f0806b..9016c1ce9 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -1002,7 +1002,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       expect hasDynamoDbEncryptionTransformsExceptionForMixedBatch?.Some?;
     }
 
-
     method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
     {
       var exp := NormalizeItem(expected);

From a0b9fb8be76519691d3f0b24e246250b6a679460 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Thu, 12 Jun 2025 14:27:04 -0700
Subject: [PATCH 13/18] Test for unconfigured table

---
 .../dafny/DDBEncryption/src/TestVectors.dfy   | 51 +++++++++++--------
 1 file changed, 30 insertions(+), 21 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 795f0806b..eaf838bca 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -202,15 +202,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       }
       expect !bad;
     }
-    method DeleteTable(client : DDB.IDynamoDBClient)
+    method DeleteTable(client : DDB.IDynamoDBClient, nameonly tableName: DDB.TableArn := TableName)
       requires client.ValidState()
       ensures client.ValidState()
       modifies client.Modifies
     {
-      var res := client.DeleteTable(DDB.DeleteTableInput(TableName := TableName));
+      var res := client.DeleteTable(DDB.DeleteTableInput(TableName := tableName));
     }
 
-    method SetupTestTable(writeConfig : TableConfig, readConfig : TableConfig)
+    method SetupTestTable(writeConfig : TableConfig, readConfig : TableConfig, nameonly createTableInput: DDB.CreateTableInput := schemaOnEncrypt)
       returns (wClient : DDB.IDynamoDBClient, rClient : DDB.IDynamoDBClient)
       ensures wClient.ValidState() && rClient.ValidState()
       ensures fresh(wClient) && fresh(wClient.Modifies)
@@ -218,8 +218,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
     {
       wClient :- expect newGazelle(writeConfig);
       rClient :- expect newGazelle(readConfig);
-      DeleteTable(wClient);
-      var _ :-  expect wClient.CreateTable(schemaOnEncrypt);
+      DeleteTable(client := wClient, tableName := createTableInput.TableName);
+      var _ :-  expect wClient.CreateTable(createTableInput);
     }
 
     function GetUsed(q : SimpleQuery) : (DDB.ExpressionAttributeNameMap, DDB.ExpressionAttributeValueMap)
@@ -850,14 +850,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
       // Create a PartiQL INSERT statement
       // 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 insertStatement := "INSERT INTO \"" + TableName + "\" VALUE {'partition_key': 'a', 'sort_key': 'b', 'attribute1': 'a'}";
       var inputForInsertStatement := DDB.ExecuteStatementInput(
-        Statement := insertStatement,
-        Parameters := None,
-        ConsistentRead := None,
-        NextToken := None,
-        ReturnConsumedCapacity := None,
-        Limit := None
+        Statement := insertStatement
       );
       var resultForInsertStatement := wClient.ExecuteStatement(inputForInsertStatement);
       expect resultForInsertStatement.Failure?, "ExecuteStatement should have failed";
@@ -870,14 +865,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
 
       // 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,
-        ConsistentRead := Some(true),
-        NextToken := None,
-        ReturnConsumedCapacity := None,
-        Limit := None
+        Statement := selectStatement
       );
       var resultForSelectStatement := rClient.ExecuteStatement(inputForSelectStatement);
       expect resultForSelectStatement.Failure?, "ExecuteStatement should have failed";
@@ -887,6 +877,25 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       expect resultForSelectStatement.error.OpaqueWithText?, "Error should have been of type OpaqueWithText";
       var hasDynamoDbEncryptionTransformsExceptionForSelectStatement? := String.HasSubString(resultForSelectStatement.error.objMessage, "ExecuteStatement not Supported on encrypted tables.");
       expect hasDynamoDbEncryptionTransformsExceptionForSelectStatement?.Some?;
+
+      // Test for unconfigured Table
+      var unConfiguredTable := "unConfiguredTable";
+      var _, _ := SetupTestTable(writeConfig, readConfig, createTableInput := MakeCreateTableInput(tableName := unConfiguredTable));
+      var insertStatementForUnconfiguredTable := "INSERT INTO \"" + unConfiguredTable + "\" VALUE {'" + HashName + "': 0, 'attribute1': 'a'}";
+      var inputInsertStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
+        Statement := insertStatementForUnconfiguredTable
+      );
+      var insertResultUnconfiguredTable := wClient.ExecuteStatement(inputInsertStatementForUnconfiguredTable);
+      expect insertResultUnconfiguredTable.Success?;
+
+      var selectStatementForUnconfiguredTable := "SELECT * FROM \"" + unConfiguredTable + "\" WHERE " + HashName + " = 0";
+      var inputSelectStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
+        Statement := selectStatementForUnconfiguredTable
+      );
+      var selectResultUnconfiguredTable := rClient.ExecuteStatement(inputSelectStatementForUnconfiguredTable);
+      selectResultUnconfiguredTable.Success?;
+
+      DeleteTable(client := wClient, tableName := unConfiguredTable);
     }
 
     method BasicIoTestExecuteTransaction(writeConfig : TableConfig, readConfig : TableConfig)
@@ -1257,11 +1266,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       )
   }
 
-  function MakeCreateTableInput() : DDB.CreateTableInput
+  function MakeCreateTableInput(nameonly tableName: DDB.TableName := TableName) : DDB.CreateTableInput
   {
     DDB.CreateTableInput (
       AttributeDefinitions := [DDB.AttributeDefinition(AttributeName := HashName, AttributeType := DDB.ScalarAttributeType.N)],
-      TableName := TableName,
+      TableName := tableName,
       KeySchema := [DDB.KeySchemaElement(AttributeName := HashName, KeyType := DDB.HASH)],
       LocalSecondaryIndexes := None,
       GlobalSecondaryIndexes := None,

From ae6659878fe12934a31fc03aaf5684d0cf09430c Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Thu, 12 Jun 2025 15:33:06 -0700
Subject: [PATCH 14/18] auto commit

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 2a820a830..341fa2921 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -893,7 +893,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         Statement := selectStatementForUnconfiguredTable
       );
       var selectResultUnconfiguredTable := rClient.ExecuteStatement(inputSelectStatementForUnconfiguredTable);
-      selectResultUnconfiguredTable.Success?;
+      expect selectResultUnconfiguredTable.Success?;
 
       DeleteTable(client := wClient, tableName := unConfiguredTable);
     }

From 03d342e7c0e93fe00e2f5120a80a076239ddc10f Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Thu, 12 Jun 2025 16:27:17 -0700
Subject: [PATCH 15/18] auto commit

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 1 +
 1 file changed, 1 insertion(+)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 341fa2921..ea57b3def 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -886,6 +886,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         Statement := insertStatementForUnconfiguredTable
       );
       var insertResultUnconfiguredTable := wClient.ExecuteStatement(inputInsertStatementForUnconfiguredTable);
+      print(insertResultUnconfiguredTable);
       expect insertResultUnconfiguredTable.Success?;
 
       var selectStatementForUnconfiguredTable := "SELECT * FROM \"" + unConfiguredTable + "\" WHERE " + HashName + " = 0";

From bc164f2781e650feb57d27ea17bafae3493bf66b Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Thu, 12 Jun 2025 17:06:59 -0700
Subject: [PATCH 16/18] auto commit

---
 .../dafny/DDBEncryption/src/TestVectors.dfy     | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index ea57b3def..0ae2ca01f 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -883,15 +883,26 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       var _, _ := SetupTestTable(writeConfig, readConfig, createTableInput := MakeCreateTableInput(tableName := unConfiguredTable));
       var insertStatementForUnconfiguredTable := "INSERT INTO \"" + unConfiguredTable + "\" VALUE {'" + HashName + "': 0, 'attribute1': 'a'}";
       var inputInsertStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
-        Statement := insertStatementForUnconfiguredTable
+        Statement := insertStatementForUnconfiguredTable,
+        Parameters := None,
+        ConsistentRead := None,
+        NextToken := None,
+        ReturnConsumedCapacity := None,
+        Limit := None,
+        ReturnValuesOnConditionCheckFailure := None
       );
       var insertResultUnconfiguredTable := wClient.ExecuteStatement(inputInsertStatementForUnconfiguredTable);
-      print(insertResultUnconfiguredTable);
       expect insertResultUnconfiguredTable.Success?;
 
       var selectStatementForUnconfiguredTable := "SELECT * FROM \"" + unConfiguredTable + "\" WHERE " + HashName + " = 0";
       var inputSelectStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
-        Statement := selectStatementForUnconfiguredTable
+        Statement := selectStatementForUnconfiguredTable,
+        Parameters := None,
+        ConsistentRead := None,
+        NextToken := None,
+        ReturnConsumedCapacity := None,
+        Limit := None,
+        ReturnValuesOnConditionCheckFailure := None
       );
       var selectResultUnconfiguredTable := rClient.ExecuteStatement(inputSelectStatementForUnconfiguredTable);
       expect selectResultUnconfiguredTable.Success?;

From 2f0c00f9f929cf83cd99299378e7239d35e30af4 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Fri, 13 Jun 2025 10:16:52 -0700
Subject: [PATCH 17/18] auto commit

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 0ae2ca01f..0639c4c1c 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -888,7 +888,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         ConsistentRead := None,
         NextToken := None,
         ReturnConsumedCapacity := None,
-        Limit := None,
+        Limit := 5,
         ReturnValuesOnConditionCheckFailure := None
       );
       var insertResultUnconfiguredTable := wClient.ExecuteStatement(inputInsertStatementForUnconfiguredTable);
@@ -901,7 +901,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         ConsistentRead := None,
         NextToken := None,
         ReturnConsumedCapacity := None,
-        Limit := None,
+        Limit := 5,
         ReturnValuesOnConditionCheckFailure := None
       );
       var selectResultUnconfiguredTable := rClient.ExecuteStatement(inputSelectStatementForUnconfiguredTable);

From 4b710a52acb3387c67240603ed6cf300e7c08ee1 Mon Sep 17 00:00:00 2001
From: rishav-karanjit <rishavkj@amazon.com>
Date: Fri, 13 Jun 2025 10:24:41 -0700
Subject: [PATCH 18/18] auto commit

---
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 0639c4c1c..580dbb3ad 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -882,13 +882,14 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       var unConfiguredTable := "unConfiguredTable";
       var _, _ := SetupTestTable(writeConfig, readConfig, createTableInput := MakeCreateTableInput(tableName := unConfiguredTable));
       var insertStatementForUnconfiguredTable := "INSERT INTO \"" + unConfiguredTable + "\" VALUE {'" + HashName + "': 0, 'attribute1': 'a'}";
+      var limit : DDB.PositiveIntegerObject := 5;
       var inputInsertStatementForUnconfiguredTable := DDB.ExecuteStatementInput(
         Statement := insertStatementForUnconfiguredTable,
         Parameters := None,
         ConsistentRead := None,
         NextToken := None,
         ReturnConsumedCapacity := None,
-        Limit := 5,
+        Limit := Some(limit),
         ReturnValuesOnConditionCheckFailure := None
       );
       var insertResultUnconfiguredTable := wClient.ExecuteStatement(inputInsertStatementForUnconfiguredTable);
@@ -901,7 +902,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         ConsistentRead := None,
         NextToken := None,
         ReturnConsumedCapacity := None,
-        Limit := 5,
+        Limit := Some(limit),
         ReturnValuesOnConditionCheckFailure := None
       );
       var selectResultUnconfiguredTable := rClient.ExecuteStatement(inputSelectStatementForUnconfiguredTable);