m

Author: Lucas McDonald

TestVectors/Makefile

@@ -107,3 +107,31 @@ transpile_implementation_rust: _remove_wrapped_client_rust
 _remove_wrapped_client_rust:
 	$(MAKE) _sed_file SED_FILE_PATH="runtimes/rust/src/deps/aws_cryptography_materialProviders.rs" \
 SED_BEFORE_STRING=' \#\[cfg(feature = "wrapped-client")\]' SED_AFTER_STRING='\/\/ Removed cfg(feature = "wrapped-client")'
+
+# TODO: Remove after wrapped client issue is fixed in Rust
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_dynamoDb_transforms.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_ITEM_ENCRYPTOR=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_structuredEncryption.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TEST_VECTORS=runtimes/rust/src/lib.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1 = "\#\[cfg(feature = \"wrapped-client\")\]"
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;'
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;'
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;'
+
+# TODO: Remove after wrapped client issue is fixed in Rust
+_polymorph_rust: _remove_wrapped_client_rust
+
+# TODO: Remove after wrapped client issue is fixed in Rust
+_remove_wrapped_client_rust:
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TEST_VECTORS) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TEST_VECTORS) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)

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/WrappedDynamoDbItemEncryptor/src/Index.dfy

@@ -3,4 +3,4 @@
 // Empty stub expected by Smithy-Dafny
 
 include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
-module WrappedItemEncryptor {}
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.wrapped" } WrappedItemEncryptor refines WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {}

TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs

@@ -8,6 +8,7 @@ use crate::implementation_from_dafny::software::amazon::cryptography::dbencrypti
 use crate::implementation_from_dafny::_Wrappers_Compile;
 use crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::client as item_encryptor_client;
 use crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::wrapped::client as wrapped_item_encryptor_client;
+use crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::conversions::error;
 
 pub mod _CreateWrappedItemEncryptor_Compile {
     pub struct _default {}
@@ -19,7 +20,13 @@ impl _CreateWrappedItemEncryptor_Compile::_default {
     ) -> 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 = item_encryptor_client::Client::from_conf(native_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));
 

TestVectors/runtimes/rust/src/lib.rs

@@ -15,8 +15,8 @@ pub mod types;
 pub mod validation;
 pub mod intercept;
 
-#[cfg(feature = "wrapped-client")]
-pub mod wrapped;
+// removed wrapped-client feature using sed;
+// removed wrapped module using sed;
 
 mod standard_library_conversions;
 mod standard_library_externs;