diff --git a/.github/workflows/test_models_rust_tests.yml b/.github/workflows/test_models_rust_tests.yml index fe1c41fde..74ce985ee 100644 --- a/.github/workflows/test_models_rust_tests.yml +++ b/.github/workflows/test_models_rust_tests.yml @@ -57,7 +57,7 @@ jobs: - name: Set up Rust uses: actions-rust-lang/setup-rust-toolchain@v1 with: - toolchain: "1.74.1" + toolchain: "1.76.0" rustflags: "" components: rustfmt diff --git a/TestModels/Resource/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/Resource/codegen-patches/rust/dafny-4.5.0.patch index 742b84333..3d05c3e4c 100644 --- a/TestModels/Resource/codegen-patches/rust/dafny-4.5.0.patch +++ b/TestModels/Resource/codegen-patches/rust/dafny-4.5.0.patch @@ -675,7 +675,7 @@ index 00000000..ba2a8a6e +pub mod builders; diff --git b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs new file mode 100644 -index 00000000..1fb85690 +index 00000000..58c53177 --- /dev/null +++ a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs @@ -0,0 +1,157 @@ @@ -684,7 +684,7 @@ index 00000000..1fb85690 +#[non_exhaustive] +#[derive(::std::clone::Clone, ::std::cmp::PartialEq, ::std::fmt::Debug)] +pub struct GetResourceDataInput { -+ pub(crate) blob_value: Option>, ++ pub(crate) blob_value: Option, + pub(crate) boolean_value: Option, + pub(crate) string_value: Option, + pub(crate) integer_value: Option, @@ -693,7 +693,7 @@ index 00000000..1fb85690 + +impl GetResourceDataInput { + #[allow(missing_docs)] // documentation missing in model -+ pub fn blob_value(&self) -> &Option> { ++ pub fn blob_value(&self) -> &Option { + &self.blob_value + } + #[allow(missing_docs)] // documentation missing in model @@ -727,7 +727,7 @@ index 00000000..1fb85690 + ::std::clone::Clone, ::std::cmp::PartialEq, ::std::default::Default, ::std::fmt::Debug, +)] +pub struct GetResourceDataInputBuilder { -+ blob_value: Option>, ++ blob_value: Option, + boolean_value: Option, + string_value: Option, + integer_value: Option, @@ -736,19 +736,19 @@ index 00000000..1fb85690 + +impl GetResourceDataInputBuilder { + #[allow(missing_docs)] // documentation missing in model -+ pub fn blob_value(mut self, input: Vec) -> Self { ++ pub fn blob_value(mut self, input: aws_smithy_types::Blob) -> Self { + self.blob_value = Some(input); + self + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn set_blob_value(mut self, input: Option>) -> Self { ++ pub fn set_blob_value(mut self, input: Option) -> Self { + self.blob_value = input; + self + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn get_blob_value(&self) -> &Option> { ++ pub fn get_blob_value(&self) -> &Option { + &self.blob_value + } + @@ -838,7 +838,7 @@ index 00000000..1fb85690 +} diff --git b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs new file mode 100644 -index 00000000..d9f1b9f4 +index 00000000..1814e59f --- /dev/null +++ a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs @@ -0,0 +1,158 @@ @@ -847,7 +847,7 @@ index 00000000..d9f1b9f4 +#[non_exhaustive] +#[derive(::std::clone::Clone, ::std::cmp::PartialEq, ::std::fmt::Debug)] +pub struct GetResourceDataOutput { -+ pub(crate) blob_value: Option>, ++ pub(crate) blob_value: Option, + pub(crate) boolean_value: Option, + pub(crate) string_value: Option, + pub(crate) integer_value: Option, @@ -856,7 +856,7 @@ index 00000000..d9f1b9f4 + +impl GetResourceDataOutput { + #[allow(missing_docs)] // documentation missing in model -+ pub fn blob_value(&self) -> &Option> { ++ pub fn blob_value(&self) -> &Option { + &self.blob_value + } + #[allow(missing_docs)] // documentation missing in model @@ -891,7 +891,7 @@ index 00000000..d9f1b9f4 + ::std::clone::Clone, ::std::cmp::PartialEq, ::std::default::Default, ::std::fmt::Debug, +)] +pub struct GetResourceDataOutputBuilder { -+ blob_value: Option>, ++ blob_value: Option, + boolean_value: Option, + string_value: Option, + integer_value: Option, @@ -900,19 +900,19 @@ index 00000000..d9f1b9f4 + +impl GetResourceDataOutputBuilder { + #[allow(missing_docs)] // documentation missing in model -+ pub fn blob_value(mut self, input: Vec) -> Self { ++ pub fn blob_value(mut self, input: aws_smithy_types::Blob) -> Self { + self.blob_value = Some(input); + self + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn set_blob_value(mut self, input: Option>) -> Self { ++ pub fn set_blob_value(mut self, input: Option) -> Self { + self.blob_value = input; + self + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn get_blob_value(&self) -> &Option> { ++ pub fn get_blob_value(&self) -> &Option { + &self.blob_value + } + @@ -1002,7 +1002,7 @@ index 00000000..d9f1b9f4 +} diff --git b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs new file mode 100644 -index 00000000..94c5d853 +index 00000000..9c1c4890 --- /dev/null +++ a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs @@ -0,0 +1,148 @@ @@ -1070,19 +1070,19 @@ index 00000000..94c5d853 + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn blob_value(mut self, input: impl ::std::convert::Into>) -> Self { ++ pub fn blob_value(mut self, input: impl ::std::convert::Into) -> Self { + self.inner = self.inner.blob_value(input.into()); + self + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn set_blob_value(mut self, input: Option>) -> Self { ++ pub fn set_blob_value(mut self, input: Option) -> Self { + self.inner = self.inner.set_blob_value(input); + self + } + + #[allow(missing_docs)] // documentation missing in model -+ pub fn get_blob_value(&self) -> &Option> { ++ pub fn get_blob_value(&self) -> &Option { + self.inner.get_blob_value() + } + diff --git a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs index 1fb856900..58c531770 100644 --- a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs +++ b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_input.rs @@ -3,7 +3,7 @@ #[non_exhaustive] #[derive(::std::clone::Clone, ::std::cmp::PartialEq, ::std::fmt::Debug)] pub struct GetResourceDataInput { - pub(crate) blob_value: Option>, + pub(crate) blob_value: Option, pub(crate) boolean_value: Option, pub(crate) string_value: Option, pub(crate) integer_value: Option, @@ -12,7 +12,7 @@ pub struct GetResourceDataInput { impl GetResourceDataInput { #[allow(missing_docs)] // documentation missing in model - pub fn blob_value(&self) -> &Option> { + pub fn blob_value(&self) -> &Option { &self.blob_value } #[allow(missing_docs)] // documentation missing in model @@ -46,7 +46,7 @@ impl GetResourceDataInput { ::std::clone::Clone, ::std::cmp::PartialEq, ::std::default::Default, ::std::fmt::Debug, )] pub struct GetResourceDataInputBuilder { - blob_value: Option>, + blob_value: Option, boolean_value: Option, string_value: Option, integer_value: Option, @@ -55,19 +55,19 @@ pub struct GetResourceDataInputBuilder { impl GetResourceDataInputBuilder { #[allow(missing_docs)] // documentation missing in model - pub fn blob_value(mut self, input: Vec) -> Self { + pub fn blob_value(mut self, input: aws_smithy_types::Blob) -> Self { self.blob_value = Some(input); self } #[allow(missing_docs)] // documentation missing in model - pub fn set_blob_value(mut self, input: Option>) -> Self { + pub fn set_blob_value(mut self, input: Option) -> Self { self.blob_value = input; self } #[allow(missing_docs)] // documentation missing in model - pub fn get_blob_value(&self) -> &Option> { + pub fn get_blob_value(&self) -> &Option { &self.blob_value } diff --git a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs index d9f1b9f42..1814e59f2 100644 --- a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs +++ b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/_get_resource_data_output.rs @@ -3,7 +3,7 @@ #[non_exhaustive] #[derive(::std::clone::Clone, ::std::cmp::PartialEq, ::std::fmt::Debug)] pub struct GetResourceDataOutput { - pub(crate) blob_value: Option>, + pub(crate) blob_value: Option, pub(crate) boolean_value: Option, pub(crate) string_value: Option, pub(crate) integer_value: Option, @@ -12,7 +12,7 @@ pub struct GetResourceDataOutput { impl GetResourceDataOutput { #[allow(missing_docs)] // documentation missing in model - pub fn blob_value(&self) -> &Option> { + pub fn blob_value(&self) -> &Option { &self.blob_value } #[allow(missing_docs)] // documentation missing in model @@ -47,7 +47,7 @@ impl GetResourceDataOutput { ::std::clone::Clone, ::std::cmp::PartialEq, ::std::default::Default, ::std::fmt::Debug, )] pub struct GetResourceDataOutputBuilder { - blob_value: Option>, + blob_value: Option, boolean_value: Option, string_value: Option, integer_value: Option, @@ -56,19 +56,19 @@ pub struct GetResourceDataOutputBuilder { impl GetResourceDataOutputBuilder { #[allow(missing_docs)] // documentation missing in model - pub fn blob_value(mut self, input: Vec) -> Self { + pub fn blob_value(mut self, input: aws_smithy_types::Blob) -> Self { self.blob_value = Some(input); self } #[allow(missing_docs)] // documentation missing in model - pub fn set_blob_value(mut self, input: Option>) -> Self { + pub fn set_blob_value(mut self, input: Option) -> Self { self.blob_value = input; self } #[allow(missing_docs)] // documentation missing in model - pub fn get_blob_value(&self) -> &Option> { + pub fn get_blob_value(&self) -> &Option { &self.blob_value } diff --git a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs index 94c5d8539..9c1c48905 100644 --- a/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs +++ b/TestModels/Resource/runtimes/rust/src/operation/get_resource_data/builders.rs @@ -62,19 +62,19 @@ impl GetResourceDataFluentBuilder { } #[allow(missing_docs)] // documentation missing in model - pub fn blob_value(mut self, input: impl ::std::convert::Into>) -> Self { + pub fn blob_value(mut self, input: impl ::std::convert::Into) -> Self { self.inner = self.inner.blob_value(input.into()); self } #[allow(missing_docs)] // documentation missing in model - pub fn set_blob_value(mut self, input: Option>) -> Self { + pub fn set_blob_value(mut self, input: Option) -> Self { self.inner = self.inner.set_blob_value(input); self } #[allow(missing_docs)] // documentation missing in model - pub fn get_blob_value(&self) -> &Option> { + pub fn get_blob_value(&self) -> &Option { self.inner.get_blob_value() } diff --git a/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs b/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs index 34d52f65b..7f2650a95 100644 --- a/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs +++ b/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs @@ -57,7 +57,7 @@ pub fn checkMostNone(name: String, output: GetResourceDataOutput) { pub fn allSome() -> GetResourceDataInput { GetResourceDataInput::builder() - .blob_value(vec![1u8]) + .blob_value(aws_smithy_types::Blob::new(vec![1u8])) .boolean_value(true) .string_value("Some".to_string()) .integer_value(1) @@ -68,7 +68,7 @@ pub fn allSome() -> GetResourceDataInput { pub fn checkSome(name: String, output: GetResourceDataOutput) { assert_eq!(Some(name + " Some"), *output.string_value()); - assert_eq!(Some(vec![1u8]), *output.blob_value()); + assert_eq!(Some(aws_smithy_types::Blob::new(vec![1u8])), *output.blob_value()); assert_eq!(Some(true), output.boolean_value()); assert_eq!(Some(1), output.integer_value()); assert_eq!(Some(1), output.long_value()); diff --git a/TestModels/aws-sdks/kms-lite/Makefile b/TestModels/aws-sdks/kms-lite/Makefile index 2739d12fd..a485f1d9d 100644 --- a/TestModels/aws-sdks/kms-lite/Makefile +++ b/TestModels/aws-sdks/kms-lite/Makefile @@ -8,7 +8,7 @@ include ../../SharedMakefile.mk NAMESPACE=com.amazonaws.kms PROJECT_SERVICES := \ - ComAmazonawsKms\ + ComAmazonawsKms SERVICE_NAMESPACE_ComAmazonawsKms=com.amazonaws.kms @@ -18,6 +18,8 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy AWS_SDK_CMD=--aws-sdk +SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/model + # This project has no dependencies # DEPENDENT-MODELS:= @@ -32,7 +34,6 @@ _polymorph_java: $(GRADLEW) polymorphJava # There is no wrapped target for aws-sdk types -_polymorph: ; _polymorph_wrapped: ; _polymorph_wrapped_dafny: ; _polymorph_wrapped_net: ; diff --git a/TestModels/aws-sdks/kms-lite/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/aws-sdks/kms-lite/codegen-patches/rust/dafny-4.5.0.patch new file mode 100644 index 000000000..e5a48c77f --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/codegen-patches/rust/dafny-4.5.0.patch @@ -0,0 +1,1239 @@ +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs +new file mode 100644 +index 00000000..b0091d98 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs +@@ -0,0 +1,88 @@ ++use crate::conversions; ++ ++struct Client { ++ inner: aws_sdk_kms::Client, ++ ++ rt: tokio::runtime::Runtime, ++} ++ ++impl dafny_runtime::UpcastObject for Client { ++ ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); ++} ++ ++impl dafny_runtime::UpcastObject for Client { ++ ::dafny_runtime::UpcastObjectFn!(dyn crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient); ++} ++ ++impl crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient ++ for Client { ++ fn Decrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ let native_result = ++ self.rt.block_on(conversions::decrypt::_decrypt_request::from_dafny(input.clone(), self.inner.clone()).send()); ++ dafny_standard_library::conversion::result_to_dafny(&native_result, ++ conversions::decrypt::_decrypt_response::to_dafny, ++ conversions::decrypt::to_dafny_error) ++ } ++ ++ fn Encrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ let native_result = ++ self.rt.block_on(conversions::encrypt::_encrypt_request::from_dafny(input.clone(), self.inner.clone()).send()); ++ dafny_standard_library::conversion::result_to_dafny(&native_result, ++ conversions::encrypt::_encrypt_response::to_dafny, ++ conversions::encrypt::to_dafny_error) ++ } ++ ++ fn GenerateDataKey(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ let native_result = ++ self.rt.block_on(conversions::generate_data_key::_generate_data_key_request::from_dafny(input.clone(), self.inner.clone()).send()); ++ dafny_standard_library::conversion::result_to_dafny(&native_result, ++ conversions::generate_data_key::_generate_data_key_response::to_dafny, ++ conversions::generate_data_key::to_dafny_error) ++ } ++ ++ fn GenerateDataKeyWithoutPlaintext(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ let native_result = ++ self.rt.block_on(conversions::generate_data_key_without_plaintext::_generate_data_key_without_plaintext_request::from_dafny(input.clone(), self.inner.clone()).send()); ++ dafny_standard_library::conversion::result_to_dafny(&native_result, ++ conversions::generate_data_key_without_plaintext::_generate_data_key_without_plaintext_response::to_dafny, ++ conversions::generate_data_key_without_plaintext::to_dafny_error) ++ } ++ ++ // Leaving untested operations out for now ++ ++ fn DeriveSharedSecret(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ todo!() ++ } ++ ++ fn GetPublicKey(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ todo!() ++ } ++ ++ fn ReEncrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { ++ todo!() ++ } ++ } ++ ++#[allow(non_snake_case)] ++impl crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny::_default { ++ pub fn KMSClient() -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Result< ++ ::dafny_runtime::Object, ++ ::std::rc::Rc ++ > ++ > { ++ let rt_result = tokio::runtime::Builder::new_current_thread() ++ .enable_all() ++ .build(); ++ if rt_result.is_err() { ++ return conversions::error::to_opaque_error_result(rt_result.err()); ++ } ++ let rt = rt_result.unwrap(); ++ ++ let shared_config = rt.block_on(aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28())); ++ let inner = aws_sdk_kms::Client::new(&shared_config); ++ let client = Client { inner, rt }; ++ let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); ++ std::rc::Rc::new(crate::implementation_from_dafny::r#_Wrappers_Compile::Result::Success { value: dafny_client }) ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions.rs +new file mode 100644 +index 00000000..8f8fb189 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions.rs +@@ -0,0 +1,19 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++pub mod generate_data_key; ++ ++pub mod generate_data_key_without_plaintext; ++ ++pub mod encrypt; ++ ++pub mod decrypt; ++ ++pub mod data_key_spec; ++ ++pub mod recipient_info; ++ ++pub mod key_encryption_mechanism; ++ ++pub mod encryption_algorithm_spec; ++ ++pub mod error; +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/data_key_spec.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/data_key_spec.rs +new file mode 100644 +index 00000000..24905032 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/data_key_spec.rs +@@ -0,0 +1,22 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++ ++pub fn to_dafny( ++ value: aws_sdk_kms::types::DataKeySpec, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new(match value { ++ aws_sdk_kms::types::DataKeySpec::Aes128 => crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_128 {}, ++ aws_sdk_kms::types::DataKeySpec::Aes256 => crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_256 {}, ++ _ => panic!() ++ }) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec, ++) -> aws_sdk_kms::types::DataKeySpec { ++ match dafny_value { ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_128 {} => aws_sdk_kms::types::DataKeySpec::Aes128, ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_256 {} => aws_sdk_kms::types::DataKeySpec::Aes256, ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt.rs +new file mode 100644 +index 00000000..68c7b13f +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt.rs +@@ -0,0 +1,45 @@ ++pub mod _decrypt_request; ++ ++pub mod _decrypt_response; ++ ++use aws_sdk_kms::error::SdkError; ++use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; ++ ++#[allow(dead_code)] ++pub fn to_dafny_error( ++ value: &::aws_smithy_runtime_api::client::result::SdkError< ++ aws_sdk_kms::operation::decrypt::DecryptError, ++ ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, ++ >, ++) -> ::std::rc::Rc { ++ match value { ++ SdkError::ServiceError(service_error) => match service_error.err() { ++ aws_sdk_kms::operation::decrypt::DecryptError::DependencyTimeoutException(e) => ++ crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::DisabledException(e) => ++ crate::conversions::error::disabled_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::DryRunOperationException(e) => ++ crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::IncorrectKeyException(e) => ++ crate::conversions::error::incorrect_key_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::InvalidCiphertextException(e) => ++ crate::conversions::error::invalid_ciphertext_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::InvalidGrantTokenException(e) => ++ crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::InvalidKeyUsageException(e) => ++ crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::KeyUnavailableException(e) => ++ crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::KmsInternalException(e) => ++ crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::KmsInvalidStateException(e) => ++ crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::decrypt::DecryptError::NotFoundException(e) => ++ crate::conversions::error::not_found_exception::to_dafny(e.clone()), ++ e => crate::conversions::error::to_opaque_error(e.to_string()), ++ }, ++ _ => { ++ crate::conversions::error::to_opaque_error(value.to_string()) ++ } ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs +new file mode 100644 +index 00000000..7bf5704d +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs +@@ -0,0 +1,88 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::operation::decrypt::DecryptInput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest::DecryptRequest { ++ CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob).Extract(), ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), ++ EncryptionContext: ++ ::std::rc::Rc::new(match value.encryption_context() { ++ Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : ++ ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, ++ |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), ++ |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} ++ }), ++ GrantTokens: ++ ::std::rc::Rc::new( ++ // Have to clone or else this becomes a borrow that can interfere with other branches ++ match value.grant_tokens.clone() { ++ Some(val) => ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { ++ value : ::dafny_runtime::Sequence::from_array( ++ &val.iter().map(|x| ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) ++ .collect() ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} ++ } ++ ), ++ Recipient: crate::conversions::recipient_info::option_to_dafny(value.recipient()), ++ DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), ++ EncryptionAlgorithm: ::std::rc::Rc::new(match value.encryption_algorithm { ++ Some(x) => crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { value: crate::conversions::encryption_algorithm_spec::to_dafny(x) }, ++ None => crate::implementation_from_dafny::_Wrappers_Compile::Option::None { } ++ }) ++ }) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest, ++ >, ++ client: aws_sdk_kms::Client, ++) -> aws_sdk_kms::operation::decrypt::builders::DecryptFluentBuilder { ++ client.decrypt() ++ .set_ciphertext_blob(Some( ++ dafny_standard_library::conversion::blob_from_dafny(dafny_value.CiphertextBlob().clone()))) ++ .set_key_id( ++ dafny_standard_library::conversion::ostring_from_dafny(dafny_value.KeyId().clone()), ++ ) ++ .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ ) ++ ), ++ _ => None ++ }) ++ .set_grant_tokens(match &**dafny_value.GrantTokens() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) ++ ), ++ _ => None ++ }) ++ .set_recipient(match &**dafny_value.Recipient() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ crate::conversions::recipient_info::from_dafny(value.clone()) ++ ), ++ _ => None ++ }) ++ .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) ++ .set_encryption_algorithm( ++ dafny_standard_library::conversion::option_from_dafny( ++ dafny_value.EncryptionAlgorithm().clone(), ++ |x| crate::conversions::encryption_algorithm_spec::from_dafny(x))) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_response.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_response.rs +new file mode 100644 +index 00000000..bc89ab27 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_response.rs +@@ -0,0 +1,17 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: &aws_sdk_kms::operation::decrypt::DecryptOutput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptResponse, ++> { ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptResponse::DecryptResponse { ++ Plaintext: dafny_standard_library::conversion::oblob_to_dafny(&value.plaintext), ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), ++ CiphertextForRecipient: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_for_recipient), ++ EncryptionAlgorithm: dafny_standard_library::conversion::option_to_dafny(&value.encryption_algorithm, ++ |x| crate::conversions::encryption_algorithm_spec::to_dafny(x.clone())), ++ }) ++} ++ ++// from_dafny ommitted to save time until we get to actual code generation +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt.rs +new file mode 100644 +index 00000000..3620a36f +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt.rs +@@ -0,0 +1,41 @@ ++pub mod _encrypt_request; ++ ++pub mod _encrypt_response; ++ ++use aws_sdk_kms::error::SdkError; ++use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; ++ ++#[allow(dead_code)] ++pub fn to_dafny_error( ++ value: &::aws_smithy_runtime_api::client::result::SdkError< ++ aws_sdk_kms::operation::encrypt::EncryptError, ++ ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, ++ >, ++) -> ::std::rc::Rc { ++ match value { ++ SdkError::ServiceError(service_error) => match service_error.err() { ++ aws_sdk_kms::operation::encrypt::EncryptError::DependencyTimeoutException(e) => ++ crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::DisabledException(e) => ++ crate::conversions::error::disabled_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::DryRunOperationException(e) => ++ crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::InvalidGrantTokenException(e) => ++ crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::InvalidKeyUsageException(e) => ++ crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::KeyUnavailableException(e) => ++ crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::KmsInternalException(e) => ++ crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::KmsInvalidStateException(e) => ++ crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::encrypt::EncryptError::NotFoundException(e) => ++ crate::conversions::error::not_found_exception::to_dafny(e.clone()), ++ e => crate::conversions::error::to_opaque_error(e.to_string()), ++ }, ++ _ => { ++ crate::conversions::error::to_opaque_error(value.to_string()) ++ } ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_request.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_request.rs +new file mode 100644 +index 00000000..936569ca +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_request.rs +@@ -0,0 +1,79 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.EncryptInput ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::operation::encrypt::EncryptInput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest::EncryptRequest { ++ Plaintext: dafny_standard_library::conversion::oblob_to_dafny(&value.plaintext).Extract(), ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id).Extract(), ++ EncryptionContext: ++ ::std::rc::Rc::new(match value.encryption_context() { ++ Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : ++ ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, ++ |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), ++ |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} ++ }), ++ GrantTokens: ++ ::std::rc::Rc::new( ++ // Have to clone or else this becomes a borrow that can interfere with other branches ++ match value.grant_tokens.clone() { ++ Some(val) => ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { ++ value : ::dafny_runtime::Sequence::from_array( ++ &val.iter().map(|x| ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) ++ .collect() ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} ++ } ++ ), ++ DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), ++ EncryptionAlgorithm: ::std::rc::Rc::new(match value.encryption_algorithm { ++ Some(x) => crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { value: crate::conversions::encryption_algorithm_spec::to_dafny(x) }, ++ None => crate::implementation_from_dafny::_Wrappers_Compile::Option::None { } ++ }) ++ }) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest, ++ >, ++ client: aws_sdk_kms::Client, ++) -> aws_sdk_kms::operation::encrypt::builders::EncryptFluentBuilder { ++ client.encrypt() ++ .set_plaintext(Some(dafny_standard_library::conversion::blob_from_dafny(dafny_value.Plaintext().clone()))) ++ .set_key_id(Some( ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.KeyId())), ++ ) ++ .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ ) ++ ), ++ _ => None ++ }) ++ .set_grant_tokens(match &**dafny_value.GrantTokens() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) ++ ), ++ _ => None ++ }) ++ .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) ++ .set_encryption_algorithm( ++ dafny_standard_library::conversion::option_from_dafny( ++ dafny_value.EncryptionAlgorithm().clone(), ++ |x| crate::conversions::encryption_algorithm_spec::from_dafny(x))) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_response.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_response.rs +new file mode 100644 +index 00000000..9a5c55dc +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_response.rs +@@ -0,0 +1,16 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: &aws_sdk_kms::operation::encrypt::EncryptOutput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptResponse, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptResponse::EncryptResponse { ++ CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob), ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), ++ EncryptionAlgorithm: dafny_standard_library::conversion::option_to_dafny(&value.encryption_algorithm, ++ |x| crate::conversions::encryption_algorithm_spec::to_dafny(x.clone())), ++ }) ++} ++ ++// from_dafny ommitted to save time until we get to actual code generation +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encryption_algorithm_spec.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encryption_algorithm_spec.rs +new file mode 100644 +index 00000000..304f1ac0 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encryption_algorithm_spec.rs +@@ -0,0 +1,32 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++ ++pub fn to_dafny( ++ value: aws_sdk_kms::types::EncryptionAlgorithmSpec, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new(match value { ++ aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha1 => ++ crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_1 { }, ++ aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha256 => ++ crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_256 { }, ++ aws_sdk_kms::types::EncryptionAlgorithmSpec::SymmetricDefault => ++ crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::SYMMETRIC_DEFAULT { }, ++ // TODO: This should not be a panic, but the Dafny image of the enum shape doesn't have an Unknown variant of any kind, ++ // so there's no way to succeed. ++ // See https://github.com/smithy-lang/smithy-dafny/issues/476. ++ // This could be handled more cleanly if conversion functions returned Results, ++ // but that would be a large and disruptie change to the overall code flow. ++ _ => panic!("Unknown enum variant: {}", value), ++ }) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec, ++) -> aws_sdk_kms::types::EncryptionAlgorithmSpec { ++ match dafny_value { ++ crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::SYMMETRIC_DEFAULT { } => aws_sdk_kms::types::EncryptionAlgorithmSpec::SymmetricDefault, ++ crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_1 { } => aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha1, ++ crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_256 { } => aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha256, ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error.rs +new file mode 100644 +index 00000000..d844a1c7 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error.rs +@@ -0,0 +1,51 @@ ++pub mod dependency_timeout_exception; ++ ++pub mod disabled_exception; ++ ++pub mod dry_run_operation_exception; ++ ++pub mod incorrect_key_exception; ++ ++pub mod invalid_ciphertext_exception; ++ ++pub mod invalid_grant_token_exception; ++ ++pub mod invalid_key_usage_exception; ++ ++pub mod key_unavailable_exception; ++ ++pub mod kms_internal_exception; ++ ++pub mod kms_invalid_state_exception; ++ ++pub mod not_found_exception; ++ ++/// Wraps up an arbitrary Rust Error value as a Dafny Error ++pub fn to_opaque_error(value: E) -> ++ ::std::rc::Rc ++{ ++ let error_obj: ::dafny_runtime::Object = ::dafny_runtime::Object(Some( ++ ::std::rc::Rc::new(::std::cell::UnsafeCell::new(value)), ++ )); ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::Opaque { ++ obj: error_obj, ++ }, ++ ) ++} ++ ++/// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure ++pub fn to_opaque_error_result(value: E) -> ++ ::std::rc::Rc< ++ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result< ++ T, ++ ::std::rc::Rc ++ > ++ > ++{ ++ ::std::rc::Rc::new( ++ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure { ++ error: to_opaque_error(value), ++ }, ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dependency_timeout_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dependency_timeout_exception.rs +new file mode 100644 +index 00000000..b2d7d133 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dependency_timeout_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::DependencyTimeoutException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::DependencyTimeoutException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/disabled_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/disabled_exception.rs +new file mode 100644 +index 00000000..14c5e6a7 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/disabled_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::DisabledException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::DisabledException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dry_run_operation_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dry_run_operation_exception.rs +new file mode 100644 +index 00000000..99206d5b +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dry_run_operation_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::DryRunOperationException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::DryRunOperationException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/incorrect_key_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/incorrect_key_exception.rs +new file mode 100644 +index 00000000..42175b79 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/incorrect_key_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::IncorrectKeyException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::IncorrectKeyException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_ciphertext_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_ciphertext_exception.rs +new file mode 100644 +index 00000000..67a392ec +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_ciphertext_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::InvalidCiphertextException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::InvalidCiphertextException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_grant_token_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_grant_token_exception.rs +new file mode 100644 +index 00000000..7f3ca6f0 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_grant_token_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::InvalidGrantTokenException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::InvalidGrantTokenException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_key_usage_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_key_usage_exception.rs +new file mode 100644 +index 00000000..b0f2bf08 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_key_usage_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::InvalidKeyUsageException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::InvalidKeyUsageException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/key_unavailable_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/key_unavailable_exception.rs +new file mode 100644 +index 00000000..e38fa034 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/key_unavailable_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::KeyUnavailableException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::KeyUnavailableException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_internal_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_internal_exception.rs +new file mode 100644 +index 00000000..23938932 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_internal_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::KmsInternalException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::KMSInternalException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_invalid_state_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_invalid_state_exception.rs +new file mode 100644 +index 00000000..1f9c6404 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_invalid_state_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::KmsInvalidStateException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::KMSInvalidStateException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/not_found_exception.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/not_found_exception.rs +new file mode 100644 +index 00000000..2956e9dc +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/not_found_exception.rs +@@ -0,0 +1,12 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++ ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::error::NotFoundException, ++) -> ::std::rc::Rc{ ++ ::std::rc::Rc::new( ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::NotFoundException { ++ message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) ++ } ++ ) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key.rs +new file mode 100644 +index 00000000..e0fd2ad0 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key.rs +@@ -0,0 +1,41 @@ ++pub mod _generate_data_key_request; ++ ++pub mod _generate_data_key_response; ++ ++use aws_sdk_kms::error::SdkError; ++use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; ++ ++#[allow(dead_code)] ++pub fn to_dafny_error( ++ value: &::aws_smithy_runtime_api::client::result::SdkError< ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError, ++ ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, ++ >, ++) -> ::std::rc::Rc { ++ match value { ++ SdkError::ServiceError(service_error) => match service_error.err() { ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::DependencyTimeoutException(e) => ++ crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::DisabledException(e) => ++ crate::conversions::error::disabled_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::DryRunOperationException(e) => ++ crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::InvalidGrantTokenException(e) => ++ crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::InvalidKeyUsageException(e) => ++ crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::KeyUnavailableException(e) => ++ crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::KmsInternalException(e) => ++ crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::KmsInvalidStateException(e) => ++ crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::NotFoundException(e) => ++ crate::conversions::error::not_found_exception::to_dafny(e.clone()), ++ e => crate::conversions::error::to_opaque_error(e.to_string()), ++ }, ++ _ => { ++ crate::conversions::error::to_opaque_error(value.to_string()) ++ } ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs +new file mode 100644 +index 00000000..e49a3e41 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs +@@ -0,0 +1,95 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::operation::generate_data_key::GenerateDataKeyInput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest::GenerateDataKeyRequest { ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id).Extract(), ++ EncryptionContext: ++ ::std::rc::Rc::new(match value.encryption_context() { ++ Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : ++ ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, ++ |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), ++ |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} ++ }), ++ NumberOfBytes: dafny_standard_library::conversion::oint_to_dafny(value.number_of_bytes), ++ KeySpec: ++ ::std::rc::Rc::new(match value.key_spec() { ++ Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { ++ value: crate::conversions::data_key_spec::to_dafny(x.clone()) ++ }, ++ _ => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} ++ }), ++ GrantTokens: ++ ::std::rc::Rc::new( ++ // Have to clone or else this becomes a borrow that can interfere with other branches ++ match value.grant_tokens.clone() { ++ Some(val) => ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { ++ value : ::dafny_runtime::Sequence::from_array( ++ &val.iter().map(|x| ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) ++ .collect() ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} ++ } ++ ), ++ Recipient: crate::conversions::recipient_info::option_to_dafny(value.recipient()), ++ DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), ++ }) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest, ++ >, ++ client: aws_sdk_kms::Client, ++) -> aws_sdk_kms::operation::generate_data_key::builders::GenerateDataKeyFluentBuilder { ++ client.generate_data_key() ++ .set_key_id(Some( ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( ++ dafny_value.KeyId(), ++ ), ++ )) ++ .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ ) ++ ), ++ _ => None ++ }) ++ .set_number_of_bytes(dafny_standard_library::conversion::oint_from_dafny(dafny_value.NumberOfBytes().clone())) ++ .set_key_spec(match &**dafny_value.KeySpec() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ crate::conversions::data_key_spec::from_dafny(value) ++ ), ++ _ => None ++ }) ++ .set_grant_tokens(match &**dafny_value.GrantTokens() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) ++ ), ++ _ => None ++ }) ++ .set_recipient(match &**dafny_value.Recipient() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ crate::conversions::recipient_info::from_dafny(value.clone()) ++ ), ++ _ => None ++ }) ++ .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_response.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_response.rs +new file mode 100644 +index 00000000..d406550d +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_response.rs +@@ -0,0 +1,16 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: &aws_sdk_kms::operation::generate_data_key::GenerateDataKeyOutput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyResponse, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyResponse::GenerateDataKeyResponse { ++ CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob), ++ Plaintext: dafny_standard_library::conversion::oblob_to_dafny(&value.plaintext), ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), ++ CiphertextForRecipient: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_for_recipient), ++ }) ++} ++ ++// from_dafny ommitted to save time until we get to actual code generation +\ No newline at end of file +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext.rs +new file mode 100644 +index 00000000..e9ea4318 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext.rs +@@ -0,0 +1,41 @@ ++pub mod _generate_data_key_without_plaintext_request; ++ ++pub mod _generate_data_key_without_plaintext_response; ++ ++use aws_sdk_kms::error::SdkError; ++use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; ++ ++#[allow(dead_code)] ++pub fn to_dafny_error( ++ value: &::aws_smithy_runtime_api::client::result::SdkError< ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError, ++ ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, ++ >, ++) -> ::std::rc::Rc { ++ match value { ++ SdkError::ServiceError(service_error) => match service_error.err() { ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::DependencyTimeoutException(e) => ++ crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::DisabledException(e) => ++ crate::conversions::error::disabled_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::DryRunOperationException(e) => ++ crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::InvalidGrantTokenException(e) => ++ crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::InvalidKeyUsageException(e) => ++ crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::KeyUnavailableException(e) => ++ crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::KmsInternalException(e) => ++ crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::KmsInvalidStateException(e) => ++ crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), ++ aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::NotFoundException(e) => ++ crate::conversions::error::not_found_exception::to_dafny(e.clone()), ++ e => crate::conversions::error::to_opaque_error(e.to_string()), ++ }, ++ _ => { ++ crate::conversions::error::to_opaque_error(value.to_string()) ++ } ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_request.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_request.rs +new file mode 100644 +index 00000000..6bda4aa0 +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_request.rs +@@ -0,0 +1,87 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextInput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextRequest, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextRequest::GenerateDataKeyWithoutPlaintextRequest { ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id).Extract(), ++ EncryptionContext: ++ ::std::rc::Rc::new(match value.encryption_context() { ++ Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : ++ ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, ++ |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), ++ |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} ++ }), ++ NumberOfBytes: dafny_standard_library::conversion::oint_to_dafny(value.number_of_bytes), ++ KeySpec: ++ ::std::rc::Rc::new(match value.key_spec() { ++ Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { ++ value: crate::conversions::data_key_spec::to_dafny(x.clone()) ++ }, ++ _ => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} ++ }), ++ GrantTokens: ++ ::std::rc::Rc::new( ++ // Have to clone or else this becomes a borrow that can interfere with other branches ++ match value.grant_tokens.clone() { ++ Some(val) => ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { ++ value : ::dafny_runtime::Sequence::from_array( ++ &val.iter().map(|x| ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) ++ .collect() ++ ) ++ }, ++ None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} ++ } ++ ), ++ DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), ++ }) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextRequest, ++ >, ++ client: aws_sdk_kms::Client ++) -> aws_sdk_kms::operation::generate_data_key_without_plaintext::builders::GenerateDataKeyWithoutPlaintextFluentBuilder{ ++ client.generate_data_key_without_plaintext() ++ .set_key_id(Some( ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( ++ dafny_value.KeyId(), ++ ), ++ )) ++ .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, ++ ) ++ ), ++ _ => None ++ }) ++ .set_number_of_bytes(dafny_standard_library::conversion::oint_from_dafny(dafny_value.NumberOfBytes().clone())) ++ .set_key_spec(match &**dafny_value.KeySpec() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ crate::conversions::data_key_spec::from_dafny(value) ++ ), ++ _ => None ++ }) ++ .set_grant_tokens(match &**dafny_value.GrantTokens() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => ++ Some( ++ ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, ++ dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) ++ ), ++ _ => None ++ }) ++ .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_response.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_response.rs +new file mode 100644 +index 00000000..ed879b5c +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_response.rs +@@ -0,0 +1,14 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: &aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextOutput ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextResponse, ++>{ ++ ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextResponse::GenerateDataKeyWithoutPlaintextResponse { ++ CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob), ++ KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), ++ }) ++} ++ ++// from_dafny ommitted to save time until we get to actual code generation +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/key_encryption_mechanism.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/key_encryption_mechanism.rs +new file mode 100644 +index 00000000..220034fd +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/key_encryption_mechanism.rs +@@ -0,0 +1,25 @@ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++ ++pub fn to_dafny( ++ value: aws_sdk_kms::types::KeyEncryptionMechanism, ++) -> ::std::rc::Rc{ ++ match value { ++ aws_sdk_kms::types::KeyEncryptionMechanism::RsaesOaepSha256 => ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::KeyEncryptionMechanism::RSAES_OAEP_SHA_256 {}), ++ // TODO: This should not be a panic, but the Dafny image of the enum shape doesn't have an Unknown variant of any kind, ++ // so there's no way to succeed. ++ // See https://github.com/smithy-lang/smithy-dafny/issues/476. ++ // This could be handled more cleanly if conversion functions returned Results, ++ // but that would be a large and disruptie change to the overall code flow. ++ _ => panic!("Unknown enum variant: {}", value), ++ } ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::KeyEncryptionMechanism, ++) -> aws_sdk_kms::types::KeyEncryptionMechanism { ++ match dafny_value { ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::KeyEncryptionMechanism::RSAES_OAEP_SHA_256 {} => aws_sdk_kms::types::KeyEncryptionMechanism::RsaesOaepSha256, ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/recipient_info.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/recipient_info.rs +new file mode 100644 +index 00000000..0b6d290b +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/recipient_info.rs +@@ -0,0 +1,89 @@ ++use aws_sdk_kms::types::KeyEncryptionMechanism; ++ ++// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. ++#[allow(dead_code)] ++pub fn to_dafny( ++ value: aws_sdk_kms::types::RecipientInfo, ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, ++>{ ++ ::std::rc::Rc::new(to_dafny_plain(&value)) ++} ++ ++pub fn to_dafny_plain( ++ value: &aws_sdk_kms::types::RecipientInfo, ++) -> crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo { ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo::RecipientInfo { ++ AttestationDocument: dafny_standard_library::conversion::oblob_to_dafny(&value.attestation_document), ++ KeyEncryptionAlgorithm: dafny_standard_library::conversion::option_to_dafny(&value.key_encryption_algorithm, ++ |x| crate::conversions::key_encryption_mechanism::to_dafny(x.clone())) ++ } ++} ++ ++pub fn option_to_dafny( ++ value: Option<&aws_sdk_kms::types::RecipientInfo>, ++) -> ::std::rc::Rc< ++ crate::implementation_from_dafny::_Wrappers_Compile::Option< ++ ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, ++ >, ++ >, ++>{ ++ let inner = match value { ++ None => crate::implementation_from_dafny::_Wrappers_Compile::Option::None {}, ++ Some(x) => crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { ++ value: ::std::rc::Rc::new(to_dafny_plain(x)), ++ }, ++ }; ++ ::std::rc::Rc::new(inner) ++} ++ ++#[allow(dead_code)] ++pub fn from_dafny( ++ dafny_value: ::std::rc::Rc< ++ crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, ++ >, ++) -> aws_sdk_kms::types::RecipientInfo { ++ aws_sdk_kms::types::RecipientInfo::builder() ++ .set_attestation_document(dafny_standard_library::conversion::oblob_from_dafny( ++ dafny_value.AttestationDocument().clone(), ++ )) ++ .set_key_encryption_algorithm(match &**dafny_value.KeyEncryptionAlgorithm() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => Some( ++ crate::conversions::key_encryption_mechanism::from_dafny(value), ++ ), ++ _ => None, ++ }) ++ .build() ++} ++ ++#[allow(dead_code)] ++pub fn plain_from_dafny( ++ dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, ++) -> aws_sdk_kms::types::RecipientInfo { ++ aws_sdk_kms::types::RecipientInfo::builder() ++ .set_attestation_document(dafny_standard_library::conversion::oblob_from_dafny( ++ dafny_value.AttestationDocument().clone(), ++ )) ++ .set_key_encryption_algorithm(match &**dafny_value.KeyEncryptionAlgorithm() { ++ crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => Some( ++ crate::conversions::key_encryption_mechanism::from_dafny(value), ++ ), ++ _ => None, ++ }) ++ .build() ++} ++ ++#[allow(dead_code)] ++pub fn option_from_dafny( ++ dafny_value: ::std::rc::Rc>>, ++) -> Option { ++ match &*dafny_value { ++ crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { value } => { ++ Some(plain_from_dafny(value)) ++ } ++ _ => None, ++ } ++} +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/lib.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/lib.rs +new file mode 100644 +index 00000000..b5e77f9a +--- /dev/null ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/lib.rs +@@ -0,0 +1,3 @@ ++mod client; ++mod conversions; ++pub mod implementation_from_dafny; +diff --git b/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs a/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs +index 1864a86b..f061a809 100644 +--- b/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs ++++ a/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs +@@ -1,5 +1,6 @@ + #![allow(warnings, unconditional_panic)] + #![allow(nonstandard_style)] ++use ::kms_lite::implementation_from_dafny::*; + + pub mod r#_TestComAmazonawsKms_Compile { + pub struct _default {} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml new file mode 100644 index 000000000..e951448b3 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml @@ -0,0 +1,20 @@ +[package] +name = "kms-lite" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +aws-smithy-runtime = {version = "1.6.0", features = ["client"] } +aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } +aws-smithy-types = "1.2.0" +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"} +dafny_standard_library = { path = "../../../../dafny-dependencies/StandardLibrary/runtimes/rust"} + +aws-sdk-kms = "1.35.0" +aws-config = "1.5.4" + +[dependencies.tokio] +version = "1.26.0" +features = ["full"] \ No newline at end of file diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs new file mode 100644 index 000000000..b0091d983 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs @@ -0,0 +1,88 @@ +use crate::conversions; + +struct Client { + inner: aws_sdk_kms::Client, + + rt: tokio::runtime::Runtime, +} + +impl dafny_runtime::UpcastObject for Client { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); +} + +impl dafny_runtime::UpcastObject for Client { + ::dafny_runtime::UpcastObjectFn!(dyn crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient); +} + +impl crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient + for Client { + fn Decrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + let native_result = + self.rt.block_on(conversions::decrypt::_decrypt_request::from_dafny(input.clone(), self.inner.clone()).send()); + dafny_standard_library::conversion::result_to_dafny(&native_result, + conversions::decrypt::_decrypt_response::to_dafny, + conversions::decrypt::to_dafny_error) + } + + fn Encrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + let native_result = + self.rt.block_on(conversions::encrypt::_encrypt_request::from_dafny(input.clone(), self.inner.clone()).send()); + dafny_standard_library::conversion::result_to_dafny(&native_result, + conversions::encrypt::_encrypt_response::to_dafny, + conversions::encrypt::to_dafny_error) + } + + fn GenerateDataKey(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + let native_result = + self.rt.block_on(conversions::generate_data_key::_generate_data_key_request::from_dafny(input.clone(), self.inner.clone()).send()); + dafny_standard_library::conversion::result_to_dafny(&native_result, + conversions::generate_data_key::_generate_data_key_response::to_dafny, + conversions::generate_data_key::to_dafny_error) + } + + fn GenerateDataKeyWithoutPlaintext(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + let native_result = + self.rt.block_on(conversions::generate_data_key_without_plaintext::_generate_data_key_without_plaintext_request::from_dafny(input.clone(), self.inner.clone()).send()); + dafny_standard_library::conversion::result_to_dafny(&native_result, + conversions::generate_data_key_without_plaintext::_generate_data_key_without_plaintext_response::to_dafny, + conversions::generate_data_key_without_plaintext::to_dafny_error) + } + + // Leaving untested operations out for now + + fn DeriveSharedSecret(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + todo!() + } + + fn GetPublicKey(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + todo!() + } + + fn ReEncrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + todo!() + } + } + +#[allow(non_snake_case)] +impl crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny::_default { + pub fn KMSClient() -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object, + ::std::rc::Rc + > + > { + let rt_result = tokio::runtime::Builder::new_current_thread() + .enable_all() + .build(); + if rt_result.is_err() { + return conversions::error::to_opaque_error_result(rt_result.err()); + } + let rt = rt_result.unwrap(); + + let shared_config = rt.block_on(aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28())); + let inner = aws_sdk_kms::Client::new(&shared_config); + let client = Client { inner, rt }; + let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); + std::rc::Rc::new(crate::implementation_from_dafny::r#_Wrappers_Compile::Result::Success { value: dafny_client }) + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions.rs new file mode 100644 index 000000000..8f8fb189c --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions.rs @@ -0,0 +1,19 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +pub mod generate_data_key; + +pub mod generate_data_key_without_plaintext; + +pub mod encrypt; + +pub mod decrypt; + +pub mod data_key_spec; + +pub mod recipient_info; + +pub mod key_encryption_mechanism; + +pub mod encryption_algorithm_spec; + +pub mod error; diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/data_key_spec.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/data_key_spec.rs new file mode 100644 index 000000000..249050328 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/data_key_spec.rs @@ -0,0 +1,22 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] + +pub fn to_dafny( + value: aws_sdk_kms::types::DataKeySpec, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new(match value { + aws_sdk_kms::types::DataKeySpec::Aes128 => crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_128 {}, + aws_sdk_kms::types::DataKeySpec::Aes256 => crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_256 {}, + _ => panic!() + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec, +) -> aws_sdk_kms::types::DataKeySpec { + match dafny_value { + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_128 {} => aws_sdk_kms::types::DataKeySpec::Aes128, + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DataKeySpec::AES_256 {} => aws_sdk_kms::types::DataKeySpec::Aes256, + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt.rs new file mode 100644 index 000000000..68c7b13f8 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt.rs @@ -0,0 +1,45 @@ +pub mod _decrypt_request; + +pub mod _decrypt_response; + +use aws_sdk_kms::error::SdkError; +use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; + +#[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_kms::operation::decrypt::DecryptError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_kms::operation::decrypt::DecryptError::DependencyTimeoutException(e) => + crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::DisabledException(e) => + crate::conversions::error::disabled_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::DryRunOperationException(e) => + crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::IncorrectKeyException(e) => + crate::conversions::error::incorrect_key_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::InvalidCiphertextException(e) => + crate::conversions::error::invalid_ciphertext_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::InvalidGrantTokenException(e) => + crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::InvalidKeyUsageException(e) => + crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::KeyUnavailableException(e) => + crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::KmsInternalException(e) => + crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::KmsInvalidStateException(e) => + crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::decrypt::DecryptError::NotFoundException(e) => + crate::conversions::error::not_found_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs new file mode 100644 index 000000000..7bf5704df --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs @@ -0,0 +1,88 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::operation::decrypt::DecryptInput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest::DecryptRequest { + CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob).Extract(), + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), + EncryptionContext: + ::std::rc::Rc::new(match value.encryption_context() { + Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : + ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), + |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} + }), + GrantTokens: + ::std::rc::Rc::new( + // Have to clone or else this becomes a borrow that can interfere with other branches + match value.grant_tokens.clone() { + Some(val) => + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { + value : ::dafny_runtime::Sequence::from_array( + &val.iter().map(|x| + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) + .collect() + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} + } + ), + Recipient: crate::conversions::recipient_info::option_to_dafny(value.recipient()), + DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), + EncryptionAlgorithm: ::std::rc::Rc::new(match value.encryption_algorithm { + Some(x) => crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { value: crate::conversions::encryption_algorithm_spec::to_dafny(x) }, + None => crate::implementation_from_dafny::_Wrappers_Compile::Option::None { } + }) + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest, + >, + client: aws_sdk_kms::Client, +) -> aws_sdk_kms::operation::decrypt::builders::DecryptFluentBuilder { + client.decrypt() + .set_ciphertext_blob(Some( + dafny_standard_library::conversion::blob_from_dafny(dafny_value.CiphertextBlob().clone()))) + .set_key_id( + dafny_standard_library::conversion::ostring_from_dafny(dafny_value.KeyId().clone()), + ) + .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + ) + ), + _ => None + }) + .set_grant_tokens(match &**dafny_value.GrantTokens() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) + ), + _ => None + }) + .set_recipient(match &**dafny_value.Recipient() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + crate::conversions::recipient_info::from_dafny(value.clone()) + ), + _ => None + }) + .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) + .set_encryption_algorithm( + dafny_standard_library::conversion::option_from_dafny( + dafny_value.EncryptionAlgorithm().clone(), + |x| crate::conversions::encryption_algorithm_spec::from_dafny(x))) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_response.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_response.rs new file mode 100644 index 000000000..bc89ab27c --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_response.rs @@ -0,0 +1,17 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: &aws_sdk_kms::operation::decrypt::DecryptOutput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptResponse, +> { + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptResponse::DecryptResponse { + Plaintext: dafny_standard_library::conversion::oblob_to_dafny(&value.plaintext), + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), + CiphertextForRecipient: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_for_recipient), + EncryptionAlgorithm: dafny_standard_library::conversion::option_to_dafny(&value.encryption_algorithm, + |x| crate::conversions::encryption_algorithm_spec::to_dafny(x.clone())), + }) +} + +// from_dafny ommitted to save time until we get to actual code generation diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt.rs new file mode 100644 index 000000000..3620a36fb --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt.rs @@ -0,0 +1,41 @@ +pub mod _encrypt_request; + +pub mod _encrypt_response; + +use aws_sdk_kms::error::SdkError; +use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; + +#[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_kms::operation::encrypt::EncryptError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_kms::operation::encrypt::EncryptError::DependencyTimeoutException(e) => + crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::DisabledException(e) => + crate::conversions::error::disabled_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::DryRunOperationException(e) => + crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::InvalidGrantTokenException(e) => + crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::InvalidKeyUsageException(e) => + crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::KeyUnavailableException(e) => + crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::KmsInternalException(e) => + crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::KmsInvalidStateException(e) => + crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::encrypt::EncryptError::NotFoundException(e) => + crate::conversions::error::not_found_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_request.rs new file mode 100644 index 000000000..936569ca9 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_request.rs @@ -0,0 +1,79 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.EncryptInput +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::operation::encrypt::EncryptInput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest::EncryptRequest { + Plaintext: dafny_standard_library::conversion::oblob_to_dafny(&value.plaintext).Extract(), + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id).Extract(), + EncryptionContext: + ::std::rc::Rc::new(match value.encryption_context() { + Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : + ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), + |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} + }), + GrantTokens: + ::std::rc::Rc::new( + // Have to clone or else this becomes a borrow that can interfere with other branches + match value.grant_tokens.clone() { + Some(val) => + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { + value : ::dafny_runtime::Sequence::from_array( + &val.iter().map(|x| + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) + .collect() + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} + } + ), + DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), + EncryptionAlgorithm: ::std::rc::Rc::new(match value.encryption_algorithm { + Some(x) => crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { value: crate::conversions::encryption_algorithm_spec::to_dafny(x) }, + None => crate::implementation_from_dafny::_Wrappers_Compile::Option::None { } + }) + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest, + >, + client: aws_sdk_kms::Client, +) -> aws_sdk_kms::operation::encrypt::builders::EncryptFluentBuilder { + client.encrypt() + .set_plaintext(Some(dafny_standard_library::conversion::blob_from_dafny(dafny_value.Plaintext().clone()))) + .set_key_id(Some( + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.KeyId())), + ) + .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + ) + ), + _ => None + }) + .set_grant_tokens(match &**dafny_value.GrantTokens() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) + ), + _ => None + }) + .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) + .set_encryption_algorithm( + dafny_standard_library::conversion::option_from_dafny( + dafny_value.EncryptionAlgorithm().clone(), + |x| crate::conversions::encryption_algorithm_spec::from_dafny(x))) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_response.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_response.rs new file mode 100644 index 000000000..9a5c55dc6 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encrypt/_encrypt_response.rs @@ -0,0 +1,16 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: &aws_sdk_kms::operation::encrypt::EncryptOutput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptResponse, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptResponse::EncryptResponse { + CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob), + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), + EncryptionAlgorithm: dafny_standard_library::conversion::option_to_dafny(&value.encryption_algorithm, + |x| crate::conversions::encryption_algorithm_spec::to_dafny(x.clone())), + }) +} + +// from_dafny ommitted to save time until we get to actual code generation diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encryption_algorithm_spec.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encryption_algorithm_spec.rs new file mode 100644 index 000000000..304f1ac01 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/encryption_algorithm_spec.rs @@ -0,0 +1,32 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] + +pub fn to_dafny( + value: aws_sdk_kms::types::EncryptionAlgorithmSpec, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new(match value { + aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha1 => + crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_1 { }, + aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha256 => + crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_256 { }, + aws_sdk_kms::types::EncryptionAlgorithmSpec::SymmetricDefault => + crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::SYMMETRIC_DEFAULT { }, + // TODO: This should not be a panic, but the Dafny image of the enum shape doesn't have an Unknown variant of any kind, + // so there's no way to succeed. + // See https://github.com/smithy-lang/smithy-dafny/issues/476. + // This could be handled more cleanly if conversion functions returned Results, + // but that would be a large and disruptie change to the overall code flow. + _ => panic!("Unknown enum variant: {}", value), + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec, +) -> aws_sdk_kms::types::EncryptionAlgorithmSpec { + match dafny_value { + crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::SYMMETRIC_DEFAULT { } => aws_sdk_kms::types::EncryptionAlgorithmSpec::SymmetricDefault, + crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_1 { } => aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha1, + crate::implementation_from_dafny::_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptionAlgorithmSpec::RSAES_OAEP_SHA_256 { } => aws_sdk_kms::types::EncryptionAlgorithmSpec::RsaesOaepSha256, + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error.rs new file mode 100644 index 000000000..d844a1c71 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error.rs @@ -0,0 +1,51 @@ +pub mod dependency_timeout_exception; + +pub mod disabled_exception; + +pub mod dry_run_operation_exception; + +pub mod incorrect_key_exception; + +pub mod invalid_ciphertext_exception; + +pub mod invalid_grant_token_exception; + +pub mod invalid_key_usage_exception; + +pub mod key_unavailable_exception; + +pub mod kms_internal_exception; + +pub mod kms_invalid_state_exception; + +pub mod not_found_exception; + +/// Wraps up an arbitrary Rust Error value as a Dafny Error +pub fn to_opaque_error(value: E) -> + ::std::rc::Rc +{ + let error_obj: ::dafny_runtime::Object = ::dafny_runtime::Object(Some( + ::std::rc::Rc::new(::std::cell::UnsafeCell::new(value)), + )); + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::Opaque { + obj: error_obj, + }, + ) +} + +/// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure +pub fn to_opaque_error_result(value: E) -> + ::std::rc::Rc< + dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result< + T, + ::std::rc::Rc + > + > +{ + ::std::rc::Rc::new( + dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure { + error: to_opaque_error(value), + }, + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dependency_timeout_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dependency_timeout_exception.rs new file mode 100644 index 000000000..b2d7d133c --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dependency_timeout_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::DependencyTimeoutException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::DependencyTimeoutException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/disabled_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/disabled_exception.rs new file mode 100644 index 000000000..14c5e6a70 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/disabled_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::DisabledException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::DisabledException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dry_run_operation_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dry_run_operation_exception.rs new file mode 100644 index 000000000..99206d5b8 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/dry_run_operation_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::DryRunOperationException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::DryRunOperationException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/incorrect_key_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/incorrect_key_exception.rs new file mode 100644 index 000000000..42175b791 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/incorrect_key_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::IncorrectKeyException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::IncorrectKeyException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_ciphertext_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_ciphertext_exception.rs new file mode 100644 index 000000000..67a392ec9 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_ciphertext_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::InvalidCiphertextException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::InvalidCiphertextException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_grant_token_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_grant_token_exception.rs new file mode 100644 index 000000000..7f3ca6f0d --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_grant_token_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::InvalidGrantTokenException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::InvalidGrantTokenException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_key_usage_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_key_usage_exception.rs new file mode 100644 index 000000000..b0f2bf08e --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/invalid_key_usage_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::InvalidKeyUsageException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::InvalidKeyUsageException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/key_unavailable_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/key_unavailable_exception.rs new file mode 100644 index 000000000..e38fa034c --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/key_unavailable_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::KeyUnavailableException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::KeyUnavailableException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_internal_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_internal_exception.rs new file mode 100644 index 000000000..239389320 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_internal_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::KmsInternalException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::KMSInternalException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_invalid_state_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_invalid_state_exception.rs new file mode 100644 index 000000000..1f9c64046 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/kms_invalid_state_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::KmsInvalidStateException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::KMSInvalidStateException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/not_found_exception.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/not_found_exception.rs new file mode 100644 index 000000000..2956e9dc4 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/error/not_found_exception.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::error::NotFoundException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::Error::NotFoundException { + message: dafny_standard_library::conversion::ostring_to_dafny(&value.message) + } + ) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key.rs new file mode 100644 index 000000000..e0fd2ad05 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key.rs @@ -0,0 +1,41 @@ +pub mod _generate_data_key_request; + +pub mod _generate_data_key_response; + +use aws_sdk_kms::error::SdkError; +use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; + +#[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::DependencyTimeoutException(e) => + crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::DisabledException(e) => + crate::conversions::error::disabled_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::DryRunOperationException(e) => + crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::InvalidGrantTokenException(e) => + crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::InvalidKeyUsageException(e) => + crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::KeyUnavailableException(e) => + crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::KmsInternalException(e) => + crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::KmsInvalidStateException(e) => + crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key::GenerateDataKeyError::NotFoundException(e) => + crate::conversions::error::not_found_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs new file mode 100644 index 000000000..e49a3e415 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs @@ -0,0 +1,95 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::operation::generate_data_key::GenerateDataKeyInput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest::GenerateDataKeyRequest { + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id).Extract(), + EncryptionContext: + ::std::rc::Rc::new(match value.encryption_context() { + Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : + ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), + |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} + }), + NumberOfBytes: dafny_standard_library::conversion::oint_to_dafny(value.number_of_bytes), + KeySpec: + ::std::rc::Rc::new(match value.key_spec() { + Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { + value: crate::conversions::data_key_spec::to_dafny(x.clone()) + }, + _ => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} + }), + GrantTokens: + ::std::rc::Rc::new( + // Have to clone or else this becomes a borrow that can interfere with other branches + match value.grant_tokens.clone() { + Some(val) => + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { + value : ::dafny_runtime::Sequence::from_array( + &val.iter().map(|x| + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) + .collect() + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} + } + ), + Recipient: crate::conversions::recipient_info::option_to_dafny(value.recipient()), + DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest, + >, + client: aws_sdk_kms::Client, +) -> aws_sdk_kms::operation::generate_data_key::builders::GenerateDataKeyFluentBuilder { + client.generate_data_key() + .set_key_id(Some( + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + dafny_value.KeyId(), + ), + )) + .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + ) + ), + _ => None + }) + .set_number_of_bytes(dafny_standard_library::conversion::oint_from_dafny(dafny_value.NumberOfBytes().clone())) + .set_key_spec(match &**dafny_value.KeySpec() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + crate::conversions::data_key_spec::from_dafny(value) + ), + _ => None + }) + .set_grant_tokens(match &**dafny_value.GrantTokens() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) + ), + _ => None + }) + .set_recipient(match &**dafny_value.Recipient() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + crate::conversions::recipient_info::from_dafny(value.clone()) + ), + _ => None + }) + .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_response.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_response.rs new file mode 100644 index 000000000..d406550db --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_response.rs @@ -0,0 +1,16 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: &aws_sdk_kms::operation::generate_data_key::GenerateDataKeyOutput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyResponse, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyResponse::GenerateDataKeyResponse { + CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob), + Plaintext: dafny_standard_library::conversion::oblob_to_dafny(&value.plaintext), + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), + CiphertextForRecipient: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_for_recipient), + }) +} + +// from_dafny ommitted to save time until we get to actual code generation \ No newline at end of file diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext.rs new file mode 100644 index 000000000..e9ea4318b --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext.rs @@ -0,0 +1,41 @@ +pub mod _generate_data_key_without_plaintext_request; + +pub mod _generate_data_key_without_plaintext_response; + +use aws_sdk_kms::error::SdkError; +use crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::*; + +#[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::DependencyTimeoutException(e) => + crate::conversions::error::dependency_timeout_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::DisabledException(e) => + crate::conversions::error::disabled_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::DryRunOperationException(e) => + crate::conversions::error::dry_run_operation_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::InvalidGrantTokenException(e) => + crate::conversions::error::invalid_grant_token_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::InvalidKeyUsageException(e) => + crate::conversions::error::invalid_key_usage_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::KeyUnavailableException(e) => + crate::conversions::error::key_unavailable_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::KmsInternalException(e) => + crate::conversions::error::kms_internal_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::KmsInvalidStateException(e) => + crate::conversions::error::kms_invalid_state_exception::to_dafny(e.clone()), + aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextError::NotFoundException(e) => + crate::conversions::error::not_found_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_request.rs new file mode 100644 index 000000000..6bda4aa02 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_request.rs @@ -0,0 +1,87 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextInput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextRequest, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextRequest::GenerateDataKeyWithoutPlaintextRequest { + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id).Extract(), + EncryptionContext: + ::std::rc::Rc::new(match value.encryption_context() { + Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value : + ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(k), + |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(v), + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} + }), + NumberOfBytes: dafny_standard_library::conversion::oint_to_dafny(value.number_of_bytes), + KeySpec: + ::std::rc::Rc::new(match value.key_spec() { + Some(x) => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { + value: crate::conversions::data_key_spec::to_dafny(x.clone()) + }, + _ => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None {} + }), + GrantTokens: + ::std::rc::Rc::new( + // Have to clone or else this becomes a borrow that can interfere with other branches + match value.grant_tokens.clone() { + Some(val) => + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { + value : ::dafny_runtime::Sequence::from_array( + &val.iter().map(|x| + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(x)) + .collect() + ) + }, + None => crate::implementation_from_dafny::r#_Wrappers_Compile::Option::None{} + } + ), + DryRun: dafny_standard_library::conversion::obool_to_dafny(value.dry_run), + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextRequest, + >, + client: aws_sdk_kms::Client +) -> aws_sdk_kms::operation::generate_data_key_without_plaintext::builders::GenerateDataKeyWithoutPlaintextFluentBuilder{ + client.generate_data_key_without_plaintext() + .set_key_id(Some( + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + dafny_value.KeyId(), + ), + )) + .set_encryption_context( match (*dafny_value.EncryptionContext()).as_ref() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, + ) + ), + _ => None + }) + .set_number_of_bytes(dafny_standard_library::conversion::oint_from_dafny(dafny_value.NumberOfBytes().clone())) + .set_key_spec(match &**dafny_value.KeySpec() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + crate::conversions::data_key_spec::from_dafny(value) + ), + _ => None + }) + .set_grant_tokens(match &**dafny_value.GrantTokens() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) + ), + _ => None + }) + .set_dry_run(dafny_standard_library::conversion::obool_from_dafny(dafny_value.DryRun().clone())) +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_response.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_response.rs new file mode 100644 index 000000000..ed879b5c7 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key_without_plaintext/_generate_data_key_without_plaintext_response.rs @@ -0,0 +1,14 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: &aws_sdk_kms::operation::generate_data_key_without_plaintext::GenerateDataKeyWithoutPlaintextOutput +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextResponse, +>{ + ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyWithoutPlaintextResponse::GenerateDataKeyWithoutPlaintextResponse { + CiphertextBlob: dafny_standard_library::conversion::oblob_to_dafny(&value.ciphertext_blob), + KeyId: dafny_standard_library::conversion::ostring_to_dafny(&value.key_id), + }) +} + +// from_dafny ommitted to save time until we get to actual code generation diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/key_encryption_mechanism.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/key_encryption_mechanism.rs new file mode 100644 index 000000000..220034fdd --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/key_encryption_mechanism.rs @@ -0,0 +1,25 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] + +pub fn to_dafny( + value: aws_sdk_kms::types::KeyEncryptionMechanism, +) -> ::std::rc::Rc{ + match value { + aws_sdk_kms::types::KeyEncryptionMechanism::RsaesOaepSha256 => ::std::rc::Rc::new(crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::KeyEncryptionMechanism::RSAES_OAEP_SHA_256 {}), + // TODO: This should not be a panic, but the Dafny image of the enum shape doesn't have an Unknown variant of any kind, + // so there's no way to succeed. + // See https://github.com/smithy-lang/smithy-dafny/issues/476. + // This could be handled more cleanly if conversion functions returned Results, + // but that would be a large and disruptie change to the overall code flow. + _ => panic!("Unknown enum variant: {}", value), + } +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::KeyEncryptionMechanism, +) -> aws_sdk_kms::types::KeyEncryptionMechanism { + match dafny_value { + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::KeyEncryptionMechanism::RSAES_OAEP_SHA_256 {} => aws_sdk_kms::types::KeyEncryptionMechanism::RsaesOaepSha256, + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/recipient_info.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/recipient_info.rs new file mode 100644 index 000000000..0b6d290b6 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/recipient_info.rs @@ -0,0 +1,89 @@ +use aws_sdk_kms::types::KeyEncryptionMechanism; + +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: aws_sdk_kms::types::RecipientInfo, +) -> ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, +>{ + ::std::rc::Rc::new(to_dafny_plain(&value)) +} + +pub fn to_dafny_plain( + value: &aws_sdk_kms::types::RecipientInfo, +) -> crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo { + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo::RecipientInfo { + AttestationDocument: dafny_standard_library::conversion::oblob_to_dafny(&value.attestation_document), + KeyEncryptionAlgorithm: dafny_standard_library::conversion::option_to_dafny(&value.key_encryption_algorithm, + |x| crate::conversions::key_encryption_mechanism::to_dafny(x.clone())) + } +} + +pub fn option_to_dafny( + value: Option<&aws_sdk_kms::types::RecipientInfo>, +) -> ::std::rc::Rc< + crate::implementation_from_dafny::_Wrappers_Compile::Option< + ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, + >, + >, +>{ + let inner = match value { + None => crate::implementation_from_dafny::_Wrappers_Compile::Option::None {}, + Some(x) => crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { + value: ::std::rc::Rc::new(to_dafny_plain(x)), + }, + }; + ::std::rc::Rc::new(inner) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, + >, +) -> aws_sdk_kms::types::RecipientInfo { + aws_sdk_kms::types::RecipientInfo::builder() + .set_attestation_document(dafny_standard_library::conversion::oblob_from_dafny( + dafny_value.AttestationDocument().clone(), + )) + .set_key_encryption_algorithm(match &**dafny_value.KeyEncryptionAlgorithm() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => Some( + crate::conversions::key_encryption_mechanism::from_dafny(value), + ), + _ => None, + }) + .build() +} + +#[allow(dead_code)] +pub fn plain_from_dafny( + dafny_value: &crate::implementation_from_dafny::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::RecipientInfo, +) -> aws_sdk_kms::types::RecipientInfo { + aws_sdk_kms::types::RecipientInfo::builder() + .set_attestation_document(dafny_standard_library::conversion::oblob_from_dafny( + dafny_value.AttestationDocument().clone(), + )) + .set_key_encryption_algorithm(match &**dafny_value.KeyEncryptionAlgorithm() { + crate::implementation_from_dafny::r#_Wrappers_Compile::Option::Some { value } => Some( + crate::conversions::key_encryption_mechanism::from_dafny(value), + ), + _ => None, + }) + .build() +} + +#[allow(dead_code)] +pub fn option_from_dafny( + dafny_value: ::std::rc::Rc>>, +) -> Option { + match &*dafny_value { + crate::implementation_from_dafny::_Wrappers_Compile::Option::Some { value } => { + Some(plain_from_dafny(value)) + } + _ => None, + } +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/lib.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/lib.rs new file mode 100644 index 000000000..b5e77f9af --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/lib.rs @@ -0,0 +1,3 @@ +mod client; +mod conversions; +pub mod implementation_from_dafny; diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/kms_lite_tests.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/kms_lite_tests.rs new file mode 100644 index 000000000..02ab4070b --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/kms_lite_tests.rs @@ -0,0 +1,6 @@ +mod tests_from_dafny; + +#[test] +fn dafny_tests() { + crate::tests_from_dafny::_module::_default::_Test__Main_() +} diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs new file mode 100644 index 000000000..f061a8096 --- /dev/null +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/tests/tests_from_dafny/mod.rs @@ -0,0 +1,325 @@ +#![allow(warnings, unconditional_panic)] +#![allow(nonstandard_style)] +use ::kms_lite::implementation_from_dafny::*; + +pub mod r#_TestComAmazonawsKms_Compile { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn workAround(literal: &::dafny_runtime::Sequence) -> super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::CiphertextType{ + literal.clone() + } + pub fn BasicDecryptTests() -> () { + let mut CiphertextBlob: ::dafny_runtime::Sequence = ::dafny_runtime::seq![ + 1, 1, 1, 0, 120, 64, 243, 140, 39, 94, 49, 9, 116, 22, 193, 7, 41, 81, 80, 87, 25, + 100, 173, 163, 239, 28, 33, 233, 76, 139, 160, 189, 188, 157, 15, 180, 20, 0, 0, 0, + 98, 48, 96, 6, 9, 42, 134, 72, 134, 247, 13, 1, 7, 6, 160, 83, 48, 81, 2, 1, 0, 48, + 76, 6, 9, 42, 134, 72, 134, 247, 13, 1, 7, 1, 48, 30, 6, 9, 96, 134, 72, 1, 101, 3, + 4, 1, 46, 48, 17, 4, 12, 196, 249, 60, 7, 21, 231, 87, 70, 216, 12, 31, 13, 2, 1, + 16, 128, 31, 222, 119, 162, 112, 88, 153, 39, 197, 21, 182, 116, 176, 120, 174, + 107, 82, 182, 223, 160, 201, 15, 29, 3, 254, 3, 208, 72, 171, 64, 207, 175 + ]; + super::r#_TestComAmazonawsKms_Compile::_default::BasicDecryptTest(&::std::rc::Rc::new(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest::DecryptRequest { + CiphertextBlob: super::r#_TestComAmazonawsKms_Compile::_default::workAround(&CiphertextBlob), + EncryptionContext: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::dafny_runtime::Map<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>>::None {}), + GrantTokens: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}), + KeyId: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Some { + value: super::r#_TestComAmazonawsKms_Compile::_default::keyId() + }), + EncryptionAlgorithm: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + Recipient: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + DryRun: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}) + }), &::dafny_runtime::seq![165, 191, 67, 62], &super::r#_TestComAmazonawsKms_Compile::_default::keyId()); + return (); + } + pub fn BasicGenerateTests() -> () { + super::r#_TestComAmazonawsKms_Compile::_default::BasicGenerateTest(&::std::rc::Rc::new(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::GenerateDataKeyRequest::GenerateDataKeyRequest { + KeyId: super::r#_TestComAmazonawsKms_Compile::_default::keyId(), + EncryptionContext: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::dafny_runtime::Map<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>>::None {}), + NumberOfBytes: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::Some { + value: 32 + }), + KeySpec: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + GrantTokens: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}), + Recipient: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + DryRun: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}) + })); + return (); + } + pub fn BasicEncryptTests() -> () { + super::r#_TestComAmazonawsKms_Compile::_default::BasicEncryptTest(&::std::rc::Rc::new(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::EncryptRequest::EncryptRequest { + KeyId: super::r#_TestComAmazonawsKms_Compile::_default::keyId(), + Plaintext: ::dafny_runtime::seq![97, 115, 100, 102], + EncryptionContext: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::dafny_runtime::Map<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>>::None {}), + GrantTokens: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}), + EncryptionAlgorithm: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + DryRun: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}) + })); + return (); + } + pub fn BasicDecryptTest( + input: &::std::rc::Rc, + expectedPlaintext: &super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::PlaintextType, + expectedKeyId: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out0 = ::dafny_runtime::MaybePlacebo::from(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny::_default::KMSClient()); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out0.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object = valueOrError0.read().Extract(); + let mut ret = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out1 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out1 = ::dafny_runtime::MaybePlacebo::from(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient::Decrypt(::dafny_runtime::md!(client.clone()), input)); + ret = ::dafny_runtime::MaybePlacebo::from(_out1.read()); + if !matches!( + (&ret.read()).as_ref(), + super::r#_Wrappers_Compile::Result::Success { .. } + ) { + panic!("Halt") + }; + let mut r#__let_tmp_rhs0: ::std::rc::Rc = ret.read().value().clone(); + let mut KeyId: ::std::rc::Rc< + super::r#_Wrappers_Compile::Option< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + > = r#__let_tmp_rhs0.KeyId().clone(); + let mut Plaintext: ::std::rc::Rc> = r#__let_tmp_rhs0.Plaintext().clone(); + let mut EncryptionAlgorithm: ::std::rc::Rc>> = r#__let_tmp_rhs0.EncryptionAlgorithm().clone(); + let mut CiphertextBlob: ::std::rc::Rc> = r#__let_tmp_rhs0.CiphertextForRecipient().clone(); + if !matches!( + (&Plaintext).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + if !matches!( + (&KeyId).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + if !(Plaintext.value().clone() == expectedPlaintext.clone()) { + panic!("Halt") + }; + if !(KeyId.value().clone() == expectedKeyId.clone()) { + panic!("Halt") + }; + return (); + } + pub fn BasicGenerateTest( + input: &::std::rc::Rc, + ) -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out2 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out2 = ::dafny_runtime::MaybePlacebo::from(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny::_default::KMSClient()); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out2.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object = valueOrError0.read().Extract(); + let mut ret = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out3 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out3 = ::dafny_runtime::MaybePlacebo::from(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient::GenerateDataKey(::dafny_runtime::md!(client.clone()), input)); + ret = ::dafny_runtime::MaybePlacebo::from(_out3.read()); + if !matches!( + (&ret.read()).as_ref(), + super::r#_Wrappers_Compile::Result::Success { .. } + ) { + panic!("Halt") + }; + let mut r#__let_tmp_rhs1: ::std::rc::Rc = ret.read().value().clone(); + let mut CiphertextBlob: ::std::rc::Rc> = r#__let_tmp_rhs1.CiphertextBlob().clone(); + let mut Plaintext: ::std::rc::Rc> = r#__let_tmp_rhs1.Plaintext().clone(); + let mut KeyId: ::std::rc::Rc< + super::r#_Wrappers_Compile::Option< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + > = r#__let_tmp_rhs1.KeyId().clone(); + let mut CiphertextForRecipient: ::std::rc::Rc> = r#__let_tmp_rhs1.CiphertextForRecipient().clone(); + if !matches!( + (&CiphertextBlob).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + if !matches!( + (&Plaintext).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + if !matches!( + (&KeyId).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + if !(Plaintext.value().cardinality() + == Into::<::dafny_runtime::DafnyInt>::into(input.NumberOfBytes().value().clone())) + { + panic!("Halt") + }; + let mut decryptInput: ::std::rc::Rc = ::std::rc::Rc::new(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest::DecryptRequest { + CiphertextBlob: CiphertextBlob.value().clone(), + EncryptionContext: input.EncryptionContext().clone(), + GrantTokens: input.GrantTokens().clone(), + KeyId: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Some { + value: KeyId.value().clone() + }), + EncryptionAlgorithm: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + Recipient: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + DryRun: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}) + }); + super::r#_TestComAmazonawsKms_Compile::_default::BasicDecryptTest( + &decryptInput, + Plaintext.value(), + input.KeyId(), + ); + return (); + } + pub fn BasicEncryptTest( + input: &::std::rc::Rc, + ) -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out4 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out4 = ::dafny_runtime::MaybePlacebo::from(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny::_default::KMSClient()); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out4.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object = valueOrError0.read().Extract(); + let mut ret = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out5 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out5 = ::dafny_runtime::MaybePlacebo::from(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::IKMSClient::Encrypt(::dafny_runtime::md!(client.clone()), input)); + ret = ::dafny_runtime::MaybePlacebo::from(_out5.read()); + if !matches!( + (&ret.read()).as_ref(), + super::r#_Wrappers_Compile::Result::Success { .. } + ) { + panic!("Halt") + }; + let mut r#__let_tmp_rhs2: ::std::rc::Rc = ret.read().value().clone(); + let mut CiphertextBlob: ::std::rc::Rc> = r#__let_tmp_rhs2.CiphertextBlob().clone(); + let mut KeyId: ::std::rc::Rc< + super::r#_Wrappers_Compile::Option< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + > = r#__let_tmp_rhs2.KeyId().clone(); + let mut EncryptionAlgorithm: ::std::rc::Rc>> = r#__let_tmp_rhs2.EncryptionAlgorithm().clone(); + if !matches!( + (&CiphertextBlob).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + if !matches!( + (&KeyId).as_ref(), + super::r#_Wrappers_Compile::Option::Some { .. } + ) { + panic!("Halt") + }; + let mut decryptInput: ::std::rc::Rc = ::std::rc::Rc::new(super::r#_software_damazon_dcryptography_dservices_dkms_dinternaldafny_dtypes::DecryptRequest::DecryptRequest { + CiphertextBlob: CiphertextBlob.value().clone(), + EncryptionContext: input.EncryptionContext().clone(), + GrantTokens: input.GrantTokens().clone(), + KeyId: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Some { + value: KeyId.value().clone() + }), + EncryptionAlgorithm: input.EncryptionAlgorithm().clone(), + Recipient: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::<::std::rc::Rc>::None {}), + DryRun: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::None {}) + }); + super::r#_TestComAmazonawsKms_Compile::_default::BasicDecryptTest( + &decryptInput, + input.Plaintext(), + input.KeyId(), + ); + return (); + } + pub fn keyId() -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> { + ::dafny_runtime::string_utf16_of( + "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f", + ) + } + pub fn TEST_REGION() -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> { + ::dafny_runtime::string_utf16_of("us-west-2") + } + } + + impl ::dafny_runtime::UpcastObject + for super::r#_TestComAmazonawsKms_Compile::_default + { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +pub mod _module { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn _Test__Main_() -> () { + let mut success: bool = true; + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestComAmazonawsKms.BasicDecryptTests: "# + )) + ); + super::r#_TestComAmazonawsKms_Compile::_default::BasicDecryptTests(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestComAmazonawsKms.BasicGenerateTests: "# + )) + ); + super::r#_TestComAmazonawsKms_Compile::_default::BasicGenerateTests(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestComAmazonawsKms.BasicEncryptTests: "# + )) + ); + super::r#_TestComAmazonawsKms_Compile::_default::BasicEncryptTests(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + if !success { + panic!("Halt") + }; + return (); + } + } + + impl ::dafny_runtime::UpcastObject for super::_module::_default { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +fn main() { + _module::_default::_Test__Main_(); +} diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index 1e8efe7e9..d65992e4a 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -67,9 +67,7 @@ transpile_java: | transpile_implementation_java transpile_test_java # StandardLibrary as a dependency transpile_rust: | transpile_implementation_rust transpile_test_rust -# Override the targets to relocate translated Rust code directly into the main crate, -# instead of the dafny_impl sub-crate. -# We also don't want to delete the src directory since we have an extern in there too. +# Override this target to not insert a dependency on the standard library. _mv_implementation_rust: mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/src/implementation_from_dafny.rs rustfmt runtimes/rust/src/implementation_from_dafny.rs diff --git a/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch index f2dc475ca..a8b1819f9 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch +++ b/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch @@ -74,10 +74,10 @@ index 00000000..fb5e7bf9 \ No newline at end of file diff --git b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs new file mode 100644 -index 00000000..a6a27f6f +index 00000000..8b20a995 --- /dev/null +++ a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs -@@ -0,0 +1,135 @@ +@@ -0,0 +1,175 @@ +use crate::implementation_from_dafny::*; + +pub fn ostring_to_dafny( @@ -158,31 +158,71 @@ index 00000000..a6a27f6f + } +} + ++pub fn blob_to_dafny( ++ input: &::aws_smithy_types::Blob, ++) -> ::dafny_runtime::Sequence { ++ ::dafny_runtime::Sequence::from_array(&input.clone().into_inner()) ++} ++ +pub fn oblob_to_dafny( -+ input: &Option>, ++ input: &Option<::aws_smithy_types::Blob>, +) -> ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>> { + let dafny_value = match input { + Some(b) => _Wrappers_Compile::Option::Some { -+ value: ::dafny_runtime::Sequence::from_array(&b), ++ value: blob_to_dafny(&b), + }, + None => _Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + ++pub fn blob_from_dafny( ++ input: ::dafny_runtime::Sequence, ++) -> ::aws_smithy_types::Blob { ++ ++ ::aws_smithy_types::Blob::new( ++ ::std::rc::Rc::try_unwrap(input.to_array()) ++ .unwrap_or_else(|rc| (*rc).clone()), ++ ) ++} ++ +pub fn oblob_from_dafny( + input: ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>>, -+) -> Option> { ++) -> Option<::aws_smithy_types::Blob> { + if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { -+ Some( -+ ::std::rc::Rc::try_unwrap(input.Extract().to_array()) -+ .unwrap_or_else(|rc| (*rc).clone()), -+ ) ++ Some(blob_from_dafny(input.Extract())) + } else { + None + } +} + ++pub fn option_from_dafny( ++ input: ::std::rc::Rc<_Wrappers_Compile::Option>, ++ converter: fn(&T) -> TR, ++) -> Option { ++ match &*input { ++ _Wrappers_Compile::Option::Some { value } => Some(converter(value)), ++ _Wrappers_Compile::Option::None { } => None, ++ _Wrappers_Compile::Option::_PhantomVariant(_) => panic!(), ++ } ++} ++ ++pub fn option_to_dafny( ++ input: &Option, ++ converter: fn(&TR) -> T, ++) -> ::std::rc::Rc<_Wrappers_Compile::Option> { ++ match input { ++ Some(value) => ::std::rc::Rc::new( ++ _Wrappers_Compile::Option::Some { ++ value: converter(&value) ++ } ++ ), ++ None => ::std::rc::Rc::new( ++ _Wrappers_Compile::Option::None {} ++ ), ++ } ++} ++ +pub fn result_from_dafny( + input: ::std::rc::Rc<_Wrappers_Compile::Result>, + converter_t: fn(&T) -> TR, @@ -196,7 +236,7 @@ index 00000000..a6a27f6f +} + +pub fn result_to_dafny( -+ input: Result, ++ input: &Result, + converter_t: fn(&TR) -> T, + converter_e: fn(&ER) -> E, +) -> ::std::rc::Rc<_Wrappers_Compile::Result> { diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml index 4e7b7b910..a682821e8 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml @@ -7,3 +7,4 @@ edition = "2021" [dependencies] dafny_runtime = { path = "../../../dafny_runtime_rust"} +aws-smithy-types = "1.2.0" diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs index a6a27f6f6..8b20a9950 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs @@ -78,31 +78,71 @@ pub fn olong_from_dafny(input: ::std::rc::Rc<_Wrappers_Compile::Option>) -> } } +pub fn blob_to_dafny( + input: &::aws_smithy_types::Blob, +) -> ::dafny_runtime::Sequence { + ::dafny_runtime::Sequence::from_array(&input.clone().into_inner()) +} + pub fn oblob_to_dafny( - input: &Option>, + input: &Option<::aws_smithy_types::Blob>, ) -> ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>> { let dafny_value = match input { Some(b) => _Wrappers_Compile::Option::Some { - value: ::dafny_runtime::Sequence::from_array(&b), + value: blob_to_dafny(&b), }, None => _Wrappers_Compile::Option::None {}, }; ::std::rc::Rc::new(dafny_value) } +pub fn blob_from_dafny( + input: ::dafny_runtime::Sequence, +) -> ::aws_smithy_types::Blob { + + ::aws_smithy_types::Blob::new( + ::std::rc::Rc::try_unwrap(input.to_array()) + .unwrap_or_else(|rc| (*rc).clone()), + ) +} + pub fn oblob_from_dafny( input: ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>>, -) -> Option> { +) -> Option<::aws_smithy_types::Blob> { if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { - Some( - ::std::rc::Rc::try_unwrap(input.Extract().to_array()) - .unwrap_or_else(|rc| (*rc).clone()), - ) + Some(blob_from_dafny(input.Extract())) } else { None } } +pub fn option_from_dafny( + input: ::std::rc::Rc<_Wrappers_Compile::Option>, + converter: fn(&T) -> TR, +) -> Option { + match &*input { + _Wrappers_Compile::Option::Some { value } => Some(converter(value)), + _Wrappers_Compile::Option::None { } => None, + _Wrappers_Compile::Option::_PhantomVariant(_) => panic!(), + } +} + +pub fn option_to_dafny( + input: &Option, + converter: fn(&TR) -> T, +) -> ::std::rc::Rc<_Wrappers_Compile::Option> { + match input { + Some(value) => ::std::rc::Rc::new( + _Wrappers_Compile::Option::Some { + value: converter(&value) + } + ), + None => ::std::rc::Rc::new( + _Wrappers_Compile::Option::None {} + ), + } +} + pub fn result_from_dafny( input: ::std::rc::Rc<_Wrappers_Compile::Result>, converter_t: fn(&T) -> TR, @@ -116,7 +156,7 @@ pub fn result_from_dafny( - input: Result, + input: &Result, converter_t: fn(&TR) -> T, converter_e: fn(&ER) -> E, ) -> ::std::rc::Rc<_Wrappers_Compile::Result> { diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java index d0440dac4..96e43710b 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java @@ -39,7 +39,6 @@ class RustTestModels extends TestModelTest { DISABLED_TESTS.add("aws-sdks/glue"); DISABLED_TESTS.add("aws-sdks/lakeformation"); DISABLED_TESTS.add("aws-sdks/kms"); - DISABLED_TESTS.add("aws-sdks/kms-lite"); DISABLED_TESTS.add("aws-sdks/sqs"); DISABLED_TESTS.add("aws-sdks/sqs-via-cli"); }