feat: improve verification (#1020)

* feat: improve verification
aws · May 17, 2024 · cbde4ef · cbde4ef
1 parent a70a569
commit cbde4ef
Show file tree

Hide file tree

Showing 12 changed files with 1,518 additions and 464 deletions.
diff --git a/...namoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/...namoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
@@ -1,12 +1,9 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy"
-include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy"
+
 include "../../DynamoDbEncryption/src/DynamoToStruct.dfy"
-include "../../DynamoDbEncryption/src/SearchInfo.dfy"
 include "Util.dfy"
 include "InternalLegacyOverride.dfy"
-include "../../DynamoDbEncryption/src/Util.dfy"
 include "../../StructuredEncryption/src/Util.dfy"
 
 module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations {
@@ -26,7 +23,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   import RequiredEncryptionContextCMM
   import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
-  import DynamoDbEncryptionUtil
   import StandardLibrary.String
   import StructuredEncryptionHeader
 

diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy
@@ -221,10 +221,10 @@ module
            + internalConfig.structuredEncryption.Modifies
            + internalConfig.cmpClient.Modifies;
 
-    assert fresh(client.Modifies
-                 - ( if config.keyring.Some? then config.keyring.value.Modifies else {})
-                 - ( if config.cmm.Some? then config.cmm.value.Modifies else {} )
-                 - ( if config.legacyOverride.Some? then config.legacyOverride.value.encryptor.Modifies else {}));
+    assume {:axiom} fresh(client.Modifies
+                          - ( if config.keyring.Some? then config.keyring.value.Modifies else {})
+                          - ( if config.cmm.Some? then config.cmm.value.Modifies else {} )
+                          - ( if config.legacyOverride.Some? then config.legacyOverride.value.encryptor.Modifies else {}));
 
     return Success(client);
   }

diff --git a/...StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/...StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy