fix: allow multi-tenant queries with allow_plaintext

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy

@@ -90,10 +90,10 @@ module QueryTransform {
       //# with the resulting decrypted [DynamoDB Item](./decrypt-item.md#dynamodb-item-1).
       var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]);
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
-
       var decrypted :- MapError(decryptRes);
-      if keyId.KeyId? {
-        :- Need(decrypted.parsedHeader.Some?, E("Decrypted query result has no parsed header."));
+
+      // No parsed header is ok, because it means ALLOW_PLAINTEXT_READ and a plain text item
+      if keyId.KeyId? && decrypted.parsedHeader.Some? {
         :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Query result has more than one Encrypted Data Key"));
         if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {
           decryptedItems := decryptedItems + [decrypted.plaintextItem];

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy

@@ -88,9 +88,10 @@ module ScanTransform {
 
       var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]);
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
-
       var decrypted :- MapError(decryptRes);
-      if keyId.KeyId? {
+
+      // No parsed header is ok, because it means ALLOW_PLAINTEXT_READ and a plain text item
+      if keyId.KeyId? && decrypted.parsedHeader.Some? {
         :- Need(decrypted.parsedHeader.Some?, E("Decrypted scan result has no parsed header."));
         :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key"));
         if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {