m

Author: Lucas McDonald

TestVectors/dafny/DDBEncryption/src/Index.dfy

@@ -4,6 +4,7 @@
 include "LibraryIndex.dfy"
 include "TestVectors.dfy"
 include "WriteSetPermutations.dfy"
+include "../../WrappedDynamoDbItemEncryptor/src/Index.dfy"
 
 module WrappedDDBEncryptionMain {
   import opened Wrappers
@@ -16,6 +17,7 @@ module WrappedDDBEncryptionMain {
   import opened JSONHelpers
   import KeyVectors
   import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
+  import WrappedItemEncryptor
 
 
   const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"

TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy

@@ -3,4 +3,15 @@
 // Empty stub expected by Smithy-Dafny
 
 include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
-module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.wrapped" } WrappedItemEncryptor refines WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {}
+include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy"
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.wrapped" } WrappedItemEncryptor refines WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {
+    
+    import ComAmazonawsDynamodbTypes
+
+    import DynamoDbItemEncryptor
+
+    function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
+    {
+        DynamoDbItemEncryptor.DefaultDynamoDbItemEncryptorConfig()
+    }
+}

TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs

@@ -18,20 +18,7 @@ impl _CreateWrappedItemEncryptor_Compile::_default {
     pub fn CreateWrappedItemEncryptor(
         config: &Rc<crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::DynamoDbItemEncryptorConfig>
     ) -> Rc<_Wrappers_Compile::Result<Object<dyn IDynamoDbItemEncryptorClient>, Rc<Error>>> {
-        let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config);
-        
-        let item_encryptor = match item_encryptor_client::Client::from_conf(native_config) {
-            Ok(client) => client,
-            Err(e) => return Rc::new(crate::r#_Wrappers_Compile::Result::Failure {
-                error: error::to_dafny(e),
-            }),
-        };
-        
-        let wrapped_encryptor = wrapped_item_encryptor_client::Client {wrapped: item_encryptor};
-        let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor));
-        
-        Rc::new(crate::r#_Wrappers_Compile::Result::Success {
-            value: dafny_encryptor,
-        })
+        // from_conf converts Dafny config to native, constructs a native client, and wraps it in a Dafny client
+        return wrapped_item_encryptor_client::Client::from_conf(config);
     }
 }

TestVectors/runtimes/rust/src/lib.rs

@@ -14,15 +14,14 @@ pub mod operation;
 pub mod types;
 pub mod validation;
 pub mod intercept;
-
-// removed wrapped-client feature using sed;
-// removed wrapped module using sed;
+pub mod wrapped;
 
 mod standard_library_conversions;
 mod standard_library_externs;
 
 pub use client::Client;
 
+pub use crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor;
 pub use crate::deps::aws_cryptography_dbEncryptionSdk_structuredEncryption;
 pub use crate::deps::aws_cryptography_keyStore;
 pub use crate::deps::aws_cryptography_materialProviders;