From 9d825671401eba9655280367ea15f26f61ea8da8 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 11:06:51 -0700 Subject: [PATCH 01/28] m --- .../src/CreateWrappedItemEncryptor.dfy | 66 +++++++++++++++++++ .../dafny/DDBEncryption/src/JsonConfig.dfy | 7 +- 2 files changed, 71 insertions(+), 2 deletions(-) create mode 100644 TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy diff --git a/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy b/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy new file mode 100644 index 000000000..6cd10ae38 --- /dev/null +++ b/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy @@ -0,0 +1,66 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy" +include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy" + +module {:extern} CreateWrappedItemEncryptor { + import opened Wrappers + import AwsCryptographyDbEncryptionSdkDynamoDbTypes + import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes + import DynamoDbItemEncryptor + import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations + + // The `ensures` clause is copy-pasted from the DynamoDbItemEncryptor client method's `ensures` clause. + method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig) + returns (output: Result) + requires config.keyring.Some? ==> + config.keyring.value.ValidState() + requires config.cmm.Some? ==> + config.cmm.value.ValidState() + requires config.legacyOverride.Some? ==> + config.legacyOverride.value.encryptor.ValidState() + modifies if config.keyring.Some? then + config.keyring.value.Modifies + else {} + modifies if config.cmm.Some? then + config.cmm.value.Modifies + else {} + modifies if config.legacyOverride.Some? then + config.legacyOverride.value.encryptor.Modifies + else {} + ensures output.Success? ==> + && output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient + && fresh(output.value) + && fresh(output.value.History) + && output.value.ValidState() + && var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config; + && fresh(output.value.Modifies - Operations.ModifiesInternalConfig(rconfig)) + && rconfig.logicalTableName == config.logicalTableName + && rconfig.partitionKeyName == config.partitionKeyName + && rconfig.sortKeyName == config.sortKeyName + && rconfig.attributeActionsOnEncrypt == config.attributeActionsOnEncrypt + && rconfig.allowedUnsignedAttributes == config.allowedUnsignedAttributes + && rconfig.allowedUnsignedAttributePrefix == config.allowedUnsignedAttributePrefix + && rconfig.algorithmSuiteId == config.algorithmSuiteId + + //= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#attribute-actions + //= type=implication + //# The [Key Action](#key-action) + //# MUST be configured to the partition attribute and, if present, sort attribute. + && rconfig.version == Operations.VersionFromActions(config.attributeActionsOnEncrypt) + && config.partitionKeyName in config.attributeActionsOnEncrypt + && config.attributeActionsOnEncrypt[config.partitionKeyName] == Operations.KeyActionFromVersion(rconfig.version) + && (config.sortKeyName.Some? ==> + && config.sortKeyName.value in config.attributeActionsOnEncrypt + && config.attributeActionsOnEncrypt[config.sortKeyName.value] == Operations.KeyActionFromVersion(rconfig.version)) + + //= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#plaintext-policy + //# If not specified, encryption and decryption MUST behave according to `FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ`. + ensures + && output.Success? + && config.plaintextOverride.None? + ==> + && var config := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config; + && config.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ? +} diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 3ae66e1f4..397a11ef9 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -3,6 +3,7 @@ include "JsonItem.dfy" include "CreateInterceptedDDBClient.dfy" +include "CreateWrappedItemEncryptor.dfy" include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy" module {:options "-functionSyntax:4"} JsonConfig { @@ -31,6 +32,8 @@ module {:options "-functionSyntax:4"} JsonConfig { import ParseJsonManifests import CreateInterceptedDDBClient import DynamoDbItemEncryptor + import CreateWrappedItemEncryptor + import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations const abc : UTF8.ValidUTF8Bytes := @@ -261,7 +264,7 @@ module {:options "-functionSyntax:4"} JsonConfig { ensures encryptor.Success? ==> && encryptor.value.ValidState() && fresh(encryptor.value) - && fresh(encryptor.value.Modifies) + && fresh(encryptor.value.Modifies - Operations.ModifiesInternalConfig(encryptor.value.config)) { :- Need(data.Object?, "A Table Config must be an object."); var logicalTableName := TableName; @@ -352,7 +355,7 @@ module {:options "-functionSyntax:4"} JsonConfig { legacyOverride := legacyOverride, plaintextOverride := plaintextOverride ); - var enc : ENC.IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig); + var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig); assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; return Success(encr); From c5f5b31ebb71c87f14f9d39ed7a4b2ce37790638 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 11:24:36 -0700 Subject: [PATCH 02/28] m --- TestVectors/Makefile | 18 +- ...onSdkDynamoDbItemEncryptorTypesWrapped.dfy | 20 + .../src/Index.dfy | 2 + .../__default.java | 33 + .../wrapped/TestDynamoDbItemEncryptor.java | 110 ++ .../net/Extern/CreateWrappedItemEncryptor.cs | 25 + .../DynamoDbItemEncryptorShim.cs | 88 ++ .../TypeConversion.cs | 1058 +++++++++++++++++ .../rust/src/create_wrapped_item_encryptor.rs | 28 + 9 files changed, 1381 insertions(+), 1 deletion(-) create mode 100644 TestVectors/dafny/WrappedDynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy create mode 100644 TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy create mode 100644 TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java create mode 100644 TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/wrapped/TestDynamoDbItemEncryptor.java create mode 100644 TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs create mode 100644 TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/DynamoDbItemEncryptorShim.cs create mode 100644 TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs create mode 100644 TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 467c1947e..57a1e2f09 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -7,14 +7,17 @@ TRANSPILE_TESTS_IN_RUST=1 include ../SharedMakefile.mk PROJECT_SERVICES := \ - DDBEncryption + DDBEncryption \ + WrappedDynamoDbItemEncryptor MAIN_SERVICE_FOR_RUST := DDBEncryption SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/DynamoDbEncryption/dafny/DynamoDbEncryption/Model OUTPUT_LOCAL_SERVICE_DDBEncryption := --local-service-test +OUTPUT_LOCAL_SERVICE_WrappedDynamoDbItemEncryptor := --local-service-test SERVICE_NAMESPACE_DDBEncryption=aws.cryptography.dbEncryptionSdk.dynamoDb +SERVICE_NAMESPACE_WrappedDynamoDbItemEncryptor=aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor MAX_RESOURCE_COUNT=10000000 # Order is important @@ -66,6 +69,8 @@ PROJECT_INDEX := \ DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \ DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \ DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \ + DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \ + DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \ STD_LIBRARY=submodules/MaterialProviders/StandardLibrary SMITHY_DEPS=submodules/MaterialProviders/model @@ -85,6 +90,17 @@ SERVICE_DEPS_DDBEncryption := \ DynamoDbEncryption/dafny/StructuredEncryption \ submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \ +SERVICE_DEPS_WrappedDynamoDbItemEncryptor := \ + submodules/MaterialProviders/AwsCryptographyPrimitives \ + submodules/MaterialProviders/ComAmazonawsKms \ + submodules/MaterialProviders/ComAmazonawsDynamodb \ + submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \ + submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \ + DynamoDbEncryption/dafny/StructuredEncryption \ + DynamoDbEncryption/dafny/DynamoDbEncryption \ + DynamoDbEncryption/dafny/DynamoDbItemEncryptor \ + submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \ + transpile_implementation_rust: _remove_wrapped_client_rust _remove_wrapped_client_rust: diff --git a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy new file mode 100644 index 000000000..14b525406 --- /dev/null +++ b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy @@ -0,0 +1,20 @@ +// 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. +include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" +include "../src/Index.dfy" +abstract module WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes + import WrappedService : AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService + function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig + method {:extern} WrappedDynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := WrappedDefaultDynamoDbItemEncryptorConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && fresh(res.value.History) + && res.value.ValidState() +} diff --git a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy new file mode 100644 index 000000000..7e2689287 --- /dev/null +++ b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy @@ -0,0 +1,2 @@ +// Empty stub expected by Smithy-Dafny +module WrappedItemEncryptor {} \ No newline at end of file diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java new file mode 100644 index 000000000..20552e29e --- /dev/null +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -0,0 +1,33 @@ +package CreateWrappedItemEncryptor_Compile; + +import Wrappers_Compile.Result; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToNative; +import software.amazon.cryptography.services.dynamodb.internaldafny.types.IItemEncryptor; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error; +import software.amazon.cryptography.services.dynamodb.internaldafny.Shim; + +public class __default { + + public static Result CreateWrappedItemEncryptor( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbItemEncryptorConfig config + ) { + try { + final DynamoDbItemEncryptorConfig nativeConfig = + ToNative.DynamoDbItemEncryptorConfig(config); + + final DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor + .builder() + .DynamoDbItemEncryptorConfig(nativeConfig) + .build(); + + final Shim wrappedEncryptor = new Shim(itemEncryptor); + + return Result.create_Success(wrappedEncryptor); + } catch (Exception e) { + return Result.create_Failure(ToDafny.Error((RuntimeException) e)); + } + } +} diff --git a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/wrapped/TestDynamoDbItemEncryptor.java b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/wrapped/TestDynamoDbItemEncryptor.java new file mode 100644 index 000000000..2a9a267b7 --- /dev/null +++ b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/wrapped/TestDynamoDbItemEncryptor.java @@ -0,0 +1,110 @@ +// 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.itemencryptor.wrapped; + +import Wrappers_Compile.Result; +import java.lang.IllegalArgumentException; +import java.lang.RuntimeException; +import java.util.Objects; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemOutput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemInput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemOutput; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient; + +public class TestDynamoDbItemEncryptor implements IDynamoDbItemEncryptorClient { + + private final DynamoDbItemEncryptor _impl; + + protected TestDynamoDbItemEncryptor(BuilderImpl builder) { + this._impl = builder.impl(); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public Result DecryptItem( + DecryptItemInput dafnyInput + ) { + try { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DecryptItemInput nativeInput = + ToNative.DecryptItemInput(dafnyInput); + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DecryptItemOutput nativeOutput = + this._impl.DecryptItem(nativeInput); + DecryptItemOutput dafnyOutput = ToDafny.DecryptItemOutput(nativeOutput); + return Result.create_Success( + DecryptItemOutput._typeDescriptor(), + Error._typeDescriptor(), + dafnyOutput + ); + } catch (RuntimeException ex) { + return Result.create_Failure( + DecryptItemOutput._typeDescriptor(), + Error._typeDescriptor(), + ToDafny.Error(ex) + ); + } + } + + public Result EncryptItem( + EncryptItemInput dafnyInput + ) { + try { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.EncryptItemInput nativeInput = + ToNative.EncryptItemInput(dafnyInput); + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.EncryptItemOutput nativeOutput = + this._impl.EncryptItem(nativeInput); + EncryptItemOutput dafnyOutput = ToDafny.EncryptItemOutput(nativeOutput); + return Result.create_Success( + EncryptItemOutput._typeDescriptor(), + Error._typeDescriptor(), + dafnyOutput + ); + } catch (RuntimeException ex) { + return Result.create_Failure( + EncryptItemOutput._typeDescriptor(), + Error._typeDescriptor(), + ToDafny.Error(ex) + ); + } + } + + public interface Builder { + Builder impl(DynamoDbItemEncryptor impl); + + DynamoDbItemEncryptor impl(); + + TestDynamoDbItemEncryptor build(); + } + + static class BuilderImpl implements Builder { + + protected DynamoDbItemEncryptor impl; + + protected BuilderImpl() {} + + public Builder impl(DynamoDbItemEncryptor impl) { + this.impl = impl; + return this; + } + + public DynamoDbItemEncryptor impl() { + return this.impl; + } + + public TestDynamoDbItemEncryptor build() { + if (Objects.isNull(this.impl())) { + throw new IllegalArgumentException( + "Missing value for required field `impl`" + ); + } + return new TestDynamoDbItemEncryptor(this); + } + } +} diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs new file mode 100644 index 000000000..4c86fa5bd --- /dev/null +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -0,0 +1,25 @@ +using Amazon.Cryptography.DatabaseEncryptionSDK.DynamoDb.ItemEncryptor; +using Amazon.Cryptography.DatabaseEncryptionSDK.Dynamodb; +using Amazon.Cryptography.Services.Dynamodb.Internaldafny; +using Amazon.Cryptography.Services.Dynamodb.Internaldafny.Types; +using Wrappers_Compile; +using _IError = software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IError; + +namespace CreateWrappedItemEncryptor_Compile +{ + public partial class __default + { + public static _IResult CreateWrappedItemEncryptor( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbItemEncryptorConfig config) + { + var nativeConfig = AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms.TypeConversion + .FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbItemEncryptorConfig( + config); + + var itemEncryptor = DynamoDbItemEncryptor.Create(nativeConfig); + var wrappedEncryptor = new Com.Amazonaws.Dynamodb.ItemEncryptorShim(itemEncryptor); + + return new Result_Success(wrappedEncryptor); + } + } +} diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/DynamoDbItemEncryptorShim.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/DynamoDbItemEncryptorShim.cs new file mode 100644 index 000000000..986ee781d --- /dev/null +++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/DynamoDbItemEncryptorShim.cs @@ -0,0 +1,88 @@ +// 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 System.Collections.Generic; +using System.IO; +using System.Linq; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped +{ + public class DynamoDbItemEncryptorShim : software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient + { + public AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptor _impl; + public DynamoDbItemEncryptorShim(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptor impl) + { + this._impl = impl; + } + public Wrappers_Compile._IResult EncryptItem(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemInput request) + { + try + { + AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemInput unWrappedRequest = TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput(request); + AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemOutput wrappedResponse = + this._impl.EncryptItem(unWrappedRequest); + return Wrappers_Compile.Result.create_Success(TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput(wrappedResponse)); + } + catch (System.Exception ex) + { + return Wrappers_Compile.Result.create_Failure(this.ConvertError(ex)); + } + + } + public Wrappers_Compile._IResult DecryptItem(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput request) + { + try + { + AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput unWrappedRequest = TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(request); + AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemOutput wrappedResponse = + this._impl.DecryptItem(unWrappedRequest); + return Wrappers_Compile.Result.create_Success(TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput(wrappedResponse)); + } + catch (System.Exception ex) + { + return Wrappers_Compile.Result.create_Failure(this.ConvertError(ex)); + } + + } + private software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError ConvertError(System.Exception error) + { + switch (error.GetType().Namespace) + { + case "AWS.Cryptography.DbEncryptionSDK.StructuredEncryption": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyDbEncryptionSdkStructuredEncryption( + AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.TypeConversion.ToDafny_CommonError(error) + ); + case "AWS.Cryptography.DbEncryptionSDK.DynamoDb": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyDbEncryptionSdkDynamoDb( + AWS.Cryptography.DbEncryptionSDK.DynamoDb.TypeConversion.ToDafny_CommonError(error) + ); + case "AWS.Cryptography.MaterialProviders": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyMaterialProviders( + AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_CommonError(error) + ); + case "Com.Amazonaws.Dynamodb": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_ComAmazonawsDynamodb( + Com.Amazonaws.Dynamodb.TypeConversion.ToDafny_CommonError(error) + ); + } + switch (error) + { + case AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorException e: + return TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException(e); + + case CollectionOfErrors collectionOfErrors: + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_CollectionOfErrors( + Dafny.Sequence + .FromArray( + collectionOfErrors.list.Select + (x => TypeConversion.ToDafny_CommonError(x)) + .ToArray()), + Dafny.Sequence.FromString(collectionOfErrors.Message) + ); + default: + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_Opaque(error); + + } + } + } +} diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs new file mode 100644 index 000000000..c7866d272 --- /dev/null +++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs @@ -0,0 +1,1058 @@ +// 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.Linq; +using System; +namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped +{ + public static class TypeConversion + { + private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z"; + + private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z"; + + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput(); converted.EncryptedItem = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(concrete._encryptedItem); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(value.EncryptedItem)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemOutput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemOutput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemOutput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemOutput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemOutput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemOutput(); converted.PlaintextItem = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M13_plaintextItem(concrete._plaintextItem); + if (concrete._parsedHeader.is_Some) converted.ParsedHeader = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M12_parsedHeader(concrete._parsedHeader); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemOutput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemOutput value) + { + value.Validate(); + AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader var_parsedHeader = value.IsSetParsedHeader() ? value.ParsedHeader : (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemOutput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M13_plaintextItem(value.PlaintextItem), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M12_parsedHeader(var_parsedHeader)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorConfig FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDynamoDbItemEncryptorConfig value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorConfig converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorConfig(); converted.LogicalTableName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_logicalTableName(concrete._logicalTableName); + converted.PartitionKeyName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_partitionKeyName(concrete._partitionKeyName); + if (concrete._sortKeyName.is_Some) converted.SortKeyName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M11_sortKeyName(concrete._sortKeyName); + converted.AttributeActionsOnEncrypt = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_attributeActionsOnEncrypt(concrete._attributeActionsOnEncrypt); + if (concrete._allowedUnsignedAttributes.is_Some) converted.AllowedUnsignedAttributes = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_allowedUnsignedAttributes(concrete._allowedUnsignedAttributes); + if (concrete._allowedUnsignedAttributePrefix.is_Some) converted.AllowedUnsignedAttributePrefix = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M30_allowedUnsignedAttributePrefix(concrete._allowedUnsignedAttributePrefix); + if (concrete._algorithmSuiteId.is_Some) converted.AlgorithmSuiteId = (AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_algorithmSuiteId(concrete._algorithmSuiteId); + if (concrete._keyring.is_Some) converted.Keyring = (AWS.Cryptography.MaterialProviders.IKeyring)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M7_keyring(concrete._keyring); + if (concrete._cmm.is_Some) converted.Cmm = (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M3_cmm(concrete._cmm); + if (concrete._legacyOverride.is_Some) converted.LegacyOverride = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M14_legacyOverride(concrete._legacyOverride); + if (concrete._plaintextOverride.is_Some) converted.PlaintextOverride = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M17_plaintextOverride(concrete._plaintextOverride); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDynamoDbItemEncryptorConfig ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorConfig value) + { + value.Validate(); + string var_sortKeyName = value.IsSetSortKeyName() ? value.SortKeyName : (string)null; + System.Collections.Generic.List var_allowedUnsignedAttributes = value.IsSetAllowedUnsignedAttributes() ? value.AllowedUnsignedAttributes : (System.Collections.Generic.List)null; + string var_allowedUnsignedAttributePrefix = value.IsSetAllowedUnsignedAttributePrefix() ? value.AllowedUnsignedAttributePrefix : (string)null; + AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId var_algorithmSuiteId = value.IsSetAlgorithmSuiteId() ? value.AlgorithmSuiteId : (AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId)null; + AWS.Cryptography.MaterialProviders.IKeyring var_keyring = value.IsSetKeyring() ? value.Keyring : (AWS.Cryptography.MaterialProviders.IKeyring)null; + AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager var_cmm = value.IsSetCmm() ? value.Cmm : (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null; + AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride var_legacyOverride = value.IsSetLegacyOverride() ? value.LegacyOverride : (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride)null; + AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride var_plaintextOverride = value.IsSetPlaintextOverride() ? value.PlaintextOverride : (AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_logicalTableName(value.LogicalTableName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_partitionKeyName(value.PartitionKeyName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M11_sortKeyName(var_sortKeyName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_attributeActionsOnEncrypt(value.AttributeActionsOnEncrypt), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_allowedUnsignedAttributes(var_allowedUnsignedAttributes), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M30_allowedUnsignedAttributePrefix(var_allowedUnsignedAttributePrefix), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_algorithmSuiteId(var_algorithmSuiteId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M7_keyring(var_keyring), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M3_cmm(var_cmm), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M14_legacyOverride(var_legacyOverride), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M17_plaintextOverride(var_plaintextOverride)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorException FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_DynamoDbItemEncryptorException value) + { + return new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorException( + FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException__M7_message(value._message) + ); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_DynamoDbItemEncryptorException ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorException value) + { + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_DynamoDbItemEncryptorException( + ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException__M7_message(value.Message) + ); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemInput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemInput(); converted.PlaintextItem = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput__M13_plaintextItem(concrete._plaintextItem); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemInput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemInput value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemInput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput__M13_plaintextItem(value.PlaintextItem)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemOutput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemOutput value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemOutput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemOutput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemOutput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemOutput(); converted.EncryptedItem = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M13_encryptedItem(concrete._encryptedItem); + if (concrete._parsedHeader.is_Some) converted.ParsedHeader = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M12_parsedHeader(concrete._parsedHeader); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemOutput ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemOutput value) + { + value.Validate(); + AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader var_parsedHeader = value.IsSetParsedHeader() ? value.ParsedHeader : (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemOutput(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M13_encryptedItem(value.EncryptedItem), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M12_parsedHeader(var_parsedHeader)); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(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__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M13_plaintextItem(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__N13_itemEncryptor__S17_DecryptItemOutput__M13_plaintextItem(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M12_parsedHeader(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)null : FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput__M12_parsedHeader(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader((AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_logicalTableName(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__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_logicalTableName(string value) + { + return ToDafny_N6_smithy__N3_api__S6_String(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_partitionKeyName(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_KeySchemaAttributeName(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_partitionKeyName(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_KeySchemaAttributeName(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M11_sortKeyName(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_KeySchemaAttributeName(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M11_sortKeyName(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_KeySchemaAttributeName((string)value)); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_attributeActionsOnEncrypt(Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(value); + } + public static Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_attributeActionsOnEncrypt(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(value); + } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_allowedUnsignedAttributes(Wrappers_Compile._IOption>> value) + { + return value.is_None ? (System.Collections.Generic.List)null : FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList(value.Extract()); + } + public static Wrappers_Compile._IOption>> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M25_allowedUnsignedAttributes(System.Collections.Generic.List value) + { + return value == null ? Wrappers_Compile.Option>>.create_None() : Wrappers_Compile.Option>>.create_Some(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList((System.Collections.Generic.List)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M30_allowedUnsignedAttributePrefix(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__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M30_allowedUnsignedAttributePrefix(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.DBEAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_algorithmSuiteId(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S19_DBEAlgorithmSuiteId(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M16_algorithmSuiteId(AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S19_DBEAlgorithmSuiteId((AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId)value)); + } + public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M7_keyring(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.MaterialProviders.IKeyring)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M7_keyring(AWS.Cryptography.MaterialProviders.IKeyring value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference((AWS.Cryptography.MaterialProviders.IKeyring)value)); + } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M3_cmm(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M3_cmm(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference((AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)value)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M14_legacyOverride(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride)null : FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M14_legacyOverride(AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride((AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride)value)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M17_plaintextOverride(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride)null : FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_PlaintextOverride(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig__M17_plaintextOverride(AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_PlaintextOverride((AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException__M7_message(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__N13_itemEncryptor__S30_DynamoDbItemEncryptorException__M7_message(string value) + { + return ToDafny_N6_smithy__N3_api__S6_String(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput__M13_plaintextItem(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__N13_itemEncryptor__S16_EncryptItemInput__M13_plaintextItem(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M13_encryptedItem(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__N13_itemEncryptor__S17_EncryptItemOutput__M13_encryptedItem(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_AttributeMap(value); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M12_parsedHeader(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)null : FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput__M12_parsedHeader(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader((AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader)value)); + } + 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.ItemEncryptor.ParsedHeader FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IParsedHeader value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.ParsedHeader concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.ParsedHeader)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader(); converted.AttributeActionsOnEncrypt = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M25_attributeActionsOnEncrypt(concrete._attributeActionsOnEncrypt); + converted.AlgorithmSuiteId = (AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M16_algorithmSuiteId(concrete._algorithmSuiteId); + converted.EncryptedDataKeys = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptedDataKeys(concrete._encryptedDataKeys); + converted.StoredEncryptionContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M23_storedEncryptionContext(concrete._storedEncryptionContext); + converted.EncryptionContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptionContext(concrete._encryptionContext); + converted.SelectorContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M15_selectorContext(concrete._selectorContext); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IParsedHeader ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.ParsedHeader value) + { + value.Validate(); + + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.ParsedHeader(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M25_attributeActionsOnEncrypt(value.AttributeActionsOnEncrypt), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M16_algorithmSuiteId(value.AlgorithmSuiteId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptedDataKeys(value.EncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M23_storedEncryptionContext(value.StoredEncryptionContext), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M15_selectorContext(value.SelectorContext)); + } + public static string FromDafny_N6_smithy__N3_api__S6_String(Dafny.ISequence value) + { + return new string(value.Elements); + } + public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S6_String(string value) + { + return Dafny.Sequence.FromString(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_KeySchemaAttributeName(Dafny.ISequence value) + { + return new string(value.Elements); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_KeySchemaAttributeName(string value) + { + return Dafny.Sequence.FromString(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value) + { + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr)); + } + public static Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(System.Collections.Generic.Dictionary value) + { + return Dafny.Map, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction>.FromCollection(value.Select(pair => + new Dafny.Pair, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction>(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Key), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Value)) + )); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList(Dafny.ISequence> value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList__M6_member)); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList(System.Collections.Generic.List value) + { + return Dafny.Sequence>.FromArray(value.Select(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList__M6_member).ToArray()); + } + public static AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S19_DBEAlgorithmSuiteId(software.amazon.cryptography.materialproviders.internaldafny.types._IDBEAlgorithmSuiteId value) + { + if (value.is_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__SYMSIG__HMAC__SHA384) return AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384; + if (value.is_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__ECDSA__P384__SYMSIG__HMAC__SHA384) return AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384; + throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId value"); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types._IDBEAlgorithmSuiteId ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S19_DBEAlgorithmSuiteId(AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId value) + { + if (AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.DBEAlgorithmSuiteId.create_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__SYMSIG__HMAC__SHA384(); + if (AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.DBEAlgorithmSuiteId.create_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__ECDSA__P384__SYMSIG__HMAC__SHA384(); + throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId value"); + } + public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(AWS.Cryptography.MaterialProviders.IKeyring value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value); + } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyOverride value) + { + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyOverride concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyOverride)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride(); converted.Policy = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M6_policy(concrete._policy); + converted.Encryptor = (AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M9_encryptor(concrete._encryptor); + converted.AttributeActionsOnEncrypt = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M25_attributeActionsOnEncrypt(concrete._attributeActionsOnEncrypt); + if (concrete._defaultAttributeFlag.is_Some) converted.DefaultAttributeFlag = (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M20_defaultAttributeFlag(concrete._defaultAttributeFlag); return converted; + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyOverride ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride(AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyOverride value) + { + value.Validate(); + AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction var_defaultAttributeFlag = value.IsSetDefaultAttributeFlag() ? value.DefaultAttributeFlag : (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyOverride(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M6_policy(value.Policy), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M9_encryptor(value.Encryptor), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M25_attributeActionsOnEncrypt(value.AttributeActionsOnEncrypt), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M20_defaultAttributeFlag(var_defaultAttributeFlag)); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_PlaintextOverride(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPlaintextOverride value) + { + if (value.is_FORCE__PLAINTEXT__WRITE__ALLOW__PLAINTEXT__READ) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ; + if (value.is_FORBID__PLAINTEXT__WRITE__ALLOW__PLAINTEXT__READ) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ; + if (value.is_FORBID__PLAINTEXT__WRITE__FORBID__PLAINTEXT__READ) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ; + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride value"); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPlaintextOverride ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_PlaintextOverride(AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride value) + { + if (AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PlaintextOverride.create_FORCE__PLAINTEXT__WRITE__ALLOW__PLAINTEXT__READ(); + if (AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PlaintextOverride.create_FORBID__PLAINTEXT__WRITE__ALLOW__PLAINTEXT__READ(); + if (AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PlaintextOverride.create_FORBID__PLAINTEXT__WRITE__FORBID__PLAINTEXT__READ(); + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.PlaintextOverride 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 System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M25_attributeActionsOnEncrypt(Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(value); + } + public static Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M25_attributeActionsOnEncrypt(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(value); + } + public static AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M16_algorithmSuiteId(software.amazon.cryptography.materialproviders.internaldafny.types._IDBEAlgorithmSuiteId value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S19_DBEAlgorithmSuiteId(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types._IDBEAlgorithmSuiteId ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M16_algorithmSuiteId(AWS.Cryptography.MaterialProviders.DBEAlgorithmSuiteId value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S19_DBEAlgorithmSuiteId(value); + } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptedDataKeys(Dafny.ISequence value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptedDataKeys(System.Collections.Generic.List value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M23_storedEncryptionContext(Dafny.IMap, Dafny.ISequence> value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); + } + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M23_storedEncryptionContext(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptionContext(Dafny.IMap, Dafny.ISequence> value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); + } + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M17_encryptionContext(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M15_selectorContext(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key(value); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S12_ParsedHeader__M15_selectorContext(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S12_CryptoAction(value); + } + public static software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S12_CryptoAction(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_AttributeNameList__M6_member(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__S17_AttributeNameList__M6_member(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(value); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M6_policy(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S12_LegacyPolicy(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M6_policy(AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S12_LegacyPolicy(value); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M9_encryptor(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M9_encryptor(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M25_attributeActionsOnEncrypt(Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value) + { + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(value); + } + public static Dafny.IMap, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M25_attributeActionsOnEncrypt(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(value); + } + public static AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M20_defaultAttributeFlag(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction)null : FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S12_CryptoAction(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_LegacyOverride__M20_defaultAttributeFlag(AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S12_CryptoAction((AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction)value)); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(Dafny.ISequence value) + { + return new string(value.Elements); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(string value) + { + return Dafny.Sequence.FromString(value); + } + public static Amazon.DynamoDBv2.Model.AttributeValue FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue value) + { + software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue concrete = (software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue)value; + var converted = new Amazon.DynamoDBv2.Model.AttributeValue(); if (value.is_S) + { + converted.S = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(concrete.dtor_S); + return converted; + } + if (value.is_N) + { + converted.N = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_N(concrete.dtor_N); + return converted; + } + if (value.is_B) + { + converted.B = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(concrete.dtor_B); + return converted; + } + if (value.is_SS) + { + converted.SS = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(concrete.dtor_SS); + return converted; + } + if (value.is_NS) + { + converted.NS = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(concrete.dtor_NS); + return converted; + } + if (value.is_BS) + { + converted.BS = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(concrete.dtor_BS); + return converted; + } + if (value.is_M) + { + converted.M = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(concrete.dtor_M); + return converted; + } + if (value.is_L) + { + converted.L = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(concrete.dtor_L); + return converted; + } + if (value.is_NULL) + { + converted.NULL = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(concrete.dtor_NULL); + return converted; + } + if (value.is_BOOL) + { + converted.BOOL = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(concrete.dtor_BOOL); + return converted; + } + throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state"); + } + public static software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(Amazon.DynamoDBv2.Model.AttributeValue value) + { + if (value.S != null) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_S(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(value.S)); + } + if (value.N != null) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_N(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_N(value.N)); + } + if (value.B != null) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B)); + } + if (value.SS.Any()) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS)); + } + if (value.NS.Any()) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS)); + } + if (value.BS.Any()) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS)); + } + if (value.IsMSet) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M)); + } + if (value.IsLSet) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L)); + } + if (value.NULL == true) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL)); + } + if (value.IsBOOLSet) + { + return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL)); + } + throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state"); + } + public static System.Collections.Generic.List FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList(Dafny.ISequence value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList__M6_member)); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList(System.Collections.Generic.List value) + { + return Dafny.Sequence.FromArray(value.Select(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList__M6_member).ToArray()); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(Dafny.IMap, Dafny.ISequence> value) + { + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(pair.Cdr)); + } + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(System.Collections.Generic.Dictionary value) + { + return Dafny.Map, Dafny.ISequence>.FromCollection(value.Select(pair => + new Dafny.Pair, Dafny.ISequence>(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(pair.Key), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(pair.Value)) + )); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M3_key(pair.Car), pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M5_value(pair.Cdr)); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key(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__S3_Key__M3_key(pair.Key), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__M5_value(pair.Value)) + )); + } + public static AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S12_CryptoAction(software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction value) + { + if (value.is_ENCRYPT__AND__SIGN) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.ENCRYPT_AND_SIGN; + if (value.is_SIGN__AND__INCLUDE__IN__ENCRYPTION__CONTEXT) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT; + if (value.is_SIGN__ONLY) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.SIGN_ONLY; + if (value.is_DO__NOTHING) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.DO_NOTHING; + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction value"); + } + public static software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S12_CryptoAction(AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction value) + { + if (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.ENCRYPT_AND_SIGN.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction.create_ENCRYPT__AND__SIGN(); + if (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction.create_SIGN__AND__INCLUDE__IN__ENCRYPTION__CONTEXT(); + if (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.SIGN_ONLY.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction.create_SIGN__ONLY(); + if (AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction.DO_NOTHING.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction.create_DO__NOTHING(); + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction value"); + } + 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; + if (value.is_FORBID__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORBID_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT; + if (value.is_FORBID__LEGACY__ENCRYPT__FORBID__LEGACY__DECRYPT) return AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORBID_LEGACY_ENCRYPT_FORBID_LEGACY_DECRYPT; + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy value"); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S12_LegacyPolicy(AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy value) + { + if (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy.create_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT(); + if (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORBID_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy.create_FORBID__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT(); + if (AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy.FORBID_LEGACY_ENCRYPT_FORBID_LEGACY_DECRYPT.Equals(value)) return software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy.create_FORBID__LEGACY__ENCRYPT__FORBID__LEGACY__DECRYPT(); + throw new System.ArgumentException("Invalid AWS.Cryptography.DbEncryptionSDK.DynamoDb.LegacyPolicy value"); + } + public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.DbEncryptionSDK.DynamoDb.TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(value); + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.DbEncryptionSDK.DynamoDb.TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_N(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_NumberAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_N(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_NumberAttributeValue(value); + } + public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(System.IO.MemoryStream value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(value); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(Dafny.ISequence> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue(value); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(System.Collections.Generic.List value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue(value); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(Dafny.ISequence> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue(value); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(System.Collections.Generic.List value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue(value); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(Dafny.ISequence> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue(value); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(System.Collections.Generic.List value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue(value); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue(value); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(System.Collections.Generic.Dictionary value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue(value); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(System.Collections.Generic.List value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue(value); + } + public static bool FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(bool value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_NullAttributeValue(value); + } + public static bool ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(bool value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_NullAttributeValue(value); + } + public static bool FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(bool value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_BooleanAttributeValue(value); + } + public static bool ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(bool value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_BooleanAttributeValue(value); + } + public static AWS.Cryptography.MaterialProviders.EncryptedDataKey FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList__M6_member(software.amazon.cryptography.materialproviders.internaldafny.types._IEncryptedDataKey value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types._IEncryptedDataKey ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_EncryptedDataKeyList__M6_member(AWS.Cryptography.MaterialProviders.EncryptedDataKey value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(Dafny.ISequence value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(string value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(Dafny.ISequence value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(string value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S3_Key__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__S3_Key__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__S3_Key__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__S3_Key__M5_value(Amazon.DynamoDBv2.Model.AttributeValue value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(Dafny.ISequence value) + { + return new string(value.Elements); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(string value) + { + return Dafny.Sequence.FromString(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_NumberAttributeValue(Dafny.ISequence value) + { + return new string(value.Elements); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_NumberAttributeValue(string value) + { + return Dafny.Sequence.FromString(value); + } + public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(Dafny.ISequence value) + { + return new System.IO.MemoryStream(value.Elements); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(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.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue(Dafny.ISequence> value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue__M6_member)); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue(System.Collections.Generic.List value) + { + return Dafny.Sequence>.FromArray(value.Select(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue__M6_member).ToArray()); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue(Dafny.ISequence> value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue__M6_member)); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue(System.Collections.Generic.List value) + { + return Dafny.Sequence>.FromArray(value.Select(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue__M6_member).ToArray()); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue(Dafny.ISequence> value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue__M6_member)); + } + public static Dafny.ISequence> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue(System.Collections.Generic.List value) + { + return Dafny.Sequence>.FromArray(value.Select(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue__M6_member).ToArray()); + } + public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) + { + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue__M3_key(pair.Car), pair => FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue__M5_value(pair.Cdr)); + } + public static Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue(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__S17_MapAttributeValue__M3_key(pair.Key), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue__M5_value(pair.Value)) + )); + } + public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue(Dafny.ISequence value) + { + return new System.Collections.Generic.List(value.Elements.Select(FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue__M6_member)); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue(System.Collections.Generic.List value) + { + return Dafny.Sequence.FromArray(value.Select(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue__M6_member).ToArray()); + } + public static bool FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_NullAttributeValue(bool value) + { + return value; + } + public static bool ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_NullAttributeValue(bool value) + { + return value; + } + public static bool FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_BooleanAttributeValue(bool value) + { + return value; + } + public static bool ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_BooleanAttributeValue(bool value) + { + return value; + } + public static AWS.Cryptography.MaterialProviders.EncryptedDataKey FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey(software.amazon.cryptography.materialproviders.internaldafny.types._IEncryptedDataKey value) + { + software.amazon.cryptography.materialproviders.internaldafny.types.EncryptedDataKey concrete = (software.amazon.cryptography.materialproviders.internaldafny.types.EncryptedDataKey)value; AWS.Cryptography.MaterialProviders.EncryptedDataKey converted = new AWS.Cryptography.MaterialProviders.EncryptedDataKey(); converted.KeyProviderId = (string)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M13_keyProviderId(concrete._keyProviderId); + converted.KeyProviderInfo = (System.IO.MemoryStream)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M15_keyProviderInfo(concrete._keyProviderInfo); + converted.Ciphertext = (System.IO.MemoryStream)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M10_ciphertext(concrete._ciphertext); return converted; + } + public static software.amazon.cryptography.materialproviders.internaldafny.types._IEncryptedDataKey ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey(AWS.Cryptography.MaterialProviders.EncryptedDataKey value) + { + value.Validate(); + + return new software.amazon.cryptography.materialproviders.internaldafny.types.EncryptedDataKey(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M13_keyProviderId(value.KeyProviderId), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M15_keyProviderInfo(value.KeyProviderInfo), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M10_ciphertext(value.Ciphertext)); + } + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(Dafny.ISequence value) + { + System.Text.UTF8Encoding utf8 = new System.Text.UTF8Encoding(false, true); + return utf8.GetString(value.Elements); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(string value) + { + System.Text.UTF8Encoding utf8 = new System.Text.UTF8Encoding(false, true); + return Dafny.Sequence.FromArray(utf8.GetBytes(value)); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue__M6_member(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue__M6_member(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue__M6_member(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_NumberAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NumberSetAttributeValue__M6_member(string value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_NumberAttributeValue(value); + } + public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue__M6_member(Dafny.ISequence value) + { + return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(value); + } + public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_BinarySetAttributeValue__M6_member(System.IO.MemoryStream value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(value); + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S17_MapAttributeValue__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__S17_MapAttributeValue__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__S17_MapAttributeValue__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__S17_MapAttributeValue__M5_value(Amazon.DynamoDBv2.Model.AttributeValue value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } + public static Amazon.DynamoDBv2.Model.AttributeValue FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_ListAttributeValue__M6_member(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__S18_ListAttributeValue__M6_member(Amazon.DynamoDBv2.Model.AttributeValue value) + { + return ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue(value); + } + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M13_keyProviderId(Dafny.ISequence value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M13_keyProviderId(string value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); + } + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M15_keyProviderInfo(Dafny.ISequence value) + { + return FromDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M15_keyProviderInfo(System.IO.MemoryStream value) + { + return ToDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M10_ciphertext(Dafny.ISequence value) + { + return FromDafny_N6_smithy__N3_api__S4_Blob(value); + } + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_EncryptedDataKey__M10_ciphertext(System.IO.MemoryStream value) + { + return ToDafny_N6_smithy__N3_api__S4_Blob(value); + } + 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.Exception FromDafny_CommonError(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError value) + { + switch (value) + { + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_AwsCryptographyDbEncryptionSdkDynamoDb dafnyVal: + return AWS.Cryptography.DbEncryptionSDK.DynamoDb.TypeConversion.FromDafny_CommonError( + dafnyVal._AwsCryptographyDbEncryptionSdkDynamoDb + ); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_AwsCryptographyDbEncryptionSdkStructuredEncryption dafnyVal: + return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.TypeConversion.FromDafny_CommonError( + dafnyVal._AwsCryptographyDbEncryptionSdkStructuredEncryption + ); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_AwsCryptographyMaterialProviders dafnyVal: + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_CommonError( + dafnyVal._AwsCryptographyMaterialProviders + ); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_AwsCryptographyPrimitives dafnyVal: + return AWS.Cryptography.Primitives.TypeConversion.FromDafny_CommonError( + dafnyVal._AwsCryptographyPrimitives + ); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_ComAmazonawsDynamodb dafnyVal: + return Com.Amazonaws.Dynamodb.TypeConversion.FromDafny_CommonError( + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_DynamoDbItemEncryptorException dafnyVal: + return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException(dafnyVal); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_CollectionOfErrors dafnyVal: + return new CollectionOfErrors( + new System.Collections.Generic.List(dafnyVal.dtor_list.CloneAsArray() + .Select(x => TypeConversion.FromDafny_CommonError(x))), + new string(dafnyVal.dtor_message.Elements)); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_Opaque dafnyVal: + return new OpaqueError(dafnyVal._obj); + case software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_OpaqueWithText dafnyVal: + return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString()); + default: + // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) + return new OpaqueError(); + } + } + public static software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError ToDafny_CommonError(System.Exception value) + { + switch (value.GetType().Namespace) + { + case "AWS.Cryptography.DbEncryptionSDK.StructuredEncryption": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyDbEncryptionSdkStructuredEncryption( + AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.TypeConversion.ToDafny_CommonError(value) + ); + case "AWS.Cryptography.DbEncryptionSDK.DynamoDb": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyDbEncryptionSdkDynamoDb( + AWS.Cryptography.DbEncryptionSDK.DynamoDb.TypeConversion.ToDafny_CommonError(value) + ); + case "AWS.Cryptography.MaterialProviders": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyMaterialProviders( + AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_CommonError(value) + ); + case "Com.Amazonaws.Dynamodb": + return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_ComAmazonawsDynamodb( + Com.Amazonaws.Dynamodb.TypeConversion.ToDafny_CommonError(value) + ); + } + switch (value) + { + case AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorException exception: + return ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException(exception); + case CollectionOfErrors collectionOfErrors: + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_CollectionOfErrors( + Dafny.Sequence + .FromArray( + collectionOfErrors.list.Select + (x => TypeConversion.ToDafny_CommonError(x)) + .ToArray()), + Dafny.Sequence.FromString(collectionOfErrors.Message) + ); + // OpaqueError is redundant, but listed for completeness. + case OpaqueError exception: + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_Opaque(exception); + case System.Exception exception: + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_Opaque(exception); + default: + // The switch MUST be complete for System.Exception, so `value` MUST NOT be an System.Exception. (How did you get here?) + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_Opaque(value); + } + } + } +} diff --git a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs new file mode 100644 index 000000000..a5ec8c028 --- /dev/null +++ b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs @@ -0,0 +1,28 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +use dafny_runtime::Rc; +use dafny_runtime::Object; +use crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::IItemEncryptor; +use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Error; +use crate::implementation_from_dafny::_Wrappers_Compile; + +pub mod _CreateWrappedItemEncryptor_Compile { + pub struct _default {} +} + +impl _CreateWrappedItemEncryptor_Compile::_default { + pub fn CreateWrappedItemEncryptor( + config: &Rc + ) -> Rc<_Wrappers_Compile::Result, Rc>> { + let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_transforms::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); + + let item_encryptor = aws_cryptography_dbencryptionsdk_dynamodb::item_encryptor::DynamoDbItemEncryptor::new(native_config); + let wrapped_encryptor = crate::deps::com_amazonaws_dynamodb::item_encryptor::ItemEncryptor { inner: item_encryptor }; + let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor)); + + Rc::new(crate::r#_Wrappers_Compile::Result::Success { + value: dafny_encryptor, + }) + } +} From 13aec15634955f0b40711b7622a7c9a788c90d15 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 11:26:53 -0700 Subject: [PATCH 03/28] m --- TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy | 2 ++ 1 file changed, 2 insertions(+) diff --git a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy index 7e2689287..422723e98 100644 --- a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy +++ b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy @@ -1,2 +1,4 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 // Empty stub expected by Smithy-Dafny module WrappedItemEncryptor {} \ No newline at end of file From b2054904d597aa9a534735d40f9d648e02cd728c Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 11:29:13 -0700 Subject: [PATCH 04/28] m --- TestVectors/Makefile | 1 + TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 57a1e2f09..0db013ad9 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -38,6 +38,7 @@ RUST_OTHER_FILES := \ runtimes/rust/src/ddb.rs \ runtimes/rust/src/concurrent_call.rs \ runtimes/rust/src/create_client.rs \ + runtimes/rust/src/create_wrapped_item_encryptor.rs \ runtimes/rust/src/dafny_libraries.rs \ runtimes/rust/src/digest.rs \ runtimes/rust/src/ecdh.rs \ diff --git a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy index 422723e98..b3cc1a680 100644 --- a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy +++ b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy @@ -1,4 +1,4 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 // Empty stub expected by Smithy-Dafny -module WrappedItemEncryptor {} \ No newline at end of file +module WrappedItemEncryptor {} From 72cccd9f57aae2a51da5ec42bb99f8c13d7e448f Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 11:56:15 -0700 Subject: [PATCH 05/28] m --- .../runtimes/net/Extern/CreateWrappedItemEncryptor.cs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs index 4c86fa5bd..e038c4fc3 100644 --- a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -1,7 +1,7 @@ -using Amazon.Cryptography.DatabaseEncryptionSDK.DynamoDb.ItemEncryptor; -using Amazon.Cryptography.DatabaseEncryptionSDK.Dynamodb; -using Amazon.Cryptography.Services.Dynamodb.Internaldafny; -using Amazon.Cryptography.Services.Dynamodb.Internaldafny.Types; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor; +using AWS.Cryptography.DbEncryptionSDK.Dynamodb; +using software.amazon.cryptography.services.dynamodb.internaldafny; +using software.amazon.cryptography.services.dynamodb.internaldafny.types; using Wrappers_Compile; using _IError = software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IError; From fb351b9ec046ae6e20b9e79e55e901510ccff819 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 12:01:59 -0700 Subject: [PATCH 06/28] m --- .../CreateWrappedItemEncryptor_Compile/__default.java | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java index 20552e29e..9a1353feb 100644 --- a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -5,13 +5,13 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny; import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToNative; -import software.amazon.cryptography.services.dynamodb.internaldafny.types.IItemEncryptor; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error; import software.amazon.cryptography.services.dynamodb.internaldafny.Shim; public class __default { - public static Result CreateWrappedItemEncryptor( + public static Result CreateWrappedItemEncryptor( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbItemEncryptorConfig config ) { try { @@ -23,7 +23,9 @@ public static Result CreateWrappedItemEncryptor( .DynamoDbItemEncryptorConfig(nativeConfig) .build(); - final Shim wrappedEncryptor = new Shim(itemEncryptor); + final TestDynamoDbItemEncryptor wrappedEncryptor = new TestDynamoDbItemEncryptor.builder() + .impl(itemEncryptor) + .build(); return Result.create_Success(wrappedEncryptor); } catch (Exception e) { From 9c9446c0cd4710297fc0417b0b348fb828f16272 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 12:05:49 -0700 Subject: [PATCH 07/28] m --- .../java/CreateWrappedItemEncryptor_Compile/__default.java | 2 +- .../runtimes/net/Extern/CreateWrappedItemEncryptor.cs | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java index 9a1353feb..e7a043d52 100644 --- a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -12,7 +12,7 @@ public class __default { public static Result CreateWrappedItemEncryptor( - software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbItemEncryptorConfig config + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config ) { try { final DynamoDbItemEncryptorConfig nativeConfig = diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs index e038c4fc3..0fe357d03 100644 --- a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -1,5 +1,5 @@ using AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor; -using AWS.Cryptography.DbEncryptionSDK.Dynamodb; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb; using software.amazon.cryptography.services.dynamodb.internaldafny; using software.amazon.cryptography.services.dynamodb.internaldafny.types; using Wrappers_Compile; @@ -9,8 +9,8 @@ namespace CreateWrappedItemEncryptor_Compile { public partial class __default { - public static _IResult CreateWrappedItemEncryptor( - software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbItemEncryptorConfig config) + public static _IResult CreateWrappedItemEncryptor( + software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDynamoDbItemEncryptorConfig config) { var nativeConfig = AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms.TypeConversion .FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbItemEncryptorConfig( From 97461b466c1c8eeb462efd74cb9ad257b48d4f5e Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 12:50:50 -0700 Subject: [PATCH 08/28] m --- TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs index 0fe357d03..cab55956e 100644 --- a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -9,7 +9,7 @@ namespace CreateWrappedItemEncryptor_Compile { public partial class __default { - public static _IResult CreateWrappedItemEncryptor( + public static _IResult CreateWrappedItemEncryptor( software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDynamoDbItemEncryptorConfig config) { var nativeConfig = AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms.TypeConversion From 46eb496d5ef443564ee0845c341482e9d9b45adb Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 12:52:27 -0700 Subject: [PATCH 09/28] m --- .../CreateWrappedItemEncryptor_Compile/__default.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java index e7a043d52..5b482479d 100644 --- a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -3,11 +3,11 @@ import Wrappers_Compile.Result; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig; -import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny; -import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToNative; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient; -import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error; -import software.amazon.cryptography.services.dynamodb.internaldafny.Shim; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.wrapped.TestDynamoDbItemEncryptor; public class __default { From 40e1d63fa51f09b7b1d4548925974ada90fe8cea Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 13:04:34 -0700 Subject: [PATCH 10/28] m --- .../java/CreateWrappedItemEncryptor_Compile/__default.java | 3 ++- TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java index 5b482479d..3d3148a26 100644 --- a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -23,7 +23,8 @@ public static Result CreateWrappedItemEncry .DynamoDbItemEncryptorConfig(nativeConfig) .build(); - final TestDynamoDbItemEncryptor wrappedEncryptor = new TestDynamoDbItemEncryptor.builder() + final TestDynamoDbItemEncryptor wrappedEncryptor = TestDynamoDbItemEncryptor + .builder() .impl(itemEncryptor) .build(); diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs index cab55956e..67d9776ca 100644 --- a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -3,7 +3,7 @@ using software.amazon.cryptography.services.dynamodb.internaldafny; using software.amazon.cryptography.services.dynamodb.internaldafny.types; using Wrappers_Compile; -using _IError = software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IError; +using _IError = software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError; namespace CreateWrappedItemEncryptor_Compile { From 40f6ae2ad1b1bb76cc531c0b58bf12def7bbffef Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 13:14:47 -0700 Subject: [PATCH 11/28] rust --- TestVectors/runtimes/rust/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/TestVectors/runtimes/rust/src/lib.rs b/TestVectors/runtimes/rust/src/lib.rs index ea26b691a..0cc483055 100644 --- a/TestVectors/runtimes/rust/src/lib.rs +++ b/TestVectors/runtimes/rust/src/lib.rs @@ -66,3 +66,4 @@ pub mod time; pub mod uuid; pub mod create_client; +pub mod create_wrapped_item_encryptor; From d3ac5fe9b714257df857669b1f18d257aa884a0f Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 13:20:45 -0700 Subject: [PATCH 12/28] m --- .../runtimes/net/Extern/CreateWrappedItemEncryptor.cs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs index 67d9776ca..1572a97fa 100644 --- a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -1,5 +1,6 @@ using AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor; using AWS.Cryptography.DbEncryptionSDK.DynamoDb; +using AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped; using software.amazon.cryptography.services.dynamodb.internaldafny; using software.amazon.cryptography.services.dynamodb.internaldafny.types; using Wrappers_Compile; @@ -12,12 +13,12 @@ public partial class __default public static _IResult CreateWrappedItemEncryptor( software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDynamoDbItemEncryptorConfig config) { - var nativeConfig = AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms.TypeConversion - .FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbItemEncryptorConfig( + var nativeConfig = AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.TypeConversion + .FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S27_DynamoDbItemEncryptorConfig( config); - var itemEncryptor = DynamoDbItemEncryptor.Create(nativeConfig); - var wrappedEncryptor = new Com.Amazonaws.Dynamodb.ItemEncryptorShim(itemEncryptor); + var itemEncryptor = new DynamoDbItemEncryptor(nativeConfig); + var wrappedEncryptor = new DynamoDbItemEncryptorShim(itemEncryptor); return new Result_Success(wrappedEncryptor); } From 93ed0f9f05be92c43bd853d7ca1a507e8dcc8b93 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 13:38:03 -0700 Subject: [PATCH 13/28] m --- TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs index 1572a97fa..726ba5118 100644 --- a/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs +++ b/TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs @@ -20,7 +20,7 @@ public partial class __default var itemEncryptor = new DynamoDbItemEncryptor(nativeConfig); var wrappedEncryptor = new DynamoDbItemEncryptorShim(itemEncryptor); - return new Result_Success(wrappedEncryptor); + return new Result_Success(wrappedEncryptor); } } } From 3368712e5290e1c5192fde4d41d1a35014e7d3b2 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 13:40:31 -0700 Subject: [PATCH 14/28] m --- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 397a11ef9..945e1b65e 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -257,7 +257,7 @@ module {:options "-functionSyntax:4"} JsonConfig { } method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient) - returns (encryptor : Result) + returns (encryptor : Result) requires keys.ValidState() modifies keys.Modifies ensures keys.ValidState() From b76146081bc030c42b1bfb19cda6adfb2729ece5 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 14:33:47 -0700 Subject: [PATCH 15/28] proof --- .../src/CreateWrappedItemEncryptor.dfy | 32 +++++++++---------- .../dafny/DDBEncryption/src/JsonConfig.dfy | 2 +- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy b/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy index 6cd10ae38..71bc6719a 100644 --- a/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy +++ b/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy @@ -14,28 +14,28 @@ module {:extern} CreateWrappedItemEncryptor { // The `ensures` clause is copy-pasted from the DynamoDbItemEncryptor client method's `ensures` clause. method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig) returns (output: Result) - requires config.keyring.Some? ==> - config.keyring.value.ValidState() - requires config.cmm.Some? ==> - config.cmm.value.ValidState() - requires config.legacyOverride.Some? ==> - config.legacyOverride.value.encryptor.ValidState() - modifies if config.keyring.Some? then - config.keyring.value.Modifies - else {} - modifies if config.cmm.Some? then - config.cmm.value.Modifies - else {} - modifies if config.legacyOverride.Some? then - config.legacyOverride.value.encryptor.Modifies - else {} + // requires config.keyring.Some? ==> + // config.keyring.value.ValidState() + // requires config.cmm.Some? ==> + // config.cmm.value.ValidState() + // requires config.legacyOverride.Some? ==> + // config.legacyOverride.value.encryptor.ValidState() + // modifies if config.keyring.Some? then + // config.keyring.value.Modifies + // else {} + // modifies if config.cmm.Some? then + // config.cmm.value.Modifies + // else {} + // modifies if config.legacyOverride.Some? then + // config.legacyOverride.value.encryptor.Modifies + // else {} ensures output.Success? ==> && output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient && fresh(output.value) && fresh(output.value.History) && output.value.ValidState() && var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config; - && fresh(output.value.Modifies - Operations.ModifiesInternalConfig(rconfig)) + && fresh(output.value.Modifies) && rconfig.logicalTableName == config.logicalTableName && rconfig.partitionKeyName == config.partitionKeyName && rconfig.sortKeyName == config.sortKeyName diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 945e1b65e..42f1bb741 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -264,7 +264,7 @@ module {:options "-functionSyntax:4"} JsonConfig { ensures encryptor.Success? ==> && encryptor.value.ValidState() && fresh(encryptor.value) - && fresh(encryptor.value.Modifies - Operations.ModifiesInternalConfig(encryptor.value.config)) + && fresh(encryptor.value.Modifies) { :- Need(data.Object?, "A Table Config must be an object."); var logicalTableName := TableName; From 35cae5f005ef9cc8202d5c43468b3240f1a57464 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 14:45:08 -0700 Subject: [PATCH 16/28] m --- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 42f1bb741..3604153e2 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -356,9 +356,10 @@ module {:options "-functionSyntax:4"} JsonConfig { plaintextOverride := plaintextOverride ); var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig); - assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; - var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; - return Success(encr); + return Success(enc); + // assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; + // var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; + // return Success(encr); } method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient) From 719bb054a5c09f5a89f2c4e8ca695a937f126e16 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 15:01:06 -0700 Subject: [PATCH 17/28] m --- .../runtimes/rust/src/create_wrapped_item_encryptor.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs index a5ec8c028..782d0eb82 100644 --- a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs +++ b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs @@ -3,8 +3,8 @@ use dafny_runtime::Rc; use dafny_runtime::Object; -use crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::IItemEncryptor; -use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Error; +use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::IDynamoDbItemEncryptorClient; +use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::Error; use crate::implementation_from_dafny::_Wrappers_Compile; pub mod _CreateWrappedItemEncryptor_Compile { @@ -13,12 +13,12 @@ pub mod _CreateWrappedItemEncryptor_Compile { impl _CreateWrappedItemEncryptor_Compile::_default { pub fn CreateWrappedItemEncryptor( - config: &Rc - ) -> Rc<_Wrappers_Compile::Result, Rc>> { + config: &Rc + ) -> Rc<_Wrappers_Compile::Result, Rc>> { let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_transforms::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); let item_encryptor = aws_cryptography_dbencryptionsdk_dynamodb::item_encryptor::DynamoDbItemEncryptor::new(native_config); - let wrapped_encryptor = crate::deps::com_amazonaws_dynamodb::item_encryptor::ItemEncryptor { inner: item_encryptor }; + let wrapped_encryptor = crate::deps::com_amazonaws_dynamodb::item_encryptor::DynamoDbItemEncryptorShim { inner: item_encryptor }; let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor)); Rc::new(crate::r#_Wrappers_Compile::Result::Success { From afd61ec233b7cd16a99987b6256ee22ba7009cac Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 15:04:34 -0700 Subject: [PATCH 18/28] mm --- .../__default.java | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java index 3d3148a26..2360403bb 100644 --- a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -2,31 +2,32 @@ import Wrappers_Compile.Result; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor; -import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative; -import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.wrapped.TestDynamoDbItemEncryptor; public class __default { - public static Result CreateWrappedItemEncryptor( + public static Result< + IDynamoDbItemEncryptorClient, + Error + > CreateWrappedItemEncryptor( software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config ) { try { final DynamoDbItemEncryptorConfig nativeConfig = ToNative.DynamoDbItemEncryptorConfig(config); - final DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor - .builder() - .DynamoDbItemEncryptorConfig(nativeConfig) - .build(); + final DynamoDbItemEncryptor itemEncryptor = + DynamoDbItemEncryptor.builder() + .DynamoDbItemEncryptorConfig(nativeConfig) + .build(); - final TestDynamoDbItemEncryptor wrappedEncryptor = TestDynamoDbItemEncryptor - .builder() - .impl(itemEncryptor) - .build(); + final TestDynamoDbItemEncryptor wrappedEncryptor = + TestDynamoDbItemEncryptor.builder().impl(itemEncryptor).build(); return Result.create_Success(wrappedEncryptor); } catch (Exception e) { From 8074ccdf5c6010e8751063ba2604315417ea4b22 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 15:17:23 -0700 Subject: [PATCH 19/28] m --- .../runtimes/rust/src/create_wrapped_item_encryptor.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs index 782d0eb82..3ea9425ea 100644 --- a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs +++ b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs @@ -15,9 +15,9 @@ impl _CreateWrappedItemEncryptor_Compile::_default { pub fn CreateWrappedItemEncryptor( config: &Rc ) -> Rc<_Wrappers_Compile::Result, Rc>> { - let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_transforms::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); + let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemencryptor::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); - let item_encryptor = aws_cryptography_dbencryptionsdk_dynamodb::item_encryptor::DynamoDbItemEncryptor::new(native_config); + let item_encryptor = aws_db_esdk::item_encryptor::Client::from_conf(native_config); let wrapped_encryptor = crate::deps::com_amazonaws_dynamodb::item_encryptor::DynamoDbItemEncryptorShim { inner: item_encryptor }; let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor)); From 8b31331c3abd4f9c1fdb16b7c5410af06fa827c7 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 17 Apr 2025 15:39:12 -0700 Subject: [PATCH 20/28] m --- .../CreateWrappedItemEncryptor_Compile/__default.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java index 2360403bb..5017f340d 100644 --- a/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java +++ b/TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java @@ -21,10 +21,10 @@ > CreateWrappedItemEncryptor( final DynamoDbItemEncryptorConfig nativeConfig = ToNative.DynamoDbItemEncryptorConfig(config); - final DynamoDbItemEncryptor itemEncryptor = - DynamoDbItemEncryptor.builder() - .DynamoDbItemEncryptorConfig(nativeConfig) - .build(); + final DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor + .builder() + .DynamoDbItemEncryptorConfig(nativeConfig) + .build(); final TestDynamoDbItemEncryptor wrappedEncryptor = TestDynamoDbItemEncryptor.builder().impl(itemEncryptor).build(); From 865171030daa1ca2ea5fe3b7364c7050e7d9dc83 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 09:26:59 -0700 Subject: [PATCH 21/28] m --- .../runtimes/rust/src/create_wrapped_item_encryptor.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs index 3ea9425ea..4022db516 100644 --- a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs +++ b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs @@ -6,6 +6,7 @@ use dafny_runtime::Object; use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::IDynamoDbItemEncryptorClient; use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::Error; use crate::implementation_from_dafny::_Wrappers_Compile; +use aws_db_esdk::item_encryptor::client as item_encryptor_client; pub mod _CreateWrappedItemEncryptor_Compile { pub struct _default {} @@ -15,11 +16,11 @@ impl _CreateWrappedItemEncryptor_Compile::_default { pub fn CreateWrappedItemEncryptor( config: &Rc ) -> Rc<_Wrappers_Compile::Result, Rc>> { - let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemencryptor::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); + let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); - let item_encryptor = aws_db_esdk::item_encryptor::Client::from_conf(native_config); - let wrapped_encryptor = crate::deps::com_amazonaws_dynamodb::item_encryptor::DynamoDbItemEncryptorShim { inner: item_encryptor }; - let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor)); + let item_encryptor = item_encryptor_client::Client::from_conf(native_config); + let wrapped_encryptor = // where is this generated? + let dafny_encryptor = // tood find Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_encryptor, From c290b042604e0825770aea6bb502297be530cee1 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 09:46:08 -0700 Subject: [PATCH 22/28] m --- .../runtimes/rust/src/create_wrapped_item_encryptor.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs index 4022db516..ac0b417c3 100644 --- a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs +++ b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs @@ -6,7 +6,7 @@ use dafny_runtime::Object; use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::IDynamoDbItemEncryptorClient; use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::Error; use crate::implementation_from_dafny::_Wrappers_Compile; -use aws_db_esdk::item_encryptor::client as item_encryptor_client; +use crate::deps::aws_db_esdk::item_encryptor::client as item_encryptor_client; pub mod _CreateWrappedItemEncryptor_Compile { pub struct _default {} @@ -20,7 +20,7 @@ impl _CreateWrappedItemEncryptor_Compile::_default { let item_encryptor = item_encryptor_client::Client::from_conf(native_config); let wrapped_encryptor = // where is this generated? - let dafny_encryptor = // tood find + let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor)); Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_encryptor, From df31a1d897611c17e800e834ef3e9072d489dab1 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 09:50:54 -0700 Subject: [PATCH 23/28] m --- .../src/CreateWrappedItemEncryptor.dfy | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy b/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy index 71bc6719a..27c84311a 100644 --- a/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy +++ b/TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy @@ -30,30 +30,30 @@ module {:extern} CreateWrappedItemEncryptor { // config.legacyOverride.value.encryptor.Modifies // else {} ensures output.Success? ==> - && output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient - && fresh(output.value) - && fresh(output.value.History) - && output.value.ValidState() - && var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config; - && fresh(output.value.Modifies) - && rconfig.logicalTableName == config.logicalTableName - && rconfig.partitionKeyName == config.partitionKeyName - && rconfig.sortKeyName == config.sortKeyName - && rconfig.attributeActionsOnEncrypt == config.attributeActionsOnEncrypt - && rconfig.allowedUnsignedAttributes == config.allowedUnsignedAttributes - && rconfig.allowedUnsignedAttributePrefix == config.allowedUnsignedAttributePrefix - && rconfig.algorithmSuiteId == config.algorithmSuiteId + && output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient + && fresh(output.value) + && fresh(output.value.History) + && output.value.ValidState() + && var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config; + && fresh(output.value.Modifies) + && rconfig.logicalTableName == config.logicalTableName + && rconfig.partitionKeyName == config.partitionKeyName + && rconfig.sortKeyName == config.sortKeyName + && rconfig.attributeActionsOnEncrypt == config.attributeActionsOnEncrypt + && rconfig.allowedUnsignedAttributes == config.allowedUnsignedAttributes + && rconfig.allowedUnsignedAttributePrefix == config.allowedUnsignedAttributePrefix + && rconfig.algorithmSuiteId == config.algorithmSuiteId - //= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#attribute-actions - //= type=implication - //# The [Key Action](#key-action) - //# MUST be configured to the partition attribute and, if present, sort attribute. - && rconfig.version == Operations.VersionFromActions(config.attributeActionsOnEncrypt) - && config.partitionKeyName in config.attributeActionsOnEncrypt - && config.attributeActionsOnEncrypt[config.partitionKeyName] == Operations.KeyActionFromVersion(rconfig.version) - && (config.sortKeyName.Some? ==> - && config.sortKeyName.value in config.attributeActionsOnEncrypt - && config.attributeActionsOnEncrypt[config.sortKeyName.value] == Operations.KeyActionFromVersion(rconfig.version)) + //= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#attribute-actions + //= type=implication + //# The [Key Action](#key-action) + //# MUST be configured to the partition attribute and, if present, sort attribute. + && rconfig.version == Operations.VersionFromActions(config.attributeActionsOnEncrypt) + && config.partitionKeyName in config.attributeActionsOnEncrypt + && config.attributeActionsOnEncrypt[config.partitionKeyName] == Operations.KeyActionFromVersion(rconfig.version) + && (config.sortKeyName.Some? ==> + && config.sortKeyName.value in config.attributeActionsOnEncrypt + && config.attributeActionsOnEncrypt[config.sortKeyName.value] == Operations.KeyActionFromVersion(rconfig.version)) //= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#plaintext-policy //# If not specified, encryption and decryption MUST behave according to `FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ`. From c12817f0bdd20f67de2dc8d0456f8d4508cab086 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 10:04:59 -0700 Subject: [PATCH 24/28] m --- .../runtimes/rust/src/create_wrapped_item_encryptor.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs index ac0b417c3..8f973a155 100644 --- a/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs +++ b/TestVectors/runtimes/rust/src/create_wrapped_item_encryptor.rs @@ -6,7 +6,8 @@ use dafny_runtime::Object; use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::IDynamoDbItemEncryptorClient; use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::Error; use crate::implementation_from_dafny::_Wrappers_Compile; -use crate::deps::aws_db_esdk::item_encryptor::client as item_encryptor_client; +use crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::client as item_encryptor_client; +use crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::wrapped::client as wrapped_item_encryptor_client; pub mod _CreateWrappedItemEncryptor_Compile { pub struct _default {} @@ -19,7 +20,7 @@ impl _CreateWrappedItemEncryptor_Compile::_default { let native_config = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor::conversions::dynamo_db_item_encryptor_config::_dynamo_db_item_encryptor_config::plain_from_dafny(config); let item_encryptor = item_encryptor_client::Client::from_conf(native_config); - let wrapped_encryptor = // where is this generated? + let wrapped_encryptor = wrapped_item_encryptor_client::Client {wrapped: item_encryptor}; let dafny_encryptor = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrapped_encryptor)); Rc::new(crate::r#_Wrappers_Compile::Result::Success { From 8ce42294bb4af96fd17f9cfa2a2eba930238f157 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 10:11:20 -0700 Subject: [PATCH 25/28] m --- .../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy | 4 ++-- TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy b/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy index ceddef25f..31c36edda 100644 --- a/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy +++ b/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy @@ -2,11 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" - // BEGIN MANUAL EDIT +// BEGIN MANUAL EDIT include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy" include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy" include "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy" - // END MANUAL EDIT +// END MANUAL EDIT abstract module WrappedAbstractAwsCryptographyDynamoDbEncryptionService { import opened Wrappers import opened StandardLibrary.UInt diff --git a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy index b3cc1a680..d8b978ab4 100644 --- a/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy +++ b/TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy @@ -1,4 +1,6 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 // Empty stub expected by Smithy-Dafny + +include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy" module WrappedItemEncryptor {} From e755164648e8c6fcb1dbd5b4abc1ec114d89c7f7 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 10:17:39 -0700 Subject: [PATCH 26/28] m --- TestVectors/runtimes/rust/Cargo.toml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml index aad1d58f9..746fae450 100644 --- a/TestVectors/runtimes/rust/Cargo.toml +++ b/TestVectors/runtimes/rust/Cargo.toml @@ -6,6 +6,10 @@ rust-version = "1.81.0" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html +[features] +default = ["wrapped-client] +wrapped-client = [] + [dependencies] aws-config = "1.5.15" aws-lc-rs = "1.12.2" From 52e29a362226c80c3addb654094545681ff35119 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 10:18:00 -0700 Subject: [PATCH 27/28] m --- TestVectors/runtimes/rust/Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml index 746fae450..06133e82c 100644 --- a/TestVectors/runtimes/rust/Cargo.toml +++ b/TestVectors/runtimes/rust/Cargo.toml @@ -7,7 +7,7 @@ rust-version = "1.81.0" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [features] -default = ["wrapped-client] +default = ["wrapped-client"] wrapped-client = [] [dependencies] From d8ea08ab4cafb137d0ec54e35ec6ac7c07c9655b Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 18 Apr 2025 10:23:16 -0700 Subject: [PATCH 28/28] m --- .../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy b/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy index 31c36edda..ceddef25f 100644 --- a/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy +++ b/TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy @@ -2,11 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" -// BEGIN MANUAL EDIT + // BEGIN MANUAL EDIT include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy" include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy" include "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy" -// END MANUAL EDIT + // END MANUAL EDIT abstract module WrappedAbstractAwsCryptographyDynamoDbEncryptionService { import opened Wrappers import opened StandardLibrary.UInt