m

Author: ajewellamz

DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dafny/dafny-4.2.0.patch

@@ -170,7 +170,7 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorServi
   import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
   import Operations : AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
   function method DefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
-  method {:vcs_split_on_every_assert} DynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := DefaultDynamoDbItemEncryptorConfig())
+  method DynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := DefaultDynamoDbItemEncryptorConfig())
     returns (res: Result<DynamoDbItemEncryptorClient, Error>)
     requires config.keyring.Some? ==>
                config.keyring.value.ValidState()

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

@@ -222,9 +222,9 @@ module
            + internalConfig.cmpClient.Modifies;
 
     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 {}));
+                          - ( 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);
   }