From eb6ea03b40456553ec291465e3cb0afed58e381d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Oct 2024 08:47:18 -0700 Subject: [PATCH] Enable full SDK test models in Rust (#584) Enables the KMS and DDB test models in Rust, mainly by hooking up union support for SDK wrappers as well, plus some miscellaneous bug fixes and some special cases where I've given up on inferring the smithy-rs logic for now. Both test models needed an extern to implement client creation externs, which I borrowed from https://github.com/aws/aws-database-encryption-sdk-dynamodb/tree/ajewell/rust/releases/rust/db_esdk/src Also added top-level make Makefile targets for fully generating and building all code for a given language! --- SmithyDafnyMakefile.mk | 10 +- .../ddb-lite/runtimes/rust/src/client.rs | 11 +- .../rust/src/conversions/attribute_value.rs | 207 ++++++++------- .../src/conversions/attribute_value_update.rs | 2 +- .../_batch_execute_statement_request.rs | 2 +- .../_batch_execute_statement_response.rs | 4 +- .../batch_get_item/_batch_get_item_request.rs | 2 +- .../_batch_get_item_response.rs | 6 +- .../conversions/batch_statement_request.rs | 2 +- .../conversions/batch_statement_response.rs | 4 +- .../_batch_write_item_request.rs | 2 +- .../_batch_write_item_response.rs | 6 +- .../src/conversions/cancellation_reason.rs | 2 +- .../rust/src/conversions/condition.rs | 2 +- .../rust/src/conversions/condition_check.rs | 4 +- .../rust/src/conversions/consumed_capacity.rs | 6 +- .../create_table/_create_table_request.rs | 16 +- .../create_table/_create_table_response.rs | 2 +- .../runtimes/rust/src/conversions/delete.rs | 4 +- .../delete_item/_delete_item_request.rs | 6 +- .../delete_item/_delete_item_response.rs | 6 +- .../rust/src/conversions/delete_request.rs | 2 +- .../_describe_table_response.rs | 2 +- .../error/transaction_canceled_exception.rs | 2 +- .../_execute_statement_request.rs | 2 +- .../_execute_statement_response.rs | 6 +- .../_execute_transaction_request.rs | 2 +- .../_execute_transaction_response.rs | 4 +- .../conversions/expected_attribute_value.rs | 4 +- .../runtimes/rust/src/conversions/get.rs | 2 +- .../conversions/get_item/_get_item_request.rs | 2 +- .../get_item/_get_item_response.rs | 4 +- .../src/conversions/global_secondary_index.rs | 4 +- .../global_secondary_index_description.rs | 6 +- .../conversions/item_collection_metrics.rs | 4 +- .../rust/src/conversions/item_response.rs | 2 +- .../src/conversions/keys_and_attributes.rs | 2 +- .../src/conversions/local_secondary_index.rs | 2 +- .../local_secondary_index_description.rs | 4 +- .../conversions/parameterized_statement.rs | 2 +- .../runtimes/rust/src/conversions/put.rs | 4 +- .../conversions/put_item/_put_item_request.rs | 6 +- .../put_item/_put_item_response.rs | 6 +- .../rust/src/conversions/put_request.rs | 2 +- .../src/conversions/query/_query_request.rs | 8 +- .../src/conversions/query/_query_response.rs | 6 +- .../src/conversions/replica_description.rs | 6 +- ...lica_global_secondary_index_description.rs | 2 +- .../rust/src/conversions/restore_summary.rs | 2 +- .../src/conversions/scan/_scan_request.rs | 6 +- .../src/conversions/scan/_scan_response.rs | 6 +- .../src/conversions/stream_specification.rs | 2 +- .../rust/src/conversions/table_description.rs | 24 +- .../_transact_get_items_request.rs | 2 +- .../_transact_get_items_response.rs | 4 +- .../src/conversions/transact_write_item.rs | 8 +- .../_transact_write_items_request.rs | 2 +- .../_transact_write_items_response.rs | 4 +- .../runtimes/rust/src/conversions/update.rs | 4 +- .../update_item/_update_item_request.rs | 8 +- .../update_item/_update_item_response.rs | 6 +- .../rust/src/conversions/write_request.rs | 4 +- TestModels/aws-sdks/ddb/Makefile | 5 + .../aws-sdks/ddb/runtimes/rust/Cargo.toml | 1 + .../aws-sdks/ddb/runtimes/rust/src/ddb.rs | 42 ++++ TestModels/aws-sdks/ddb/src/Index.dfy | 2 +- .../kms-lite/runtimes/rust/src/client.rs | 11 +- .../conversions/decrypt/_decrypt_request.rs | 2 +- .../_derive_shared_secret_request.rs | 2 +- .../_generate_data_key_request.rs | 2 +- TestModels/aws-sdks/kms/Makefile | 5 + TestModels/aws-sdks/kms/Model/model.json | 41 --- .../aws-sdks/kms/runtimes/rust/Cargo.toml | 5 +- .../aws-sdks/kms/runtimes/rust/src/kms.rs | 88 +++++++ TestModels/aws-sdks/kms/src/Index.dfy | 2 +- .../polymorph/smithyrust/RustTestModels.java | 2 - .../amazon/polymorph/CodegenEngine.java | 34 +-- .../generator/AbstractRustShimGenerator.java | 92 ++++++- .../generator/RustAwsSdkShimGenerator.java | 236 +++++++++++++----- .../generator/RustLibraryShimGenerator.java | 80 +----- .../rust/conversions/standard_structure.rs | 4 +- .../runtimes/rust/conversions/union.rs | 4 +- 82 files changed, 677 insertions(+), 469 deletions(-) create mode 100644 TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs create mode 100644 TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 9bff30356..636b877fe 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -450,6 +450,8 @@ _polymorph_rust: $(if $(RUST_BENERATED), , _polymorph) ########################## .NET targets +net: polymorph_dafny transpile_net polymorph_net test_net + transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_pre_transpile, ) transpile_net: | transpile_implementation_net transpile_test_net transpile_dependencies_net transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, ) @@ -499,6 +501,8 @@ format_net-check: ########################## Java targets +java: polymorph_dafny transpile_java polymorph_java build_java test_java + build_java: transpile_java mvn_local_deploy_dependencies $(GRADLEW) -p runtimes/java build @@ -553,6 +557,8 @@ test_java: ########################## Rust targets +rust: polymorph_dafny transpile_rust polymorph_rust test_rust + # The Dafny Rust code generator only supports a single crate for everything, # so (among other consequences) we compile src and test code together. transpile_rust: | transpile_implementation_rust transpile_dependencies_rust @@ -583,7 +589,7 @@ _mv_implementation_rust: # Pre-process the Dafny-generated Rust code to remove them. sed -i -e 's/[[:space:]]*$$//' runtimes/rust/src/implementation_from_dafny.rs - rustfmt runtimes/rust/src/implementation_from_dafny.rs + rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs rm -rf implementation_from_dafny-rust patch_after_transpile_rust: @@ -632,6 +638,8 @@ clean: _clean ########################## Python targets +net: polymorph_dafny transpile_python polymorph_python test_python + # Python MUST transpile dependencies first to generate .dtr files transpile_python: $(if $(ENABLE_EXTERN_PROCESSING), _no_extern_pre_transpile, ) transpile_python: | transpile_dependencies_python transpile_implementation_python transpile_test_python diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs index d2be04dbe..879c0f2da 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs @@ -4,8 +4,8 @@ use std::sync::LazyLock; use crate::conversions; -struct Client { - inner: aws_sdk_dynamodb::Client +pub struct Client { + pub inner: aws_sdk_dynamodb::Client } /// A runtime for executing operations on the asynchronous client in a blocking manner. @@ -27,7 +27,7 @@ impl dafny_runtime::UpcastObject) + fn BatchExecuteStatement(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc @@ -206,9 +206,8 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: crate::standard_library_conversions::result_to_dafny(&native_result, conversions::update_item::_update_item_response::to_dafny, conversions::update_item::to_dafny_error) -} } - -#[allow(non_snake_case)] +} +} #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { pub fn DynamoDBClient() -> ::std::rc::Rc< crate::r#_Wrappers_Compile::Result< diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value.rs index 4db758320..f587a7cc9 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value.rs @@ -1,110 +1,129 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. -// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. - #[allow(dead_code)] pub fn to_dafny( value: &aws_sdk_dynamodb::types::AttributeValue, -) -> ::std::rc::Rc{ - ::std::rc::Rc::new( - match value { - aws_sdk_dynamodb::types::AttributeValue::B(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B { - B: crate::standard_library_conversions::blob_to_dafny(x) - }, - aws_sdk_dynamodb::types::AttributeValue::Bool(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL { - BOOL: *x - }, - aws_sdk_dynamodb::types::AttributeValue::Bs(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS { - BS: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, crate::standard_library_conversions::blob_to_dafny) - }, - aws_sdk_dynamodb::types::AttributeValue::L(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L { - L: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, to_dafny) - }, - aws_sdk_dynamodb::types::AttributeValue::M(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M { - M: dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, - |s| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s), - to_dafny) - }, - aws_sdk_dynamodb::types::AttributeValue::N(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N { - N: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x) - }, - aws_sdk_dynamodb::types::AttributeValue::Ns(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS { - NS: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |s| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(s)) - }, - aws_sdk_dynamodb::types::AttributeValue::Null(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL { - NULL: *x - }, +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue, +> { + ::std::rc::Rc::new(match value { aws_sdk_dynamodb::types::AttributeValue::S(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S { - S: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x) - }, - aws_sdk_dynamodb::types::AttributeValue::Ss(x) => - crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS { - SS: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |s| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(s)) - }, + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S { + S: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x), + }, +aws_sdk_dynamodb::types::AttributeValue::N(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N { + N: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x), + }, +aws_sdk_dynamodb::types::AttributeValue::B(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B { + B: crate::standard_library_conversions::blob_to_dafny(&x), + }, +aws_sdk_dynamodb::types::AttributeValue::Ss(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS { + SS: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x, + |e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&e), +) +, + }, +aws_sdk_dynamodb::types::AttributeValue::Ns(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS { + NS: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x, + |e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&e), +) +, + }, +aws_sdk_dynamodb::types::AttributeValue::Bs(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS { + BS: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x, + |e| crate::standard_library_conversions::blob_to_dafny(&e), +) +, + }, +aws_sdk_dynamodb::types::AttributeValue::M(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M { + M: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&x.clone(), + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), + |v| crate::conversions::attribute_value::to_dafny(&v) +, +) +, + }, +aws_sdk_dynamodb::types::AttributeValue::L(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L { + L: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x, + |e| crate::conversions::attribute_value::to_dafny(&e) +, +) +, + }, +aws_sdk_dynamodb::types::AttributeValue::Null(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL { + NULL: x.clone(), + }, +aws_sdk_dynamodb::types::AttributeValue::Bool(x) => + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL { + BOOL: x.clone(), + }, _ => panic!("Unknown union variant: {:?}", value), - } - ) + }) } + #[allow(dead_code)] pub fn from_dafny( dafny_value: ::std::rc::Rc< crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue, >, ) -> aws_sdk_dynamodb::types::AttributeValue { - match &*dafny_value { - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S { S } => - aws_sdk_dynamodb::types::AttributeValue::S( - dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(S) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N { N } => - aws_sdk_dynamodb::types::AttributeValue::N( - dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(N) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B { B } => - aws_sdk_dynamodb::types::AttributeValue::B( - crate::standard_library_conversions::blob_from_dafny(B.clone()) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS { SS } => - aws_sdk_dynamodb::types::AttributeValue::Ss( - dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(SS, - dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS { NS } => - aws_sdk_dynamodb::types::AttributeValue::Ss( - dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(NS, - dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS { BS } => - aws_sdk_dynamodb::types::AttributeValue::Bs( - dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(BS, - |b| crate::standard_library_conversions::blob_from_dafny(b.clone())) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M { M } => - aws_sdk_dynamodb::types::AttributeValue::M( - dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(M, - dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string, - |v| from_dafny(v.clone())) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L { L } => - aws_sdk_dynamodb::types::AttributeValue::L( - dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(L, - |v| from_dafny(v.clone())) - ), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL { NULL } => - aws_sdk_dynamodb::types::AttributeValue::Null(*NULL), - crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL { BOOL } => - aws_sdk_dynamodb::types::AttributeValue::Bool(*BOOL), - } + match &::std::rc::Rc::unwrap_or_clone(dafny_value) { + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S { + S: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::S(dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(x)), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N { + N: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::N(dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(x)), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B { + B: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::B(crate::standard_library_conversions::blob_from_dafny(x.clone())), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS { + SS: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::Ss(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x, + |e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(e), +) +), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS { + NS: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::Ns(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x, + |e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(e), +) +), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS { + BS: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::Bs(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x, + |e| crate::standard_library_conversions::blob_from_dafny(e.clone()), +) +), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M { + M: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::M(::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(&x, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| crate::conversions::attribute_value::from_dafny(v.clone()) +, +) +), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L { + L: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::L(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x, + |e| crate::conversions::attribute_value::from_dafny(e.clone()) +, +) +), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL { + NULL: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::Null(x .clone()), +crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL { + BOOL: x @ _, +} => aws_sdk_dynamodb::types::AttributeValue::Bool(x .clone()), + } } diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value_update.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value_update.rs index 86c19d09a..f2178c927 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value_update.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/attribute_value_update.rs @@ -8,7 +8,7 @@ pub fn to_dafny( ::std::rc::Rc::new( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValueUpdate::AttributeValueUpdate { Value: ::std::rc::Rc::new(match &value.value { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::attribute_value::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::attribute_value::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_request.rs index caa461b81..1680275de 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_request.rs @@ -9,7 +9,7 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput::BatchExecuteStatementInput { Statements: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.statements.clone().unwrap(), - |e| crate::conversions::batch_statement_request::to_dafny(e) + |e| crate::conversions::batch_statement_request::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_response.rs index c5a849115..56cae1bdc 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_response.rs @@ -11,7 +11,7 @@ pub fn to_dafny( Responses: ::std::rc::Rc::new(match &value.responses { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::batch_statement_response::to_dafny(e) + |e| crate::conversions::batch_statement_response::to_dafny(&e) , ) }, @@ -21,7 +21,7 @@ pub fn to_dafny( ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::consumed_capacity::to_dafny(e) + |e| crate::conversions::consumed_capacity::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_request.rs index b229b88f8..96e770b44 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_request.rs @@ -10,7 +10,7 @@ pub fn to_dafny( ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchGetItemInput::BatchGetItemInput { RequestItems: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.request_items.clone().unwrap(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::keys_and_attributes::to_dafny(v) + |v| crate::conversions::keys_and_attributes::to_dafny(&v) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_response.rs index b669ded2f..a905095ef 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_get_item/_batch_get_item_response.rs @@ -16,7 +16,7 @@ pub fn to_dafny( |v| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, |e| ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&e.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -32,7 +32,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::keys_and_attributes::to_dafny(v) + |v| crate::conversions::keys_and_attributes::to_dafny(&v) , ) }, @@ -42,7 +42,7 @@ pub fn to_dafny( ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::consumed_capacity::to_dafny(e) + |e| crate::conversions::consumed_capacity::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_request.rs index 61e266d0f..60caba238 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_request.rs @@ -11,7 +11,7 @@ pub fn to_dafny( Parameters: ::std::rc::Rc::new(match &value.parameters { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::attribute_value::to_dafny(e) + |e| crate::conversions::attribute_value::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_response.rs index 32cd7a882..bc392ae9e 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_response.rs @@ -8,7 +8,7 @@ pub fn to_dafny( ::std::rc::Rc::new( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementResponse::BatchStatementResponse { Error: ::std::rc::Rc::new(match &value.error { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::batch_statement_error::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::batch_statement_error::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -18,7 +18,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_request.rs index 385e366b4..8273ddb16 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_request.rs @@ -11,7 +11,7 @@ pub fn to_dafny( RequestItems: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.request_items.clone().unwrap(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), |v| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, - |e| crate::conversions::write_request::to_dafny(e) + |e| crate::conversions::write_request::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_response.rs index 48975d627..1896a75b6 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_response.rs @@ -14,7 +14,7 @@ pub fn to_dafny( ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), |v| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, - |e| crate::conversions::write_request::to_dafny(e) + |e| crate::conversions::write_request::to_dafny(&e) , ) , @@ -29,7 +29,7 @@ pub fn to_dafny( ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), |v| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, - |e| crate::conversions::item_collection_metrics::to_dafny(e) + |e| crate::conversions::item_collection_metrics::to_dafny(&e) , ) , @@ -41,7 +41,7 @@ pub fn to_dafny( ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::consumed_capacity::to_dafny(e) + |e| crate::conversions::consumed_capacity::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/cancellation_reason.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/cancellation_reason.rs index 22c895ff8..02def6098 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/cancellation_reason.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/cancellation_reason.rs @@ -12,7 +12,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition.rs index fe940f3d8..78de17aa7 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition.rs @@ -10,7 +10,7 @@ pub fn to_dafny( AttributeValueList: ::std::rc::Rc::new(match &value.attribute_value_list { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::attribute_value::to_dafny(e) + |e| crate::conversions::attribute_value::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition_check.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition_check.rs index 3b07f2af2..b73a3f866 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition_check.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/condition_check.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ConditionCheck::ConditionCheck { Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -31,7 +31,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/consumed_capacity.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/consumed_capacity.rs index 728de76fe..474227783 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/consumed_capacity.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/consumed_capacity.rs @@ -12,7 +12,7 @@ pub fn to_dafny( ReadCapacityUnits: crate::standard_library_conversions::odouble_to_dafny(&value.read_capacity_units), WriteCapacityUnits: crate::standard_library_conversions::odouble_to_dafny(&value.write_capacity_units), Table: ::std::rc::Rc::new(match &value.table { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -21,7 +21,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::capacity::to_dafny(v) + |v| crate::conversions::capacity::to_dafny(&v) , ) }, @@ -33,7 +33,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::capacity::to_dafny(v) + |v| crate::conversions::capacity::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_request.rs index 40c6d22ce..12aefbb73 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_request.rs @@ -9,20 +9,20 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::CreateTableInput::CreateTableInput { AttributeDefinitions: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.attribute_definitions.clone().unwrap(), - |e| crate::conversions::attribute_definition::to_dafny(e) + |e| crate::conversions::attribute_definition::to_dafny(&e) , ) , TableName: crate::standard_library_conversions::ostring_to_dafny(&value.table_name) .Extract(), KeySchema: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.key_schema.clone().unwrap(), - |e| crate::conversions::key_schema_element::to_dafny(e) + |e| crate::conversions::key_schema_element::to_dafny(&e) , ) , LocalSecondaryIndexes: ::std::rc::Rc::new(match &value.local_secondary_indexes { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::local_secondary_index::to_dafny(e) + |e| crate::conversions::local_secondary_index::to_dafny(&e) , ) }, @@ -32,7 +32,7 @@ pub fn to_dafny( GlobalSecondaryIndexes: ::std::rc::Rc::new(match &value.global_secondary_indexes { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::global_secondary_index::to_dafny(e) + |e| crate::conversions::global_secondary_index::to_dafny(&e) , ) }, @@ -45,24 +45,24 @@ pub fn to_dafny( }) , ProvisionedThroughput: ::std::rc::Rc::new(match &value.provisioned_throughput { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , StreamSpecification: ::std::rc::Rc::new(match &value.stream_specification { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::stream_specification::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::stream_specification::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , SSESpecification: ::std::rc::Rc::new(match &value.sse_specification { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::sse_specification::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::sse_specification::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , Tags: ::std::rc::Rc::new(match &value.tags { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::tag::to_dafny(e) + |e| crate::conversions::tag::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_response.rs index 90ed15bc7..ee61b5a61 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/create_table/_create_table_response.rs @@ -9,7 +9,7 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::CreateTableOutput::CreateTableOutput { TableDescription: ::std::rc::Rc::new(match &value.table_description { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_description::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_description::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete.rs index 6e1247872..eeee3a6da 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Delete::Delete { Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -31,7 +31,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_request.rs index f368775db..27d98b407 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_request.rs @@ -11,7 +11,7 @@ pub fn to_dafny( TableName: crate::standard_library_conversions::ostring_to_dafny(&value.table_name) .Extract(), Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone().unwrap(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -20,7 +20,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::expected_attribute_value::to_dafny(v) + |v| crate::conversions::expected_attribute_value::to_dafny(&v) , ) }, @@ -64,7 +64,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_response.rs index 25d450253..e22195757 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_item/_delete_item_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -21,12 +21,12 @@ pub fn to_dafny( }) , ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , ItemCollectionMetrics: ::std::rc::Rc::new(match &value.item_collection_metrics { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::item_collection_metrics::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::item_collection_metrics::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_request.rs index 6d292b803..9b0b59c5f 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_request.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::DeleteRequest::DeleteRequest { Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/describe_table/_describe_table_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/describe_table/_describe_table_response.rs index 9851c556e..1ab636bfa 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/describe_table/_describe_table_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/describe_table/_describe_table_response.rs @@ -9,7 +9,7 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::DescribeTableOutput::DescribeTableOutput { Table: ::std::rc::Rc::new(match &value.table { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_description::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_description::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/transaction_canceled_exception.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/transaction_canceled_exception.rs index a425c6b21..8f58cbb23 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/transaction_canceled_exception.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/transaction_canceled_exception.rs @@ -11,7 +11,7 @@ pub fn to_dafny( CancellationReasons: ::std::rc::Rc::new(match &value.cancellation_reasons { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::cancellation_reason::to_dafny(e) + |e| crate::conversions::cancellation_reason::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_request.rs index 8c75e9b28..a43043c55 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_request.rs @@ -12,7 +12,7 @@ pub fn to_dafny( Parameters: ::std::rc::Rc::new(match &value.parameters { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::attribute_value::to_dafny(e) + |e| crate::conversions::attribute_value::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_response.rs index fd8941e62..8e4bf4fb6 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, |e| ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&e.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -24,7 +24,7 @@ pub fn to_dafny( , NextToken: crate::standard_library_conversions::ostring_to_dafny(&value.next_token), ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -33,7 +33,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_request.rs index fd54ef4bb..cb83e7474 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_request.rs @@ -9,7 +9,7 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteTransactionInput::ExecuteTransactionInput { TransactStatements: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.transact_statements.clone().unwrap(), - |e| crate::conversions::parameterized_statement::to_dafny(e) + |e| crate::conversions::parameterized_statement::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_response.rs index 0dcc37480..e0d211637 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_response.rs @@ -11,7 +11,7 @@ pub fn to_dafny( Responses: ::std::rc::Rc::new(match &value.responses { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::item_response::to_dafny(e) + |e| crate::conversions::item_response::to_dafny(&e) , ) }, @@ -21,7 +21,7 @@ pub fn to_dafny( ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::consumed_capacity::to_dafny(e) + |e| crate::conversions::consumed_capacity::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/expected_attribute_value.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/expected_attribute_value.rs index 59623dc8e..d3c94f824 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/expected_attribute_value.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/expected_attribute_value.rs @@ -8,7 +8,7 @@ pub fn to_dafny( ::std::rc::Rc::new( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExpectedAttributeValue::ExpectedAttributeValue { Value: ::std::rc::Rc::new(match &value.value { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::attribute_value::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::attribute_value::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -21,7 +21,7 @@ pub fn to_dafny( AttributeValueList: ::std::rc::Rc::new(match &value.attribute_value_list { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::attribute_value::to_dafny(e) + |e| crate::conversions::attribute_value::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get.rs index 36e98856e..5d3c0bd90 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Get::Get { Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_request.rs index 6b59a55dc..d9aef3e00 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_request.rs @@ -11,7 +11,7 @@ pub fn to_dafny( TableName: crate::standard_library_conversions::ostring_to_dafny(&value.table_name) .Extract(), Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone().unwrap(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_response.rs index 8851313d9..b94e8d4c7 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get_item/_get_item_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -21,7 +21,7 @@ pub fn to_dafny( }) , ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index.rs index 2bf766300..6d88e8255 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index.rs @@ -9,14 +9,14 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::GlobalSecondaryIndex::GlobalSecondaryIndex { IndexName: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&value.index_name), KeySchema: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.key_schema, - |e| crate::conversions::key_schema_element::to_dafny(e) + |e| crate::conversions::key_schema_element::to_dafny(&e) , ) , Projection: crate::conversions::projection::to_dafny(&value.projection.clone().unwrap()) , ProvisionedThroughput: ::std::rc::Rc::new(match &value.provisioned_throughput { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index_description.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index_description.rs index c7ff210f9..6f07b1db7 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index_description.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/global_secondary_index_description.rs @@ -11,7 +11,7 @@ pub fn to_dafny( KeySchema: ::std::rc::Rc::new(match &value.key_schema { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::key_schema_element::to_dafny(e) + |e| crate::conversions::key_schema_element::to_dafny(&e) , ) }, @@ -19,7 +19,7 @@ pub fn to_dafny( }) , Projection: ::std::rc::Rc::new(match &value.projection { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::projection::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::projection::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -30,7 +30,7 @@ pub fn to_dafny( , Backfilling: crate::standard_library_conversions::obool_to_dafny(&value.backfilling), ProvisionedThroughput: ::std::rc::Rc::new(match &value.provisioned_throughput { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_description::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_description::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_collection_metrics.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_collection_metrics.rs index 31d752b41..ebeaf9965 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_collection_metrics.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_collection_metrics.rs @@ -12,7 +12,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -22,7 +22,7 @@ pub fn to_dafny( SizeEstimateRangeGB: ::std::rc::Rc::new(match &value.size_estimate_range_gb { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::standard_library_conversions::double_to_dafny(*e), + |e| crate::standard_library_conversions::double_to_dafny(e.clone()), ) }, None => crate::r#_Wrappers_Compile::Option::None {} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_response.rs index 7997abf1f..170bfe7cf 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_response.rs @@ -12,7 +12,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/keys_and_attributes.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/keys_and_attributes.rs index e99a7097d..35bf525b2 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/keys_and_attributes.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/keys_and_attributes.rs @@ -10,7 +10,7 @@ pub fn to_dafny( Keys: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.keys, |e| ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&e.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index.rs index 34bd28213..d95675cf7 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::LocalSecondaryIndex::LocalSecondaryIndex { IndexName: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&value.index_name), KeySchema: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.key_schema, - |e| crate::conversions::key_schema_element::to_dafny(e) + |e| crate::conversions::key_schema_element::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index_description.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index_description.rs index 6b0b4678b..3af48fb4f 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index_description.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/local_secondary_index_description.rs @@ -11,7 +11,7 @@ pub fn to_dafny( KeySchema: ::std::rc::Rc::new(match &value.key_schema { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::key_schema_element::to_dafny(e) + |e| crate::conversions::key_schema_element::to_dafny(&e) , ) }, @@ -19,7 +19,7 @@ pub fn to_dafny( }) , Projection: ::std::rc::Rc::new(match &value.projection { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::projection::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::projection::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/parameterized_statement.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/parameterized_statement.rs index bd89af80d..4d14930e9 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/parameterized_statement.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/parameterized_statement.rs @@ -11,7 +11,7 @@ pub fn to_dafny( Parameters: ::std::rc::Rc::new(match &value.parameters { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::attribute_value::to_dafny(e) + |e| crate::conversions::attribute_value::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put.rs index 3d52d4513..c3b4d3f23 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Put::Put { Item: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.item.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -31,7 +31,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_request.rs index 451f09040..2c6f0a8af 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_request.rs @@ -11,7 +11,7 @@ pub fn to_dafny( TableName: crate::standard_library_conversions::ostring_to_dafny(&value.table_name) .Extract(), Item: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.item.clone().unwrap(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -20,7 +20,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::expected_attribute_value::to_dafny(v) + |v| crate::conversions::expected_attribute_value::to_dafny(&v) , ) }, @@ -64,7 +64,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_response.rs index 6d8631ea5..12d79678d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_item/_put_item_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -21,12 +21,12 @@ pub fn to_dafny( }) , ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , ItemCollectionMetrics: ::std::rc::Rc::new(match &value.item_collection_metrics { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::item_collection_metrics::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::item_collection_metrics::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_request.rs index 7674c503d..47e6efe2d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_request.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::PutRequest::PutRequest { Item: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.item.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_request.rs index bd0cc079b..8bd79e88d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_request.rs @@ -31,7 +31,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::condition::to_dafny(v) + |v| crate::conversions::condition::to_dafny(&v) , ) }, @@ -43,7 +43,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::condition::to_dafny(v) + |v| crate::conversions::condition::to_dafny(&v) , ) }, @@ -61,7 +61,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -92,7 +92,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_response.rs index 78805f9e0..79e4dcaf5 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/query/_query_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, |e| ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&e.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -29,7 +29,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -37,7 +37,7 @@ pub fn to_dafny( }) , ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_description.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_description.rs index 5396777c6..594ddbf4d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_description.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_description.rs @@ -17,14 +17,14 @@ pub fn to_dafny( ReplicaStatusPercentProgress: crate::standard_library_conversions::ostring_to_dafny(&value.replica_status_percent_progress), KMSMasterKeyId: crate::standard_library_conversions::ostring_to_dafny(&value.kms_master_key_id), ProvisionedThroughputOverride: ::std::rc::Rc::new(match &value.provisioned_throughput_override { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_override::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_override::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , GlobalSecondaryIndexes: ::std::rc::Rc::new(match &value.global_secondary_indexes { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::replica_global_secondary_index_description::to_dafny(e) + |e| crate::conversions::replica_global_secondary_index_description::to_dafny(&e) , ) }, @@ -33,7 +33,7 @@ pub fn to_dafny( , ReplicaInaccessibleDateTime: crate::standard_library_conversions::otimestamp_to_dafny(&value.replica_inaccessible_date_time), ReplicaTableClassSummary: ::std::rc::Rc::new(match &value.replica_table_class_summary { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_class_summary::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_class_summary::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_global_secondary_index_description.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_global_secondary_index_description.rs index 38110b06e..42873feb2 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_global_secondary_index_description.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/replica_global_secondary_index_description.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ReplicaGlobalSecondaryIndexDescription::ReplicaGlobalSecondaryIndexDescription { IndexName: crate::standard_library_conversions::ostring_to_dafny(&value.index_name), ProvisionedThroughputOverride: ::std::rc::Rc::new(match &value.provisioned_throughput_override { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_override::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_override::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/restore_summary.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/restore_summary.rs index 4ed50a790..f5e889989 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/restore_summary.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/restore_summary.rs @@ -10,7 +10,7 @@ pub fn to_dafny( SourceBackupArn: crate::standard_library_conversions::ostring_to_dafny(&value.source_backup_arn), SourceTableArn: crate::standard_library_conversions::ostring_to_dafny(&value.source_table_arn), RestoreDateTime: crate::standard_library_conversions::timestamp_to_dafny(&value.restore_date_time), - RestoreInProgress: value.restore_in_progress, + RestoreInProgress: value.restore_in_progress.clone(), } ) } #[allow(dead_code)] diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_request.rs index d21631828..11bbfec8c 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_request.rs @@ -30,7 +30,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::condition::to_dafny(v) + |v| crate::conversions::condition::to_dafny(&v) , ) }, @@ -47,7 +47,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -79,7 +79,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_response.rs index ea5f8e705..e4c7c742d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/scan/_scan_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, |e| ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&e.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -29,7 +29,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -37,7 +37,7 @@ pub fn to_dafny( }) , ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/stream_specification.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/stream_specification.rs index 2134aac35..add526e05 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/stream_specification.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/stream_specification.rs @@ -7,7 +7,7 @@ pub fn to_dafny( ) -> ::std::rc::Rc{ ::std::rc::Rc::new( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::StreamSpecification::StreamSpecification { - StreamEnabled: value.stream_enabled, + StreamEnabled: value.stream_enabled.clone(), StreamViewType: ::std::rc::Rc::new(match &value.stream_view_type { Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::stream_view_type::to_dafny(x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/table_description.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/table_description.rs index 020a86581..2a99d390c 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/table_description.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/table_description.rs @@ -10,7 +10,7 @@ pub fn to_dafny( AttributeDefinitions: ::std::rc::Rc::new(match &value.attribute_definitions { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::attribute_definition::to_dafny(e) + |e| crate::conversions::attribute_definition::to_dafny(&e) , ) }, @@ -21,7 +21,7 @@ pub fn to_dafny( KeySchema: ::std::rc::Rc::new(match &value.key_schema { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::key_schema_element::to_dafny(e) + |e| crate::conversions::key_schema_element::to_dafny(&e) , ) }, @@ -35,7 +35,7 @@ pub fn to_dafny( , CreationDateTime: crate::standard_library_conversions::otimestamp_to_dafny(&value.creation_date_time), ProvisionedThroughput: ::std::rc::Rc::new(match &value.provisioned_throughput { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_description::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::provisioned_throughput_description::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -44,14 +44,14 @@ pub fn to_dafny( TableArn: crate::standard_library_conversions::ostring_to_dafny(&value.table_arn), TableId: crate::standard_library_conversions::ostring_to_dafny(&value.table_id), BillingModeSummary: ::std::rc::Rc::new(match &value.billing_mode_summary { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::billing_mode_summary::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::billing_mode_summary::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , LocalSecondaryIndexes: ::std::rc::Rc::new(match &value.local_secondary_indexes { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::local_secondary_index_description::to_dafny(e) + |e| crate::conversions::local_secondary_index_description::to_dafny(&e) , ) }, @@ -61,7 +61,7 @@ pub fn to_dafny( GlobalSecondaryIndexes: ::std::rc::Rc::new(match &value.global_secondary_indexes { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::global_secondary_index_description::to_dafny(e) + |e| crate::conversions::global_secondary_index_description::to_dafny(&e) , ) }, @@ -69,7 +69,7 @@ pub fn to_dafny( }) , StreamSpecification: ::std::rc::Rc::new(match &value.stream_specification { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::stream_specification::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::stream_specification::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , @@ -79,7 +79,7 @@ pub fn to_dafny( Replicas: ::std::rc::Rc::new(match &value.replicas { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::replica_description::to_dafny(e) + |e| crate::conversions::replica_description::to_dafny(&e) , ) }, @@ -87,22 +87,22 @@ pub fn to_dafny( }) , RestoreSummary: ::std::rc::Rc::new(match &value.restore_summary { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::restore_summary::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::restore_summary::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , SSEDescription: ::std::rc::Rc::new(match &value.sse_description { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::sse_description::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::sse_description::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , ArchivalSummary: ::std::rc::Rc::new(match &value.archival_summary { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::archival_summary::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::archival_summary::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , TableClassSummary: ::std::rc::Rc::new(match &value.table_class_summary { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_class_summary::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::table_class_summary::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_request.rs index 9bd307348..c5f54a394 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_request.rs @@ -9,7 +9,7 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItemsInput::TransactGetItemsInput { TransactItems: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.transact_items.clone().unwrap(), - |e| crate::conversions::transact_get_item::to_dafny(e) + |e| crate::conversions::transact_get_item::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_response.rs index 1512b7b14..04eeb2699 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_response.rs @@ -11,7 +11,7 @@ pub fn to_dafny( ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::consumed_capacity::to_dafny(e) + |e| crate::conversions::consumed_capacity::to_dafny(&e) , ) }, @@ -21,7 +21,7 @@ pub fn to_dafny( Responses: ::std::rc::Rc::new(match &value.responses { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::item_response::to_dafny(e) + |e| crate::conversions::item_response::to_dafny(&e) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_item.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_item.rs index 01684f337..732e79df3 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_item.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_item.rs @@ -8,22 +8,22 @@ pub fn to_dafny( ::std::rc::Rc::new( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactWriteItem::TransactWriteItem { ConditionCheck: ::std::rc::Rc::new(match &value.condition_check { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::condition_check::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::condition_check::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , Put: ::std::rc::Rc::new(match &value.put { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::put::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::put::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , Delete: ::std::rc::Rc::new(match &value.delete { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::delete::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::delete::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , Update: ::std::rc::Rc::new(match &value.update { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::update::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::update::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_request.rs index 09003096b..93a0bd3cf 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_request.rs @@ -9,7 +9,7 @@ pub fn to_dafny( >{ ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactWriteItemsInput::TransactWriteItemsInput { TransactItems: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.transact_items.clone().unwrap(), - |e| crate::conversions::transact_write_item::to_dafny(e) + |e| crate::conversions::transact_write_item::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_response.rs index 234b73e26..c7c245a01 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_write_items/_transact_write_items_response.rs @@ -11,7 +11,7 @@ pub fn to_dafny( ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, - |e| crate::conversions::consumed_capacity::to_dafny(e) + |e| crate::conversions::consumed_capacity::to_dafny(&e) , ) }, @@ -24,7 +24,7 @@ pub fn to_dafny( ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), |v| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, - |e| crate::conversions::item_collection_metrics::to_dafny(e) + |e| crate::conversions::item_collection_metrics::to_dafny(&e) , ) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update.rs index d37e6f18b..2c0bc9b1d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update.rs @@ -9,7 +9,7 @@ pub fn to_dafny( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Update::Update { Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -32,7 +32,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_request.rs index 0366b8a42..d565fa848 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_request.rs @@ -11,7 +11,7 @@ pub fn to_dafny( TableName: crate::standard_library_conversions::ostring_to_dafny(&value.table_name) .Extract(), Key: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.key.clone().unwrap(), |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) , @@ -20,7 +20,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value_update::to_dafny(v) + |v| crate::conversions::attribute_value_update::to_dafny(&v) , ) }, @@ -32,7 +32,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::expected_attribute_value::to_dafny(v) + |v| crate::conversions::expected_attribute_value::to_dafny(&v) , ) }, @@ -77,7 +77,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_response.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_response.rs index fd3cc6909..7edf31aba 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_response.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/update_item/_update_item_response.rs @@ -13,7 +13,7 @@ pub fn to_dafny( Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k), - |v| crate::conversions::attribute_value::to_dafny(v) + |v| crate::conversions::attribute_value::to_dafny(&v) , ) }, @@ -21,12 +21,12 @@ pub fn to_dafny( }) , ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::consumed_capacity::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , ItemCollectionMetrics: ::std::rc::Rc::new(match &value.item_collection_metrics { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::item_collection_metrics::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::item_collection_metrics::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/write_request.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/write_request.rs index b3010b7cf..b42b9c88d 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/write_request.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/write_request.rs @@ -8,12 +8,12 @@ pub fn to_dafny( ::std::rc::Rc::new( crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::WriteRequest::WriteRequest { PutRequest: ::std::rc::Rc::new(match &value.put_request { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::put_request::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::put_request::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , DeleteRequest: ::std::rc::Rc::new(match &value.delete_request { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::delete_request::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::delete_request::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/ddb/Makefile b/TestModels/aws-sdks/ddb/Makefile index f7944f828..2cc808994 100644 --- a/TestModels/aws-sdks/ddb/Makefile +++ b/TestModels/aws-sdks/ddb/Makefile @@ -5,6 +5,11 @@ CORES=2 ENABLE_EXTERN_PROCESSING=1 +TRANSPILE_TESTS_IN_RUST=1 + +RUST_OTHER_FILES := \ + runtimes/rust/src/ddb.rs + include ../../SharedMakefile.mk PROJECT_SERVICES := \ diff --git a/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml index 7d4f268ec..d834361e2 100644 --- a/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml @@ -10,6 +10,7 @@ wrapped-client = [] [dependencies] aws-sdk-dynamodb = "1.45.0" +aws-config = "1.5.4" aws-smithy-runtime = {version = "1.6.0", features = ["client"] } aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } aws-smithy-types = "1.2.0" diff --git a/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs b/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs new file mode 100644 index 000000000..8fd807b65 --- /dev/null +++ b/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs @@ -0,0 +1,42 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +#![deny(warnings, unconditional_panic)] +#![deny(nonstandard_style)] +#![deny(clippy::all)] + +use std::sync::LazyLock; + +static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| { + tokio::runtime::Builder::new_multi_thread() + .enable_all() + .build() + .unwrap() +}); + +#[allow(non_snake_case)] +impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { + pub fn DynamoDBClient() -> ::std::rc::Rc< + crate::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object, + ::std::rc::Rc + > + >{ + let shared_config = match tokio::runtime::Handle::try_current() { + Ok(curr) => tokio::task::block_in_place(|| { + curr.block_on(async { + aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await + }) + }), + Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults( + aws_config::BehaviorVersion::v2024_03_28(), + )), + }; + let inner = aws_sdk_dynamodb::Client::new(&shared_config); + let client = crate::client::Client { inner }; + let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); + std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + value: dafny_client, + }) + } +} diff --git a/TestModels/aws-sdks/ddb/src/Index.dfy b/TestModels/aws-sdks/ddb/src/Index.dfy index a0eabd8e8..9a7d9eb58 100644 --- a/TestModels/aws-sdks/ddb/src/Index.dfy +++ b/TestModels/aws-sdks/ddb/src/Index.dfy @@ -3,7 +3,7 @@ include "../Model/ComAmazonawsDynamodbTypes.dfy" -module Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService { +module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny"} Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService { function method DefaultDynamoDBClientConfigType() : DynamoDBClientConfigType { DynamoDBClientConfigType diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs index 2513001ef..f17b4a4f1 100644 --- a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/client.rs @@ -4,8 +4,8 @@ use std::sync::LazyLock; use crate::conversions; -struct Client { - inner: aws_sdk_kms::Client +pub struct Client { + pub inner: aws_sdk_kms::Client } /// A runtime for executing operations on the asynchronous client in a blocking manner. @@ -27,7 +27,7 @@ impl dafny_runtime::UpcastObject) + fn Decrypt(&mut self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc @@ -122,9 +122,8 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::type crate::standard_library_conversions::result_to_dafny(&native_result, conversions::update_primary_region::_update_primary_region_response::to_dafny, conversions::update_primary_region::to_dafny_error) -} } - -#[allow(non_snake_case)] +} +} #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { pub fn KMSClient() -> ::std::rc::Rc< crate::r#_Wrappers_Compile::Result< diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs index 33af777b0..c35addf12 100644 --- a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/decrypt/_decrypt_request.rs @@ -36,7 +36,7 @@ pub fn to_dafny( }) , Recipient: ::std::rc::Rc::new(match &value.recipient { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::recipient_info::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::recipient_info::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/derive_shared_secret/_derive_shared_secret_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/derive_shared_secret/_derive_shared_secret_request.rs index 7bfa77584..f51a35e14 100644 --- a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/derive_shared_secret/_derive_shared_secret_request.rs +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/derive_shared_secret/_derive_shared_secret_request.rs @@ -22,7 +22,7 @@ pub fn to_dafny( , DryRun: crate::standard_library_conversions::obool_to_dafny(&value.dry_run), Recipient: ::std::rc::Rc::new(match &value.recipient { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::recipient_info::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::recipient_info::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs index 5faa10147..8fc481842 100644 --- a/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/src/conversions/generate_data_key/_generate_data_key_request.rs @@ -36,7 +36,7 @@ pub fn to_dafny( }) , Recipient: ::std::rc::Rc::new(match &value.recipient { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::recipient_info::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::recipient_info::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) , diff --git a/TestModels/aws-sdks/kms/Makefile b/TestModels/aws-sdks/kms/Makefile index f4240123f..87e4a5a70 100644 --- a/TestModels/aws-sdks/kms/Makefile +++ b/TestModels/aws-sdks/kms/Makefile @@ -5,6 +5,11 @@ CORES=2 ENABLE_EXTERN_PROCESSING=1 +TRANSPILE_TESTS_IN_RUST=1 + +RUST_OTHER_FILES := \ + runtimes/rust/src/kms.rs + include ../../SharedMakefile.mk NAMESPACE=com.amazonaws.kms diff --git a/TestModels/aws-sdks/kms/Model/model.json b/TestModels/aws-sdks/kms/Model/model.json index 512c7f262..89aa4fcf3 100644 --- a/TestModels/aws-sdks/kms/Model/model.json +++ b/TestModels/aws-sdks/kms/Model/model.json @@ -3660,23 +3660,6 @@ } } }, - "com.amazonaws.kms#ListKeysRequest": { - "type": "structure", - "members": { - "Limit": { - "target": "com.amazonaws.kms#LimitType", - "traits": { - "smithy.api#documentation": "

Use this parameter to specify the maximum number of items to return. When this\n value is present, KMS does not return more than the specified number of items, but it might\n return fewer.

\n

This value is optional. If you include a value, it must be between\n 1 and 1000, inclusive. If you do not include a value, it defaults to 100.

" - } - }, - "Marker": { - "target": "com.amazonaws.kms#MarkerType", - "traits": { - "smithy.api#documentation": "

Use this parameter in a subsequent request after you receive a response with\n truncated results. Set it to the value of NextMarker from the truncated response\n you just received.

" - } - } - } - }, "com.amazonaws.kms#ListResourceTags": { "type": "operation", "input": { @@ -3750,30 +3733,6 @@ } } }, - "com.amazonaws.kms#ListRetirableGrantsRequest": { - "type": "structure", - "members": { - "Limit": { - "target": "com.amazonaws.kms#LimitType", - "traits": { - "smithy.api#documentation": "

Use this parameter to specify the maximum number of items to return. When this\n value is present, KMS does not return more than the specified number of items, but it might\n return fewer.

\n

This value is optional. If you include a value, it must be between 1\n and 100, inclusive. If you do not include a value, it defaults to 50.

" - } - }, - "Marker": { - "target": "com.amazonaws.kms#MarkerType", - "traits": { - "smithy.api#documentation": "

Use this parameter in a subsequent request after you receive a response with\n truncated results. Set it to the value of NextMarker from the truncated response\n you just received.

" - } - }, - "RetiringPrincipal": { - "target": "com.amazonaws.kms#PrincipalIdType", - "traits": { - "smithy.api#documentation": "

The retiring principal for which to list grants. Enter a principal in your\n Amazon Web Services account.

\n

To specify the retiring principal, use the Amazon Resource Name (ARN) of an\n Amazon Web Services principal. Valid Amazon Web Services principals include Amazon Web Services accounts (root), IAM users, federated\n users, and assumed role users. For examples of the ARN syntax for specifying a principal, see\n Amazon Web Services Identity and Access Management (IAM) in the Example ARNs section of the\n Amazon Web Services General Reference.

", - "smithy.api#required": {} - } - } - } - }, "com.amazonaws.kms#MalformedPolicyDocumentException": { "type": "structure", "members": { diff --git a/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml index 1e9fce0cd..71777152a 100644 --- a/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "aws_sdk_ddb" +name = "kms" version = "0.1.0" edition = "2021" @@ -10,13 +10,14 @@ wrapped-client = [] [dependencies] aws-sdk-kms = "1.43.0" +aws-config = "1.5.4" aws-smithy-runtime = {version = "1.6.0", features = ["client"] } aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } aws-smithy-types = "1.2.0" dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"} [dev-dependencies] -aws_sdk_ddb = { path = ".", features = ["wrapped-client"] } +kms = { path = ".", features = ["wrapped-client"] } [dependencies.tokio] version = "1.26.0" diff --git a/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs b/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs new file mode 100644 index 000000000..330cebfeb --- /dev/null +++ b/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs @@ -0,0 +1,88 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +#![deny(warnings, unconditional_panic)] +#![deny(nonstandard_style)] +#![deny(clippy::all)] + +use aws_config::Region; +use std::any::Any; +use std::sync::LazyLock; + +static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| { + tokio::runtime::Builder::new_multi_thread() + .enable_all() + .build() + .unwrap() +}); + +impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { + #[allow(non_snake_case)] + pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc, ::std::rc::Rc>>{ + let region = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + region, + ); + + let shared_config = match tokio::runtime::Handle::try_current() { + Ok(curr) => tokio::task::block_in_place(|| { + curr.block_on(async { + aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await + }) + }), + Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults( + aws_config::BehaviorVersion::v2024_03_28(), + )), + }; + + let shared_config = shared_config + .to_builder() + .region(Region::new(region)) + .build(); + let inner = aws_sdk_kms::Client::new(&shared_config); + let client = crate::client::Client { inner }; + let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); + std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + value: dafny_client, + }) + } + + #[allow(non_snake_case)] + pub fn KMSClient() -> ::std::rc::Rc, ::std::rc::Rc>>{ + let shared_config = match tokio::runtime::Handle::try_current() { + Ok(curr) => tokio::task::block_in_place(|| { + curr.block_on(async { + aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await + }) + }), + Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults( + aws_config::BehaviorVersion::v2024_03_28(), + )), + }; + + let inner = aws_sdk_kms::Client::new(&shared_config); + let client = crate::client::Client { inner }; + let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); + std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + value: dafny_client, + }) + } + + #[allow(non_snake_case)] + pub fn RegionMatch( + kmsClient: &::dafny_runtime::Object, + region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) -> ::std::rc::Rc> { + let region = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + region, + ); + let any = dafny_runtime::cast_any_object!(kmsClient); + let client = dafny_runtime::cast_object!(any, crate::client::Client); + let flag = match client.as_ref().inner.config().region() { + Some(r) => r.as_ref() == region, + None => false, + }; + ::std::rc::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) + } +} diff --git a/TestModels/aws-sdks/kms/src/Index.dfy b/TestModels/aws-sdks/kms/src/Index.dfy index 1dc13bea5..1fccebe35 100644 --- a/TestModels/aws-sdks/kms/src/Index.dfy +++ b/TestModels/aws-sdks/kms/src/Index.dfy @@ -3,7 +3,7 @@ include "../Model/ComAmazonawsKmsTypes.dfy" -module Com.Amazonaws.Kms refines AbstractComAmazonawsKmsService { +module {:extern "software.amazon.cryptography.services.kms.internaldafny"} Com.Amazonaws.Kms refines AbstractComAmazonawsKmsService { function method DefaultKMSClientConfigType() : KMSClientConfigType { KMSClientConfigType diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java index 9c7a0c557..7eea6a965 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java @@ -29,10 +29,8 @@ class RustTestModels extends TestModelTest { DISABLED_TESTS.add("SimpleTypes/SimpleByte"); DISABLED_TESTS.add("SimpleTypes/SimpleFloat"); DISABLED_TESTS.add("SimpleTypes/SimpleShort"); - DISABLED_TESTS.add("aws-sdks/ddb"); DISABLED_TESTS.add("aws-sdks/glue"); DISABLED_TESTS.add("aws-sdks/lakeformation"); - DISABLED_TESTS.add("aws-sdks/kms"); DISABLED_TESTS.add("aws-sdks/sqs"); DISABLED_TESTS.add("aws-sdks/sqs-via-cli"); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java index 884f960f4..6f83c0ec8 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java @@ -678,41 +678,11 @@ private void generateRust(final Path outputDir) { "Rust code generation is incomplete and may not function correctly!" ); - // Clear out all contents of src first to make sure if we didn't intend to generate it, - // it doesn't show up as generated code. This ensures patching has the right baseline. - // It would be great to do this for all languages, - // but we're not currently precise enough and do multiple passes - // to generate code for things like wrapped services. - // - // Be sure to NOT delete src/implementation_from_dafny.rs though, - // by temporarily moving it out of src/ - // - // Note this has no effect if we're being run from the Smithy build plugin, - // since outputDir will be something like `build/smithyprojections/...` - // and therefore not have any existing content. - Path outputSrcDir = outputDir.resolve("src"); - Path implementationFromDafnyPath = outputSrcDir.resolve( - "implementation_from_dafny.rs" - ); - Path tmpPath = null; - try { - if (Files.exists(implementationFromDafnyPath)) { - tmpPath = outputDir.resolve("implementation_from_dafny.rs"); - Files.move(implementationFromDafnyPath, tmpPath); - } - software.amazon.smithy.utils.IoUtils.rmdir(outputSrcDir); - outputSrcDir.toFile().mkdirs(); - if (tmpPath != null) { - Files.move(tmpPath, implementationFromDafnyPath); - } - } catch (IOException e) { - throw new RuntimeException(e); - } - if (awsSdkStyle) { RustAwsSdkShimGenerator generator = new RustAwsSdkShimGenerator( model, - serviceShape + serviceShape, + generationAspects ); generator.generate(outputDir); } else { diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java index 5de4db741..035367936 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java @@ -8,6 +8,7 @@ import java.util.Collection; import java.util.HashMap; import java.util.LinkedHashMap; +import java.util.List; import java.util.Locale; import java.util.Map; import java.util.Optional; @@ -542,18 +543,23 @@ protected TokenTree fromDafny( } } case DOUBLE -> { - if (isRustOption) { + if (isDafnyOption) { yield TokenTree.of( "crate::standard_library_conversions::odouble_from_dafny(%s.clone())".formatted( dafnyValue ) ); } else { - yield TokenTree.of( + TokenTree result = TokenTree.of( "crate::standard_library_conversions::double_from_dafny(&%s.clone())".formatted( dafnyValue ) ); + if (isRustOption) { + result = + TokenTree.of(TokenTree.of("Some("), result, TokenTree.of(")")); + } + yield result; } } case TIMESTAMP -> { @@ -912,6 +918,80 @@ protected RustFile enumConversionModule(final EnumShape enumShape) { ); } + protected RustFile unionConversionModule(final UnionShape unionShape) { + final Map variables = MapUtils.merge( + serviceVariables(), + unionVariables(unionShape) + ); + + final List> perMemberVariables = unionShape + .members() + .stream() + .map(memberShape -> { + final Map memberVariables = MapUtils.merge( + variables, + unionMemberVariables(memberShape) + ); + final Shape targetShape = model.expectShape(memberShape.getTarget()); + memberVariables.put( + "innerToDafny", + toDafny(targetShape, "x", false, false).toString() + ); + memberVariables.put( + "innerFromDafny", + fromDafny(targetShape, "x", false, false).toString() + ); + return memberVariables; + }) + .toList(); + + variables.put( + "toDafnyVariants", + perMemberVariables + .stream() + .map(memberVariables -> + IOUtils.evalTemplate( + """ + $qualifiedRustUnionName:L::$rustUnionMemberName:L(x) => + crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L::$dafnyUnionMemberName:L { + $dafnyUnionMemberName:L: $innerToDafny:L, + }, + """, + memberVariables + ) + ) + .collect(Collectors.joining("\n")) + ); + variables.put( + "fromDafnyVariants", + perMemberVariables + .stream() + .map(memberVariables -> + IOUtils.evalTemplate( + """ + crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L::$dafnyUnionMemberName:L { + $dafnyUnionMemberName:L: x @ _, + } => $qualifiedRustUnionName:L::$rustUnionMemberName:L($innerFromDafny:L), + """, + memberVariables + ) + ) + .collect(Collectors.joining("\n")) + ); + + final String content = IOUtils.evalTemplate( + getClass(), + "runtimes/rust/conversions/union.rs", + variables + ); + final Path path = Path.of( + "src", + "conversions", + "%s.rs".formatted(toSnakeCase(unionName(unionShape))) + ); + return new RustFile(path, TokenTree.of(content)); + } + /** * Generates values for variables commonly used in service-specific templates. */ @@ -1088,8 +1168,8 @@ protected String rustStructureName(final StructureShape structureShape) { protected String qualifiedRustStructureType( final StructureShape structureShape ) { - return "%s::types::%s".formatted( - topLevelNameForShape(structureShape), + return "%s::%s".formatted( + getRustTypesModuleName(), rustStructureName(structureShape) ); } @@ -1228,8 +1308,8 @@ protected String rustUnionName(final UnionShape unionShape) { } protected String qualifiedRustUnionName(final UnionShape unionShape) { - return "%s::types::%s".formatted( - topLevelNameForShape(unionShape), + return "%s::%s".formatted( + getRustTypesModuleName(), rustUnionName(unionShape) ); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java index 4779b873e..00223efad 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java @@ -7,12 +7,15 @@ import java.nio.file.Path; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Locale; import java.util.Map; import java.util.Set; import java.util.stream.Collectors; import java.util.stream.Stream; +import software.amazon.polymorph.CodegenEngine; import software.amazon.polymorph.traits.DafnyUtf8BytesTrait; +import software.amazon.polymorph.utils.IOUtils; import software.amazon.polymorph.utils.MapUtils; import software.amazon.polymorph.utils.ModelUtils; import software.amazon.polymorph.utils.TokenTree; @@ -26,7 +29,11 @@ import software.amazon.smithy.model.shapes.Shape; import software.amazon.smithy.model.shapes.ShapeId; import software.amazon.smithy.model.shapes.StructureShape; +import software.amazon.smithy.model.shapes.UnionShape; +import software.amazon.smithy.model.traits.BoxTrait; +import software.amazon.smithy.model.traits.DefaultTrait; import software.amazon.smithy.model.traits.EnumTrait; +import software.amazon.smithy.rust.codegen.core.smithy.traits.RustBoxTrait; /** * Generates all Rust modules needed to wrap @@ -37,8 +44,15 @@ // putContext method, instead of trying to work purely functionality with map literals. public class RustAwsSdkShimGenerator extends AbstractRustShimGenerator { - public RustAwsSdkShimGenerator(Model model, ServiceShape service) { + private final Set generationAspects; + + public RustAwsSdkShimGenerator( + Model model, + ServiceShape service, + Set generationAspects + ) { super(model, service); + this.generationAspects = generationAspects; } @Override @@ -61,23 +75,40 @@ protected Set rustFiles() { result.add(conversionsModule()); result.addAll(allOperationConversionModules()); result.addAll(allStructureConversionModules()); + result.addAll(allUnionConversionModules()); result.add(conversionsErrorModule()); result.add(conversionsClientModule()); - // TODO union conversion modules return result; } private RustFile clientModule() { final Map variables = serviceVariables(); + variables.put( + "operations", + TokenTree + .of( + service + .getOperations() + .stream() + .map(id -> + operationClientFunction( + model.expectShape(id, OperationShape.class) + ) + ) + ) + .lineSeparated() + .toString() + ); + var preamble = TokenTree.of( evalTemplate( """ use std::sync::LazyLock; use crate::conversions; - struct Client { - inner: $sdkCrate:L::Client + pub struct Client { + pub inner: $sdkCrate:L::Client } /// A runtime for executing operations on the asynchronous client in a blocking manner. @@ -99,51 +130,49 @@ private RustFile clientModule() { impl crate::r#$dafnyTypesModuleName:L::I$clientName:L for Client { - + $operations:L + } """, variables ) ); - var operations = TokenTree - .of( - service - .getOperations() - .stream() - .map(id -> - operationClientFunction(model.expectShape(id, OperationShape.class)) - ) - ) - .lineSeparated(); - - var postamble = TokenTree.of( - evalTemplate( - """ - } - - #[allow(non_snake_case)] - impl crate::r#$dafnyInternalModuleName:L::_default { - pub fn $clientName:L() -> ::std::rc::Rc< - crate::r#_Wrappers_Compile::Result< - ::dafny_runtime::Object, - ::std::rc::Rc - > - > { - let shared_config = dafny_tokio_runtime.block_on(aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28())); - let inner = $sdkCrate:L::Client::new(&shared_config); - let client = Client { inner }; - let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client }) - } - } - """, - variables + final TokenTree postamble; + if ( + generationAspects.contains( + CodegenEngine.GenerationAspect.CLIENT_CONSTRUCTORS ) - ); + ) { + postamble = + TokenTree.of( + evalTemplate( + """ + #[allow(non_snake_case)] + impl crate::r#$dafnyInternalModuleName:L::_default { + pub fn $clientName:L() -> ::std::rc::Rc< + crate::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object, + ::std::rc::Rc + > + > { + let shared_config = dafny_tokio_runtime.block_on(aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28())); + let inner = $sdkCrate:L::Client::new(&shared_config); + let client = Client { inner }; + let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); + std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client }) + } + } + """, + variables + ) + ); + } else { + postamble = TokenTree.empty(); + } return new RustFile( Path.of("src", "client.rs"), - TokenTree.of(preamble, operations, postamble) + TokenTree.of(preamble, postamble) ); } @@ -221,6 +250,40 @@ protected Set allStructureConversionModules() { .collect(Collectors.toSet()); } + @Override + protected boolean shouldGenerateStructForStructure( + StructureShape structureShape + ) { + return ( + super.shouldGenerateStructForStructure(structureShape) && + !isInputOrOutputStructure(structureShape) && + // TODO: Filter to shapes in the service closure (this one's an example of an orphan) + !structureShape + .getId() + .equals( + ShapeId.from( + "com.amazonaws.dynamodb#KinesisStreamingDestinationInput" + ) + ) && + !structureShape + .getId() + .equals( + ShapeId.from( + "com.amazonaws.dynamodb#KinesisStreamingDestinationOutput" + ) + ) + ); + } + + protected Set allUnionConversionModules() { + return model + .getUnionShapes() + .stream() + .filter(this::shouldGenerateEnumForUnion) + .map(this::unionConversionModule) + .collect(Collectors.toSet()); + } + @Override protected TokenTree operationRequestToDafnyFunction( final OperationShape operationShape @@ -267,10 +330,28 @@ protected boolean isRustFieldRequired( final Shape targetShape = model.expectShape(member.getTarget()); return ( super.isRustFieldRequired(parent, member) || - (operationIndex.isOutputStructure(parent) && targetShape.isIntegerShape()) + (operationIndex.isOutputStructure(parent) && + ((!targetShape.hasTrait(BoxTrait.class) && + (targetShape.isIntegerShape() || targetShape.isLongShape())) || + targetShape.isListShape())) || + (!operationIndex.isInputStructure(parent) && + targetShape.isBooleanShape() && + targetShape.hasTrait(DefaultTrait.class)) || + // TODO: I'm giving up on figuring out these ones for now + SPECIAL_CASE_REQUIRED_MEMBERS.contains(member.getId()) ); } + private static final Set SPECIAL_CASE_REQUIRED_MEMBERS = Set.of( + ShapeId.from("com.amazonaws.dynamodb#ImportTableDescription$ErrorCount"), + ShapeId.from( + "com.amazonaws.dynamodb#ImportTableDescription$ProcessedItemCount" + ), + ShapeId.from( + "com.amazonaws.dynamodb#ImportTableDescription$ImportedItemCount" + ) + ); + @Override protected boolean isStructureBuilderFallible( final StructureShape structureShape @@ -469,7 +550,10 @@ protected TokenTree errorVariantToDafny( ); String errorName = toPascalCase(errorShape.getId().getName()); variables.put("errorName", errorName); - variables.put("snakeCaseErrorName", toSnakeCase(errorName)); + variables.put( + "snakeCaseErrorName", + toSnakeCase(errorShape.getId().getName()) + ); return TokenTree.of( evalTemplate( @@ -650,14 +734,22 @@ protected TokenTree toDafny( } } case BOOLEAN -> { - if (isRustOption) { - yield TokenTree.of( - "crate::standard_library_conversions::obool_to_dafny(&%s)".formatted( - rustValue - ) - ); + if (isDafnyOption) { + if (isRustOption) { + yield TokenTree.of( + "crate::standard_library_conversions::obool_to_dafny(&%s)".formatted( + rustValue + ) + ); + } else { + yield TokenTree.of( + "crate::standard_library_conversions::obool_to_dafny(&Some(%s))".formatted( + rustValue + ) + ); + } } else { - yield TokenTree.of(rustValue); + yield TokenTree.of("%s.clone()".formatted(rustValue)); } } case INTEGER -> { @@ -680,26 +772,42 @@ protected TokenTree toDafny( } } case LONG -> { - if (isRustOption) { - yield TokenTree.of( - "crate::standard_library_conversions::olong_to_dafny(&%s)".formatted( - rustValue - ) - ); + if (isDafnyOption) { + if (isRustOption) { + yield TokenTree.of( + "crate::standard_library_conversions::olong_to_dafny(&%s)".formatted( + rustValue + ) + ); + } else { + yield TokenTree.of( + "crate::standard_library_conversions::olong_to_dafny(&Some(%s))".formatted( + rustValue + ) + ); + } } else { yield TokenTree.of(rustValue); } } case DOUBLE -> { - if (isRustOption) { - yield TokenTree.of( - "crate::standard_library_conversions::odouble_to_dafny(&%s)".formatted( - rustValue - ) - ); + if (isDafnyOption) { + if (isRustOption) { + yield TokenTree.of( + "crate::standard_library_conversions::odouble_to_dafny(&%s)".formatted( + rustValue + ) + ); + } else { + yield TokenTree.of( + "crate::standard_library_conversions::double_to_dafny(&Some(%s))".formatted( + rustValue + ) + ); + } } else { yield TokenTree.of( - "crate::standard_library_conversions::double_to_dafny(*%s)".formatted( + "crate::standard_library_conversions::double_to_dafny(%s.clone())".formatted( rustValue ) ); @@ -844,7 +952,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - crate::conversions::%s::to_dafny(%s) + crate::conversions::%s::to_dafny(&%s) """.formatted(structureShapeName, rustValue) ); } @@ -852,7 +960,7 @@ protected TokenTree toDafny( yield TokenTree.of( """ ::std::rc::Rc::new(match &%s { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::%s::to_dafny(x) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::%s::to_dafny(&x) }, None => crate::_Wrappers_Compile::Option::None { } }) """.formatted(rustValue, structureShapeName) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java index 27e2a8556..6f1a5c272 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java @@ -1186,80 +1186,6 @@ private RustFile standardStructureConversionModule( return new RustFile(path, TokenTree.of(content)); } - private RustFile unionConversionModule(final UnionShape unionShape) { - final Map variables = MapUtils.merge( - serviceVariables(), - unionVariables(unionShape) - ); - - final List> perMemberVariables = unionShape - .members() - .stream() - .map(memberShape -> { - final Map memberVariables = MapUtils.merge( - variables, - unionMemberVariables(memberShape) - ); - final Shape targetShape = model.expectShape(memberShape.getTarget()); - memberVariables.put( - "innerToDafny", - toDafny(targetShape, "x", false, false).toString() - ); - memberVariables.put( - "innerFromDafny", - fromDafny(targetShape, "x", false, false).toString() - ); - return memberVariables; - }) - .toList(); - - variables.put( - "toDafnyVariants", - perMemberVariables - .stream() - .map(memberVariables -> - IOUtils.evalTemplate( - """ - $qualifiedRustUnionName:L::$rustUnionMemberName:L(x) => - crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L::$dafnyUnionMemberName:L { - $dafnyUnionMemberName:L: $innerToDafny:L, - }, - """, - memberVariables - ) - ) - .collect(Collectors.joining("\n")) - ); - variables.put( - "fromDafnyVariants", - perMemberVariables - .stream() - .map(memberVariables -> - IOUtils.evalTemplate( - """ - crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L::$dafnyUnionMemberName:L { - $dafnyUnionMemberName:L: x @ _, - } => $qualifiedRustUnionName:L::$rustUnionMemberName:L($innerFromDafny:L), - """, - memberVariables - ) - ) - .collect(Collectors.joining("\n")) - ); - - final String content = IOUtils.evalTemplate( - getClass(), - "runtimes/rust/conversions/union.rs", - variables - ); - final Path path = Path.of( - "src", - "conversions", - "%s.rs".formatted(toSnakeCase(unionName(unionShape))) - ); - return new RustFile(path, TokenTree.of(content)); - } - private RustFile resourceConversionModule(final ResourceShape resourceShape) { final Map variables = MapUtils.merge( serviceVariables(), @@ -1964,13 +1890,13 @@ protected TokenTree toDafny( if (isRustOption) { yield TokenTree.of( """ - %s::conversions::%s::to_dafny(%s.clone().unwrap()) + %s::conversions::%s::to_dafny(&%s.clone().unwrap()) """.formatted(prefix, structureShapeName, rustValue) ); } else { yield TokenTree.of( """ - %s::conversions::%s::to_dafny(%s.clone()) + %s::conversions::%s::to_dafny(&%s.clone()) """.formatted(prefix, structureShapeName, rustValue) ); } @@ -1978,7 +1904,7 @@ protected TokenTree toDafny( yield TokenTree.of( """ ::std::rc::Rc::new(match &%s { - Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::%s::to_dafny(x.clone()) }, + Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::%s::to_dafny(&x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } }) """.formatted(rustValue, prefix, structureShapeName) diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs index 0cade9d80..ca6869c2f 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs @@ -1,10 +1,10 @@ #[allow(dead_code)] pub fn to_dafny( - value: $qualifiedRustStructureType:L, + value: &$qualifiedRustStructureType:L, ) -> ::std::rc::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, > { - ::std::rc::Rc::new(to_dafny_plain(value)) + ::std::rc::Rc::new(to_dafny_plain(value.clone())) } #[allow(dead_code)] diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs index ac44e0bec..199e095b4 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs @@ -1,12 +1,12 @@ #[allow(dead_code)] pub fn to_dafny( - value: $qualifiedRustUnionName:L, + value: &$qualifiedRustUnionName:L, ) -> ::std::rc::Rc< crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L, > { ::std::rc::Rc::new(match value { $toDafnyVariants:L - $qualifiedRustUnionName:L::Unknown => unreachable!(), + _ => panic!("Unknown union variant: {:?}", value), }) }