diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index ee2f298ac..4700779b8 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -91,8 +91,10 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald class IDynamoDbEncryptionClientCallHistory { ghost constructor() { CreateDynamoDbEncryptionBranchKeyIdSupplier := []; + GetEncryptedDataKeyDescription := []; } ghost var CreateDynamoDbEncryptionBranchKeyIdSupplier: seq>> + ghost var GetEncryptedDataKeyDescription: seq>> } trait {:termination false} IDynamoDbEncryptionClient { @@ -145,6 +147,21 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output) ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)] + predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result) + // The public method to be called by library consumers + method GetEncryptedDataKeyDescription ( input: GetEncryptedDataKeyDescriptionInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetEncryptedDataKeyDescription + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output) + ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)] + } datatype DynamoDbEncryptionConfig = | DynamoDbEncryptionConfig ( @@ -232,6 +249,13 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig ( nameonly tableEncryptionConfigs: DynamoDbTableEncryptionConfigList ) + datatype EncryptedDataKeyDescription = | EncryptedDataKeyDescription ( + nameonly keyProviderId: string , + nameonly keyProviderInfo: Option := Option.None , + nameonly branchKeyId: Option := Option.None , + nameonly branchKeyVersion: Option := Option.None + ) + type EncryptedDataKeyDescriptionList = seq datatype EncryptedPart = | EncryptedPart ( nameonly name: string , nameonly prefix: Prefix @@ -246,6 +270,15 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald datatype GetBranchKeyIdFromDdbKeyOutput = | GetBranchKeyIdFromDdbKeyOutput ( nameonly branchKeyId: string ) + datatype GetEncryptedDataKeyDescriptionInput = | GetEncryptedDataKeyDescriptionInput ( + nameonly input: GetEncryptedDataKeyDescriptionUnion + ) + datatype GetEncryptedDataKeyDescriptionOutput = | GetEncryptedDataKeyDescriptionOutput ( + nameonly EncryptedDataKeyDescriptionOutput: EncryptedDataKeyDescriptionList + ) + datatype GetEncryptedDataKeyDescriptionUnion = + | header(header: seq) + | item(item: ComAmazonawsDynamodbTypes.AttributeMap) datatype GetPrefix = | GetPrefix ( nameonly length: int32 ) @@ -510,6 +543,26 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService History.CreateDynamoDbEncryptionBranchKeyIdSupplier := History.CreateDynamoDbEncryptionBranchKeyIdSupplier + [DafnyCallEvent(input, output)]; } + predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result) + {Operations.GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetEncryptedDataKeyDescription ( input: GetEncryptedDataKeyDescriptionInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetEncryptedDataKeyDescription + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output) + ensures History.GetEncryptedDataKeyDescription == old(History.GetEncryptedDataKeyDescription) + [DafnyCallEvent(input, output)] + { + output := Operations.GetEncryptedDataKeyDescription(config, input); + History.GetEncryptedDataKeyDescription := History.GetEncryptedDataKeyDescription + [DafnyCallEvent(input, output)]; + } + } } abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations { @@ -541,4 +594,20 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations { && fresh(output.value.branchKeyIdSupplier) && fresh ( output.value.branchKeyIdSupplier.Modifies - ModifiesInternalConfig(config) - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output) + + + predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result) + // The private method to be refined by the library developer + + + method GetEncryptedDataKeyDescription ( config: InternalConfig , input: GetEncryptedDataKeyDescriptionInput ) + 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 GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output) } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index 5d21749f6..b4c0066f9 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -20,6 +20,7 @@ use aws.cryptography.keyStore#KeyStore use aws.cryptography.dbEncryptionSdk.structuredEncryption#CryptoAction use com.amazonaws.dynamodb#DynamoDB_20120810 +use com.amazonaws.dynamodb#AttributeMap use com.amazonaws.dynamodb#TableName use com.amazonaws.dynamodb#AttributeName use com.amazonaws.dynamodb#Key @@ -42,11 +43,69 @@ use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders ] ) service DynamoDbEncryption { - version: "2022-11-21", - operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier ], + version: "2024-04-02", + operations: [ CreateDynamoDbEncryptionBranchKeyIdSupplier, GetEncryptedDataKeyDescription], errors: [ DynamoDbEncryptionException ] } +@javadoc("Returns encrypted data key description.") +operation GetEncryptedDataKeyDescription { + input: GetEncryptedDataKeyDescriptionInput, + output: GetEncryptedDataKeyDescriptionOutput, +} + +@javadoc("Input for getting encrypted data key description.") +structure GetEncryptedDataKeyDescriptionInput { + @required + input: GetEncryptedDataKeyDescriptionUnion +} + +//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#input +//= type=implication +//# This operation MUST take in either of the following: +//# - A binary [header](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md) +//# - A [encrypted DynamoDB item](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/ff9f08a355a20c81540e4ca652e09aaeffe90c4b/specification/dynamodb-encryption-client/encrypt-item.md#encrypted-dynamodb-item) + +union GetEncryptedDataKeyDescriptionUnion { + @javadoc("A binary header value.") + header: Blob, + @javadoc("A DynamoDB item.") + item: AttributeMap, +} + +@javadoc("Output for getting encrypted data key description.") +structure GetEncryptedDataKeyDescriptionOutput { + @required + @javadoc("A list of encrypted data key description.") + EncryptedDataKeyDescriptionOutput: EncryptedDataKeyDescriptionList +} + +list EncryptedDataKeyDescriptionList { + member: EncryptedDataKeyDescription +} + +//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#output +//= type=implication +//# This operation MUST return the following: +//# - [keyProviderId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-id) +//#- [keyProviderInfo](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for AWS Cryptographic Materials Provider Keyring) +//#- [branchKeyId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring) +//#- [branchKeyVersion](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring) + +structure EncryptedDataKeyDescription { + @required + @javadoc("Key provider id of the encrypted data key.") + keyProviderId: String, + + @javadoc("Key provider information of the encrypted data key.") + keyProviderInfo: String, + + @javadoc("Branch key id of the encrypted data key.") + branchKeyId: String, + + @javadoc("Branch key version of the encrypted data key.") + branchKeyVersion: String +} // The top level DynamoDbEncryption local service takes in no config structure DynamoDbEncryptionConfig { } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy index 23b45586e..c1379da88 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy @@ -5,6 +5,15 @@ include "DynamoDbEncryptionBranchKeyIdSupplier.dfy" module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations { import DynamoDbEncryptionBranchKeyIdSupplier + import EdkWrapping + import UUID + import AlgorithmSuites + import Header = StructuredEncryptionHeader + import opened DynamoDbEncryptionUtil + + const SALT_LENGTH := 16 + const IV_LENGTH := 12 + const VERSION_LENGTH := 16 predicate ValidInternalConfig?(config: InternalConfig) {true} @@ -33,4 +42,72 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt ) ); } + predicate GetEncryptedDataKeyDescriptionEnsuresPublicly(input: GetEncryptedDataKeyDescriptionInput , output: Result) + {true} + + method GetEncryptedDataKeyDescription(config: InternalConfig, input: GetEncryptedDataKeyDescriptionInput) + returns (output: Result) + ensures GetEncryptedDataKeyDescriptionEnsuresPublicly(input, output) + { + var header; + match input.input + { + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //# - If the input is an encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get the binary header. + case item(item) =>{ + :- Need("aws_dbe_head" in item && item["aws_dbe_head"].B?, E("Header not found in the DynamoDB item.")); + header := item["aws_dbe_head"].B; + } + case header(headerItem) => + header := headerItem; + } + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //# - This operation MUST deserialize the header bytes according to the header format. + var deserializedHeader :- Header.PartialDeserialize(header).MapFailure(e => AwsCryptographyDbEncryptionSdkStructuredEncryption(e)); + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //# - This operation MUST extract the dataKeys from the deserialize header. + var datakeys := deserializedHeader.dataKeys; + var list : EncryptedDataKeyDescriptionList := []; + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key. + for i := 0 to |datakeys| { + var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e)); + var extractedKeyProviderIdInfo:= Option.None; + var expectedBranchKeyVersion := Option.None; + if ("aws-kms" <= extractedKeyProviderId) { + :- Need(deserializedHeader.flavor == 0 || deserializedHeader.flavor == 1, E("Invalid format flavor.")); + var algorithmSuite; + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //# - This operation MUST extract the Format Flavor from the deserialize header. + if deserializedHeader.flavor == 0{ + algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384; + } else { + algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384; + } + var maybeKeyProviderIdInfo :- UTF8.Decode(datakeys[i].keyProviderInfo).MapFailure(e => E(e)); + extractedKeyProviderIdInfo := Some(maybeKeyProviderIdInfo); + if extractedKeyProviderId == "aws-kms-hierarchy" { + var providerWrappedMaterial :- EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).MapFailure(e => AwsCryptographyMaterialProviders(e)); + var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH; + var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH; + :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index.")); + :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length.")); + var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX]; + var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e)); + expectedBranchKeyVersion := Some(maybeBranchKeyVersion); + } + } + var singleDataKeyOutput := EncryptedDataKeyDescription( + keyProviderId := extractedKeyProviderId, + keyProviderInfo := extractedKeyProviderIdInfo, + branchKeyId := extractedKeyProviderIdInfo, + branchKeyVersion := expectedBranchKeyVersion + ); + list := list + [singleDataKeyOutput]; + } + + output := Success(GetEncryptedDataKeyDescriptionOutput( + EncryptedDataKeyDescriptionOutput := list + )); + } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy new file mode 100644 index 000000000..2f5cb02a8 --- /dev/null +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy @@ -0,0 +1,287 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/Index.dfy" + +module DynamoDbGetEncryptedDataKeyDescriptionTest { + import DynamoDbEncryption + import opened StandardLibrary.UInt + import opened StructuredEncryptionHeader + import opened StructuredEncryptionUtil + import opened UTF8 + import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes + import UUID + import ComAmazonawsDynamodbTypes + import EdkWrapping + import AlgorithmSuites + + // THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT + const testVersion : Version := 1 + const testFlavor0 : Flavor := 0 + const testFlavor1 : Flavor := 1 + const testMsgID : MessageID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32] + const testLegend : Legend := [0x65, 0x73] + const testEncContext : CMPEncryptionContext := map[EncodeAscii("abc") := EncodeAscii("def")] + const testAwsKmsDataKey := CMP.EncryptedDataKey( + keyProviderId := EncodeAscii("aws-kms") , + keyProviderInfo := EncodeAscii("keyproviderInfo"), + ciphertext := [1, 2, 3, 4, 5]) + const testAwsKmsHDataKey := CMP.EncryptedDataKey( + keyProviderId := EncodeAscii("aws-kms-hierarchy") , + keyProviderInfo := EncodeAscii("keyproviderInfo"), + ciphertext := [ + 64, 92, 115, 7, 85, 121, 112, 79, 69, 12, 82, 25, 67, 34, + 11, 66, 93, 45, 40, 23, 90, 61, 16, 28, 59, 114, 52, 122, + 50, 23, 11, 101, 48, 53, 30, 120, 51, 74, 77, 53, 57, 99, + 53, 13, 30, 21, 109, 85, 15, 86, 47, 84, 91, 85, 87, 60, 4, + 56, 67, 74, 29, 87, 85, 106, 8, 82, 63, 114, 100, 110, 68, + 58, 83, 24, 111, 41, 21, 91, 122, 61, 118, 37, 72, 38, 67, 2, + 17, 61, 17, 121, 7, 90, 117, 49, 30, 20, 89, 68, 33, 111, + 107, 5, 120, 20, 95, 78, 70, 2, 49, 84, 39, 50, 40, 40, 115, + 114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81, + 24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72]) + const testRawRsaDataKey := CMP.EncryptedDataKey( + keyProviderId := EncodeAscii("raw-rsa") , + keyProviderInfo := [1, 2, 3, 4, 5], + ciphertext := [6, 7, 8, 9]) + const testAwsKmsRsaDataKey := CMP.EncryptedDataKey( + keyProviderId := EncodeAscii("aws-kms-rsa") , + keyProviderInfo := EncodeAscii("keyproviderInfo"), + ciphertext := [1, 2, 3, 4, 5]) + + method CreatePartialHeader(version : Version, flavor : Flavor, msgID : MessageID, legend : Legend, encContext : CMPEncryptionContext, dataKeyList : CMPEncryptedDataKeyList) + returns (result: PartialHeader) + ensures result.version == version + ensures result.flavor == flavor + ensures result.msgID == msgID + ensures result.legend == legend + ensures result.encContext == encContext + ensures result.dataKeys == dataKeyList + { + result := PartialHeader ( + version := version, + flavor := flavor, + msgID := msgID, + legend := legend, + encContext := encContext, + dataKeys := dataKeyList + ); + } + + method {:test} TestHeaderInputAwsKmsDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.header(header := serializedHeader) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + } + + method {:test} TestHeaderInputAwsKmsHDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.header(header := serializedHeader) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms-hierarchy"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + + assertBranchKey(actualDataKeyDescription); + } + + method {:test} TestHeaderInputRawRsaDataKeyDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testRawRsaDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.header(header := serializedHeader) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "raw-rsa"; + } + + method {:test} TestHeaderInputAwsKmsRsaDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsRsaDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.header(header := serializedHeader) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms-rsa"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + } + + + method {:test} TestDDBItemInputAwsKmsDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)]; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.item(item := attr) + ); + + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + } + + method {:test} TestDDBItemInputAwsKmsHDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor0, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)]; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.item(item := attr) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms-hierarchy"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + + assertBranchKey(actualDataKeyDescription); + } + + method {:test} TestDDBItemInputRawRsaDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testRawRsaDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)]; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.item(item := attr) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "raw-rsa"; + } + + method {:test} TestDDBItemInputAwsKmsRsaDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsRsaDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)]; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.item(item := attr) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms-rsa"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + } + + method {:test} TestHeaderMultiDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey, testAwsKmsRsaDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.header(header := serializedHeader) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 2; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[1].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[1].keyProviderId == "aws-kms-rsa"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[1].keyProviderInfo.value == "keyproviderInfo"; + } + + method {:test} TestDDBItemInputMultiDataKeyCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey, testAwsKmsRsaDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)]; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.item(item := attr) + ); + var actualDataKeyDescription :- expect ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 2; + + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //= type=test + //# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key. + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 2; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderId == "aws-kms"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo"; + + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[1].keyProviderInfo.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[1].keyProviderId == "aws-kms-rsa"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[1].keyProviderInfo.value == "keyproviderInfo"; + } + + method {:test} TestNoHeaderFailureCase() + { + var expectedHead := CreatePartialHeader(testVersion, testFlavor1, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]); + var serializedHeader := expectedHead.serialize() + expectedHead.msgID; + var attr := map["wrong_header_attribute" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)]; + var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); + var inputVariable: Types.GetEncryptedDataKeyDescriptionInput := + Types.GetEncryptedDataKeyDescriptionInput( + input := Types.item(item := attr) + ); + var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable); + + expect actualDataKeyDescription.IsFailure(); + expect actualDataKeyDescription.error.DynamoDbEncryptionException?; + expect actualDataKeyDescription.error.message == "Header not found in the DynamoDB item."; + } + + method assertBranchKey(actualDataKeyDescription : Types.GetEncryptedDataKeyDescriptionOutput) + { + expect |actualDataKeyDescription.EncryptedDataKeyDescriptionOutput| == 1; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].branchKeyId.Some?; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].branchKeyVersion.Some?; + + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].branchKeyId.value == "keyproviderInfo"; + expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].branchKeyVersion.value == "155b7a3d-7625-4826-4302-113d1179075a"; + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryption.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryption.java index df1ae96f0..4ae4177d6 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryption.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryption.java @@ -13,6 +13,8 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CreateDynamoDbEncryptionBranchKeyIdSupplierInput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CreateDynamoDbEncryptionBranchKeyIdSupplierOutput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbEncryptionConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput; public class DynamoDbEncryption { @@ -62,6 +64,27 @@ public CreateDynamoDbEncryptionBranchKeyIdSupplierOutput CreateDynamoDbEncryptio ); } + /** + * Returns encrypted data key description. + * + * @param input Input for getting encrypted data key description. + * @return Output for getting encrypted data key description. + */ + public GetEncryptedDataKeyDescriptionOutput GetEncryptedDataKeyDescription( + GetEncryptedDataKeyDescriptionInput input + ) { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput dafnyValue = + ToDafny.GetEncryptedDataKeyDescriptionInput(input); + Result< + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput, + Error + > result = this._impl.GetEncryptedDataKeyDescription(dafnyValue); + if (result.is_Failure()) { + throw ToNative.Error(result.dtor_error()); + } + return ToNative.GetEncryptedDataKeyDescriptionOutput(result.dtor_value()); + } + protected IDynamoDbEncryptionClient impl() { return this._impl; } diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java index fd041a8a3..88677a441 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java @@ -27,11 +27,15 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbEncryptionConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTableEncryptionConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedPart; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error_DynamoDbEncryptionException; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyInput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetPrefix; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetSegment; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetSegments; @@ -377,6 +381,49 @@ public static DynamoDbTablesEncryptionConfig DynamoDbTablesEncryptionConfig( return new DynamoDbTablesEncryptionConfig(tableEncryptionConfigs); } + public static EncryptedDataKeyDescription EncryptedDataKeyDescription( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescription nativeValue + ) { + DafnySequence keyProviderId; + keyProviderId = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.keyProviderId() + ); + Option> keyProviderInfo; + keyProviderInfo = + Objects.nonNull(nativeValue.keyProviderInfo()) + ? Option.create_Some( + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.keyProviderInfo() + ) + ) + : Option.create_None(); + Option> branchKeyId; + branchKeyId = + Objects.nonNull(nativeValue.branchKeyId()) + ? Option.create_Some( + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.branchKeyId() + ) + ) + : Option.create_None(); + Option> branchKeyVersion; + branchKeyVersion = + Objects.nonNull(nativeValue.branchKeyVersion()) + ? Option.create_Some( + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.branchKeyVersion() + ) + ) + : Option.create_None(); + return new EncryptedDataKeyDescription( + keyProviderId, + keyProviderInfo, + branchKeyId, + branchKeyVersion + ); + } + public static EncryptedPart EncryptedPart( software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedPart nativeValue ) { @@ -418,6 +465,29 @@ public static GetBranchKeyIdFromDdbKeyOutput GetBranchKeyIdFromDdbKeyOutput( return new GetBranchKeyIdFromDdbKeyOutput(branchKeyId); } + public static GetEncryptedDataKeyDescriptionInput GetEncryptedDataKeyDescriptionInput( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput nativeValue + ) { + GetEncryptedDataKeyDescriptionUnion input; + input = ToDafny.GetEncryptedDataKeyDescriptionUnion(nativeValue.input()); + return new GetEncryptedDataKeyDescriptionInput(input); + } + + public static GetEncryptedDataKeyDescriptionOutput GetEncryptedDataKeyDescriptionOutput( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput nativeValue + ) { + DafnySequence< + ? extends EncryptedDataKeyDescription + > encryptedDataKeyDescriptionOutput; + encryptedDataKeyDescriptionOutput = + ToDafny.EncryptedDataKeyDescriptionList( + nativeValue.EncryptedDataKeyDescriptionOutput() + ); + return new GetEncryptedDataKeyDescriptionOutput( + encryptedDataKeyDescriptionOutput + ); + } + public static GetPrefix GetPrefix( software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetPrefix nativeValue ) { @@ -788,6 +858,30 @@ public static BeaconStyle BeaconStyle( ); } + public static GetEncryptedDataKeyDescriptionUnion GetEncryptedDataKeyDescriptionUnion( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionUnion nativeValue + ) { + if (Objects.nonNull(nativeValue.header())) { + return GetEncryptedDataKeyDescriptionUnion.create_header( + software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence( + nativeValue.header() + ) + ); + } + if (Objects.nonNull(nativeValue.item())) { + return GetEncryptedDataKeyDescriptionUnion.create_item( + software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeMap( + nativeValue.item() + ) + ); + } + throw new IllegalArgumentException( + "Cannot convert " + + nativeValue + + " to software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion." + ); + } + public static VirtualTransform VirtualTransform( software.amazon.cryptography.dbencryptionsdk.dynamodb.model.VirtualTransform nativeValue ) { @@ -882,6 +976,20 @@ public static DafnySequence ConstructorPartList( ); } + public static DafnySequence< + ? extends EncryptedDataKeyDescription + > EncryptedDataKeyDescriptionList( + List< + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescription + > nativeValue + ) { + return software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( + nativeValue, + software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny::EncryptedDataKeyDescription, + EncryptedDataKeyDescription._typeDescriptor() + ); + } + public static DafnySequence EncryptedPartsList( List< software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedPart diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java index 933c696e1..bd4b65bc4 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java @@ -30,9 +30,13 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbEncryptionException; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbTableEncryptionConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbTablesEncryptionConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescription; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedPart; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetBranchKeyIdFromDdbKeyInput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetBranchKeyIdFromDdbKeyOutput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionUnion; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetPrefix; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetSegment; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetSegments; @@ -360,6 +364,40 @@ public static DynamoDbTablesEncryptionConfig DynamoDbTablesEncryptionConfig( return nativeBuilder.build(); } + public static EncryptedDataKeyDescription EncryptedDataKeyDescription( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription dafnyValue + ) { + EncryptedDataKeyDescription.Builder nativeBuilder = + EncryptedDataKeyDescription.builder(); + nativeBuilder.keyProviderId( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_keyProviderId() + ) + ); + if (dafnyValue.dtor_keyProviderInfo().is_Some()) { + nativeBuilder.keyProviderInfo( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_keyProviderInfo().dtor_value() + ) + ); + } + if (dafnyValue.dtor_branchKeyId().is_Some()) { + nativeBuilder.branchKeyId( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_branchKeyId().dtor_value() + ) + ); + } + if (dafnyValue.dtor_branchKeyVersion().is_Some()) { + nativeBuilder.branchKeyVersion( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_branchKeyVersion().dtor_value() + ) + ); + } + return nativeBuilder.build(); + } + public static EncryptedPart EncryptedPart( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedPart dafnyValue ) { @@ -403,6 +441,30 @@ public static GetBranchKeyIdFromDdbKeyOutput GetBranchKeyIdFromDdbKeyOutput( return nativeBuilder.build(); } + public static GetEncryptedDataKeyDescriptionInput GetEncryptedDataKeyDescriptionInput( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput dafnyValue + ) { + GetEncryptedDataKeyDescriptionInput.Builder nativeBuilder = + GetEncryptedDataKeyDescriptionInput.builder(); + nativeBuilder.input( + ToNative.GetEncryptedDataKeyDescriptionUnion(dafnyValue.dtor_input()) + ); + return nativeBuilder.build(); + } + + public static GetEncryptedDataKeyDescriptionOutput GetEncryptedDataKeyDescriptionOutput( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput dafnyValue + ) { + GetEncryptedDataKeyDescriptionOutput.Builder nativeBuilder = + GetEncryptedDataKeyDescriptionOutput.builder(); + nativeBuilder.EncryptedDataKeyDescriptionOutput( + ToNative.EncryptedDataKeyDescriptionList( + dafnyValue.dtor_EncryptedDataKeyDescriptionOutput() + ) + ); + return nativeBuilder.build(); + } + public static GetPrefix GetPrefix( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetPrefix dafnyValue ) { @@ -724,6 +786,28 @@ public static BeaconStyle BeaconStyle( return nativeBuilder.build(); } + public static GetEncryptedDataKeyDescriptionUnion GetEncryptedDataKeyDescriptionUnion( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion dafnyValue + ) { + GetEncryptedDataKeyDescriptionUnion.Builder nativeBuilder = + GetEncryptedDataKeyDescriptionUnion.builder(); + if (dafnyValue.is_header()) { + nativeBuilder.header( + software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer( + dafnyValue.dtor_header() + ) + ); + } + if (dafnyValue.is_item()) { + nativeBuilder.item( + software.amazon.cryptography.services.dynamodb.internaldafny.ToNative.AttributeMap( + dafnyValue.dtor_item() + ) + ); + } + return nativeBuilder.build(); + } + public static VirtualTransform VirtualTransform( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.VirtualTransform dafnyValue ) { @@ -801,6 +885,19 @@ public static List ConstructorPartList( ); } + public static List< + EncryptedDataKeyDescription + > EncryptedDataKeyDescriptionList( + DafnySequence< + ? extends software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription + > dafnyValue + ) { + return software.amazon.smithy.dafny.conversion.ToNative.Aggregate.GenericToList( + dafnyValue, + software.amazon.cryptography.dbencryptionsdk.dynamodb.ToNative::EncryptedDataKeyDescription + ); + } + public static List EncryptedPartsList( DafnySequence< ? extends software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedPart diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/EncryptedDataKeyDescription.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/EncryptedDataKeyDescription.java new file mode 100644 index 000000000..14ce01777 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/EncryptedDataKeyDescription.java @@ -0,0 +1,181 @@ +// 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. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.Objects; + +public class EncryptedDataKeyDescription { + + /** + * Key provider id of the encrypted data key. + */ + private final String keyProviderId; + + /** + * Key provider information of the encrypted data key. + */ + private final String keyProviderInfo; + + /** + * Branch key id of the encrypted data key. + */ + private final String branchKeyId; + + /** + * Branch key version of the encrypted data key. + */ + private final String branchKeyVersion; + + protected EncryptedDataKeyDescription(BuilderImpl builder) { + this.keyProviderId = builder.keyProviderId(); + this.keyProviderInfo = builder.keyProviderInfo(); + this.branchKeyId = builder.branchKeyId(); + this.branchKeyVersion = builder.branchKeyVersion(); + } + + /** + * @return Key provider id of the encrypted data key. + */ + public String keyProviderId() { + return this.keyProviderId; + } + + /** + * @return Key provider information of the encrypted data key. + */ + public String keyProviderInfo() { + return this.keyProviderInfo; + } + + /** + * @return Branch key id of the encrypted data key. + */ + public String branchKeyId() { + return this.branchKeyId; + } + + /** + * @return Branch key version of the encrypted data key. + */ + public String branchKeyVersion() { + return this.branchKeyVersion; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param keyProviderId Key provider id of the encrypted data key. + */ + Builder keyProviderId(String keyProviderId); + + /** + * @return Key provider id of the encrypted data key. + */ + String keyProviderId(); + + /** + * @param keyProviderInfo Key provider information of the encrypted data key. + */ + Builder keyProviderInfo(String keyProviderInfo); + + /** + * @return Key provider information of the encrypted data key. + */ + String keyProviderInfo(); + + /** + * @param branchKeyId Branch key id of the encrypted data key. + */ + Builder branchKeyId(String branchKeyId); + + /** + * @return Branch key id of the encrypted data key. + */ + String branchKeyId(); + + /** + * @param branchKeyVersion Branch key version of the encrypted data key. + */ + Builder branchKeyVersion(String branchKeyVersion); + + /** + * @return Branch key version of the encrypted data key. + */ + String branchKeyVersion(); + + EncryptedDataKeyDescription build(); + } + + static class BuilderImpl implements Builder { + + protected String keyProviderId; + + protected String keyProviderInfo; + + protected String branchKeyId; + + protected String branchKeyVersion; + + protected BuilderImpl() {} + + protected BuilderImpl(EncryptedDataKeyDescription model) { + this.keyProviderId = model.keyProviderId(); + this.keyProviderInfo = model.keyProviderInfo(); + this.branchKeyId = model.branchKeyId(); + this.branchKeyVersion = model.branchKeyVersion(); + } + + public Builder keyProviderId(String keyProviderId) { + this.keyProviderId = keyProviderId; + return this; + } + + public String keyProviderId() { + return this.keyProviderId; + } + + public Builder keyProviderInfo(String keyProviderInfo) { + this.keyProviderInfo = keyProviderInfo; + return this; + } + + public String keyProviderInfo() { + return this.keyProviderInfo; + } + + public Builder branchKeyId(String branchKeyId) { + this.branchKeyId = branchKeyId; + return this; + } + + public String branchKeyId() { + return this.branchKeyId; + } + + public Builder branchKeyVersion(String branchKeyVersion) { + this.branchKeyVersion = branchKeyVersion; + return this; + } + + public String branchKeyVersion() { + return this.branchKeyVersion; + } + + public EncryptedDataKeyDescription build() { + if (Objects.isNull(this.keyProviderId())) { + throw new IllegalArgumentException( + "Missing value for required field `keyProviderId`" + ); + } + return new EncryptedDataKeyDescription(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/EncryptedDataKeyDescriptionOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/EncryptedDataKeyDescriptionOutput.java new file mode 100644 index 000000000..f9f99732c --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/EncryptedDataKeyDescriptionOutput.java @@ -0,0 +1,133 @@ +// 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. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.Objects; + +public class EncryptedDataKeyDescriptionOutput { + + private final String keyProviderId; + + private final String keyProviderInfo; + + private final String branchKeyId; + + private final String branchKeyVersion; + + protected EncryptedDataKeyDescriptionOutput(BuilderImpl builder) { + this.keyProviderId = builder.keyProviderId(); + this.keyProviderInfo = builder.keyProviderInfo(); + this.branchKeyId = builder.branchKeyId(); + this.branchKeyVersion = builder.branchKeyVersion(); + } + + public String keyProviderId() { + return this.keyProviderId; + } + + public String keyProviderInfo() { + return this.keyProviderInfo; + } + + public String branchKeyId() { + return this.branchKeyId; + } + + public String branchKeyVersion() { + return this.branchKeyVersion; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + Builder keyProviderId(String keyProviderId); + + String keyProviderId(); + + Builder keyProviderInfo(String keyProviderInfo); + + String keyProviderInfo(); + + Builder branchKeyId(String branchKeyId); + + String branchKeyId(); + + Builder branchKeyVersion(String branchKeyVersion); + + String branchKeyVersion(); + + EncryptedDataKeyDescriptionOutput build(); + } + + static class BuilderImpl implements Builder { + + protected String keyProviderId; + + protected String keyProviderInfo; + + protected String branchKeyId; + + protected String branchKeyVersion; + + protected BuilderImpl() {} + + protected BuilderImpl(EncryptedDataKeyDescriptionOutput model) { + this.keyProviderId = model.keyProviderId(); + this.keyProviderInfo = model.keyProviderInfo(); + this.branchKeyId = model.branchKeyId(); + this.branchKeyVersion = model.branchKeyVersion(); + } + + public Builder keyProviderId(String keyProviderId) { + this.keyProviderId = keyProviderId; + return this; + } + + public String keyProviderId() { + return this.keyProviderId; + } + + public Builder keyProviderInfo(String keyProviderInfo) { + this.keyProviderInfo = keyProviderInfo; + return this; + } + + public String keyProviderInfo() { + return this.keyProviderInfo; + } + + public Builder branchKeyId(String branchKeyId) { + this.branchKeyId = branchKeyId; + return this; + } + + public String branchKeyId() { + return this.branchKeyId; + } + + public Builder branchKeyVersion(String branchKeyVersion) { + this.branchKeyVersion = branchKeyVersion; + return this; + } + + public String branchKeyVersion() { + return this.branchKeyVersion; + } + + public EncryptedDataKeyDescriptionOutput build() { + if (Objects.isNull(this.keyProviderId())) { + throw new IllegalArgumentException( + "Missing value for required field `keyProviderId`" + ); + } + return new EncryptedDataKeyDescriptionOutput(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionInput.java new file mode 100644 index 000000000..71ed715d2 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionInput.java @@ -0,0 +1,67 @@ +// 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. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.Objects; + +/** + * Input for getting encrypted data key description. + */ +public class GetEncryptedDataKeyDescriptionInput { + + private final GetEncryptedDataKeyDescriptionUnion input; + + protected GetEncryptedDataKeyDescriptionInput(BuilderImpl builder) { + this.input = builder.input(); + } + + public GetEncryptedDataKeyDescriptionUnion input() { + return this.input; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + Builder input(GetEncryptedDataKeyDescriptionUnion input); + + GetEncryptedDataKeyDescriptionUnion input(); + + GetEncryptedDataKeyDescriptionInput build(); + } + + static class BuilderImpl implements Builder { + + protected GetEncryptedDataKeyDescriptionUnion input; + + protected BuilderImpl() {} + + protected BuilderImpl(GetEncryptedDataKeyDescriptionInput model) { + this.input = model.input(); + } + + public Builder input(GetEncryptedDataKeyDescriptionUnion input) { + this.input = input; + return this; + } + + public GetEncryptedDataKeyDescriptionUnion input() { + return this.input; + } + + public GetEncryptedDataKeyDescriptionInput build() { + if (Objects.isNull(this.input())) { + throw new IllegalArgumentException( + "Missing value for required field `input`" + ); + } + return new GetEncryptedDataKeyDescriptionInput(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionOutput.java new file mode 100644 index 000000000..42448b411 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionOutput.java @@ -0,0 +1,93 @@ +// 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. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.List; +import java.util.Objects; + +/** + * Output for getting encrypted data key description. + */ +public class GetEncryptedDataKeyDescriptionOutput { + + /** + * A list of encrypted data key description. + */ + private final List< + EncryptedDataKeyDescription + > EncryptedDataKeyDescriptionOutput; + + protected GetEncryptedDataKeyDescriptionOutput(BuilderImpl builder) { + this.EncryptedDataKeyDescriptionOutput = + builder.EncryptedDataKeyDescriptionOutput(); + } + + /** + * @return A list of encrypted data key description. + */ + public List EncryptedDataKeyDescriptionOutput() { + return this.EncryptedDataKeyDescriptionOutput; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param EncryptedDataKeyDescriptionOutput A list of encrypted data key description. + */ + Builder EncryptedDataKeyDescriptionOutput( + List EncryptedDataKeyDescriptionOutput + ); + + /** + * @return A list of encrypted data key description. + */ + List EncryptedDataKeyDescriptionOutput(); + + GetEncryptedDataKeyDescriptionOutput build(); + } + + static class BuilderImpl implements Builder { + + protected List< + EncryptedDataKeyDescription + > EncryptedDataKeyDescriptionOutput; + + protected BuilderImpl() {} + + protected BuilderImpl(GetEncryptedDataKeyDescriptionOutput model) { + this.EncryptedDataKeyDescriptionOutput = + model.EncryptedDataKeyDescriptionOutput(); + } + + public Builder EncryptedDataKeyDescriptionOutput( + List EncryptedDataKeyDescriptionOutput + ) { + this.EncryptedDataKeyDescriptionOutput = + EncryptedDataKeyDescriptionOutput; + return this; + } + + public List< + EncryptedDataKeyDescription + > EncryptedDataKeyDescriptionOutput() { + return this.EncryptedDataKeyDescriptionOutput; + } + + public GetEncryptedDataKeyDescriptionOutput build() { + if (Objects.isNull(this.EncryptedDataKeyDescriptionOutput())) { + throw new IllegalArgumentException( + "Missing value for required field `EncryptedDataKeyDescriptionOutput`" + ); + } + return new GetEncryptedDataKeyDescriptionOutput(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionUnion.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionUnion.java new file mode 100644 index 000000000..ae8d95673 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/GetEncryptedDataKeyDescriptionUnion.java @@ -0,0 +1,128 @@ +// 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. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.nio.ByteBuffer; +import java.util.Map; +import java.util.Objects; +import software.amazon.awssdk.services.dynamodb.model.AttributeValue; + +public class GetEncryptedDataKeyDescriptionUnion { + + /** + * A binary header value. + */ + private final ByteBuffer header; + + /** + * A DynamoDB item. + */ + private final Map item; + + protected GetEncryptedDataKeyDescriptionUnion(BuilderImpl builder) { + this.header = builder.header(); + this.item = builder.item(); + } + + /** + * @return A binary header value. + */ + public ByteBuffer header() { + return this.header; + } + + /** + * @return A DynamoDB item. + */ + public Map item() { + return this.item; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param header A binary header value. + */ + Builder header(ByteBuffer header); + + /** + * @return A binary header value. + */ + ByteBuffer header(); + + /** + * @param item A DynamoDB item. + */ + Builder item(Map item); + + /** + * @return A DynamoDB item. + */ + Map item(); + + GetEncryptedDataKeyDescriptionUnion build(); + } + + static class BuilderImpl implements Builder { + + protected ByteBuffer header; + + protected Map item; + + protected BuilderImpl() {} + + protected BuilderImpl(GetEncryptedDataKeyDescriptionUnion model) { + this.header = model.header(); + this.item = model.item(); + } + + public Builder header(ByteBuffer header) { + this.header = header; + return this; + } + + public ByteBuffer header() { + return this.header; + } + + public Builder item(Map item) { + this.item = item; + return this; + } + + public Map item() { + return this.item; + } + + public GetEncryptedDataKeyDescriptionUnion build() { + if (!onlyOneNonNull()) { + throw new IllegalArgumentException( + "`GetEncryptedDataKeyDescriptionUnion` is a Union. A Union MUST have one and only one value set." + ); + } + return new GetEncryptedDataKeyDescriptionUnion(this); + } + + private boolean onlyOneNonNull() { + Object[] allValues = { this.header, this.item }; + boolean haveOneNonNull = false; + for (Object o : allValues) { + if (Objects.nonNull(o)) { + if (haveOneNonNull) { + return false; + } + haveOneNonNull = true; + } + } + return haveOneNonNull; + } + } +} diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/DynamoDbEncryption.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/DynamoDbEncryption.cs index e20ef0ee3..99cfc88b5 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/DynamoDbEncryption.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/DynamoDbEncryption.cs @@ -33,5 +33,12 @@ public AWS.Cryptography.DbEncryptionSDK.DynamoDb.CreateDynamoDbEncryptionBranchK if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); return TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S49_CreateDynamoDbEncryptionBranchKeyIdSupplierOutput(result.dtor_value); } + public AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput GetEncryptedDataKeyDescription(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput input) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionInput internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput(input); + Wrappers_Compile._IResult result = _impl.GetEncryptedDataKeyDescription(internalInput); + if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); + return TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput(result.dtor_value); + } } } diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/EncryptedDataKeyDescription.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/EncryptedDataKeyDescription.cs new file mode 100644 index 000000000..33bd04ec5 --- /dev/null +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/EncryptedDataKeyDescription.cs @@ -0,0 +1,56 @@ +// 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. +using System; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb +{ + public class EncryptedDataKeyDescription + { + private string _keyProviderId; + private string _keyProviderInfo; + private string _branchKeyId; + private string _branchKeyVersion; + public string KeyProviderId + { + get { return this._keyProviderId; } + set { this._keyProviderId = value; } + } + public bool IsSetKeyProviderId() + { + return this._keyProviderId != null; + } + public string KeyProviderInfo + { + get { return this._keyProviderInfo; } + set { this._keyProviderInfo = value; } + } + public bool IsSetKeyProviderInfo() + { + return this._keyProviderInfo != null; + } + public string BranchKeyId + { + get { return this._branchKeyId; } + set { this._branchKeyId = value; } + } + public bool IsSetBranchKeyId() + { + return this._branchKeyId != null; + } + public string BranchKeyVersion + { + get { return this._branchKeyVersion; } + set { this._branchKeyVersion = value; } + } + public bool IsSetBranchKeyVersion() + { + return this._branchKeyVersion != null; + } + public void Validate() + { + if (!IsSetKeyProviderId()) throw new System.ArgumentException("Missing value for required property 'KeyProviderId'"); + + } + } +} diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/EncryptedDataKeyDescriptionOutput.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/EncryptedDataKeyDescriptionOutput.cs new file mode 100644 index 000000000..b7b9d3897 --- /dev/null +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/EncryptedDataKeyDescriptionOutput.cs @@ -0,0 +1,56 @@ +// 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. +using System; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb +{ + public class EncryptedDataKeyDescriptionOutput + { + private string _keyProviderId; + private string _keyProviderInfo; + private string _branchKeyId; + private string _branchKeyVersion; + public string KeyProviderId + { + get { return this._keyProviderId; } + set { this._keyProviderId = value; } + } + public bool IsSetKeyProviderId() + { + return this._keyProviderId != null; + } + public string KeyProviderInfo + { + get { return this._keyProviderInfo; } + set { this._keyProviderInfo = value; } + } + public bool IsSetKeyProviderInfo() + { + return this._keyProviderInfo != null; + } + public string BranchKeyId + { + get { return this._branchKeyId; } + set { this._branchKeyId = value; } + } + public bool IsSetBranchKeyId() + { + return this._branchKeyId != null; + } + public string BranchKeyVersion + { + get { return this._branchKeyVersion; } + set { this._branchKeyVersion = value; } + } + public bool IsSetBranchKeyVersion() + { + return this._branchKeyVersion != null; + } + public void Validate() + { + if (!IsSetKeyProviderId()) throw new System.ArgumentException("Missing value for required property 'KeyProviderId'"); + + } + } +} diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionInput.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionInput.cs new file mode 100644 index 000000000..9517b6dc0 --- /dev/null +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionInput.cs @@ -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. +using System; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb +{ + public class GetEncryptedDataKeyDescriptionInput + { + private AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion _input; + public AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion Input + { + get { return this._input; } + set { this._input = value; } + } + public bool IsSetInput() + { + return this._input != null; + } + public void Validate() + { + if (!IsSetInput()) throw new System.ArgumentException("Missing value for required property 'Input'"); + + } + } +} diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionOutput.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionOutput.cs new file mode 100644 index 000000000..e18046288 --- /dev/null +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionOutput.cs @@ -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. +using System; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb +{ + public class GetEncryptedDataKeyDescriptionOutput + { + private System.Collections.Generic.List _encryptedDataKeyDescriptionOutput; + public System.Collections.Generic.List EncryptedDataKeyDescriptionOutput + { + get { return this._encryptedDataKeyDescriptionOutput; } + set { this._encryptedDataKeyDescriptionOutput = value; } + } + public bool IsSetEncryptedDataKeyDescriptionOutput() + { + return this._encryptedDataKeyDescriptionOutput != null; + } + public void Validate() + { + if (!IsSetEncryptedDataKeyDescriptionOutput()) throw new System.ArgumentException("Missing value for required property 'EncryptedDataKeyDescriptionOutput'"); + + } + } +} diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionUnion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionUnion.cs new file mode 100644 index 000000000..52333120e --- /dev/null +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/GetEncryptedDataKeyDescriptionUnion.cs @@ -0,0 +1,40 @@ +// 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. +using System; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb +{ + public class GetEncryptedDataKeyDescriptionUnion + { + private System.IO.MemoryStream _header; + private System.Collections.Generic.Dictionary _item; + public System.IO.MemoryStream Header + { + get { return this._header; } + set { this._header = value; } + } + public bool IsSetHeader() + { + return this._header != null; + } + public System.Collections.Generic.Dictionary Item + { + get { return this._item; } + set { this._item = value; } + } + public bool IsSetItem() + { + return this._item != null; + } + public void Validate() + { + var numberOfPropertiesSet = Convert.ToUInt16(IsSetHeader()) + + Convert.ToUInt16(IsSetItem()); + if (numberOfPropertiesSet == 0) throw new System.ArgumentException("No union value set"); + + if (numberOfPropertiesSet > 1) throw new System.ArgumentException("Multiple union values set"); + + } + } +} diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs index ff93147e2..a2a04f8ca 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs @@ -179,6 +179,53 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_GetBranchKeyIdFromDdbKeyOutput__M11_branchKeyId(value.BranchKeyId)); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionInput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput(); converted.Input = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(concrete._input); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionInput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(value.Input)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionOutput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput(); converted.EncryptedDataKeyDescriptionOutput = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(concrete._EncryptedDataKeyDescriptionOutput); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionOutput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(value.EncryptedDataKeyDescriptionOutput)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion)value; + var converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion(); if (value.is_header) + { + converted.Header = FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(concrete.dtor_header); + return converted; + } + if (value.is_item) + { + converted.Item = FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(concrete.dtor_item); + return converted; + } + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion state"); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion value) + { + value.Validate(); if (value.IsSetHeader()) + { + return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion.create_header(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(value.Header)); + } + if (value.IsSetItem()) + { + return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion.create_item(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(value.Item)); + } + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion state"); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S12_LegacyPolicy(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy value) { if (value.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT; @@ -376,6 +423,38 @@ public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncr { return ToDafny_N6_smithy__N3_api__S6_String(value); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(value); + } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(Dafny.ISequence value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(System.Collections.Generic.List value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(value); + } + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(Dafny.ISequence value) + { + return FromDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(System.IO.MemoryStream value) + { + return ToDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_VirtualTransform__M5_upper(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IUpper value) { return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_Upper(value); @@ -552,6 +631,37 @@ public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S6_String(string new Dafny.Pair, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue>(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M3_key(pair.Key), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M5_value(pair.Value)) )); } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(Dafny.ISequence value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member)); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(System.Collections.Generic.List value) + { + return Dafny.Sequence.FromArray(value.Select(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member).ToArray()); + } + public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny.ISequence value) + { + return new System.IO.MemoryStream(value.Elements); + } + public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) + { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } + return Dafny.Sequence.FromArray(value.ToArray()); + + } + public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(pair.Car), pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(pair.Cdr)); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(System.Collections.Generic.Dictionary value) + { + return Dafny.Map, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue>.FromCollection(value.Select(pair => + new Dafny.Pair, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue>(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(pair.Key), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(pair.Value)) + )); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_Upper(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IUpper value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Upper concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Upper)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper(); return converted; @@ -708,6 +818,30 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types { return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member(AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static Amazon.DynamoDBv2.Model.AttributeValue FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } + public static software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(Amazon.DynamoDBv2.Model.AttributeValue value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S6_Insert__M7_literal(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); @@ -957,6 +1091,21 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types } throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state"); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription(); converted.KeyProviderId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(concrete._keyProviderId); + if (concrete._keyProviderInfo.is_Some) converted.KeyProviderInfo = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(concrete._keyProviderInfo); + if (concrete._branchKeyId.is_Some) converted.BranchKeyId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(concrete._branchKeyId); + if (concrete._branchKeyVersion.is_Some) converted.BranchKeyVersion = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(concrete._branchKeyVersion); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription value) + { + value.Validate(); + string var_keyProviderInfo = value.IsSetKeyProviderInfo() ? value.KeyProviderInfo : (string)null; + string var_branchKeyId = value.IsSetBranchKeyId() ? value.BranchKeyId : (string)null; + string var_branchKeyVersion = value.IsSetBranchKeyVersion() ? value.BranchKeyVersion : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(value.KeyProviderId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(var_keyProviderInfo), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(var_branchKeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(var_branchKeyVersion)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S4_Char(Dafny.ISequence value) { return new string(value.Elements); @@ -1085,6 +1234,38 @@ public static bool ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue { return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_BooleanAttributeValue(value); } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(Dafny.ISequence value) + { + return FromDafny_N6_smithy__N3_api__S6_String(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(string value) + { + return ToDafny_N6_smithy__N3_api__S6_String(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static AWS.Cryptography.MaterialProviders.DefaultCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S12_DefaultCache(software.amazon.cryptography.materialproviders.internaldafny.types._IDefaultCache value) { software.amazon.cryptography.materialproviders.internaldafny.types.DefaultCache concrete = (software.amazon.cryptography.materialproviders.internaldafny.types.DefaultCache)value; AWS.Cryptography.MaterialProviders.DefaultCache converted = new AWS.Cryptography.MaterialProviders.DefaultCache(); converted.EntryCapacity = (int)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S12_DefaultCache__M13_entryCapacity(concrete._entryCapacity); return converted; diff --git a/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/GetEncryptedDataKeyDescriptionExample.java b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/GetEncryptedDataKeyDescriptionExample.java new file mode 100644 index 000000000..6c096f761 --- /dev/null +++ b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/GetEncryptedDataKeyDescriptionExample.java @@ -0,0 +1,94 @@ +package software.amazon.cryptography.examples; + +import software.amazon.awssdk.regions.Region; +import software.amazon.awssdk.services.dynamodb.model.*; +import software.amazon.awssdk.services.dynamodb.DynamoDbClient; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.DynamoDbEncryption; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbEncryptionConfig; + +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionUnion; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput; +import java.nio.ByteBuffer; + +import java.util.HashMap; +import java.util.Map; +import java.util.*; + +public class GetEncryptedDataKeyDescriptionExample{ + public static void getEncryptedDataKeyDescription( + String tableName, String partitionKey, String partitionKeyVal, String sortKeyName, String sortKeyValue, + String expectedKeyProviderId, String expectedKeyProviderInfo, String expectedBranchKeyId, String expectedBranchKeyVersion + ) { + + // 1. Create a new AWS SDK DynamoDb client. This client will be used to get item from the DynamoDB table + DynamoDbClient ddb = DynamoDbClient.builder() + .build(); + + // 2. Get item from the DynamoDB table. This item will be used to Get Encrypted DataKey Description + HashMap keyToGet = new HashMap<>(); + keyToGet.put(partitionKey, AttributeValue.builder() + .s(partitionKeyVal) + .build()); + keyToGet.put(sortKeyName, AttributeValue.builder() + .n(sortKeyValue) + .build()); + GetItemRequest request = GetItemRequest.builder() + .tableName(tableName) + .key(keyToGet) + .build(); + Map returnedItem = ddb.getItem(request).item(); + if (returnedItem.isEmpty()) + System.out.format("No item found with the key %s!\n", partitionKey); + + // 3. Prepare the input for GetEncryptedDataKeyDescription method. + // This input can be a DynamoDB item or a header. For now, we are giving input as a DynamoDB item + // but users can also extract the header from the attribute "aws_dbe_head" in the DynamoDB table + // and use it for GetEncryptedDataKeyDescription method. + DynamoDbEncryption ddbEnc = DynamoDbEncryption.builder() + .DynamoDbEncryptionConfig(DynamoDbEncryptionConfig.builder().build()) + .build(); + GetEncryptedDataKeyDescriptionUnion InputUnion = GetEncryptedDataKeyDescriptionUnion.builder() + .item(returnedItem) + .build(); + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput input = GetEncryptedDataKeyDescriptionInput.builder() + .input(InputUnion) + .build(); + GetEncryptedDataKeyDescriptionOutput output = ddbEnc.GetEncryptedDataKeyDescription(input); + + // In the following code, we are giving input as header instead of a complete DynamoDB item + // This code is provided solely to demo how the alternative approach works. So, it is commented. + + // String header_attribute = "aws_dbe_head"; + // ByteBuffer header = returnedItem.get(header_attribute).b().asByteBuffer(); + // GetEncryptedDataKeyDescriptionUnion InputUnion = GetEncryptedDataKeyDescriptionUnion.builder() + // .header(header) + // .build(); + + // Assert everything + assert output.EncryptedDataKeyDescriptionOutput().get(0).keyProviderId().equals(expectedKeyProviderId); + if(expectedKeyProviderId.startsWith("aws-kms")) { + assert output.EncryptedDataKeyDescriptionOutput().get(0).keyProviderInfo().equals(expectedKeyProviderInfo); + } + if(output.EncryptedDataKeyDescriptionOutput().get(0).keyProviderId().equals("aws-kms-hierarchy")) { + assert output.EncryptedDataKeyDescriptionOutput().get(0).branchKeyId().equals(expectedBranchKeyId); + assert output.EncryptedDataKeyDescriptionOutput().get(0).branchKeyVersion().equals(expectedBranchKeyVersion); + } + } + public static void main(final String[] args) { + if (args.length < 9) { + throw new IllegalArgumentException("To run this example, include the tableName, partitionKey, partitionKeyVal," + + "sortKeyName, sortKeyValue, expectedKeyProviderId, expectedKeyProviderInfo, expectedBranchKeyId and expectedBranchKeyVersion in args"); + } + final String tableName = args[0]; + final String partitionKey = args[1]; + final String partitionKeyVal = args[2]; + final String sortKeyName = args[3]; + final String sortKeyValue = args[4]; + final String expectedKeyProviderId = args[5]; + final String expectedKeyProviderInfo = args[6]; + final String expectedBranchKeyId = args[7]; + final String expectedBranchKeyVersion = args[8]; + getEncryptedDataKeyDescription(tableName, partitionKey, partitionKeyVal, sortKeyName, sortKeyValue, expectedKeyProviderId, expectedKeyProviderInfo, expectedBranchKeyId, expectedBranchKeyVersion); + } +} \ No newline at end of file diff --git a/Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/TestGetEncryptedDataKeyDescriptionExample.java b/Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/TestGetEncryptedDataKeyDescriptionExample.java new file mode 100644 index 000000000..475bb6e5b --- /dev/null +++ b/Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/TestGetEncryptedDataKeyDescriptionExample.java @@ -0,0 +1,10 @@ +package software.amazon.cryptography.examples; + +import org.testng.annotations.Test; + +public class TestGetEncryptedDataKeyDescriptionExample { + @Test + public void TestGetEncryptedDataKeyDescription() { + GetEncryptedDataKeyDescriptionExample.getEncryptedDataKeyDescription(TestUtils.TEST_DDB_TABLE_NAME,"partition_key","BasicPutGetExample","sort_key","0","aws-kms",TestUtils.TEST_KMS_KEY_ID,null,null); + } +} \ No newline at end of file diff --git a/Examples/runtimes/net/src/Examples.cs b/Examples/runtimes/net/src/Examples.cs index f4a84288d..64ed261b4 100644 --- a/Examples/runtimes/net/src/Examples.cs +++ b/Examples/runtimes/net/src/Examples.cs @@ -12,6 +12,7 @@ static async Task Main() ItemEncryptDecryptExample.PutItemGetItem(); await BasicPutGetExample.PutItemGetItem(); + await GetEncryptedDataKeyDescriptionExample.GetEncryptedDataKeyDescription(); await MultiPutGetExample.MultiPutGet(); await ClientSupplierExample.ClientSupplierPutItemGetItem(); await MultiMrkKeyringExample.MultiMrkKeyringGetItemPutItem(); diff --git a/Examples/runtimes/net/src/GetEncryptedDataKeyDescriptionExample.cs b/Examples/runtimes/net/src/GetEncryptedDataKeyDescriptionExample.cs new file mode 100644 index 000000000..c4300cb51 --- /dev/null +++ b/Examples/runtimes/net/src/GetEncryptedDataKeyDescriptionExample.cs @@ -0,0 +1,60 @@ +using System; +using System.Diagnostics; +using System.Net; +using System.Threading.Tasks; +using System.Collections.Generic; +using Amazon.DynamoDBv2.Model; +using Amazon.DynamoDBv2; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; + +public class GetEncryptedDataKeyDescriptionExample +{ + public static async Task GetEncryptedDataKeyDescription() + { + var kmsKeyId = TestUtils.TEST_KMS_KEY_ID; + var ddbTableName = TestUtils.TEST_DDB_TABLE_NAME; + var ddbEnc = new DynamoDbEncryption(new DynamoDbEncryptionConfig()); + + // 1. Define keys that will be used to retrieve item from the DynamoDB table. + var keyToGet = new Dictionary + { + ["partition_key"] = new AttributeValue("BasicPutGetExample"), + ["sort_key"] = new AttributeValue { N = "0" }, + }; + + // 2. Create a Amazon DynamoDB Client and retrieve item from DynamoDB table + var ddb = new AmazonDynamoDBClient(); + GetItemRequest getRequest = new GetItemRequest + { + Key = keyToGet, + TableName = ddbTableName, + }; + GetItemResponse getResponse = await ddb.GetItemAsync(getRequest); + + // Demonstrate that GetItem succeeded + Debug.Assert(getResponse.HttpStatusCode == HttpStatusCode.OK); + + // 3. Extract the item from the dynamoDB table and prepare input for the GetEncryptedDataKeyDescription method. + // Here, we are sending dynamodb item but you can also input the header itself by extracting the header from + // "aws_dbe_head" attribute in the dynamoDB item. The part of the code where we send input as the header is commented. + var returnedItem = getResponse.Item; + GetEncryptedDataKeyDescriptionUnion InputUnion = new GetEncryptedDataKeyDescriptionUnion(); + InputUnion.Item = returnedItem; + + // The code below shows how we can send header as the input to the DynamoDB. This code is written to demo the + // alternative approach. So, it is commented. + + // string header_attribute = "aws_dbe_head"; + // InputUnion.Header = returnedItem[header_attribute].B; + + GetEncryptedDataKeyDescriptionInput Input = new GetEncryptedDataKeyDescriptionInput(); + Input.Input = InputUnion; + GetEncryptedDataKeyDescriptionOutput output = ddbEnc.GetEncryptedDataKeyDescription(Input); + + // 4. Get encrypted DataKey Descriptions from GetEncryptedDataKeyDescription method output and assert if its true. + var encryptedDataKeyDescriptions = output.EncryptedDataKeyDescriptionOutput; + Debug.Assert(encryptedDataKeyDescriptions[0].KeyProviderId == "aws-kms"); + Debug.Assert(encryptedDataKeyDescriptions[0].KeyProviderInfo == kmsKeyId); + } +} + diff --git a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java index c1749520d..acf30bd1e 100644 --- a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java +++ b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java @@ -13,6 +13,8 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.CreateDynamoDbEncryptionBranchKeyIdSupplierInput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.CreateDynamoDbEncryptionBranchKeyIdSupplierOutput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.IDynamoDbEncryptionClient; public class TestDynamoDbEncryption implements IDynamoDbEncryptionClient { @@ -46,6 +48,25 @@ > CreateDynamoDbEncryptionBranchKeyIdSupplier( } } + public Result< + GetEncryptedDataKeyDescriptionOutput, + Error + > GetEncryptedDataKeyDescription( + GetEncryptedDataKeyDescriptionInput dafnyInput + ) { + try { + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput nativeInput = + ToNative.GetEncryptedDataKeyDescriptionInput(dafnyInput); + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput nativeOutput = + this._impl.GetEncryptedDataKeyDescription(nativeInput); + GetEncryptedDataKeyDescriptionOutput dafnyOutput = + ToDafny.GetEncryptedDataKeyDescriptionOutput(nativeOutput); + return Result.create_Success(dafnyOutput); + } catch (RuntimeException ex) { + return Result.create_Failure(ToDafny.Error(ex)); + } + } + public interface Builder { Builder impl(DynamoDbEncryption impl); diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/DynamoDbEncryptionShim.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/DynamoDbEncryptionShim.cs index e7c16dc46..cc97276fc 100644 --- a/TestVectors/runtimes/net/Generated/DDBEncryption/DynamoDbEncryptionShim.cs +++ b/TestVectors/runtimes/net/Generated/DDBEncryption/DynamoDbEncryptionShim.cs @@ -28,6 +28,21 @@ public DynamoDbEncryptionShim(AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDb return Wrappers_Compile.Result.create_Failure(this.ConvertError(ex)); } + } + public Wrappers_Compile._IResult GetEncryptedDataKeyDescription(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionInput request) + { + try + { + AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput unWrappedRequest = TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput(request); + AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput wrappedResponse = + this._impl.GetEncryptedDataKeyDescription(unWrappedRequest); + return Wrappers_Compile.Result.create_Success(TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput(wrappedResponse)); + } + catch (System.Exception ex) + { + return Wrappers_Compile.Result.create_Failure(this.ConvertError(ex)); + } + } private software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IError ConvertError(System.Exception error) { diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs index c4b5803f8..6a0902fa9 100644 --- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs +++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs @@ -142,6 +142,53 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_GetBranchKeyIdFromDdbKeyOutput__M11_branchKeyId(value.BranchKeyId)); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionInput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput(); converted.Input = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(concrete._input); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionInput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionInput value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(value.Input)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionOutput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput(); converted.EncryptedDataKeyDescriptionOutput = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(concrete._EncryptedDataKeyDescriptionOutput); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionOutput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionOutput value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(value.EncryptedDataKeyDescriptionOutput)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion)value; + var converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion(); if (value.is_header) + { + converted.Header = FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(concrete.dtor_header); + return converted; + } + if (value.is_item) + { + converted.Item = FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(concrete.dtor_item); + return converted; + } + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion state"); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion value) + { + value.Validate(); if (value.IsSetHeader()) + { + return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion.create_header(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(value.Header)); + } + if (value.IsSetItem()) + { + return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion.create_item(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(value.Item)); + } + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion state"); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S12_LegacyPolicy(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy value) { if (value.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT; @@ -339,6 +386,38 @@ public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncr { return ToDafny_N6_smithy__N3_api__S6_String(value); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IGetEncryptedDataKeyDescriptionUnion ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionInput__M5_input(AWS.Cryptography.DbEncryptionSDK.DynamoDb.GetEncryptedDataKeyDescriptionUnion value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion(value); + } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(Dafny.ISequence value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S36_GetEncryptedDataKeyDescriptionOutput__M33_EncryptedDataKeyDescriptionOutput(System.Collections.Generic.List value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(value); + } + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(Dafny.ISequence value) + { + return FromDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M6_header(System.IO.MemoryStream value) + { + return ToDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S35_GetEncryptedDataKeyDescriptionUnion__M4_item(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_VirtualTransform__M5_upper(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IUpper value) { return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_Upper(value); @@ -508,6 +587,37 @@ public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S6_String(string new Dafny.Pair, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue>(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M3_key(pair.Key), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M5_value(pair.Value)) )); } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(Dafny.ISequence value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member)); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList(System.Collections.Generic.List value) + { + return Dafny.Sequence.FromArray(value.Select(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member).ToArray()); + } + public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny.ISequence value) + { + return new System.IO.MemoryStream(value.Elements); + } + public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) + { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } + return Dafny.Sequence.FromArray(value.ToArray()); + + } + public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(pair.Car), pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(pair.Cdr)); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(System.Collections.Generic.Dictionary value) + { + return Dafny.Map, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue>.FromCollection(value.Select(pair => + new Dafny.Pair, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue>(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(pair.Key), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(pair.Value)) + )); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_Upper(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IUpper value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Upper concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Upper)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.Upper(); return converted; @@ -664,6 +774,30 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types { return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S31_EncryptedDataKeyDescriptionList__M6_member(AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M3_key(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static Amazon.DynamoDBv2.Model.AttributeValue FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } + public static software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap__M5_value(Amazon.DynamoDBv2.Model.AttributeValue value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S6_Insert__M7_literal(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); @@ -913,6 +1047,21 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types } throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state"); } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription(); converted.KeyProviderId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(concrete._keyProviderId); + if (concrete._keyProviderInfo.is_Some) converted.KeyProviderInfo = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(concrete._keyProviderInfo); + if (concrete._branchKeyId.is_Some) converted.BranchKeyId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(concrete._branchKeyId); + if (concrete._branchKeyVersion.is_Some) converted.BranchKeyVersion = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(concrete._branchKeyVersion); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IEncryptedDataKeyDescription ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription(AWS.Cryptography.DbEncryptionSDK.DynamoDb.EncryptedDataKeyDescription value) + { + value.Validate(); + string var_keyProviderInfo = value.IsSetKeyProviderInfo() ? value.KeyProviderInfo : (string)null; + string var_branchKeyId = value.IsSetBranchKeyId() ? value.BranchKeyId : (string)null; + string var_branchKeyVersion = value.IsSetBranchKeyVersion() ? value.BranchKeyVersion : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescription(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(value.KeyProviderId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(var_keyProviderInfo), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(var_branchKeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(var_branchKeyVersion)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S4_Char(Dafny.ISequence value) { return new string(value.Elements); @@ -1041,6 +1190,38 @@ public static bool ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue { return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_BooleanAttributeValue(value); } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(Dafny.ISequence value) + { + return FromDafny_N6_smithy__N3_api__S6_String(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M13_keyProviderId(string value) + { + return ToDafny_N6_smithy__N3_api__S6_String(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M15_keyProviderInfo(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M11_branchKeyId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S27_EncryptedDataKeyDescription__M16_branchKeyVersion(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static AWS.Cryptography.MaterialProviders.DefaultCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S12_DefaultCache(software.amazon.cryptography.materialproviders.internaldafny.types._IDefaultCache value) { software.amazon.cryptography.materialproviders.internaldafny.types.DefaultCache concrete = (software.amazon.cryptography.materialproviders.internaldafny.types.DefaultCache)value; AWS.Cryptography.MaterialProviders.DefaultCache converted = new AWS.Cryptography.MaterialProviders.DefaultCache(); converted.EntryCapacity = (int)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S12_DefaultCache__M13_entryCapacity(concrete._entryCapacity); return converted; diff --git a/specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md b/specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md new file mode 100644 index 000000000..d45395d79 --- /dev/null +++ b/specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md @@ -0,0 +1,39 @@ +[//]: # "Copyright Amazon.com Inc. or its affiliates. All Rights Reserved." +[//]: # "SPDX-License-Identifier: CC-BY-SA-4.0" + +# DynamoDb Get Encrypted Data Key Description + +## Overview + +Keyring's Encrypted Data Key serialization includes metadata like key provider id, key provider info, branch Key id (only Hierarchy Keyring), and the version of the branch Key (only Hierarchy Keyring). Encrypted Data Key Description operation provides a way for the customers to get these meta data. This operation will provide them with an insight of the keys the data is encrypted with. + +## Operation + +### Input + +This operation MUST take in either of the following: +- A binary [header](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md) +- A [encrypted DynamoDB item](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/ff9f08a355a20c81540e4ca652e09aaeffe90c4b/specification/dynamodb-encryption-client/encrypt-item.md#encrypted-dynamodb-item) + +### Output + +This operation MUST return the following: + +- [keyProviderId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-id) +- [keyProviderInfo](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for AWS Cryptographic Materials Provider Keyring) +- [branchKeyId](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring) +- [branchKeyVersion](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/structured-encryption/header.md#key-provider-information) (only for hierarchy keyring) + +### Behavior + +- The operation MUST NEVER DECRYPT the Data Keys. +- The operation MUST NOT access the network in any way. +- If the input is an encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get the binary header. +- This operation MUST deserialize the header bytes according to the header format. +- This operation MUST extract the Format Flavor from the deserialize header. Format Flavor is used to identify the algorithm suite. +- This operation MUST extract the dataKeys from the deserialize header. +- For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key. + - If the Data Key does not belong to AWS Cryptographic Materials Provider Keyring, the operation will only return keyProviderId. + - This description SHOULD be as detailed as possible, parsing but NOT decrypting the cipher-text field of the Data Key for embedded fields such as the Hierarchical Keyring’s branchKeyVersion. + +