Skip to content

Commit

Permalink
Add more operations to ddb-lite, fix a small codegen bug (#520)
Browse files Browse the repository at this point in the history
  • Loading branch information
robin-aws authored Aug 22, 2024
1 parent 0d4266e commit ec8f2a3
Show file tree
Hide file tree
Showing 34 changed files with 1,522 additions and 3 deletions.
3 changes: 3 additions & 0 deletions SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -553,6 +553,9 @@ transpile_dependencies_rust: transpile_dependencies
_mv_implementation_rust:
mkdir -p runtimes/rust/src
mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/src/implementation_from_dafny.rs
# rustfmt has a recurring bug where it leaves behind trailing spaces and then complains about it.
# 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
rm -rf implementation_from_dafny-rust

Expand Down
306 changes: 306 additions & 0 deletions TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy

Large diffs are not rendered by default.

60 changes: 60 additions & 0 deletions TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,18 @@ impl dafny_runtime::UpcastObject<dyn crate::r#software::amazon::cryptography::se

impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::IDynamoDBClient
for Client {
fn BatchExecuteStatement(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementOutput>,
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
>
> {
let native_result =
self.rt.block_on(conversions::batch_execute_statement::_batch_execute_statement_request::from_dafny(input.clone(), self.inner.clone()).send());
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::batch_execute_statement::_batch_execute_statement_response::to_dafny,
conversions::batch_execute_statement::to_dafny_error)
}
fn BatchGetItem(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchGetItemInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchGetItemOutput>,
Expand All @@ -30,6 +42,18 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::batch_get_item::_batch_get_item_response::to_dafny,
conversions::batch_get_item::to_dafny_error)
}
fn BatchWriteItem(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchWriteItemInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchWriteItemOutput>,
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
>
> {
let native_result =
self.rt.block_on(conversions::batch_write_item::_batch_write_item_request::from_dafny(input.clone(), self.inner.clone()).send());
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::batch_write_item::_batch_write_item_response::to_dafny,
conversions::batch_write_item::to_dafny_error)
}
fn CreateTable(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::CreateTableInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
Expand Down Expand Up @@ -66,6 +90,30 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::describe_table::_describe_table_response::to_dafny,
conversions::describe_table::to_dafny_error)
}
fn ExecuteStatement(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementOutput>,
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
>
> {
let native_result =
self.rt.block_on(conversions::execute_statement::_execute_statement_request::from_dafny(input.clone(), self.inner.clone()).send());
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::execute_statement::_execute_statement_response::to_dafny,
conversions::execute_statement::to_dafny_error)
}
fn ExecuteTransaction(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteTransactionInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteTransactionOutput>,
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
>
> {
let native_result =
self.rt.block_on(conversions::execute_transaction::_execute_transaction_request::from_dafny(input.clone(), self.inner.clone()).send());
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::execute_transaction::_execute_transaction_response::to_dafny,
conversions::execute_transaction::to_dafny_error)
}
fn GetItem(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::GetItemInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
Expand Down Expand Up @@ -114,6 +162,18 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::scan::_scan_response::to_dafny,
conversions::scan::to_dafny_error)
}
fn TransactGetItems(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItemsInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItemsOutput>,
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
>
> {
let native_result =
self.rt.block_on(conversions::transact_get_items::_transact_get_items_request::from_dafny(input.clone(), self.inner.clone()).send());
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::transact_get_items::_transact_get_items_response::to_dafny,
conversions::transact_get_items::to_dafny_error)
}
fn TransactWriteItems(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactWriteItemsInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
Expand Down
32 changes: 32 additions & 0 deletions TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,20 @@ pub mod archival_summary;

pub mod attribute_value_update;

pub mod batch_execute_statement;

pub mod batch_get_item;

pub mod batch_statement_error;

pub mod batch_statement_error_code_enum;

pub mod batch_statement_request;

pub mod batch_statement_response;

pub mod batch_write_item;

pub mod billing_mode;

pub mod billing_mode_summary;
Expand All @@ -37,12 +49,20 @@ pub mod archival_summary;

pub mod delete_item;

pub mod delete_request;

pub mod describe_table;

pub mod error;

pub mod execute_statement;

pub mod execute_transaction;

pub mod expected_attribute_value;

pub mod get;

pub mod get_item;

pub mod global_secondary_index;
Expand All @@ -53,6 +73,8 @@ pub mod archival_summary;

pub mod item_collection_metrics;

pub mod item_response;

pub mod key_schema_element;

pub mod key_type;
Expand All @@ -63,6 +85,8 @@ pub mod archival_summary;

pub mod local_secondary_index_description;

pub mod parameterized_statement;

pub mod projection;

pub mod projection_type;
Expand All @@ -77,6 +101,8 @@ pub mod archival_summary;

pub mod put_item;

pub mod put_request;

pub mod query;

pub mod replica_description;
Expand Down Expand Up @@ -123,10 +149,16 @@ pub mod archival_summary;

pub mod tag;

pub mod transact_get_item;

pub mod transact_get_items;

pub mod transact_write_item;

pub mod transact_write_items;

pub mod update;

pub mod update_item;

pub mod write_request;
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// 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.
pub mod _batch_execute_statement_request;

pub mod _batch_execute_statement_response;
#[allow(dead_code)]
pub fn to_dafny_error(
value: &::aws_smithy_runtime_api::client::result::SdkError<
aws_sdk_dynamodb::operation::batch_execute_statement::BatchExecuteStatementError,
::aws_smithy_runtime_api::client::orchestrator::HttpResponse,
>,
) -> ::std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error> {
match value {
aws_sdk_dynamodb::error::SdkError::ServiceError(service_error) => match service_error.err() {
aws_sdk_dynamodb::operation::batch_execute_statement::BatchExecuteStatementError::InternalServerError(e) =>
crate::conversions::error::internal_server_error::to_dafny(e.clone()),
aws_sdk_dynamodb::operation::batch_execute_statement::BatchExecuteStatementError::RequestLimitExceeded(e) =>
crate::conversions::error::request_limit_exceeded::to_dafny(e.clone()),
e => crate::conversions::error::to_opaque_error(e.to_string()),
},
_ => {
crate::conversions::error::to_opaque_error(value.to_string())
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
// 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.
#[allow(dead_code)]
pub fn to_dafny(
value: &aws_sdk_dynamodb::operation::batch_execute_statement::BatchExecuteStatementInput
) -> ::std::rc::Rc<
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput,
>{
::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)
,
)
,
ReturnConsumedCapacity: ::std::rc::Rc::new(match &value.return_consumed_capacity {
Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::return_consumed_capacity::to_dafny(x.clone()) },
None => crate::_Wrappers_Compile::Option::None { }
})
,
})
}
#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput,
>,
client: aws_sdk_dynamodb::Client,
) -> aws_sdk_dynamodb::operation::batch_execute_statement::builders::BatchExecuteStatementFluentBuilder {
client.batch_execute_statement()
.set_statements(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(dafny_value.Statements(),
|e| crate::conversions::batch_statement_request::from_dafny(e.clone())
,
)
))
.set_return_consumed_capacity(match &**dafny_value.ReturnConsumedCapacity() {
crate::r#_Wrappers_Compile::Option::Some { value } => Some(
crate::conversions::return_consumed_capacity::from_dafny(value)
),
_ => None,
}
)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
// 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.
#[allow(dead_code)]
pub fn to_dafny(
value: &aws_sdk_dynamodb::operation::batch_execute_statement::BatchExecuteStatementOutput
) -> ::std::rc::Rc<
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementOutput,
>{
::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementOutput::BatchExecuteStatementOutput {
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)
,
)
},
None => crate::r#_Wrappers_Compile::Option::None {}
})
,
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)
,
)
},
None => crate::r#_Wrappers_Compile::Option::None {}
})
,
})
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
// 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::BatchStatementError,
) -> ::std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementError>{
::std::rc::Rc::new(
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementError::BatchStatementError {
Code: ::std::rc::Rc::new(match &value.code {
Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::batch_statement_error_code_enum::to_dafny(x.clone()) },
None => crate::_Wrappers_Compile::Option::None { }
})
,
Message: crate::standard_library_conversions::ostring_to_dafny(&value.message),
}
)
} #[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementError,
>,
) -> aws_sdk_dynamodb::types::BatchStatementError {
aws_sdk_dynamodb::types::BatchStatementError::builder()
.set_code(match &**dafny_value.Code() {
crate::r#_Wrappers_Compile::Option::Some { value } => Some(
crate::conversions::batch_statement_error_code_enum::from_dafny(value)
),
_ => None,
}
)
.set_message(crate::standard_library_conversions::ostring_from_dafny(dafny_value.Message().clone()))
.build()

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
// 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.
#[allow(dead_code)]

