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