feat: improve error message for missing key

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -227,7 +227,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     //# If this item does not have a sort key attribute,
     //# the DynamoDB Item Context MUST NOT contain the key `aws-crypto-sort-name`.
     ensures ret.Success? && config.sortKeyName.None? ==>
-      SORT_NAME !in ret.value
+              SORT_NAME !in ret.value
   {
     UTF8.EncodeAsciiUnique();
     :- Need(config.partitionKeyName in item, DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted"));
@@ -514,15 +514,47 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   {
     // We can formally verify these properties, but it is too resource intensive
     :- Need(forall k <- schema.content.SchemaMap :: InSignatureScope(config, k),
-            DynamoDbItemEncryptorException( message := "Recieved unexpected Crypto Schema: mismatch with signature scope"));
+            DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope"));
     :- Need(forall k <- schema.content.SchemaMap :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k),
-            DynamoDbItemEncryptorException( message := "Recieved unexpected Crypto Schema: Invalid attribute names"));
+            DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: Invalid attribute names"));
     Success(map k <- schema.content.SchemaMap :: k := schema.content.SchemaMap[k].content.Action)
   }
 
   predicate EncryptItemEnsuresPublicly(input: EncryptItemInput, output: Result<EncryptItemOutput, Error>)
   {true}
 
+  function method GetItemNames(item : ComAmazonawsDynamodbTypes.AttributeMap) : string
+  {
+    var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess);
+    if |keys| == 0 then
+      "item is empty"
+    else
+      Join(keys, " ")
+  }
+
+  function method KeyMissingMsg(
+    config: InternalConfig,
+    item : ComAmazonawsDynamodbTypes.AttributeMap,
+    tag : string)
+    : string
+  {
+    "On " + tag + " : "
+    +
+    (if config.partitionKeyName !in item then
+       "Partition key '" + config.partitionKeyName + "' does not exist in item. "
+     else
+       "")
+
+    +
+    (if config.sortKeyName.Some? &&  config.sortKeyName.value !in item then
+       "Sort key '" + config.sortKeyName.value + "' does not exist in item. "
+     else
+       "")
+
+    + "Item contains these attributes : "
+    + GetItemNames(item) + "."
+  }
+
   // public Encrypt method
   method {:vcs_split_on_every_assert} EncryptItem(config: InternalConfig, input: EncryptItemInput)
     returns (output: Result<EncryptItemOutput, Error>)
@@ -621,7 +653,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     :- Need(
       && config.partitionKeyName in input.plaintextItem
       && (config.sortKeyName.None? || config.sortKeyName.value in input.plaintextItem)
-    , DynamoDbItemEncryptorException( message := "Configuration mismatch partition or sort key does not exist in item."));
+    , E(KeyMissingMsg(config, input.plaintextItem, "Encrypt")));
 
     if |input.plaintextItem| > MAX_ATTRIBUTE_COUNT {
       var actCount := String.Base10Int2String(|input.plaintextItem|);
@@ -839,7 +871,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     :- Need(
       && config.partitionKeyName in input.encryptedItem
       && (config.sortKeyName.None? || config.sortKeyName.value in input.encryptedItem)
-    , DynamoDbItemEncryptorException( message := "Configuration mismatch partition or sort key does not exist in item."));
+    , DynamoDbItemEncryptorException( message := KeyMissingMsg(config, input.encryptedItem, "Decrypt")));
 
     //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
     //# If a [Legacy Policy](./ddb-table-encryption-config.md#legacy-policy) of

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy

@@ -39,15 +39,15 @@ module DynamoDbItemEncryptorTest {
     );
     expect encryptRes.Failure?;
     expect encryptRes.error == Types.AwsCryptographyDbEncryptionSdkDynamoDb(
-      DDBE.DynamoDbEncryptionException(message := "No Crypto Action configured for attribute unknown"));
+                                 DDBE.DynamoDbEncryptionException(message := "No Crypto Action configured for attribute unknown"));
   }
 
   method {:test} TestMissingSortKey() {
     var config := TestFixtures.GetEncryptorConfig();
     var inputItem := map["bar" := DDBS("key"), "encrypt" := DDBS("foo"), "sign" := DDBS("bar"), "nothing" := DDBS("baz")];
     var config2 := config.(
-      sortKeyName := Some("sort"),
-      attributeActionsOnEncrypt := config.attributeActionsOnEncrypt["sort" := CSE.SIGN_ONLY]
+    sortKeyName := Some("sort"),
+    attributeActionsOnEncrypt := config.attributeActionsOnEncrypt["sort" := CSE.SIGN_ONLY]
     );
     var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config2);
     var encryptRes := encryptor.EncryptItem(
@@ -56,7 +56,9 @@ module DynamoDbItemEncryptorTest {
       )
     );
     expect encryptRes.Failure?;
-    expect encryptRes.error == Types.DynamoDbItemEncryptorException(message := "Configuration mismatch partition or sort key does not exist in item.");
+    expect encryptRes.error == Types.DynamoDbItemEncryptorException(
+                                 message := "On Encrypt : Sort key 'sort' does not exist in item. Item contains these attributes : bar encrypt nothing sign."
+                               );
   }
 
   method {:test} TestRoundTrip() {
@@ -148,7 +150,7 @@ module DynamoDbItemEncryptorTest {
     expect |parsedHeader.value.encryptedDataKeys| == 1;
   }
 
-    method {:test} TestTooManyAttributes() {
+  method {:test} TestTooManyAttributes() {
     var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
     var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
     for i := 0 to MAX_ATTRIBUTE_COUNT {

DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptorTest.java

@@ -506,7 +506,7 @@ public void TestPutWithInvalidCryptoAction() {
 
     @Test(
             expectedExceptions = DynamoDbItemEncryptorException.class,
-            expectedExceptionsMessageRegExp = "Configuration mismatch partition or sort key does not exist in item."
+            expectedExceptionsMessageRegExp = "On Encrypt : Partition key 'partition_key' does not exist in item. Item contains these attributes : attr1 attr2 sort_key."
     )
     public void TestPutMissingPartition() {
         Map<String, AttributeValue> item = createTestItem("foo", "10", "bar", "awol");
@@ -530,7 +530,7 @@ public void TestPutMissingPartition() {
 
     @Test(
             expectedExceptions = DynamoDbItemEncryptorException.class,
-            expectedExceptionsMessageRegExp = "Configuration mismatch partition or sort key does not exist in item."
+            expectedExceptionsMessageRegExp = "On Encrypt : Sort key 'sort_key' does not exist in item. Item contains these attributes : attr1 attr2 partition_key."
     )
     public void TestPutMissingSort() {
         Map<String, AttributeValue> item = createTestItem("foo", "10", "bar", "awol");