pub fn to_dafny(
value: aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum,
) -> ::std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum>{
::std::rc::Rc::new(match value {
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ConditionalCheckFailed => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ConditionalCheckFailed {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ItemCollectionSizeLimitExceeded => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ItemCollectionSizeLimitExceeded {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::RequestLimitExceeded => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::RequestLimitExceeded {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ValidationError => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ValidationError {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ProvisionedThroughputExceeded => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ProvisionedThroughputExceeded {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::TransactionConflict => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::TransactionConflict {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ThrottlingError => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ThrottlingError {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::InternalServerError => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::InternalServerError {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ResourceNotFound => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ResourceNotFound {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::AccessDenied => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::AccessDenied {},
aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::DuplicateItem => crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::DuplicateItem {},
_ => panic!("Unknown enum variant: {}", value),
})
}
#[allow(dead_code)]
pub fn from_dafny(
dafny_value: &crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum,
) -> aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum {
match dafny_value {
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ConditionalCheckFailed {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ConditionalCheckFailed,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ItemCollectionSizeLimitExceeded {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ItemCollectionSizeLimitExceeded,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::RequestLimitExceeded {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::RequestLimitExceeded,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ValidationError {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ValidationError,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ProvisionedThroughputExceeded {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ProvisionedThroughputExceeded,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::TransactionConflict {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::TransactionConflict,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ThrottlingError {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ThrottlingError,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::InternalServerError {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::InternalServerError,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::ResourceNotFound {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::ResourceNotFound,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::AccessDenied {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::AccessDenied,
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementErrorCodeEnum::DuplicateItem {} => aws_sdk_dynamodb::types::BatchStatementErrorCodeEnum::DuplicateItem,
}
}
Loading

0 comments on commit ec8f2a3

Please sign in to comment.