chore: remove assert to fix verification (#1360)

aws · Sep 13, 2024 · 8849c1e · 8849c1e
1 parent 303a8bd
commit 8849c1e
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 20 deletions.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy
@@ -92,16 +92,6 @@ module QueryTransform {
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
       var decrypted :- MapError(decryptRes);
 
-      // If the decrypted result was plaintext, i.e. has no parsedHeader
-      // then this is expected IFF the table config allows plaintext read
-      assert decrypted.parsedHeader.None? ==>
-          && EncOps.IsPlaintextItem(encryptedItems[x])
-          && !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
-          && (
-               || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-               || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-             );
-
       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 {

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
@@ -90,16 +90,6 @@ module ScanTransform {
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
       var decrypted :- MapError(decryptRes);
 
-      // If the decrypted result was plaintext, i.e. has no parsedHeader
-      // then this is expected IFF the table config allows plaintext read
-      assert decrypted.parsedHeader.None? ==>
-          && EncOps.IsPlaintextItem(encryptedItems[x])
-          && !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
-          && (
-               || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-               || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-             );
-
       if keyId.KeyId? && decrypted.parsedHeader.Some? {
         :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key"));
         if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {