Skip to main content

aws_esdk/deps/com_amazonaws_kms/
client.rs

1// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2// SPDX-License-Identifier: Apache-2.0
3// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4use std::future::Future;
5use tokio::runtime::Builder;
6use tokio::runtime::Handle;
7use tokio::runtime::RuntimeFlavor;
8
9pub fn escape_to_async<F, O>(fut: F) -> O
10where
11    F: Future<Output = O> + Send,
12    O: Send,
13{
14    match Handle::try_current() {
15        Ok(handle) => match handle.runtime_flavor() {
16            RuntimeFlavor::CurrentThread => std::thread::scope(move |t| {
17                t.spawn(move || {
18                    Builder::new_current_thread()
19                        .enable_all()
20                        .build()
21                        .unwrap()
22                        .block_on(fut)
23                })
24                .join()
25                .unwrap()
26            }),
27            _ => tokio::task::block_in_place(move || handle.block_on(fut)),
28        },
29        Err(_) => Builder::new_current_thread()
30            .enable_all()
31            .build()
32            .unwrap()
33            .block_on(fut),
34    }
35}
36
37use crate::deps::com_amazonaws_kms::conversions;
38
39#[derive(::std::clone::Clone, ::std::fmt::Debug)]
40pub struct Client {
41    pub inner: aws_sdk_kms::Client,
42}
43
44impl ::std::cmp::PartialEq for Client {
45    fn eq(&self, other: &Self) -> bool {
46        false
47    }
48}
49
50impl ::std::convert::Into<Client> for aws_sdk_kms::Client {
51    fn into(self) -> Client {
52        Client { inner: self }
53    }
54}
55
56impl dafny_runtime::UpcastObject<::dafny_runtime::DynAny> for Client {
57    ::dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny);
58}
59
60impl dafny_runtime::UpcastObject<dyn crate::r#software::amazon::cryptography::services::kms::internaldafny::types::IKMSClient> for Client {
61          ::dafny_runtime::UpcastObjectFn!(dyn crate::r#software::amazon::cryptography::services::kms::internaldafny::types::IKMSClient);
62        }
63
64impl crate::r#software::amazon::cryptography::services::kms::internaldafny::types::IKMSClient
65    for Client
66{
67    fn CancelKeyDeletion(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CancelKeyDeletionRequest>)
68  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
69    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CancelKeyDeletionResponse>,
70    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
71  >
72    >{
73        let inner_input = crate::deps::com_amazonaws_kms::conversions::cancel_key_deletion::_cancel_key_deletion_request::from_dafny(input.clone());
74        let native_result = escape_to_async(
75            self.inner
76                .cancel_key_deletion()
77                .set_key_id(inner_input.r#key_id)
78                .send(),
79        );
80        crate::standard_library_conversions::result_to_dafny(&native_result,
81    crate::deps::com_amazonaws_kms::conversions::cancel_key_deletion::_cancel_key_deletion_response::to_dafny,
82    crate::deps::com_amazonaws_kms::conversions::cancel_key_deletion::to_dafny_error)
83    }
84 fn ConnectCustomKeyStore(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ConnectCustomKeyStoreRequest>)
85  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
86    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ConnectCustomKeyStoreResponse>,
87    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
88  >
89    >{
90        let inner_input = crate::deps::com_amazonaws_kms::conversions::connect_custom_key_store::_connect_custom_key_store_request::from_dafny(input.clone());
91        let native_result = escape_to_async(
92            self.inner
93                .connect_custom_key_store()
94                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
95                .send(),
96        );
97        crate::standard_library_conversions::result_to_dafny(&native_result,
98    crate::deps::com_amazonaws_kms::conversions::connect_custom_key_store::_connect_custom_key_store_response::to_dafny,
99    crate::deps::com_amazonaws_kms::conversions::connect_custom_key_store::to_dafny_error)
100    }
101    fn CreateAlias(
102        &self,
103        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateAliasRequest>,
104    ) -> dafny_runtime::Rc<
105        crate::r#_Wrappers_Compile::Result<
106            (),
107            dafny_runtime::Rc<
108                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
109            >,
110        >,
111    > {
112        let inner_input = crate::deps::com_amazonaws_kms::conversions::create_alias::_create_alias_request::from_dafny(input.clone());
113        let native_result = escape_to_async(
114            self.inner
115                .create_alias()
116                .set_alias_name(inner_input.r#alias_name)
117                .set_target_key_id(inner_input.r#target_key_id)
118                .send(),
119        );
120        crate::standard_library_conversions::result_to_dafny(
121            &native_result,
122            |x| (),
123            crate::deps::com_amazonaws_kms::conversions::create_alias::to_dafny_error,
124        )
125    }
126 fn CreateCustomKeyStore(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateCustomKeyStoreRequest>)
127  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
128    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateCustomKeyStoreResponse>,
129    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
130  >
131    >{
132        let inner_input = crate::deps::com_amazonaws_kms::conversions::create_custom_key_store::_create_custom_key_store_request::from_dafny(input.clone());
133        let native_result = escape_to_async(
134            self.inner
135                .create_custom_key_store()
136                .set_custom_key_store_name(inner_input.r#custom_key_store_name)
137                .set_cloud_hsm_cluster_id(inner_input.r#cloud_hsm_cluster_id)
138                .set_trust_anchor_certificate(inner_input.r#trust_anchor_certificate)
139                .set_key_store_password(inner_input.r#key_store_password)
140                .set_custom_key_store_type(inner_input.r#custom_key_store_type)
141                .set_xks_proxy_uri_endpoint(inner_input.r#xks_proxy_uri_endpoint)
142                .set_xks_proxy_uri_path(inner_input.r#xks_proxy_uri_path)
143                .set_xks_proxy_vpc_endpoint_service_name(
144                    inner_input.r#xks_proxy_vpc_endpoint_service_name,
145                )
146                .set_xks_proxy_authentication_credential(
147                    inner_input.r#xks_proxy_authentication_credential,
148                )
149                .set_xks_proxy_connectivity(inner_input.r#xks_proxy_connectivity)
150                .send(),
151        );
152        crate::standard_library_conversions::result_to_dafny(&native_result,
153    crate::deps::com_amazonaws_kms::conversions::create_custom_key_store::_create_custom_key_store_response::to_dafny,
154    crate::deps::com_amazonaws_kms::conversions::create_custom_key_store::to_dafny_error)
155    }
156 fn CreateGrant(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateGrantRequest>)
157  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
158    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateGrantResponse>,
159    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
160  >
161    >{
162        let inner_input = crate::deps::com_amazonaws_kms::conversions::create_grant::_create_grant_request::from_dafny(input.clone());
163        let native_result = escape_to_async(
164            self.inner
165                .create_grant()
166                .set_key_id(inner_input.r#key_id)
167                .set_grantee_principal(inner_input.r#grantee_principal)
168                .set_retiring_principal(inner_input.r#retiring_principal)
169                .set_operations(inner_input.r#operations)
170                .set_constraints(inner_input.r#constraints)
171                .set_grant_tokens(inner_input.r#grant_tokens)
172                .set_name(inner_input.r#name)
173                .set_dry_run(inner_input.r#dry_run)
174                .send(),
175        );
176        crate::standard_library_conversions::result_to_dafny(&native_result,
177    crate::deps::com_amazonaws_kms::conversions::create_grant::_create_grant_response::to_dafny,
178    crate::deps::com_amazonaws_kms::conversions::create_grant::to_dafny_error)
179    }
180 fn CreateKey(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateKeyRequest>)
181  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
182    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::CreateKeyResponse>,
183    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
184  >
185    >{
186        let inner_input = crate::deps::com_amazonaws_kms::conversions::create_key::_create_key_request::from_dafny(input.clone());
187        let native_result = escape_to_async(
188            self.inner
189                .create_key()
190                .set_policy(inner_input.r#policy)
191                .set_description(inner_input.r#description)
192                .set_key_usage(inner_input.r#key_usage)
193                .set_customer_master_key_spec(inner_input.r#customer_master_key_spec)
194                .set_key_spec(inner_input.r#key_spec)
195                .set_origin(inner_input.r#origin)
196                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
197                .set_bypass_policy_lockout_safety_check(
198                    inner_input.r#bypass_policy_lockout_safety_check,
199                )
200                .set_tags(inner_input.r#tags)
201                .set_multi_region(inner_input.r#multi_region)
202                .set_xks_key_id(inner_input.r#xks_key_id)
203                .send(),
204        );
205        crate::standard_library_conversions::result_to_dafny(
206            &native_result,
207            crate::deps::com_amazonaws_kms::conversions::create_key::_create_key_response::to_dafny,
208            crate::deps::com_amazonaws_kms::conversions::create_key::to_dafny_error,
209        )
210    }
211 fn Decrypt(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DecryptRequest>)
212  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
213    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DecryptResponse>,
214    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
215  >
216    >{
217        let inner_input =
218            crate::deps::com_amazonaws_kms::conversions::decrypt::_decrypt_request::from_dafny(
219                input.clone(),
220            );
221        let native_result = escape_to_async(
222            self.inner
223                .decrypt()
224                .set_ciphertext_blob(inner_input.r#ciphertext_blob)
225                .set_encryption_context(inner_input.r#encryption_context)
226                .set_grant_tokens(inner_input.r#grant_tokens)
227                .set_key_id(inner_input.r#key_id)
228                .set_encryption_algorithm(inner_input.r#encryption_algorithm)
229                .set_recipient(inner_input.r#recipient)
230                .set_dry_run(inner_input.r#dry_run)
231                .send(),
232        );
233        crate::standard_library_conversions::result_to_dafny(
234            &native_result,
235            crate::deps::com_amazonaws_kms::conversions::decrypt::_decrypt_response::to_dafny,
236            crate::deps::com_amazonaws_kms::conversions::decrypt::to_dafny_error,
237        )
238    }
239    fn DeleteAlias(
240        &self,
241        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DeleteAliasRequest>,
242    ) -> dafny_runtime::Rc<
243        crate::r#_Wrappers_Compile::Result<
244            (),
245            dafny_runtime::Rc<
246                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
247            >,
248        >,
249    > {
250        let inner_input = crate::deps::com_amazonaws_kms::conversions::delete_alias::_delete_alias_request::from_dafny(input.clone());
251        let native_result = escape_to_async(
252            self.inner
253                .delete_alias()
254                .set_alias_name(inner_input.r#alias_name)
255                .send(),
256        );
257        crate::standard_library_conversions::result_to_dafny(
258            &native_result,
259            |x| (),
260            crate::deps::com_amazonaws_kms::conversions::delete_alias::to_dafny_error,
261        )
262    }
263 fn DeleteCustomKeyStore(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DeleteCustomKeyStoreRequest>)
264  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
265    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DeleteCustomKeyStoreResponse>,
266    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
267  >
268    >{
269        let inner_input = crate::deps::com_amazonaws_kms::conversions::delete_custom_key_store::_delete_custom_key_store_request::from_dafny(input.clone());
270        let native_result = escape_to_async(
271            self.inner
272                .delete_custom_key_store()
273                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
274                .send(),
275        );
276        crate::standard_library_conversions::result_to_dafny(&native_result,
277    crate::deps::com_amazonaws_kms::conversions::delete_custom_key_store::_delete_custom_key_store_response::to_dafny,
278    crate::deps::com_amazonaws_kms::conversions::delete_custom_key_store::to_dafny_error)
279    }
280    fn DeleteImportedKeyMaterial(
281        &self,
282        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DeleteImportedKeyMaterialRequest>,
283    ) -> dafny_runtime::Rc<
284        crate::r#_Wrappers_Compile::Result<
285            (),
286            dafny_runtime::Rc<
287                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
288            >,
289        >,
290    > {
291        let inner_input = crate::deps::com_amazonaws_kms::conversions::delete_imported_key_material::_delete_imported_key_material_request::from_dafny(input.clone());
292        let native_result = escape_to_async(
293            self.inner
294                .delete_imported_key_material()
295                .set_key_id(inner_input.r#key_id)
296                .send(),
297        );
298        crate::standard_library_conversions::result_to_dafny(&native_result,
299    |x| (),
300    crate::deps::com_amazonaws_kms::conversions::delete_imported_key_material::to_dafny_error)
301    }
302 fn DeriveSharedSecret(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DeriveSharedSecretRequest>)
303  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
304    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DeriveSharedSecretResponse>,
305    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
306  >
307    >{
308        let inner_input = crate::deps::com_amazonaws_kms::conversions::derive_shared_secret::_derive_shared_secret_request::from_dafny(input.clone());
309        let native_result = escape_to_async(
310            self.inner
311                .derive_shared_secret()
312                .set_key_id(inner_input.r#key_id)
313                .set_key_agreement_algorithm(inner_input.r#key_agreement_algorithm)
314                .set_public_key(inner_input.r#public_key)
315                .set_grant_tokens(inner_input.r#grant_tokens)
316                .set_dry_run(inner_input.r#dry_run)
317                .set_recipient(inner_input.r#recipient)
318                .send(),
319        );
320        crate::standard_library_conversions::result_to_dafny(&native_result,
321    crate::deps::com_amazonaws_kms::conversions::derive_shared_secret::_derive_shared_secret_response::to_dafny,
322    crate::deps::com_amazonaws_kms::conversions::derive_shared_secret::to_dafny_error)
323    }
324 fn DescribeCustomKeyStores(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DescribeCustomKeyStoresRequest>)
325  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
326    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DescribeCustomKeyStoresResponse>,
327    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
328  >
329    >{
330        let inner_input = crate::deps::com_amazonaws_kms::conversions::describe_custom_key_stores::_describe_custom_key_stores_request::from_dafny(input.clone());
331        let native_result = escape_to_async(
332            self.inner
333                .describe_custom_key_stores()
334                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
335                .set_custom_key_store_name(inner_input.r#custom_key_store_name)
336                .set_limit(inner_input.r#limit)
337                .set_marker(inner_input.r#marker)
338                .send(),
339        );
340        crate::standard_library_conversions::result_to_dafny(&native_result,
341    crate::deps::com_amazonaws_kms::conversions::describe_custom_key_stores::_describe_custom_key_stores_response::to_dafny,
342    crate::deps::com_amazonaws_kms::conversions::describe_custom_key_stores::to_dafny_error)
343    }
344 fn DescribeKey(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DescribeKeyRequest>)
345  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
346    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DescribeKeyResponse>,
347    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
348  >
349    >{
350        let inner_input = crate::deps::com_amazonaws_kms::conversions::describe_key::_describe_key_request::from_dafny(input.clone());
351        let native_result = escape_to_async(
352            self.inner
353                .describe_key()
354                .set_key_id(inner_input.r#key_id)
355                .set_grant_tokens(inner_input.r#grant_tokens)
356                .send(),
357        );
358        crate::standard_library_conversions::result_to_dafny(&native_result,
359    crate::deps::com_amazonaws_kms::conversions::describe_key::_describe_key_response::to_dafny,
360    crate::deps::com_amazonaws_kms::conversions::describe_key::to_dafny_error)
361    }
362    fn DisableKey(
363        &self,
364        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DisableKeyRequest>,
365    ) -> dafny_runtime::Rc<
366        crate::r#_Wrappers_Compile::Result<
367            (),
368            dafny_runtime::Rc<
369                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
370            >,
371        >,
372    > {
373        let inner_input = crate::deps::com_amazonaws_kms::conversions::disable_key::_disable_key_request::from_dafny(input.clone());
374        let native_result = escape_to_async(
375            self.inner
376                .disable_key()
377                .set_key_id(inner_input.r#key_id)
378                .send(),
379        );
380        crate::standard_library_conversions::result_to_dafny(
381            &native_result,
382            |x| (),
383            crate::deps::com_amazonaws_kms::conversions::disable_key::to_dafny_error,
384        )
385    }
386    fn DisableKeyRotation(
387        &self,
388        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DisableKeyRotationRequest>,
389    ) -> dafny_runtime::Rc<
390        crate::r#_Wrappers_Compile::Result<
391            (),
392            dafny_runtime::Rc<
393                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
394            >,
395        >,
396    > {
397        let inner_input = crate::deps::com_amazonaws_kms::conversions::disable_key_rotation::_disable_key_rotation_request::from_dafny(input.clone());
398        let native_result = escape_to_async(
399            self.inner
400                .disable_key_rotation()
401                .set_key_id(inner_input.r#key_id)
402                .send(),
403        );
404        crate::standard_library_conversions::result_to_dafny(
405            &native_result,
406            |x| (),
407            crate::deps::com_amazonaws_kms::conversions::disable_key_rotation::to_dafny_error,
408        )
409    }
410 fn DisconnectCustomKeyStore(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DisconnectCustomKeyStoreRequest>)
411  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
412    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::DisconnectCustomKeyStoreResponse>,
413    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
414  >
415    >{
416        let inner_input = crate::deps::com_amazonaws_kms::conversions::disconnect_custom_key_store::_disconnect_custom_key_store_request::from_dafny(input.clone());
417        let native_result = escape_to_async(
418            self.inner
419                .disconnect_custom_key_store()
420                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
421                .send(),
422        );
423        crate::standard_library_conversions::result_to_dafny(&native_result,
424    crate::deps::com_amazonaws_kms::conversions::disconnect_custom_key_store::_disconnect_custom_key_store_response::to_dafny,
425    crate::deps::com_amazonaws_kms::conversions::disconnect_custom_key_store::to_dafny_error)
426    }
427    fn EnableKey(
428        &self,
429        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::EnableKeyRequest>,
430    ) -> dafny_runtime::Rc<
431        crate::r#_Wrappers_Compile::Result<
432            (),
433            dafny_runtime::Rc<
434                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
435            >,
436        >,
437    > {
438        let inner_input = crate::deps::com_amazonaws_kms::conversions::enable_key::_enable_key_request::from_dafny(input.clone());
439        let native_result = escape_to_async(
440            self.inner
441                .enable_key()
442                .set_key_id(inner_input.r#key_id)
443                .send(),
444        );
445        crate::standard_library_conversions::result_to_dafny(
446            &native_result,
447            |x| (),
448            crate::deps::com_amazonaws_kms::conversions::enable_key::to_dafny_error,
449        )
450    }
451    fn EnableKeyRotation(
452        &self,
453        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::EnableKeyRotationRequest>,
454    ) -> dafny_runtime::Rc<
455        crate::r#_Wrappers_Compile::Result<
456            (),
457            dafny_runtime::Rc<
458                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
459            >,
460        >,
461    > {
462        let inner_input = crate::deps::com_amazonaws_kms::conversions::enable_key_rotation::_enable_key_rotation_request::from_dafny(input.clone());
463        let native_result = escape_to_async(
464            self.inner
465                .enable_key_rotation()
466                .set_key_id(inner_input.r#key_id)
467                .set_rotation_period_in_days(inner_input.r#rotation_period_in_days)
468                .send(),
469        );
470        crate::standard_library_conversions::result_to_dafny(
471            &native_result,
472            |x| (),
473            crate::deps::com_amazonaws_kms::conversions::enable_key_rotation::to_dafny_error,
474        )
475    }
476 fn Encrypt(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::EncryptRequest>)
477  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
478    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::EncryptResponse>,
479    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
480  >
481    >{
482        let inner_input =
483            crate::deps::com_amazonaws_kms::conversions::encrypt::_encrypt_request::from_dafny(
484                input.clone(),
485            );
486        let native_result = escape_to_async(
487            self.inner
488                .encrypt()
489                .set_key_id(inner_input.r#key_id)
490                .set_plaintext(inner_input.r#plaintext)
491                .set_encryption_context(inner_input.r#encryption_context)
492                .set_grant_tokens(inner_input.r#grant_tokens)
493                .set_encryption_algorithm(inner_input.r#encryption_algorithm)
494                .set_dry_run(inner_input.r#dry_run)
495                .send(),
496        );
497        crate::standard_library_conversions::result_to_dafny(
498            &native_result,
499            crate::deps::com_amazonaws_kms::conversions::encrypt::_encrypt_response::to_dafny,
500            crate::deps::com_amazonaws_kms::conversions::encrypt::to_dafny_error,
501        )
502    }
503 fn GenerateDataKey(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyRequest>)
504  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
505    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyResponse>,
506    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
507  >
508    >{
509        let inner_input = crate::deps::com_amazonaws_kms::conversions::generate_data_key::_generate_data_key_request::from_dafny(input.clone());
510        let native_result = escape_to_async(
511            self.inner
512                .generate_data_key()
513                .set_key_id(inner_input.r#key_id)
514                .set_encryption_context(inner_input.r#encryption_context)
515                .set_number_of_bytes(inner_input.r#number_of_bytes)
516                .set_key_spec(inner_input.r#key_spec)
517                .set_grant_tokens(inner_input.r#grant_tokens)
518                .set_recipient(inner_input.r#recipient)
519                .set_dry_run(inner_input.r#dry_run)
520                .send(),
521        );
522        crate::standard_library_conversions::result_to_dafny(&native_result,
523    crate::deps::com_amazonaws_kms::conversions::generate_data_key::_generate_data_key_response::to_dafny,
524    crate::deps::com_amazonaws_kms::conversions::generate_data_key::to_dafny_error)
525    }
526 fn GenerateDataKeyPair(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyPairRequest>)
527  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
528    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyPairResponse>,
529    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
530  >
531    >{
532        let inner_input = crate::deps::com_amazonaws_kms::conversions::generate_data_key_pair::_generate_data_key_pair_request::from_dafny(input.clone());
533        let native_result = escape_to_async(
534            self.inner
535                .generate_data_key_pair()
536                .set_encryption_context(inner_input.r#encryption_context)
537                .set_key_id(inner_input.r#key_id)
538                .set_key_pair_spec(inner_input.r#key_pair_spec)
539                .set_grant_tokens(inner_input.r#grant_tokens)
540                .set_recipient(inner_input.r#recipient)
541                .set_dry_run(inner_input.r#dry_run)
542                .send(),
543        );
544        crate::standard_library_conversions::result_to_dafny(&native_result,
545    crate::deps::com_amazonaws_kms::conversions::generate_data_key_pair::_generate_data_key_pair_response::to_dafny,
546    crate::deps::com_amazonaws_kms::conversions::generate_data_key_pair::to_dafny_error)
547    }
548 fn GenerateDataKeyPairWithoutPlaintext(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyPairWithoutPlaintextRequest>)
549  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
550    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyPairWithoutPlaintextResponse>,
551    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
552  >
553    >{
554        let inner_input = crate::deps::com_amazonaws_kms::conversions::generate_data_key_pair_without_plaintext::_generate_data_key_pair_without_plaintext_request::from_dafny(input.clone());
555        let native_result = escape_to_async(
556            self.inner
557                .generate_data_key_pair_without_plaintext()
558                .set_encryption_context(inner_input.r#encryption_context)
559                .set_key_id(inner_input.r#key_id)
560                .set_key_pair_spec(inner_input.r#key_pair_spec)
561                .set_grant_tokens(inner_input.r#grant_tokens)
562                .set_dry_run(inner_input.r#dry_run)
563                .send(),
564        );
565        crate::standard_library_conversions::result_to_dafny(&native_result,
566    crate::deps::com_amazonaws_kms::conversions::generate_data_key_pair_without_plaintext::_generate_data_key_pair_without_plaintext_response::to_dafny,
567    crate::deps::com_amazonaws_kms::conversions::generate_data_key_pair_without_plaintext::to_dafny_error)
568    }
569 fn GenerateDataKeyWithoutPlaintext(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyWithoutPlaintextRequest>)
570  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
571    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateDataKeyWithoutPlaintextResponse>,
572    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
573  >
574    >{
575        let inner_input = crate::deps::com_amazonaws_kms::conversions::generate_data_key_without_plaintext::_generate_data_key_without_plaintext_request::from_dafny(input.clone());
576        let native_result = escape_to_async(
577            self.inner
578                .generate_data_key_without_plaintext()
579                .set_key_id(inner_input.r#key_id)
580                .set_encryption_context(inner_input.r#encryption_context)
581                .set_key_spec(inner_input.r#key_spec)
582                .set_number_of_bytes(inner_input.r#number_of_bytes)
583                .set_grant_tokens(inner_input.r#grant_tokens)
584                .set_dry_run(inner_input.r#dry_run)
585                .send(),
586        );
587        crate::standard_library_conversions::result_to_dafny(&native_result,
588    crate::deps::com_amazonaws_kms::conversions::generate_data_key_without_plaintext::_generate_data_key_without_plaintext_response::to_dafny,
589    crate::deps::com_amazonaws_kms::conversions::generate_data_key_without_plaintext::to_dafny_error)
590    }
591 fn GenerateMac(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateMacRequest>)
592  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
593    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateMacResponse>,
594    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
595  >
596    >{
597        let inner_input = crate::deps::com_amazonaws_kms::conversions::generate_mac::_generate_mac_request::from_dafny(input.clone());
598        let native_result = escape_to_async(
599            self.inner
600                .generate_mac()
601                .set_message(inner_input.r#message)
602                .set_key_id(inner_input.r#key_id)
603                .set_mac_algorithm(inner_input.r#mac_algorithm)
604                .set_grant_tokens(inner_input.r#grant_tokens)
605                .set_dry_run(inner_input.r#dry_run)
606                .send(),
607        );
608        crate::standard_library_conversions::result_to_dafny(&native_result,
609    crate::deps::com_amazonaws_kms::conversions::generate_mac::_generate_mac_response::to_dafny,
610    crate::deps::com_amazonaws_kms::conversions::generate_mac::to_dafny_error)
611    }
612 fn GenerateRandom(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateRandomRequest>)
613  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
614    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GenerateRandomResponse>,
615    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
616  >
617    >{
618        let inner_input = crate::deps::com_amazonaws_kms::conversions::generate_random::_generate_random_request::from_dafny(input.clone());
619        let native_result = escape_to_async(
620            self.inner
621                .generate_random()
622                .set_number_of_bytes(inner_input.r#number_of_bytes)
623                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
624                .set_recipient(inner_input.r#recipient)
625                .send(),
626        );
627        crate::standard_library_conversions::result_to_dafny(&native_result,
628    crate::deps::com_amazonaws_kms::conversions::generate_random::_generate_random_response::to_dafny,
629    crate::deps::com_amazonaws_kms::conversions::generate_random::to_dafny_error)
630    }
631 fn GetKeyPolicy(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetKeyPolicyRequest>)
632  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
633    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetKeyPolicyResponse>,
634    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
635  >
636    >{
637        let inner_input = crate::deps::com_amazonaws_kms::conversions::get_key_policy::_get_key_policy_request::from_dafny(input.clone());
638        let native_result = escape_to_async(
639            self.inner
640                .get_key_policy()
641                .set_key_id(inner_input.r#key_id)
642                .set_policy_name(inner_input.r#policy_name)
643                .send(),
644        );
645        crate::standard_library_conversions::result_to_dafny(&native_result,
646    crate::deps::com_amazonaws_kms::conversions::get_key_policy::_get_key_policy_response::to_dafny,
647    crate::deps::com_amazonaws_kms::conversions::get_key_policy::to_dafny_error)
648    }
649 fn GetKeyRotationStatus(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetKeyRotationStatusRequest>)
650  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
651    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetKeyRotationStatusResponse>,
652    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
653  >
654    >{
655        let inner_input = crate::deps::com_amazonaws_kms::conversions::get_key_rotation_status::_get_key_rotation_status_request::from_dafny(input.clone());
656        let native_result = escape_to_async(
657            self.inner
658                .get_key_rotation_status()
659                .set_key_id(inner_input.r#key_id)
660                .send(),
661        );
662        crate::standard_library_conversions::result_to_dafny(&native_result,
663    crate::deps::com_amazonaws_kms::conversions::get_key_rotation_status::_get_key_rotation_status_response::to_dafny,
664    crate::deps::com_amazonaws_kms::conversions::get_key_rotation_status::to_dafny_error)
665    }
666 fn GetParametersForImport(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetParametersForImportRequest>)
667  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
668    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetParametersForImportResponse>,
669    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
670  >
671    >{
672        let inner_input = crate::deps::com_amazonaws_kms::conversions::get_parameters_for_import::_get_parameters_for_import_request::from_dafny(input.clone());
673        let native_result = escape_to_async(
674            self.inner
675                .get_parameters_for_import()
676                .set_key_id(inner_input.r#key_id)
677                .set_wrapping_algorithm(inner_input.r#wrapping_algorithm)
678                .set_wrapping_key_spec(inner_input.r#wrapping_key_spec)
679                .send(),
680        );
681        crate::standard_library_conversions::result_to_dafny(&native_result,
682    crate::deps::com_amazonaws_kms::conversions::get_parameters_for_import::_get_parameters_for_import_response::to_dafny,
683    crate::deps::com_amazonaws_kms::conversions::get_parameters_for_import::to_dafny_error)
684    }
685 fn GetPublicKey(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetPublicKeyRequest>)
686  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
687    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GetPublicKeyResponse>,
688    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
689  >
690    >{
691        let inner_input = crate::deps::com_amazonaws_kms::conversions::get_public_key::_get_public_key_request::from_dafny(input.clone());
692        let native_result = escape_to_async(
693            self.inner
694                .get_public_key()
695                .set_key_id(inner_input.r#key_id)
696                .set_grant_tokens(inner_input.r#grant_tokens)
697                .send(),
698        );
699        crate::standard_library_conversions::result_to_dafny(&native_result,
700    crate::deps::com_amazonaws_kms::conversions::get_public_key::_get_public_key_response::to_dafny,
701    crate::deps::com_amazonaws_kms::conversions::get_public_key::to_dafny_error)
702    }
703 fn ImportKeyMaterial(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ImportKeyMaterialRequest>)
704  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
705    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ImportKeyMaterialResponse>,
706    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
707  >
708    >{
709        let inner_input = crate::deps::com_amazonaws_kms::conversions::import_key_material::_import_key_material_request::from_dafny(input.clone());
710        let native_result = escape_to_async(
711            self.inner
712                .import_key_material()
713                .set_key_id(inner_input.r#key_id)
714                .set_import_token(inner_input.r#import_token)
715                .set_encrypted_key_material(inner_input.r#encrypted_key_material)
716                .set_valid_to(inner_input.r#valid_to)
717                .set_expiration_model(inner_input.r#expiration_model)
718                .send(),
719        );
720        crate::standard_library_conversions::result_to_dafny(&native_result,
721    crate::deps::com_amazonaws_kms::conversions::import_key_material::_import_key_material_response::to_dafny,
722    crate::deps::com_amazonaws_kms::conversions::import_key_material::to_dafny_error)
723    }
724 fn ListAliases(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListAliasesRequest>)
725  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
726    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListAliasesResponse>,
727    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
728  >
729    >{
730        let inner_input = crate::deps::com_amazonaws_kms::conversions::list_aliases::_list_aliases_request::from_dafny(input.clone());
731        let native_result = escape_to_async(
732            self.inner
733                .list_aliases()
734                .set_key_id(inner_input.r#key_id)
735                .set_limit(inner_input.r#limit)
736                .set_marker(inner_input.r#marker)
737                .send(),
738        );
739        crate::standard_library_conversions::result_to_dafny(&native_result,
740    crate::deps::com_amazonaws_kms::conversions::list_aliases::_list_aliases_response::to_dafny,
741    crate::deps::com_amazonaws_kms::conversions::list_aliases::to_dafny_error)
742    }
743 fn ListGrants(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListGrantsRequest>)
744  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
745    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListGrantsResponse>,
746    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
747  >
748    >{
749        let inner_input = crate::deps::com_amazonaws_kms::conversions::list_grants::_list_grants_request::from_dafny(input.clone());
750        let native_result = escape_to_async(
751            self.inner
752                .list_grants()
753                .set_limit(inner_input.r#limit)
754                .set_marker(inner_input.r#marker)
755                .set_key_id(inner_input.r#key_id)
756                .set_grant_id(inner_input.r#grant_id)
757                .set_grantee_principal(inner_input.r#grantee_principal)
758                .send(),
759        );
760        crate::standard_library_conversions::result_to_dafny(&native_result,
761    crate::deps::com_amazonaws_kms::conversions::list_grants::_list_grants_response::to_dafny,
762    crate::deps::com_amazonaws_kms::conversions::list_grants::to_dafny_error)
763    }
764 fn ListKeyPolicies(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListKeyPoliciesRequest>)
765  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
766    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListKeyPoliciesResponse>,
767    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
768  >
769    >{
770        let inner_input = crate::deps::com_amazonaws_kms::conversions::list_key_policies::_list_key_policies_request::from_dafny(input.clone());
771        let native_result = escape_to_async(
772            self.inner
773                .list_key_policies()
774                .set_key_id(inner_input.r#key_id)
775                .set_limit(inner_input.r#limit)
776                .set_marker(inner_input.r#marker)
777                .send(),
778        );
779        crate::standard_library_conversions::result_to_dafny(&native_result,
780    crate::deps::com_amazonaws_kms::conversions::list_key_policies::_list_key_policies_response::to_dafny,
781    crate::deps::com_amazonaws_kms::conversions::list_key_policies::to_dafny_error)
782    }
783 fn ListKeyRotations(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListKeyRotationsRequest>)
784  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
785    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListKeyRotationsResponse>,
786    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
787  >
788    >{
789        let inner_input = crate::deps::com_amazonaws_kms::conversions::list_key_rotations::_list_key_rotations_request::from_dafny(input.clone());
790        let native_result = escape_to_async(
791            self.inner
792                .list_key_rotations()
793                .set_key_id(inner_input.r#key_id)
794                .set_limit(inner_input.r#limit)
795                .set_marker(inner_input.r#marker)
796                .send(),
797        );
798        crate::standard_library_conversions::result_to_dafny(&native_result,
799    crate::deps::com_amazonaws_kms::conversions::list_key_rotations::_list_key_rotations_response::to_dafny,
800    crate::deps::com_amazonaws_kms::conversions::list_key_rotations::to_dafny_error)
801    }
802 fn ListKeys(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListKeysRequest>)
803  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
804    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListKeysResponse>,
805    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
806  >
807    >{
808        let inner_input =
809            crate::deps::com_amazonaws_kms::conversions::list_keys::_list_keys_request::from_dafny(
810                input.clone(),
811            );
812        let native_result = escape_to_async(
813            self.inner
814                .list_keys()
815                .set_limit(inner_input.r#limit)
816                .set_marker(inner_input.r#marker)
817                .send(),
818        );
819        crate::standard_library_conversions::result_to_dafny(
820            &native_result,
821            crate::deps::com_amazonaws_kms::conversions::list_keys::_list_keys_response::to_dafny,
822            crate::deps::com_amazonaws_kms::conversions::list_keys::to_dafny_error,
823        )
824    }
825 fn ListResourceTags(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListResourceTagsRequest>)
826  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
827    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ListResourceTagsResponse>,
828    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
829  >
830    >{
831        let inner_input = crate::deps::com_amazonaws_kms::conversions::list_resource_tags::_list_resource_tags_request::from_dafny(input.clone());
832        let native_result = escape_to_async(
833            self.inner
834                .list_resource_tags()
835                .set_key_id(inner_input.r#key_id)
836                .set_limit(inner_input.r#limit)
837                .set_marker(inner_input.r#marker)
838                .send(),
839        );
840        crate::standard_library_conversions::result_to_dafny(&native_result,
841    crate::deps::com_amazonaws_kms::conversions::list_resource_tags::_list_resource_tags_response::to_dafny,
842    crate::deps::com_amazonaws_kms::conversions::list_resource_tags::to_dafny_error)
843    }
844    fn PutKeyPolicy(
845        &self,
846        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::PutKeyPolicyRequest>,
847    ) -> dafny_runtime::Rc<
848        crate::r#_Wrappers_Compile::Result<
849            (),
850            dafny_runtime::Rc<
851                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
852            >,
853        >,
854    > {
855        let inner_input = crate::deps::com_amazonaws_kms::conversions::put_key_policy::_put_key_policy_request::from_dafny(input.clone());
856        let native_result = escape_to_async(
857            self.inner
858                .put_key_policy()
859                .set_key_id(inner_input.r#key_id)
860                .set_policy_name(inner_input.r#policy_name)
861                .set_policy(inner_input.r#policy)
862                .set_bypass_policy_lockout_safety_check(
863                    inner_input.r#bypass_policy_lockout_safety_check,
864                )
865                .send(),
866        );
867        crate::standard_library_conversions::result_to_dafny(
868            &native_result,
869            |x| (),
870            crate::deps::com_amazonaws_kms::conversions::put_key_policy::to_dafny_error,
871        )
872    }
873 fn ReEncrypt(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ReEncryptRequest>)
874  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
875    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ReEncryptResponse>,
876    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
877  >
878    >{
879        let inner_input = crate::deps::com_amazonaws_kms::conversions::re_encrypt::_re_encrypt_request::from_dafny(input.clone());
880        let native_result = escape_to_async(
881            self.inner
882                .re_encrypt()
883                .set_ciphertext_blob(inner_input.r#ciphertext_blob)
884                .set_source_encryption_context(inner_input.r#source_encryption_context)
885                .set_source_key_id(inner_input.r#source_key_id)
886                .set_destination_key_id(inner_input.r#destination_key_id)
887                .set_destination_encryption_context(inner_input.r#destination_encryption_context)
888                .set_source_encryption_algorithm(inner_input.r#source_encryption_algorithm)
889                .set_destination_encryption_algorithm(
890                    inner_input.r#destination_encryption_algorithm,
891                )
892                .set_grant_tokens(inner_input.r#grant_tokens)
893                .set_dry_run(inner_input.r#dry_run)
894                .send(),
895        );
896        crate::standard_library_conversions::result_to_dafny(
897            &native_result,
898            crate::deps::com_amazonaws_kms::conversions::re_encrypt::_re_encrypt_response::to_dafny,
899            crate::deps::com_amazonaws_kms::conversions::re_encrypt::to_dafny_error,
900        )
901    }
902 fn ReplicateKey(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ReplicateKeyRequest>)
903  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
904    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ReplicateKeyResponse>,
905    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
906  >
907    >{
908        let inner_input = crate::deps::com_amazonaws_kms::conversions::replicate_key::_replicate_key_request::from_dafny(input.clone());
909        let native_result = escape_to_async(
910            self.inner
911                .replicate_key()
912                .set_key_id(inner_input.r#key_id)
913                .set_replica_region(inner_input.r#replica_region)
914                .set_policy(inner_input.r#policy)
915                .set_bypass_policy_lockout_safety_check(
916                    inner_input.r#bypass_policy_lockout_safety_check,
917                )
918                .set_description(inner_input.r#description)
919                .set_tags(inner_input.r#tags)
920                .send(),
921        );
922        crate::standard_library_conversions::result_to_dafny(&native_result,
923    crate::deps::com_amazonaws_kms::conversions::replicate_key::_replicate_key_response::to_dafny,
924    crate::deps::com_amazonaws_kms::conversions::replicate_key::to_dafny_error)
925    }
926    fn RetireGrant(
927        &self,
928        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::RetireGrantRequest>,
929    ) -> dafny_runtime::Rc<
930        crate::r#_Wrappers_Compile::Result<
931            (),
932            dafny_runtime::Rc<
933                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
934            >,
935        >,
936    > {
937        let inner_input = crate::deps::com_amazonaws_kms::conversions::retire_grant::_retire_grant_request::from_dafny(input.clone());
938        let native_result = escape_to_async(
939            self.inner
940                .retire_grant()
941                .set_grant_token(inner_input.r#grant_token)
942                .set_key_id(inner_input.r#key_id)
943                .set_grant_id(inner_input.r#grant_id)
944                .set_dry_run(inner_input.r#dry_run)
945                .send(),
946        );
947        crate::standard_library_conversions::result_to_dafny(
948            &native_result,
949            |x| (),
950            crate::deps::com_amazonaws_kms::conversions::retire_grant::to_dafny_error,
951        )
952    }
953    fn RevokeGrant(
954        &self,
955        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::RevokeGrantRequest>,
956    ) -> dafny_runtime::Rc<
957        crate::r#_Wrappers_Compile::Result<
958            (),
959            dafny_runtime::Rc<
960                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
961            >,
962        >,
963    > {
964        let inner_input = crate::deps::com_amazonaws_kms::conversions::revoke_grant::_revoke_grant_request::from_dafny(input.clone());
965        let native_result = escape_to_async(
966            self.inner
967                .revoke_grant()
968                .set_key_id(inner_input.r#key_id)
969                .set_grant_id(inner_input.r#grant_id)
970                .set_dry_run(inner_input.r#dry_run)
971                .send(),
972        );
973        crate::standard_library_conversions::result_to_dafny(
974            &native_result,
975            |x| (),
976            crate::deps::com_amazonaws_kms::conversions::revoke_grant::to_dafny_error,
977        )
978    }
979 fn RotateKeyOnDemand(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::RotateKeyOnDemandRequest>)
980  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
981    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::RotateKeyOnDemandResponse>,
982    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
983  >
984    >{
985        let inner_input = crate::deps::com_amazonaws_kms::conversions::rotate_key_on_demand::_rotate_key_on_demand_request::from_dafny(input.clone());
986        let native_result = escape_to_async(
987            self.inner
988                .rotate_key_on_demand()
989                .set_key_id(inner_input.r#key_id)
990                .send(),
991        );
992        crate::standard_library_conversions::result_to_dafny(&native_result,
993    crate::deps::com_amazonaws_kms::conversions::rotate_key_on_demand::_rotate_key_on_demand_response::to_dafny,
994    crate::deps::com_amazonaws_kms::conversions::rotate_key_on_demand::to_dafny_error)
995    }
996 fn ScheduleKeyDeletion(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ScheduleKeyDeletionRequest>)
997  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
998    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::ScheduleKeyDeletionResponse>,
999    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
1000  >
1001    >{
1002        let inner_input = crate::deps::com_amazonaws_kms::conversions::schedule_key_deletion::_schedule_key_deletion_request::from_dafny(input.clone());
1003        let native_result = escape_to_async(
1004            self.inner
1005                .schedule_key_deletion()
1006                .set_key_id(inner_input.r#key_id)
1007                .set_pending_window_in_days(inner_input.r#pending_window_in_days)
1008                .send(),
1009        );
1010        crate::standard_library_conversions::result_to_dafny(&native_result,
1011    crate::deps::com_amazonaws_kms::conversions::schedule_key_deletion::_schedule_key_deletion_response::to_dafny,
1012    crate::deps::com_amazonaws_kms::conversions::schedule_key_deletion::to_dafny_error)
1013    }
1014 fn Sign(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::SignRequest>)
1015  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
1016    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::SignResponse>,
1017    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
1018  >
1019    >{
1020        let inner_input =
1021            crate::deps::com_amazonaws_kms::conversions::sign::_sign_request::from_dafny(
1022                input.clone(),
1023            );
1024        let native_result = escape_to_async(
1025            self.inner
1026                .sign()
1027                .set_key_id(inner_input.r#key_id)
1028                .set_message(inner_input.r#message)
1029                .set_message_type(inner_input.r#message_type)
1030                .set_grant_tokens(inner_input.r#grant_tokens)
1031                .set_signing_algorithm(inner_input.r#signing_algorithm)
1032                .set_dry_run(inner_input.r#dry_run)
1033                .send(),
1034        );
1035        crate::standard_library_conversions::result_to_dafny(
1036            &native_result,
1037            crate::deps::com_amazonaws_kms::conversions::sign::_sign_response::to_dafny,
1038            crate::deps::com_amazonaws_kms::conversions::sign::to_dafny_error,
1039        )
1040    }
1041    fn TagResource(
1042        &self,
1043        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::TagResourceRequest>,
1044    ) -> dafny_runtime::Rc<
1045        crate::r#_Wrappers_Compile::Result<
1046            (),
1047            dafny_runtime::Rc<
1048                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
1049            >,
1050        >,
1051    > {
1052        let inner_input = crate::deps::com_amazonaws_kms::conversions::tag_resource::_tag_resource_request::from_dafny(input.clone());
1053        let native_result = escape_to_async(
1054            self.inner
1055                .tag_resource()
1056                .set_key_id(inner_input.r#key_id)
1057                .set_tags(inner_input.r#tags)
1058                .send(),
1059        );
1060        crate::standard_library_conversions::result_to_dafny(
1061            &native_result,
1062            |x| (),
1063            crate::deps::com_amazonaws_kms::conversions::tag_resource::to_dafny_error,
1064        )
1065    }
1066    fn UntagResource(
1067        &self,
1068        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::UntagResourceRequest>,
1069    ) -> dafny_runtime::Rc<
1070        crate::r#_Wrappers_Compile::Result<
1071            (),
1072            dafny_runtime::Rc<
1073                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
1074            >,
1075        >,
1076    > {
1077        let inner_input = crate::deps::com_amazonaws_kms::conversions::untag_resource::_untag_resource_request::from_dafny(input.clone());
1078        let native_result = escape_to_async(
1079            self.inner
1080                .untag_resource()
1081                .set_key_id(inner_input.r#key_id)
1082                .set_tag_keys(inner_input.r#tag_keys)
1083                .send(),
1084        );
1085        crate::standard_library_conversions::result_to_dafny(
1086            &native_result,
1087            |x| (),
1088            crate::deps::com_amazonaws_kms::conversions::untag_resource::to_dafny_error,
1089        )
1090    }
1091    fn UpdateAlias(
1092        &self,
1093        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::UpdateAliasRequest>,
1094    ) -> dafny_runtime::Rc<
1095        crate::r#_Wrappers_Compile::Result<
1096            (),
1097            dafny_runtime::Rc<
1098                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
1099            >,
1100        >,
1101    > {
1102        let inner_input = crate::deps::com_amazonaws_kms::conversions::update_alias::_update_alias_request::from_dafny(input.clone());
1103        let native_result = escape_to_async(
1104            self.inner
1105                .update_alias()
1106                .set_alias_name(inner_input.r#alias_name)
1107                .set_target_key_id(inner_input.r#target_key_id)
1108                .send(),
1109        );
1110        crate::standard_library_conversions::result_to_dafny(
1111            &native_result,
1112            |x| (),
1113            crate::deps::com_amazonaws_kms::conversions::update_alias::to_dafny_error,
1114        )
1115    }
1116 fn UpdateCustomKeyStore(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::UpdateCustomKeyStoreRequest>)
1117  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
1118    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::UpdateCustomKeyStoreResponse>,
1119    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
1120  >
1121    >{
1122        let inner_input = crate::deps::com_amazonaws_kms::conversions::update_custom_key_store::_update_custom_key_store_request::from_dafny(input.clone());
1123        let native_result = escape_to_async(
1124            self.inner
1125                .update_custom_key_store()
1126                .set_custom_key_store_id(inner_input.r#custom_key_store_id)
1127                .set_new_custom_key_store_name(inner_input.r#new_custom_key_store_name)
1128                .set_key_store_password(inner_input.r#key_store_password)
1129                .set_cloud_hsm_cluster_id(inner_input.r#cloud_hsm_cluster_id)
1130                .set_xks_proxy_uri_endpoint(inner_input.r#xks_proxy_uri_endpoint)
1131                .set_xks_proxy_uri_path(inner_input.r#xks_proxy_uri_path)
1132                .set_xks_proxy_vpc_endpoint_service_name(
1133                    inner_input.r#xks_proxy_vpc_endpoint_service_name,
1134                )
1135                .set_xks_proxy_authentication_credential(
1136                    inner_input.r#xks_proxy_authentication_credential,
1137                )
1138                .set_xks_proxy_connectivity(inner_input.r#xks_proxy_connectivity)
1139                .send(),
1140        );
1141        crate::standard_library_conversions::result_to_dafny(&native_result,
1142    crate::deps::com_amazonaws_kms::conversions::update_custom_key_store::_update_custom_key_store_response::to_dafny,
1143    crate::deps::com_amazonaws_kms::conversions::update_custom_key_store::to_dafny_error)
1144    }
1145    fn UpdateKeyDescription(
1146        &self,
1147        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::UpdateKeyDescriptionRequest>,
1148    ) -> dafny_runtime::Rc<
1149        crate::r#_Wrappers_Compile::Result<
1150            (),
1151            dafny_runtime::Rc<
1152                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
1153            >,
1154        >,
1155    > {
1156        let inner_input = crate::deps::com_amazonaws_kms::conversions::update_key_description::_update_key_description_request::from_dafny(input.clone());
1157        let native_result = escape_to_async(
1158            self.inner
1159                .update_key_description()
1160                .set_key_id(inner_input.r#key_id)
1161                .set_description(inner_input.r#description)
1162                .send(),
1163        );
1164        crate::standard_library_conversions::result_to_dafny(
1165            &native_result,
1166            |x| (),
1167            crate::deps::com_amazonaws_kms::conversions::update_key_description::to_dafny_error,
1168        )
1169    }
1170    fn UpdatePrimaryRegion(
1171        &self,
1172        input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::UpdatePrimaryRegionRequest>,
1173    ) -> dafny_runtime::Rc<
1174        crate::r#_Wrappers_Compile::Result<
1175            (),
1176            dafny_runtime::Rc<
1177                crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error,
1178            >,
1179        >,
1180    > {
1181        let inner_input = crate::deps::com_amazonaws_kms::conversions::update_primary_region::_update_primary_region_request::from_dafny(input.clone());
1182        let native_result = escape_to_async(
1183            self.inner
1184                .update_primary_region()
1185                .set_key_id(inner_input.r#key_id)
1186                .set_primary_region(inner_input.r#primary_region)
1187                .send(),
1188        );
1189        crate::standard_library_conversions::result_to_dafny(
1190            &native_result,
1191            |x| (),
1192            crate::deps::com_amazonaws_kms::conversions::update_primary_region::to_dafny_error,
1193        )
1194    }
1195 fn Verify(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::VerifyRequest>)
1196  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
1197    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::VerifyResponse>,
1198    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
1199  >
1200    >{
1201        let inner_input =
1202            crate::deps::com_amazonaws_kms::conversions::verify::_verify_request::from_dafny(
1203                input.clone(),
1204            );
1205        let native_result = escape_to_async(
1206            self.inner
1207                .verify()
1208                .set_key_id(inner_input.r#key_id)
1209                .set_message(inner_input.r#message)
1210                .set_message_type(inner_input.r#message_type)
1211                .set_signature(inner_input.r#signature)
1212                .set_signing_algorithm(inner_input.r#signing_algorithm)
1213                .set_grant_tokens(inner_input.r#grant_tokens)
1214                .set_dry_run(inner_input.r#dry_run)
1215                .send(),
1216        );
1217        crate::standard_library_conversions::result_to_dafny(
1218            &native_result,
1219            crate::deps::com_amazonaws_kms::conversions::verify::_verify_response::to_dafny,
1220            crate::deps::com_amazonaws_kms::conversions::verify::to_dafny_error,
1221        )
1222    }
1223 fn VerifyMac(&self, input: &dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::VerifyMacRequest>)
1224  -> dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<
1225    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::VerifyMacResponse>,
1226    dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::kms::internaldafny::types::Error>
1227  >
1228    >{
1229        let inner_input = crate::deps::com_amazonaws_kms::conversions::verify_mac::_verify_mac_request::from_dafny(input.clone());
1230        let native_result = escape_to_async(
1231            self.inner
1232                .verify_mac()
1233                .set_message(inner_input.r#message)
1234                .set_key_id(inner_input.r#key_id)
1235                .set_mac_algorithm(inner_input.r#mac_algorithm)
1236                .set_mac(inner_input.r#mac)
1237                .set_grant_tokens(inner_input.r#grant_tokens)
1238                .set_dry_run(inner_input.r#dry_run)
1239                .send(),
1240        );
1241        crate::standard_library_conversions::result_to_dafny(
1242            &native_result,
1243            crate::deps::com_amazonaws_kms::conversions::verify_mac::_verify_mac_response::to_dafny,
1244            crate::deps::com_amazonaws_kms::conversions::verify_mac::to_dafny_error,
1245        )
1246    }
1247}