From ec8f2a36e9cb2256762449b2d3793d11822740b8 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 22 Aug 2024 12:35:24 -0700 Subject: [PATCH] Add more operations to ddb-lite, fix a small codegen bug (#520) --- SmithyDafnyMakefile.mk | 3 + .../model/ComAmazonawsDynamodbTypes.dfy | 306 ++++++++++++++++++ .../ddb-lite/runtimes/rust/src/client.rs | 60 ++++ .../ddb-lite/runtimes/rust/src/conversions.rs | 32 ++ .../conversions/batch_execute_statement.rs | 26 ++ .../_batch_execute_statement_request.rs | 43 +++ .../_batch_execute_statement_response.rs | 32 ++ .../src/conversions/batch_statement_error.rs | 37 +++ .../batch_statement_error_code_enum.rs | 41 +++ .../conversions/batch_statement_request.rs | 48 +++ .../conversions/batch_statement_response.rs | 60 ++++ .../rust/src/conversions/batch_write_item.rs | 34 ++ .../_batch_write_item_request.rs | 63 ++++ .../_batch_write_item_response.rs | 52 +++ .../rust/src/conversions/delete_request.rs | 35 ++ .../runtimes/rust/src/conversions/error.rs | 2 + .../error/duplicate_item_exception.rs | 15 + .../rust/src/conversions/execute_statement.rs | 38 +++ .../_execute_statement_request.rs | 62 ++++ .../_execute_statement_response.rs | 44 +++ .../src/conversions/execute_transaction.rs | 36 +++ .../_execute_transaction_request.rs | 45 +++ .../_execute_transaction_response.rs | 32 ++ .../runtimes/rust/src/conversions/get.rs | 61 ++++ .../rust/src/conversions/item_response.rs | 47 +++ .../conversions/parameterized_statement.rs | 46 +++ .../rust/src/conversions/put_request.rs | 35 ++ .../rust/src/conversions/transact_get_item.rs | 27 ++ .../src/conversions/transact_get_items.rs | 34 ++ .../_transact_get_items_request.rs | 43 +++ .../_transact_get_items_response.rs | 32 ++ .../rust/src/conversions/write_request.rs | 45 +++ .../aws-sdks/ddb-lite/smithy-build.json | 2 +- .../generator/RustAwsSdkShimGenerator.java | 7 +- 34 files changed, 1522 insertions(+), 3 deletions(-) create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error_code_enum.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/duplicate_item_exception.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/parameterized_statement.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_item.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_request.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_response.rs create mode 100644 TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/write_request.rs diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 7d9b292c2..5523fa83e 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -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 diff --git a/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy b/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy index 0cb9c804f..cdd49100d 100644 --- a/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy +++ b/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy @@ -58,6 +58,14 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty predicate method IsValid_BackupArn(x: string) { ( 37 <= |x| <= 1024 ) } + datatype BatchExecuteStatementInput = | BatchExecuteStatementInput ( + nameonly Statements: PartiQLBatchRequest , + nameonly ReturnConsumedCapacity: Option := Option.None + ) + datatype BatchExecuteStatementOutput = | BatchExecuteStatementOutput ( + nameonly Responses: Option := Option.None , + nameonly ConsumedCapacity: Option := Option.None + ) datatype BatchGetItemInput = | BatchGetItemInput ( nameonly RequestItems: BatchGetRequestMap , nameonly ReturnConsumedCapacity: Option := Option.None @@ -72,6 +80,46 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ( 1 <= |x| <= 100 ) } type BatchGetResponseMap = map + datatype BatchStatementError = | BatchStatementError ( + nameonly Code: Option := Option.None , + nameonly Message: Option := Option.None + ) + datatype BatchStatementErrorCodeEnum = + | ConditionalCheckFailed + | ItemCollectionSizeLimitExceeded + | RequestLimitExceeded + | ValidationError + | ProvisionedThroughputExceeded + | TransactionConflict + | ThrottlingError + | InternalServerError + | ResourceNotFound + | AccessDenied + | DuplicateItem + datatype BatchStatementRequest = | BatchStatementRequest ( + nameonly Statement: PartiQLStatement , + nameonly Parameters: Option := Option.None , + nameonly ConsistentRead: Option := Option.None + ) + datatype BatchStatementResponse = | BatchStatementResponse ( + nameonly Error: Option := Option.None , + nameonly TableName: Option := Option.None , + nameonly Item: Option := Option.None + ) + datatype BatchWriteItemInput = | BatchWriteItemInput ( + nameonly RequestItems: BatchWriteItemRequestMap , + nameonly ReturnConsumedCapacity: Option := Option.None , + nameonly ReturnItemCollectionMetrics: Option := Option.None + ) + datatype BatchWriteItemOutput = | BatchWriteItemOutput ( + nameonly UnprocessedItems: Option := Option.None , + nameonly ItemCollectionMetrics: Option := Option.None , + nameonly ConsumedCapacity: Option := Option.None + ) + type BatchWriteItemRequestMap = x: map | IsValid_BatchWriteItemRequestMap(x) witness * + predicate method IsValid_BatchWriteItemRequestMap(x: map) { + ( 1 <= |x| <= 25 ) + } datatype BillingMode = | PROVISIONED | PAY_PER_REQUEST @@ -188,6 +236,9 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty nameonly ConsumedCapacity: Option := Option.None , nameonly ItemCollectionMetrics: Option := Option.None ) + datatype DeleteRequest = | DeleteRequest ( + nameonly Key: Key + ) datatype DescribeTableInput = | DescribeTableInput ( nameonly TableName: TableName ) @@ -196,25 +247,35 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ) class IDynamoDBClientCallHistory { ghost constructor() { + BatchExecuteStatement := []; BatchGetItem := []; + BatchWriteItem := []; CreateTable := []; DeleteItem := []; DescribeTable := []; + ExecuteStatement := []; + ExecuteTransaction := []; GetItem := []; PutItem := []; Query := []; Scan := []; + TransactGetItems := []; TransactWriteItems := []; UpdateItem := []; } + ghost var BatchExecuteStatement: seq>> ghost var BatchGetItem: seq>> + ghost var BatchWriteItem: seq>> ghost var CreateTable: seq>> ghost var DeleteItem: seq>> ghost var DescribeTable: seq>> + ghost var ExecuteStatement: seq>> + ghost var ExecuteTransaction: seq>> ghost var GetItem: seq>> ghost var PutItem: seq>> ghost var Query: seq>> ghost var Scan: seq>> + ghost var TransactGetItems: seq>> ghost var TransactWriteItems: seq>> ghost var UpdateItem: seq>> } @@ -245,6 +306,21 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty predicate ValidState() ensures ValidState() ==> History in Modifies ghost const History: IDynamoDBClientCallHistory + predicate BatchExecuteStatementEnsuresPublicly(input: BatchExecuteStatementInput , output: Result) + // The public method to be called by library consumers + method BatchExecuteStatement ( input: BatchExecuteStatementInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`BatchExecuteStatement + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures BatchExecuteStatementEnsuresPublicly(input, output) + ensures History.BatchExecuteStatement == old(History.BatchExecuteStatement) + [DafnyCallEvent(input, output)] + predicate BatchGetItemEnsuresPublicly(input: BatchGetItemInput , output: Result) // The public method to be called by library consumers method BatchGetItem ( input: BatchGetItemInput ) @@ -260,6 +336,21 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ensures BatchGetItemEnsuresPublicly(input, output) ensures History.BatchGetItem == old(History.BatchGetItem) + [DafnyCallEvent(input, output)] + predicate BatchWriteItemEnsuresPublicly(input: BatchWriteItemInput , output: Result) + // The public method to be called by library consumers + method BatchWriteItem ( input: BatchWriteItemInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`BatchWriteItem + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures BatchWriteItemEnsuresPublicly(input, output) + ensures History.BatchWriteItem == old(History.BatchWriteItem) + [DafnyCallEvent(input, output)] + predicate CreateTableEnsuresPublicly(input: CreateTableInput , output: Result) // The public method to be called by library consumers method CreateTable ( input: CreateTableInput ) @@ -305,6 +396,36 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ensures DescribeTableEnsuresPublicly(input, output) ensures History.DescribeTable == old(History.DescribeTable) + [DafnyCallEvent(input, output)] + predicate ExecuteStatementEnsuresPublicly(input: ExecuteStatementInput , output: Result) + // The public method to be called by library consumers + method ExecuteStatement ( input: ExecuteStatementInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`ExecuteStatement + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures ExecuteStatementEnsuresPublicly(input, output) + ensures History.ExecuteStatement == old(History.ExecuteStatement) + [DafnyCallEvent(input, output)] + + predicate ExecuteTransactionEnsuresPublicly(input: ExecuteTransactionInput , output: Result) + // The public method to be called by library consumers + method ExecuteTransaction ( input: ExecuteTransactionInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`ExecuteTransaction + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures ExecuteTransactionEnsuresPublicly(input, output) + ensures History.ExecuteTransaction == old(History.ExecuteTransaction) + [DafnyCallEvent(input, output)] + predicate GetItemEnsuresPublicly(input: GetItemInput , output: Result) // The public method to be called by library consumers method GetItem ( input: GetItemInput ) @@ -365,6 +486,21 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ensures ScanEnsuresPublicly(input, output) ensures History.Scan == old(History.Scan) + [DafnyCallEvent(input, output)] + predicate TransactGetItemsEnsuresPublicly(input: TransactGetItemsInput , output: Result) + // The public method to be called by library consumers + method TransactGetItems ( input: TransactGetItemsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`TransactGetItems + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures TransactGetItemsEnsuresPublicly(input, output) + ensures History.TransactGetItems == old(History.TransactGetItems) + [DafnyCallEvent(input, output)] + predicate TransactWriteItemsEnsuresPublicly(input: TransactWriteItemsInput , output: Result) // The public method to be called by library consumers method TransactWriteItems ( input: TransactWriteItemsInput ) @@ -397,6 +533,29 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty } type ErrorMessage = string + datatype ExecuteStatementInput = | ExecuteStatementInput ( + nameonly Statement: PartiQLStatement , + nameonly Parameters: Option := Option.None , + nameonly ConsistentRead: Option := Option.None , + nameonly NextToken: Option := Option.None , + nameonly ReturnConsumedCapacity: Option := Option.None , + nameonly Limit: Option := Option.None + ) + datatype ExecuteStatementOutput = | ExecuteStatementOutput ( + nameonly Items: Option := Option.None , + nameonly NextToken: Option := Option.None , + nameonly ConsumedCapacity: Option := Option.None , + nameonly LastEvaluatedKey: Option := Option.None + ) + datatype ExecuteTransactionInput = | ExecuteTransactionInput ( + nameonly TransactStatements: ParameterizedStatements , + nameonly ClientRequestToken: Option := Option.None , + nameonly ReturnConsumedCapacity: Option := Option.None + ) + datatype ExecuteTransactionOutput = | ExecuteTransactionOutput ( + nameonly Responses: Option := Option.None , + nameonly ConsumedCapacity: Option := Option.None + ) type ExpectedAttributeMap = map datatype ExpectedAttributeValue = | ExpectedAttributeValue ( nameonly Value: Option := Option.None , @@ -409,6 +568,12 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty type ExpressionAttributeValueMap = map type ExpressionAttributeValueVariable = string type FilterConditionMap = map + datatype Get = | Get ( + nameonly Key: Key , + nameonly TableName: TableName , + nameonly ProjectionExpression: Option := Option.None , + nameonly ExpressionAttributeNames: Option := Option.None + ) datatype GetItemInput = | GetItemInput ( nameonly TableName: TableName , nameonly Key: Key , @@ -464,6 +629,13 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty } type ItemCollectionSizeEstimateRange = seq type ItemList = seq + datatype ItemResponse = | ItemResponse ( + nameonly Item: Option := Option.None + ) + type ItemResponseList = x: seq | IsValid_ItemResponseList(x) witness * + predicate method IsValid_ItemResponseList(x: seq) { + ( 1 <= |x| <= 25 ) + } type Key = map type KeyConditions = map type KeyExpression = string @@ -528,6 +700,27 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty type NullAttributeValue = bool type NumberAttributeValue = string type NumberSetAttributeValue = seq + datatype ParameterizedStatement = | ParameterizedStatement ( + nameonly Statement: PartiQLStatement , + nameonly Parameters: Option := Option.None + ) + type ParameterizedStatements = x: seq | IsValid_ParameterizedStatements(x) witness * + predicate method IsValid_ParameterizedStatements(x: seq) { + ( 1 <= |x| <= 25 ) + } + type PartiQLBatchRequest = x: seq | IsValid_PartiQLBatchRequest(x) witness * + predicate method IsValid_PartiQLBatchRequest(x: seq) { + ( 1 <= |x| <= 25 ) + } + type PartiQLBatchResponse = seq + type PartiQLNextToken = x: string | IsValid_PartiQLNextToken(x) witness * + predicate method IsValid_PartiQLNextToken(x: string) { + ( 1 <= |x| <= 32768 ) + } + type PartiQLStatement = x: string | IsValid_PartiQLStatement(x) witness * + predicate method IsValid_PartiQLStatement(x: string) { + ( 1 <= |x| <= 8192 ) + } type PositiveIntegerObject = x: int32 | IsValid_PositiveIntegerObject(x) witness * predicate method IsValid_PositiveIntegerObject(x: int32) { ( 1 <= x ) @@ -536,6 +729,10 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty predicate method IsValid_PositiveLongObject(x: int64) { ( 1 <= x ) } + type PreparedStatementParameters = x: seq | IsValid_PreparedStatementParameters(x) witness * + predicate method IsValid_PreparedStatementParameters(x: seq) { + ( 1 <= |x| ) + } datatype Projection = | Projection ( nameonly ProjectionType: Option := Option.None , nameonly NonKeyAttributes: Option := Option.None @@ -585,6 +782,9 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty nameonly ConsumedCapacity: Option := Option.None , nameonly ItemCollectionMetrics: Option := Option.None ) + datatype PutRequest = | PutRequest ( + nameonly Item: PutItemInputAttributeMap + ) datatype QueryInput = | QueryInput ( nameonly TableName: TableName , nameonly IndexName: Option := Option.None , @@ -801,6 +1001,21 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty predicate method IsValid_TagValueString(x: string) { ( 0 <= |x| <= 256 ) } + datatype TransactGetItem = | TransactGetItem ( + nameonly Get: Get + ) + type TransactGetItemList = x: seq | IsValid_TransactGetItemList(x) witness * + predicate method IsValid_TransactGetItemList(x: seq) { + ( 1 <= |x| <= 25 ) + } + datatype TransactGetItemsInput = | TransactGetItemsInput ( + nameonly TransactItems: TransactGetItemList , + nameonly ReturnConsumedCapacity: Option := Option.None + ) + datatype TransactGetItemsOutput = | TransactGetItemsOutput ( + nameonly ConsumedCapacity: Option := Option.None , + nameonly Responses: Option := Option.None + ) datatype TransactWriteItem = | TransactWriteItem ( nameonly ConditionCheck: Option := Option.None , nameonly Put: Option := Option.None , @@ -850,11 +1065,22 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty nameonly ConsumedCapacity: Option := Option.None , nameonly ItemCollectionMetrics: Option := Option.None ) + datatype WriteRequest = | WriteRequest ( + nameonly PutRequest: Option := Option.None , + nameonly DeleteRequest: Option := Option.None + ) + type WriteRequests = x: seq | IsValid_WriteRequests(x) witness * + predicate method IsValid_WriteRequests(x: seq) { + ( 1 <= |x| <= 25 ) + } datatype Error = // Local Error structures are listed here | ConditionalCheckFailedException ( nameonly message: Option := Option.None ) + | DuplicateItemException ( + nameonly message: Option := Option.None + ) | IdempotentParameterMismatchException ( nameonly Message: Option := Option.None ) @@ -929,6 +1155,22 @@ abstract module AbstractComAmazonawsDynamodbOperations { type InternalConfig predicate ValidInternalConfig?(config: InternalConfig) function ModifiesInternalConfig(config: InternalConfig): set + predicate BatchExecuteStatementEnsuresPublicly(input: BatchExecuteStatementInput , output: Result) + // The private method to be refined by the library developer + + + method BatchExecuteStatement ( config: InternalConfig , input: BatchExecuteStatementInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures BatchExecuteStatementEnsuresPublicly(input, output) + + predicate BatchGetItemEnsuresPublicly(input: BatchGetItemInput , output: Result) // The private method to be refined by the library developer @@ -945,6 +1187,22 @@ abstract module AbstractComAmazonawsDynamodbOperations { ensures BatchGetItemEnsuresPublicly(input, output) + predicate BatchWriteItemEnsuresPublicly(input: BatchWriteItemInput , output: Result) + // The private method to be refined by the library developer + + + method BatchWriteItem ( config: InternalConfig , input: BatchWriteItemInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures BatchWriteItemEnsuresPublicly(input, output) + + predicate CreateTableEnsuresPublicly(input: CreateTableInput , output: Result) // The private method to be refined by the library developer @@ -993,6 +1251,38 @@ abstract module AbstractComAmazonawsDynamodbOperations { ensures DescribeTableEnsuresPublicly(input, output) + predicate ExecuteStatementEnsuresPublicly(input: ExecuteStatementInput , output: Result) + // The private method to be refined by the library developer + + + method ExecuteStatement ( config: InternalConfig , input: ExecuteStatementInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures ExecuteStatementEnsuresPublicly(input, output) + + + predicate ExecuteTransactionEnsuresPublicly(input: ExecuteTransactionInput , output: Result) + // The private method to be refined by the library developer + + + method ExecuteTransaction ( config: InternalConfig , input: ExecuteTransactionInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures ExecuteTransactionEnsuresPublicly(input, output) + + predicate GetItemEnsuresPublicly(input: GetItemInput , output: Result) // The private method to be refined by the library developer @@ -1057,6 +1347,22 @@ abstract module AbstractComAmazonawsDynamodbOperations { ensures ScanEnsuresPublicly(input, output) + predicate TransactGetItemsEnsuresPublicly(input: TransactGetItemsInput , output: Result) + // The private method to be refined by the library developer + + + method TransactGetItems ( config: InternalConfig , input: TransactGetItemsInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures TransactGetItemsEnsuresPublicly(input, output) + + predicate TransactWriteItemsEnsuresPublicly(input: TransactWriteItemsInput , output: Result) // The private method to be refined by the library developer 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 eb39b2f15..9db90962c 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs @@ -19,6 +19,18 @@ impl dafny_runtime::UpcastObject) + -> std::rc::Rc, + std::rc::Rc + > +> { + 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) -> std::rc::Rc, @@ -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) + -> std::rc::Rc, + std::rc::Rc + > +> { + 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) -> std::rc::Rc) + -> std::rc::Rc, + std::rc::Rc + > +> { + 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) + -> std::rc::Rc, + std::rc::Rc + > +> { + 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) -> std::rc::Rc) + -> std::rc::Rc, + std::rc::Rc + > +> { + 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) -> std::rc::Rc, +) -> ::std::rc::Rc { + 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()) + } + } +} 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 new file mode 100644 index 000000000..c68a6aa5c --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_request.rs @@ -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, +} +) +} 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 new file mode 100644 index 000000000..7c656f7ca --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_execute_statement/_batch_execute_statement_response.rs @@ -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 {} +}) +, + }) +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error.rs new file mode 100644 index 000000000..f2c72538c --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error.rs @@ -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{ + ::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() + +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error_code_enum.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error_code_enum.rs new file mode 100644 index 000000000..93746fece --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_error_code_enum.rs @@ -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{ + ::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, + } +} 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 new file mode 100644 index 000000000..3c2ef3f34 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_request.rs @@ -0,0 +1,48 @@ +// 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::BatchStatementRequest, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementRequest::BatchStatementRequest { + Statement: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&value.statement), + 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) +, + ) + }, + None => crate::r#_Wrappers_Compile::Option::None {} +}) +, + ConsistentRead: crate::standard_library_conversions::obool_to_dafny(&value.consistent_read), + } + ) +} #[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchStatementRequest, + >, +) -> aws_sdk_dynamodb::types::BatchStatementRequest { + aws_sdk_dynamodb::types::BatchStatementRequest::builder() + .set_statement(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.Statement()) )) + .set_parameters(match (*dafny_value.Parameters()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + |e| crate::conversions::attribute_value::from_dafny(e.clone()) +, + ) + ), + _ => None +} +) + .set_consistent_read(crate::standard_library_conversions::obool_from_dafny(dafny_value.ConsistentRead().clone())) + .build() + .unwrap() +} 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 new file mode 100644 index 000000000..40f105090 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_statement_response.rs @@ -0,0 +1,60 @@ +// 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::BatchStatementResponse, +) -> ::std::rc::Rc{ + ::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) }, + None => crate::_Wrappers_Compile::Option::None { } +}) +, + TableName: crate::standard_library_conversions::ostring_to_dafny(&value.table_name), + Item: +::std::rc::Rc::new(match &value.item { + 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) +, + ) + }, + None => crate::r#_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::BatchStatementResponse, + >, +) -> aws_sdk_dynamodb::types::BatchStatementResponse { + aws_sdk_dynamodb::types::BatchStatementResponse::builder() + .set_error(match (*dafny_value.Error()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some(crate::conversions::batch_statement_error::from_dafny(value.clone())), + _ => None, +} +) + .set_table_name(crate::standard_library_conversions::ostring_from_dafny(dafny_value.TableName().clone())) + .set_item(match (*dafny_value.Item()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| crate::conversions::attribute_value::from_dafny(v.clone()) +, + ) + ), + _ => None +} +) + .build() + +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item.rs new file mode 100644 index 000000000..14082361d --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item.rs @@ -0,0 +1,34 @@ +// 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_write_item_request; + + pub mod _batch_write_item_response; + #[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + aws_sdk_dynamodb::error::SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError::InternalServerError(e) => + crate::conversions::error::internal_server_error::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError::InvalidEndpointException(e) => + crate::conversions::error::invalid_endpoint_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError::ResourceNotFoundException(e) => + crate::conversions::error::resource_not_found_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError::RequestLimitExceeded(e) => + crate::conversions::error::request_limit_exceeded::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError::ItemCollectionSizeLimitExceededException(e) => + crate::conversions::error::item_collection_size_limit_exceeded_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::batch_write_item::BatchWriteItemError::ProvisionedThroughputExceededException(e) => + crate::conversions::error::provisioned_throughput_exceeded_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/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 new file mode 100644 index 000000000..4334945a2 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_request.rs @@ -0,0 +1,63 @@ +// 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_write_item::BatchWriteItemInput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchWriteItemInput, +>{ + ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchWriteItemInput::BatchWriteItemInput { + 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) +, +) +, +) +, + 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 { } +}) +, + ReturnItemCollectionMetrics: ::std::rc::Rc::new(match &value.return_item_collection_metrics { + Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::return_item_collection_metrics::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::BatchWriteItemInput, + >, + client: aws_sdk_dynamodb::Client, +) -> aws_sdk_dynamodb::operation::batch_write_item::builders::BatchWriteItemFluentBuilder { + client.batch_write_item() + .set_request_items(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(&dafny_value.RequestItems(), + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(v, + |e| crate::conversions::write_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, +} +) + .set_return_item_collection_metrics(match &**dafny_value.ReturnItemCollectionMetrics() { + crate::r#_Wrappers_Compile::Option::Some { value } => Some( + crate::conversions::return_item_collection_metrics::from_dafny(value) + ), + _ => None, +} +) +} 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 new file mode 100644 index 000000000..ab6b7a901 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/batch_write_item/_batch_write_item_response.rs @@ -0,0 +1,52 @@ +// 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_write_item::BatchWriteItemOutput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchWriteItemOutput, +>{ + ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchWriteItemOutput::BatchWriteItemOutput { + UnprocessedItems: +::std::rc::Rc::new(match &value.unprocessed_items { + 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| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, + |e| crate::conversions::write_request::to_dafny(&e) +, +) +, + ) + }, + None => crate::r#_Wrappers_Compile::Option::None {} +}) +, + ItemCollectionMetrics: +::std::rc::Rc::new(match &value.item_collection_metrics { + 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| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v, + |e| crate::conversions::item_collection_metrics::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 {} +}) +, + }) +} 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 new file mode 100644 index 000000000..6bccb165d --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/delete_request.rs @@ -0,0 +1,35 @@ +// 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::DeleteRequest, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + 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) +, +) +, + } + ) +} #[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::DeleteRequest, + >, +) -> aws_sdk_dynamodb::types::DeleteRequest { + aws_sdk_dynamodb::types::DeleteRequest::builder() + .set_key(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(&dafny_value.Key(), + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| crate::conversions::attribute_value::from_dafny(v.clone()) +, +) + )) + .build() + .unwrap() +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error.rs index 3d50f7a32..b8bcd2586 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error.rs +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error.rs @@ -3,6 +3,8 @@ // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. pub mod conditional_check_failed_exception; + pub mod duplicate_item_exception; + pub mod idempotent_parameter_mismatch_exception; pub mod internal_server_error; diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/duplicate_item_exception.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/duplicate_item_exception.rs new file mode 100644 index 000000000..da130dca3 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/error/duplicate_item_exception.rs @@ -0,0 +1,15 @@ +// 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::error::DuplicateItemException, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error::DuplicateItemException { + message: crate::standard_library_conversions::ostring_to_dafny(&value.message), + } + ) +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement.rs new file mode 100644 index 000000000..7e872a28d --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement.rs @@ -0,0 +1,38 @@ +// 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 _execute_statement_request; + + pub mod _execute_statement_response; + #[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + aws_sdk_dynamodb::error::SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::InternalServerError(e) => + crate::conversions::error::internal_server_error::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::ResourceNotFoundException(e) => + crate::conversions::error::resource_not_found_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::DuplicateItemException(e) => + crate::conversions::error::duplicate_item_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::RequestLimitExceeded(e) => + crate::conversions::error::request_limit_exceeded::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::TransactionConflictException(e) => + crate::conversions::error::transaction_conflict_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::ConditionalCheckFailedException(e) => + crate::conversions::error::conditional_check_failed_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::ItemCollectionSizeLimitExceededException(e) => + crate::conversions::error::item_collection_size_limit_exceeded_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_statement::ExecuteStatementError::ProvisionedThroughputExceededException(e) => + crate::conversions::error::provisioned_throughput_exceeded_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/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 new file mode 100644 index 000000000..1fd100243 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_request.rs @@ -0,0 +1,62 @@ +// 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::execute_statement::ExecuteStatementInput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementInput, +>{ + ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementInput::ExecuteStatementInput { + Statement: crate::standard_library_conversions::ostring_to_dafny(&value.statement) .Extract(), + 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) +, + ) + }, + None => crate::r#_Wrappers_Compile::Option::None {} +}) +, + ConsistentRead: crate::standard_library_conversions::obool_to_dafny(&value.consistent_read), + NextToken: crate::standard_library_conversions::ostring_to_dafny(&value.next_token), + 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 { } +}) +, + Limit: crate::standard_library_conversions::oint_to_dafny(value.limit), + }) +} + #[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementInput, + >, + client: aws_sdk_dynamodb::Client, +) -> aws_sdk_dynamodb::operation::execute_statement::builders::ExecuteStatementFluentBuilder { + client.execute_statement() + .set_statement(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.Statement()) )) + .set_parameters(match (*dafny_value.Parameters()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + |e| crate::conversions::attribute_value::from_dafny(e.clone()) +, + ) + ), + _ => None +} +) + .set_consistent_read(crate::standard_library_conversions::obool_from_dafny(dafny_value.ConsistentRead().clone())) + .set_next_token(crate::standard_library_conversions::ostring_from_dafny(dafny_value.NextToken().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, +} +) + .set_limit(crate::standard_library_conversions::oint_from_dafny(dafny_value.Limit().clone())) +} 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 new file mode 100644 index 000000000..6f057eaa8 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_statement/_execute_statement_response.rs @@ -0,0 +1,44 @@ +// 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::execute_statement::ExecuteStatementOutput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementOutput, +>{ + ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteStatementOutput::ExecuteStatementOutput { + Items: ::std::rc::Rc::new(match &value.items { + Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : + ::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) +, +) +, + ) + }, + None => crate::r#_Wrappers_Compile::Option::None {} +}) +, + 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) }, + None => crate::_Wrappers_Compile::Option::None { } +}) +, + LastEvaluatedKey: +::std::rc::Rc::new(match &value.last_evaluated_key { + 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) +, + ) + }, + None => crate::r#_Wrappers_Compile::Option::None {} +}) +, + }) +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction.rs new file mode 100644 index 000000000..ad263e4d8 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction.rs @@ -0,0 +1,36 @@ +// 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 _execute_transaction_request; + + pub mod _execute_transaction_response; + #[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + aws_sdk_dynamodb::error::SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::InternalServerError(e) => + crate::conversions::error::internal_server_error::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::ResourceNotFoundException(e) => + crate::conversions::error::resource_not_found_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::IdempotentParameterMismatchException(e) => + crate::conversions::error::idempotent_parameter_mismatch_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::TransactionCanceledException(e) => + crate::conversions::error::transaction_canceled_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::RequestLimitExceeded(e) => + crate::conversions::error::request_limit_exceeded::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::ProvisionedThroughputExceededException(e) => + crate::conversions::error::provisioned_throughput_exceeded_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::execute_transaction::ExecuteTransactionError::TransactionInProgressException(e) => + crate::conversions::error::transaction_in_progress_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/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 new file mode 100644 index 000000000..2171edb6f --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_request.rs @@ -0,0 +1,45 @@ +// 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::execute_transaction::ExecuteTransactionInput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteTransactionInput, +>{ + ::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) +, +) +, + ClientRequestToken: crate::standard_library_conversions::ostring_to_dafny(&value.client_request_token), + 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::ExecuteTransactionInput, + >, + client: aws_sdk_dynamodb::Client, +) -> aws_sdk_dynamodb::operation::execute_transaction::builders::ExecuteTransactionFluentBuilder { + client.execute_transaction() + .set_transact_statements(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(dafny_value.TransactStatements(), + |e| crate::conversions::parameterized_statement::from_dafny(e.clone()) +, +) + )) + .set_client_request_token(crate::standard_library_conversions::ostring_from_dafny(dafny_value.ClientRequestToken().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, +} +) +} 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 new file mode 100644 index 000000000..26d6e4460 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/execute_transaction/_execute_transaction_response.rs @@ -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::execute_transaction::ExecuteTransactionOutput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteTransactionOutput, +>{ + ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ExecuteTransactionOutput::ExecuteTransactionOutput { + 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) +, + ) + }, + 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 {} +}) +, + }) +} 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 new file mode 100644 index 000000000..be1536b92 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/get.rs @@ -0,0 +1,61 @@ +// 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::Get, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + 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) +, +) +, + TableName: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&value.table_name), + ProjectionExpression: crate::standard_library_conversions::ostring_to_dafny(&value.projection_expression), + ExpressionAttributeNames: +::std::rc::Rc::new(match &value.expression_attribute_names { + 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| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&v), + ) + }, + None => crate::r#_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::Get, + >, +) -> aws_sdk_dynamodb::types::Get { + aws_sdk_dynamodb::types::Get::builder() + .set_key(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(&dafny_value.Key(), + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| crate::conversions::attribute_value::from_dafny(v.clone()) +, +) + )) + .set_table_name(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.TableName()) )) + .set_projection_expression(crate::standard_library_conversions::ostring_from_dafny(dafny_value.ProjectionExpression().clone())) + .set_expression_attribute_names(match (*dafny_value.ExpressionAttributeNames()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(v), + ) + ), + _ => None +} +) + .build() + .unwrap() +} 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 new file mode 100644 index 000000000..848abcacc --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/item_response.rs @@ -0,0 +1,47 @@ +// 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::ItemResponse, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ItemResponse::ItemResponse { + Item: +::std::rc::Rc::new(match &value.item { + 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) +, + ) + }, + None => crate::r#_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::ItemResponse, + >, +) -> aws_sdk_dynamodb::types::ItemResponse { + aws_sdk_dynamodb::types::ItemResponse::builder() + .set_item(match (*dafny_value.Item()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value, + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| crate::conversions::attribute_value::from_dafny(v.clone()) +, + ) + ), + _ => None +} +) + .build() + +} 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 new file mode 100644 index 000000000..dc4779246 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/parameterized_statement.rs @@ -0,0 +1,46 @@ +// 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::ParameterizedStatement, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::ParameterizedStatement::ParameterizedStatement { + Statement: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&value.statement), + 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) +, + ) + }, + None => crate::r#_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::ParameterizedStatement, + >, +) -> aws_sdk_dynamodb::types::ParameterizedStatement { + aws_sdk_dynamodb::types::ParameterizedStatement::builder() + .set_statement(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.Statement()) )) + .set_parameters(match (*dafny_value.Parameters()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some( + ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value, + |e| crate::conversions::attribute_value::from_dafny(e.clone()) +, + ) + ), + _ => None +} +) + .build() + .unwrap() +} 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 new file mode 100644 index 000000000..c1ef5c346 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/put_request.rs @@ -0,0 +1,35 @@ +// 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::PutRequest, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + 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) +, +) +, + } + ) +} #[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::PutRequest, + >, +) -> aws_sdk_dynamodb::types::PutRequest { + aws_sdk_dynamodb::types::PutRequest::builder() + .set_item(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(&dafny_value.Item(), + |k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k), + |v| crate::conversions::attribute_value::from_dafny(v.clone()) +, +) + )) + .build() + .unwrap() +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_item.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_item.rs new file mode 100644 index 000000000..8c4f8ced8 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_item.rs @@ -0,0 +1,27 @@ +// 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::TransactGetItem, +) -> ::std::rc::Rc{ + ::std::rc::Rc::new( + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItem::TransactGetItem { + Get: crate::conversions::get::to_dafny(&value.get.clone().unwrap()) +, + } + ) +} #[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItem, + >, +) -> aws_sdk_dynamodb::types::TransactGetItem { + aws_sdk_dynamodb::types::TransactGetItem::builder() + .set_get(Some( crate::conversions::get::from_dafny(dafny_value.Get().clone()) + )) + .build() + +} diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items.rs b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items.rs new file mode 100644 index 000000000..e66edabeb --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items.rs @@ -0,0 +1,34 @@ +// 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 _transact_get_items_request; + + pub mod _transact_get_items_response; + #[allow(dead_code)] +pub fn to_dafny_error( + value: &::aws_smithy_runtime_api::client::result::SdkError< + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError, + ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, + >, +) -> ::std::rc::Rc { + match value { + aws_sdk_dynamodb::error::SdkError::ServiceError(service_error) => match service_error.err() { + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError::InternalServerError(e) => + crate::conversions::error::internal_server_error::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError::InvalidEndpointException(e) => + crate::conversions::error::invalid_endpoint_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError::ResourceNotFoundException(e) => + crate::conversions::error::resource_not_found_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError::TransactionCanceledException(e) => + crate::conversions::error::transaction_canceled_exception::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError::RequestLimitExceeded(e) => + crate::conversions::error::request_limit_exceeded::to_dafny(e.clone()), + aws_sdk_dynamodb::operation::transact_get_items::TransactGetItemsError::ProvisionedThroughputExceededException(e) => + crate::conversions::error::provisioned_throughput_exceeded_exception::to_dafny(e.clone()), + e => crate::conversions::error::to_opaque_error(e.to_string()), + }, + _ => { + crate::conversions::error::to_opaque_error(value.to_string()) + } + } +} diff --git a/TestModels/aws-sdks/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 new file mode 100644 index 000000000..fe0f4f1c2 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_request.rs @@ -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::transact_get_items::TransactGetItemsInput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItemsInput, +>{ + ::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) +, +) +, + 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::TransactGetItemsInput, + >, + client: aws_sdk_dynamodb::Client, +) -> aws_sdk_dynamodb::operation::transact_get_items::builders::TransactGetItemsFluentBuilder { + client.transact_get_items() + .set_transact_items(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(dafny_value.TransactItems(), + |e| crate::conversions::transact_get_item::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, +} +) +} 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 new file mode 100644 index 000000000..db295c367 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/transact_get_items/_transact_get_items_response.rs @@ -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::transact_get_items::TransactGetItemsOutput +) -> ::std::rc::Rc< + crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItemsOutput, +>{ + ::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::TransactGetItemsOutput::TransactGetItemsOutput { + 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 {} +}) +, + 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) +, + ) + }, + None => crate::r#_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 new file mode 100644 index 000000000..e70631be3 --- /dev/null +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/src/conversions/write_request.rs @@ -0,0 +1,45 @@ +// 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::WriteRequest, +) -> ::std::rc::Rc{ + ::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) }, + 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) }, + 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::WriteRequest, + >, +) -> aws_sdk_dynamodb::types::WriteRequest { + aws_sdk_dynamodb::types::WriteRequest::builder() + .set_put_request(match (*dafny_value.PutRequest()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some(crate::conversions::put_request::from_dafny(value.clone())), + _ => None, +} +) + .set_delete_request(match (*dafny_value.DeleteRequest()).as_ref() { + crate::r#_Wrappers_Compile::Option::Some { value } => + Some(crate::conversions::delete_request::from_dafny(value.clone())), + _ => None, +} +) + .build() + +} diff --git a/TestModels/aws-sdks/ddb-lite/smithy-build.json b/TestModels/aws-sdks/ddb-lite/smithy-build.json index 02ebccba7..d651382ac 100644 --- a/TestModels/aws-sdks/ddb-lite/smithy-build.json +++ b/TestModels/aws-sdks/ddb-lite/smithy-build.json @@ -6,7 +6,7 @@ { "name": "excludeShapesBySelector", "args": { - "selector": "operation :not([id|name = BatchGetItem, GetItem, PutItem, UpdateItem, TransactWriteItems, DeleteItem, Query, Scan, CreateTable, DescribeTable])" + "selector": "operation :not([id|name = BatchGetItem, GetItem, PutItem, UpdateItem, TransactWriteItems, DeleteItem, Query, Scan, CreateTable, DescribeTable, BatchExecuteStatement, BatchWriteItem, ExecuteStatement, ExecuteTransaction, TransactGetItems])" } }, { 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 3eb1d9e1d..60fd8e5d7 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 @@ -1510,11 +1510,14 @@ private TokenTree structureFromDafnyFunction( sdkId ); // The builders smithy-rs generates only validate that required fields are provided, - // and only produce `Result<...>` values if there are any required fields. + // and only produce `Result<...>` values if there are any required fields + // (...that aren't structures, for some reason) String unwrapIfNeeded = structureShape .members() .stream() - .anyMatch(m -> m.isRequired()) + .anyMatch(m -> + m.isRequired() && !model.expectShape(m.getTarget()).isStructureShape() + ) ? ".unwrap()" : ""; Map variables = Map.of(