m

Author: Lucas McDonald

TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy

@@ -2,11 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0
 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
 include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
-// BEGIN MANUAL EDIT
+  // BEGIN MANUAL EDIT
 include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy"
 include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy"
 include "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy"
-// END MANUAL EDIT
+  // END MANUAL EDIT
 abstract module WrappedAbstractAwsCryptographyDynamoDbEncryptionService {
   import opened Wrappers
   import opened StandardLibrary.UInt

TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy

@@ -11,24 +11,8 @@ module {:extern} CreateWrappedItemEncryptor {
   import DynamoDbItemEncryptor
   import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
 
-  // The `ensures` clause is copy-pasted from the DynamoDbItemEncryptor client method's `ensures` clause.
   method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig)
     returns (output: Result<ENC.IDynamoDbItemEncryptorClient, ENC.Error>)
-    // requires config.keyring.Some? ==>
-    //   config.keyring.value.ValidState()
-    // requires config.cmm.Some? ==>
-    //   config.cmm.value.ValidState()
-    // requires config.legacyOverride.Some? ==>
-    //   config.legacyOverride.value.encryptor.ValidState()
-    // modifies if config.keyring.Some? then
-    //     config.keyring.value.Modifies
-    //   else {}
-    // modifies if config.cmm.Some? then
-    //     config.cmm.value.Modifies
-    //   else {}
-    // modifies if config.legacyOverride.Some? then
-    //            config.legacyOverride.value.encryptor.Modifies
-    //          else {}
     ensures output.Success? ==>
               && output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient
               && fresh(output.value)

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

@@ -357,9 +357,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
       );
     var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig);
     return Success(enc);
-    // assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
-    // var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
-    // return Success(encr);
   }
 
   method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)

TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy

@@ -5,13 +5,13 @@
 include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
 include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy"
 module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.wrapped" } WrappedItemEncryptor refines WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {
-    
-    import ComAmazonawsDynamodbTypes
 
-    import DynamoDbItemEncryptor
+  import ComAmazonawsDynamodbTypes
 
-    function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
-    {
-        DynamoDbItemEncryptor.DefaultDynamoDbItemEncryptorConfig()
-    }
+  import DynamoDbItemEncryptor
+
+  function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
+  {
+    DynamoDbItemEncryptor.DefaultDynamoDbItemEncryptorConfig()
+  }
 }

TestVectors/runtimes/rust/src/lib.rs

@@ -14,6 +14,7 @@ pub mod operation;
 pub mod types;
 pub mod validation;
 pub mod intercept;
+#[cfg(feature = "wrapped-client")]
 pub mod wrapped;
 
 mod standard_library_conversions;