AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go

// Code generated by smithy-go-codegen DO NOT EDIT.

package awscryptographymaterialproviderssmithygenerated

import (
	"unicode/utf8"

	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb/comamazonawsdynamodbsmithygenerated"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms/ComAmazonawsKmsTypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms/KMSwrapped"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms/comamazonawskmssmithygenerated"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/AwsCryptographyKeyStoreTypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/AwsCryptographyMaterialProvidersTypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/awscryptographykeystoresmithygenerated"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/awscryptographykeystoresmithygeneratedtypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/awscryptographymaterialproviderssmithygeneratedtypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/AwsCryptographyPrimitivesTypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/awscryptographyprimitivessmithygenerated"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/awscryptographyprimitivessmithygeneratedtypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/UTF8"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers"
	"github.com/aws/aws-sdk-go-v2/service/kms"
	kmstypes "github.com/aws/aws-sdk-go-v2/service/kms/types"
	"github.com/aws/smithy-go"
	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
)

func CreateAwsKmsDiscoveryKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsDiscoveryKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsDiscoveryKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsDiscoveryKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsDiscoveryKeyringInput_.Create_CreateAwsKmsDiscoveryKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryKeyringInput_kmsClient_ToDafny(nativeInput.KmsClient), Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryKeyringInput_discoveryFilter_ToDafny(nativeInput.DiscoveryFilter), Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsDiscoveryMultiKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsDiscoveryMultiKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsDiscoveryMultiKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsDiscoveryMultiKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsDiscoveryMultiKeyringInput_.Create_CreateAwsKmsDiscoveryMultiKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryMultiKeyringInput_regions_ToDafny(nativeInput.Regions), Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryMultiKeyringInput_discoveryFilter_ToDafny(nativeInput.DiscoveryFilter), func() Wrappers.Option {
			if (nativeInput.ClientSupplier) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(ClientSupplier_ToDafny(nativeInput.ClientSupplier))
		}(), Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryMultiKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsEcdhKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsEcdhKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsEcdhKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsEcdhKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsEcdhKeyringInput_.Create_CreateAwsKmsEcdhKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_KeyAgreementScheme_ToDafny(nativeInput.KeyAgreementScheme), Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_curveSpec_ToDafny(nativeInput.CurveSpec), Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_kmsClient_ToDafny(nativeInput.KmsClient), Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsHierarchicalKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsHierarchicalKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsHierarchicalKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsHierarchicalKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsHierarchicalKeyringInput_.Create_CreateAwsKmsHierarchicalKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_branchKeyId_ToDafny(nativeInput.BranchKeyId), func() Wrappers.Option {
			if (nativeInput.BranchKeyIdSupplier) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(BranchKeyIdSupplier_ToDafny(nativeInput.BranchKeyIdSupplier))
		}(), Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_keyStore_ToDafny(nativeInput.KeyStore), Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_ttlSeconds_ToDafny(nativeInput.TtlSeconds), Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_cache_ToDafny(nativeInput.Cache), Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_partitionId_ToDafny(nativeInput.PartitionId))
	}()

}

func CreateAwsKmsKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsKeyringInput_.Create_CreateAwsKmsKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsKeyringInput_kmsKeyId_ToDafny(nativeInput.KmsKeyId), Aws_cryptography_materialProviders_CreateAwsKmsKeyringInput_kmsClient_ToDafny(nativeInput.KmsClient), Aws_cryptography_materialProviders_CreateAwsKmsKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsMrkDiscoveryKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsMrkDiscoveryKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkDiscoveryKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkDiscoveryKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsMrkDiscoveryKeyringInput_.Create_CreateAwsKmsMrkDiscoveryKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_kmsClient_ToDafny(nativeInput.KmsClient), Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_discoveryFilter_ToDafny(nativeInput.DiscoveryFilter), Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens), Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_region_ToDafny(nativeInput.Region))
	}()

}

func CreateAwsKmsMrkDiscoveryMultiKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsMrkDiscoveryMultiKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkDiscoveryMultiKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkDiscoveryMultiKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsMrkDiscoveryMultiKeyringInput_.Create_CreateAwsKmsMrkDiscoveryMultiKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryMultiKeyringInput_regions_ToDafny(nativeInput.Regions), Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryMultiKeyringInput_discoveryFilter_ToDafny(nativeInput.DiscoveryFilter), func() Wrappers.Option {
			if (nativeInput.ClientSupplier) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(ClientSupplier_ToDafny(nativeInput.ClientSupplier))
		}(), Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryMultiKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsMrkKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsMrkKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsMrkKeyringInput_.Create_CreateAwsKmsMrkKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsMrkKeyringInput_kmsKeyId_ToDafny(nativeInput.KmsKeyId), Aws_cryptography_materialProviders_CreateAwsKmsMrkKeyringInput_kmsClient_ToDafny(nativeInput.KmsClient), Aws_cryptography_materialProviders_CreateAwsKmsMrkKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsMrkMultiKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsMrkMultiKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkMultiKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMrkMultiKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsMrkMultiKeyringInput_.Create_CreateAwsKmsMrkMultiKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsMrkMultiKeyringInput_generator_ToDafny(nativeInput.Generator), Aws_cryptography_materialProviders_CreateAwsKmsMrkMultiKeyringInput_kmsKeyIds_ToDafny(nativeInput.KmsKeyIds), func() Wrappers.Option {
			if (nativeInput.ClientSupplier) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(ClientSupplier_ToDafny(nativeInput.ClientSupplier))
		}(), Aws_cryptography_materialProviders_CreateAwsKmsMrkMultiKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsMultiKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsMultiKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMultiKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMultiKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsMultiKeyringInput_.Create_CreateAwsKmsMultiKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsMultiKeyringInput_generator_ToDafny(nativeInput.Generator), Aws_cryptography_materialProviders_CreateAwsKmsMultiKeyringInput_kmsKeyIds_ToDafny(nativeInput.KmsKeyIds), func() Wrappers.Option {
			if (nativeInput.ClientSupplier) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(ClientSupplier_ToDafny(nativeInput.ClientSupplier))
		}(), Aws_cryptography_materialProviders_CreateAwsKmsMultiKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateAwsKmsRsaKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateAwsKmsRsaKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateAwsKmsRsaKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateAwsKmsRsaKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateAwsKmsRsaKeyringInput_.Create_CreateAwsKmsRsaKeyringInput_(Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_publicKey_ToDafny(nativeInput.PublicKey), Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_kmsKeyId_ToDafny(nativeInput.KmsKeyId), Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_encryptionAlgorithm_ToDafny(nativeInput.EncryptionAlgorithm), Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_kmsClient_ToDafny(nativeInput.KmsClient), Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_grantTokens_ToDafny(nativeInput.GrantTokens))
	}()

}

func CreateCryptographicMaterialsCacheInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateCryptographicMaterialsCacheInput) AwsCryptographyMaterialProvidersTypes.CreateCryptographicMaterialsCacheInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateCryptographicMaterialsCacheInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateCryptographicMaterialsCacheInput_.Create_CreateCryptographicMaterialsCacheInput_(Aws_cryptography_materialProviders_CreateCryptographicMaterialsCacheInput_cache_ToDafny(nativeInput.Cache))
	}()

}

func CreateDefaultClientSupplierInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateDefaultClientSupplierInput) AwsCryptographyMaterialProvidersTypes.CreateDefaultClientSupplierInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateDefaultClientSupplierInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateDefaultClientSupplierInput_.Create_CreateDefaultClientSupplierInput_()
	}()

}

func CreateDefaultCryptographicMaterialsManagerInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateDefaultCryptographicMaterialsManagerInput) AwsCryptographyMaterialProvidersTypes.CreateDefaultCryptographicMaterialsManagerInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateDefaultCryptographicMaterialsManagerInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateDefaultCryptographicMaterialsManagerInput_.Create_CreateDefaultCryptographicMaterialsManagerInput_(Keyring_ToDafny(nativeInput.Keyring))
	}()

}

func CreateMultiKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateMultiKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateMultiKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateMultiKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateMultiKeyringInput_.Create_CreateMultiKeyringInput_(func() Wrappers.Option {
			if (nativeInput.Generator) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(Keyring_ToDafny(nativeInput.Generator))
		}(), Aws_cryptography_materialProviders_CreateMultiKeyringInput_childKeyrings_ToDafny(nativeInput.ChildKeyrings))
	}()

}

func CreateRawAesKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateRawAesKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateRawAesKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateRawAesKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateRawAesKeyringInput_.Create_CreateRawAesKeyringInput_(Aws_cryptography_materialProviders_CreateRawAesKeyringInput_keyNamespace_ToDafny(nativeInput.KeyNamespace), Aws_cryptography_materialProviders_CreateRawAesKeyringInput_keyName_ToDafny(nativeInput.KeyName), Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingKey_ToDafny(nativeInput.WrappingKey), Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingAlg_ToDafny(nativeInput.WrappingAlg))
	}()

}

func CreateRawEcdhKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateRawEcdhKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateRawEcdhKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateRawEcdhKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateRawEcdhKeyringInput_.Create_CreateRawEcdhKeyringInput_(Aws_cryptography_materialProviders_CreateRawEcdhKeyringInput_KeyAgreementScheme_ToDafny(nativeInput.KeyAgreementScheme), Aws_cryptography_materialProviders_CreateRawEcdhKeyringInput_curveSpec_ToDafny(nativeInput.CurveSpec))
	}()

}

func CreateRawRsaKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateRawRsaKeyringInput) AwsCryptographyMaterialProvidersTypes.CreateRawRsaKeyringInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateRawRsaKeyringInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateRawRsaKeyringInput_.Create_CreateRawRsaKeyringInput_(Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_keyNamespace_ToDafny(nativeInput.KeyNamespace), Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_keyName_ToDafny(nativeInput.KeyName), Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_paddingScheme_ToDafny(nativeInput.PaddingScheme), Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_publicKey_ToDafny(nativeInput.PublicKey), Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_privateKey_ToDafny(nativeInput.PrivateKey))
	}()

}

func CreateRequiredEncryptionContextCMMInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CreateRequiredEncryptionContextCMMInput) AwsCryptographyMaterialProvidersTypes.CreateRequiredEncryptionContextCMMInput {

	return func() AwsCryptographyMaterialProvidersTypes.CreateRequiredEncryptionContextCMMInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_CreateRequiredEncryptionContextCMMInput_.Create_CreateRequiredEncryptionContextCMMInput_(func() Wrappers.Option {
			if (nativeInput.UnderlyingCMM) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(CryptographicMaterialsManager_ToDafny(nativeInput.UnderlyingCMM))
		}(), func() Wrappers.Option {
			if (nativeInput.Keyring) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(Keyring_ToDafny(nativeInput.Keyring))
		}(), Aws_cryptography_materialProviders_CreateRequiredEncryptionContextCMMInput_requiredEncryptionContextKeys_ToDafny(nativeInput.RequiredEncryptionContextKeys))
	}()

}

func DecryptionMaterials_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

	return func() AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(nativeInput.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(nativeInput.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(nativeInput.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(nativeInput.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(nativeInput.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(nativeInput.SymmetricSigningKey))
	}()

}

func EncryptionMaterials_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

	return func() AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(nativeInput.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(nativeInput.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(nativeInput.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(nativeInput.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(nativeInput.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(nativeInput.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(nativeInput.SymmetricSigningKeys))
	}()

}

func GetAlgorithmSuiteInfoInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetAlgorithmSuiteInfoInput) dafny.Sequence {

	return Aws_cryptography_materialProviders_GetAlgorithmSuiteInfoInput_binaryId_ToDafny(nativeInput.BinaryId)

}

func AlgorithmSuiteInfo_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteInfo) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo {

	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo {

		return AwsCryptographyMaterialProvidersTypes.Companion_AlgorithmSuiteInfo_.Create_AlgorithmSuiteInfo_(Aws_cryptography_materialProviders_AlgorithmSuiteInfo_id_ToDafny(nativeOutput.Id), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_binaryId_ToDafny(nativeOutput.BinaryId), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_messageVersion_ToDafny(nativeOutput.MessageVersion), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_encrypt_ToDafny(nativeOutput.Encrypt), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_kdf_ToDafny(nativeOutput.Kdf), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_commitment_ToDafny(nativeOutput.Commitment), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_signature_ToDafny(nativeOutput.Signature), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_symmetricSignature_ToDafny(nativeOutput.SymmetricSignature), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_edkWrapping_ToDafny(nativeOutput.EdkWrapping))
	}()

}

func InitializeDecryptionMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InitializeDecryptionMaterialsInput) AwsCryptographyMaterialProvidersTypes.InitializeDecryptionMaterialsInput {

	return func() AwsCryptographyMaterialProvidersTypes.InitializeDecryptionMaterialsInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_InitializeDecryptionMaterialsInput_.Create_InitializeDecryptionMaterialsInput_(Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_requiredEncryptionContextKeys_ToDafny(nativeInput.RequiredEncryptionContextKeys))
	}()

}

func InitializeEncryptionMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InitializeEncryptionMaterialsInput) AwsCryptographyMaterialProvidersTypes.InitializeEncryptionMaterialsInput {

	return func() AwsCryptographyMaterialProvidersTypes.InitializeEncryptionMaterialsInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_InitializeEncryptionMaterialsInput_.Create_InitializeEncryptionMaterialsInput_(Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_requiredEncryptionContextKeys_ToDafny(nativeInput.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_signingKey_ToDafny(nativeInput.SigningKey), Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_verificationKey_ToDafny(nativeInput.VerificationKey))
	}()

}

func ValidateCommitmentPolicyOnDecryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.ValidateCommitmentPolicyOnDecryptInput) AwsCryptographyMaterialProvidersTypes.ValidateCommitmentPolicyOnDecryptInput {

	return func() AwsCryptographyMaterialProvidersTypes.ValidateCommitmentPolicyOnDecryptInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnDecryptInput_.Create_ValidateCommitmentPolicyOnDecryptInput_(Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnDecryptInput_algorithm_ToDafny(nativeInput.Algorithm), Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnDecryptInput_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy))
	}()

}

func ValidateCommitmentPolicyOnEncryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.ValidateCommitmentPolicyOnEncryptInput) AwsCryptographyMaterialProvidersTypes.ValidateCommitmentPolicyOnEncryptInput {

	return func() AwsCryptographyMaterialProvidersTypes.ValidateCommitmentPolicyOnEncryptInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnEncryptInput_.Create_ValidateCommitmentPolicyOnEncryptInput_(Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnEncryptInput_algorithm_ToDafny(nativeInput.Algorithm), Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnEncryptInput_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy))
	}()

}

func ValidDecryptionMaterialsTransitionInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.ValidDecryptionMaterialsTransitionInput) AwsCryptographyMaterialProvidersTypes.ValidDecryptionMaterialsTransitionInput {

	return func() AwsCryptographyMaterialProvidersTypes.ValidDecryptionMaterialsTransitionInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_ValidDecryptionMaterialsTransitionInput_.Create_ValidDecryptionMaterialsTransitionInput_(Aws_cryptography_materialProviders_ValidDecryptionMaterialsTransitionInput_start_ToDafny(nativeInput.Start), Aws_cryptography_materialProviders_ValidDecryptionMaterialsTransitionInput_stop_ToDafny(nativeInput.Stop))
	}()

}

func ValidEncryptionMaterialsTransitionInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.ValidEncryptionMaterialsTransitionInput) AwsCryptographyMaterialProvidersTypes.ValidEncryptionMaterialsTransitionInput {

	return func() AwsCryptographyMaterialProvidersTypes.ValidEncryptionMaterialsTransitionInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_ValidEncryptionMaterialsTransitionInput_.Create_ValidEncryptionMaterialsTransitionInput_(Aws_cryptography_materialProviders_ValidEncryptionMaterialsTransitionInput_start_ToDafny(nativeInput.Start), Aws_cryptography_materialProviders_ValidEncryptionMaterialsTransitionInput_stop_ToDafny(nativeInput.Stop))
	}()

}

func GetBranchKeyIdInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetBranchKeyIdInput) AwsCryptographyMaterialProvidersTypes.GetBranchKeyIdInput {

	return func() AwsCryptographyMaterialProvidersTypes.GetBranchKeyIdInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetBranchKeyIdInput_.Create_GetBranchKeyIdInput_(Aws_cryptography_materialProviders_GetBranchKeyIdInput_encryptionContext_ToDafny(nativeInput.EncryptionContext))
	}()

}

func GetBranchKeyIdOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.GetBranchKeyIdOutput) AwsCryptographyMaterialProvidersTypes.GetBranchKeyIdOutput {

	return func() AwsCryptographyMaterialProvidersTypes.GetBranchKeyIdOutput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetBranchKeyIdOutput_.Create_GetBranchKeyIdOutput_(Aws_cryptography_materialProviders_GetBranchKeyIdOutput_branchKeyId_ToDafny(nativeOutput.BranchKeyId))
	}()

}

func BranchKeyIdSupplier_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IBranchKeyIdSupplier) AwsCryptographyMaterialProvidersTypes.IBranchKeyIdSupplier {
	val, ok := nativeResource.(*BranchKeyIdSupplier)
	if ok {
		return val.Impl
	}
	return BranchKeyIdSupplier{&BranchKeyIdSupplierNativeWrapper{Impl: nativeResource}}.Impl

}

func GetClientInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetClientInput) AwsCryptographyMaterialProvidersTypes.GetClientInput {

	return func() AwsCryptographyMaterialProvidersTypes.GetClientInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetClientInput_.Create_GetClientInput_(Aws_cryptography_materialProviders_GetClientInput_region_ToDafny(nativeInput.Region))
	}()

}

func ClientSupplier_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IClientSupplier) AwsCryptographyMaterialProvidersTypes.IClientSupplier {
	val, ok := nativeResource.(*ClientSupplier)
	if ok {
		return val.Impl
	}
	return ClientSupplier{&ClientSupplierNativeWrapper{Impl: nativeResource}}.Impl

}

func DeleteCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.DeleteCacheEntryInput) AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput {

	return func() AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_DeleteCacheEntryInput_.Create_DeleteCacheEntryInput_(Aws_cryptography_materialProviders_DeleteCacheEntryInput_identifier_ToDafny(nativeInput.Identifier))
	}()

}

func GetCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput) AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput {

	return func() AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetCacheEntryInput_.Create_GetCacheEntryInput_(Aws_cryptography_materialProviders_GetCacheEntryInput_identifier_ToDafny(nativeInput.Identifier), Aws_cryptography_materialProviders_GetCacheEntryInput_bytesUsed_ToDafny(nativeInput.BytesUsed))
	}()

}

func GetCacheEntryOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryOutput) AwsCryptographyMaterialProvidersTypes.GetCacheEntryOutput {

	return func() AwsCryptographyMaterialProvidersTypes.GetCacheEntryOutput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetCacheEntryOutput_.Create_GetCacheEntryOutput_(Aws_cryptography_materialProviders_GetCacheEntryOutput_materials_ToDafny(nativeOutput.Materials), Aws_cryptography_materialProviders_GetCacheEntryOutput_creationTime_ToDafny(nativeOutput.CreationTime), Aws_cryptography_materialProviders_GetCacheEntryOutput_expiryTime_ToDafny(nativeOutput.ExpiryTime), Aws_cryptography_materialProviders_GetCacheEntryOutput_messagesUsed_ToDafny(nativeOutput.MessagesUsed), Aws_cryptography_materialProviders_GetCacheEntryOutput_bytesUsed_ToDafny(nativeOutput.BytesUsed))
	}()

}

func PutCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.PutCacheEntryInput) AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput {

	return func() AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_PutCacheEntryInput_.Create_PutCacheEntryInput_(Aws_cryptography_materialProviders_PutCacheEntryInput_identifier_ToDafny(nativeInput.Identifier), Aws_cryptography_materialProviders_PutCacheEntryInput_materials_ToDafny(nativeInput.Materials), Aws_cryptography_materialProviders_PutCacheEntryInput_creationTime_ToDafny(nativeInput.CreationTime), Aws_cryptography_materialProviders_PutCacheEntryInput_expiryTime_ToDafny(nativeInput.ExpiryTime), Aws_cryptography_materialProviders_PutCacheEntryInput_messagesUsed_ToDafny(nativeInput.MessagesUsed), Aws_cryptography_materialProviders_PutCacheEntryInput_bytesUsed_ToDafny(nativeInput.BytesUsed))
	}()

}

func UpdateUsageMetadataInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.UpdateUsageMetadataInput) AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput {

	return func() AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_UpdateUsageMetadataInput_.Create_UpdateUsageMetadataInput_(Aws_cryptography_materialProviders_UpdateUsageMetadataInput_identifier_ToDafny(nativeInput.Identifier), Aws_cryptography_materialProviders_UpdateUsageMetadataInput_bytesUsed_ToDafny(nativeInput.BytesUsed))
	}()

}

func CryptographicMaterialsCache_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache {
	val, ok := nativeResource.(*CryptographicMaterialsCache)
	if ok {
		return val.Impl
	}
	return CryptographicMaterialsCache{&CryptographicMaterialsCacheNativeWrapper{Impl: nativeResource}}.Impl

}

func DecryptMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput) AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput {

	return func() AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptMaterialsInput_.Create_DecryptMaterialsInput_(Aws_cryptography_materialProviders_DecryptMaterialsInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), Aws_cryptography_materialProviders_DecryptMaterialsInput_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy), Aws_cryptography_materialProviders_DecryptMaterialsInput_encryptedDataKeys_ToDafny(nativeInput.EncryptedDataKeys), Aws_cryptography_materialProviders_DecryptMaterialsInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), Aws_cryptography_materialProviders_DecryptMaterialsInput_reproducedEncryptionContext_ToDafny(nativeInput.ReproducedEncryptionContext))
	}()

}

func DecryptMaterialsOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsOutput) AwsCryptographyMaterialProvidersTypes.DecryptMaterialsOutput {

	return func() AwsCryptographyMaterialProvidersTypes.DecryptMaterialsOutput {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptMaterialsOutput_.Create_DecryptMaterialsOutput_(Aws_cryptography_materialProviders_DecryptMaterialsOutput_decryptionMaterials_ToDafny(nativeOutput.DecryptionMaterials))
	}()

}

func GetEncryptionMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput) AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput {

	return func() AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetEncryptionMaterialsInput_.Create_GetEncryptionMaterialsInput_(Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy), Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_maxPlaintextLength_ToDafny(nativeInput.MaxPlaintextLength), Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_requiredEncryptionContextKeys_ToDafny(nativeInput.RequiredEncryptionContextKeys))
	}()

}

func GetEncryptionMaterialsOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsOutput) AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsOutput {

	return func() AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsOutput {

		return AwsCryptographyMaterialProvidersTypes.Companion_GetEncryptionMaterialsOutput_.Create_GetEncryptionMaterialsOutput_(Aws_cryptography_materialProviders_GetEncryptionMaterialsOutput_encryptionMaterials_ToDafny(nativeOutput.EncryptionMaterials))
	}()

}

func CryptographicMaterialsManager_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager {
	val, ok := nativeResource.(*CryptographicMaterialsManager)
	if ok {
		return val.Impl
	}
	return CryptographicMaterialsManager{&CryptographicMaterialsManagerNativeWrapper{Impl: nativeResource}}.Impl

}

func OnDecryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput) AwsCryptographyMaterialProvidersTypes.OnDecryptInput {

	return func() AwsCryptographyMaterialProvidersTypes.OnDecryptInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_OnDecryptInput_.Create_OnDecryptInput_(Aws_cryptography_materialProviders_OnDecryptInput_materials_ToDafny(nativeInput.Materials), Aws_cryptography_materialProviders_OnDecryptInput_encryptedDataKeys_ToDafny(nativeInput.EncryptedDataKeys))
	}()

}

func OnDecryptOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptOutput) AwsCryptographyMaterialProvidersTypes.OnDecryptOutput {

	return func() AwsCryptographyMaterialProvidersTypes.OnDecryptOutput {

		return AwsCryptographyMaterialProvidersTypes.Companion_OnDecryptOutput_.Create_OnDecryptOutput_(Aws_cryptography_materialProviders_OnDecryptOutput_materials_ToDafny(nativeOutput.Materials))
	}()

}

func OnEncryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput) AwsCryptographyMaterialProvidersTypes.OnEncryptInput {

	return func() AwsCryptographyMaterialProvidersTypes.OnEncryptInput {

		return AwsCryptographyMaterialProvidersTypes.Companion_OnEncryptInput_.Create_OnEncryptInput_(Aws_cryptography_materialProviders_OnEncryptInput_materials_ToDafny(nativeInput.Materials))
	}()

}

func OnEncryptOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptOutput) AwsCryptographyMaterialProvidersTypes.OnEncryptOutput {

	return func() AwsCryptographyMaterialProvidersTypes.OnEncryptOutput {

		return AwsCryptographyMaterialProvidersTypes.Companion_OnEncryptOutput_.Create_OnEncryptOutput_(Aws_cryptography_materialProviders_OnEncryptOutput_materials_ToDafny(nativeOutput.Materials))
	}()

}

func Keyring_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IKeyring) AwsCryptographyMaterialProvidersTypes.IKeyring {
	val, ok := nativeResource.(*Keyring)
	if ok {
		return val.Impl
	}
	return Keyring{&KeyringNativeWrapper{Impl: nativeResource}}.Impl

}

func AwsCryptographicMaterialProvidersException_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(Aws_cryptography_materialProviders_AwsCryptographicMaterialProvidersException_message_ToDafny(nativeInput.Message))
	}()

}

func EntryAlreadyExists_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.EntryAlreadyExists) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_EntryAlreadyExists_(Aws_cryptography_materialProviders_EntryAlreadyExists_message_ToDafny(nativeInput.Message))
	}()

}

func EntryDoesNotExist_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.EntryDoesNotExist) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_EntryDoesNotExist_(Aws_cryptography_materialProviders_EntryDoesNotExist_message_ToDafny(nativeInput.Message))
	}()

}

func InFlightTTLExceeded_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InFlightTTLExceeded) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InFlightTTLExceeded_(Aws_cryptography_materialProviders_InFlightTTLExceeded_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidAlgorithmSuiteInfo_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfo) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidAlgorithmSuiteInfo_(Aws_cryptography_materialProviders_InvalidAlgorithmSuiteInfo_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidAlgorithmSuiteInfoOnDecrypt_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfoOnDecrypt) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidAlgorithmSuiteInfoOnDecrypt_(Aws_cryptography_materialProviders_InvalidAlgorithmSuiteInfoOnDecrypt_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidAlgorithmSuiteInfoOnEncrypt_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfoOnEncrypt) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidAlgorithmSuiteInfoOnEncrypt_(Aws_cryptography_materialProviders_InvalidAlgorithmSuiteInfoOnEncrypt_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidDecryptionMaterials_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidDecryptionMaterials) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidDecryptionMaterials_(Aws_cryptography_materialProviders_InvalidDecryptionMaterials_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidDecryptionMaterialsTransition_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidDecryptionMaterialsTransition) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidDecryptionMaterialsTransition_(Aws_cryptography_materialProviders_InvalidDecryptionMaterialsTransition_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidEncryptionMaterials_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidEncryptionMaterials) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidEncryptionMaterials_(Aws_cryptography_materialProviders_InvalidEncryptionMaterials_message_ToDafny(nativeInput.Message))
	}()

}

func InvalidEncryptionMaterialsTransition_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.InvalidEncryptionMaterialsTransition) AwsCryptographyMaterialProvidersTypes.Error {
	return func() AwsCryptographyMaterialProvidersTypes.Error {

		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InvalidEncryptionMaterialsTransition_(Aws_cryptography_materialProviders_InvalidEncryptionMaterialsTransition_message_ToDafny(nativeInput.Message))
	}()

}

func CollectionOfErrors_Input_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.CollectionOfErrors) AwsCryptographyMaterialProvidersTypes.Error {
	var e []interface{}
	for _, i2 := range nativeInput.ListOfErrors {
		e = append(e, Error_ToDafny(i2))
	}
	return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_CollectionOfErrors_(dafny.SeqOf(e...), func() dafny.Sequence {
		res, err := UTF8.DecodeFromNativeGoByteArray([]byte(nativeInput.Message))
		if err != nil {
			panic("invalid utf8 input provided")
		}
		return res
	}())
}
func OpaqueError_Input_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OpaqueError) AwsCryptographyMaterialProvidersTypes.Error {
	return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_Opaque_(nativeInput.ErrObject)
}

func Error_ToDafny(err error) AwsCryptographyMaterialProvidersTypes.Error {
	switch err.(type) {
	// Service Errors
	case awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException:
		return AwsCryptographicMaterialProvidersException_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException))

	case awscryptographymaterialproviderssmithygeneratedtypes.EntryAlreadyExists:
		return EntryAlreadyExists_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.EntryAlreadyExists))

	case awscryptographymaterialproviderssmithygeneratedtypes.EntryDoesNotExist:
		return EntryDoesNotExist_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.EntryDoesNotExist))

	case awscryptographymaterialproviderssmithygeneratedtypes.InFlightTTLExceeded:
		return InFlightTTLExceeded_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InFlightTTLExceeded))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfo:
		return InvalidAlgorithmSuiteInfo_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfo))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfoOnDecrypt:
		return InvalidAlgorithmSuiteInfoOnDecrypt_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfoOnDecrypt))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfoOnEncrypt:
		return InvalidAlgorithmSuiteInfoOnEncrypt_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidAlgorithmSuiteInfoOnEncrypt))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidDecryptionMaterials:
		return InvalidDecryptionMaterials_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidDecryptionMaterials))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidDecryptionMaterialsTransition:
		return InvalidDecryptionMaterialsTransition_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidDecryptionMaterialsTransition))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidEncryptionMaterials:
		return InvalidEncryptionMaterials_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidEncryptionMaterials))

	case awscryptographymaterialproviderssmithygeneratedtypes.InvalidEncryptionMaterialsTransition:
		return InvalidEncryptionMaterialsTransition_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.InvalidEncryptionMaterialsTransition))

	//DependentErrors
	case awscryptographyprimitivessmithygeneratedtypes.AwsCryptographicPrimitivesBaseException:
		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(awscryptographyprimitivessmithygenerated.Error_ToDafny(err))

	case awscryptographykeystoresmithygeneratedtypes.KeyStoreBaseException:
		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographyKeyStore_(awscryptographykeystoresmithygenerated.Error_ToDafny(err))

	case *smithy.OperationError:
		if err.(*smithy.OperationError).Service() == "DynamoDB" {
			DynamoDBError := comamazonawsdynamodbsmithygenerated.Error_ToDafny(err)
			return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_ComAmazonawsDynamodb_(DynamoDBError)
		}
		if err.(*smithy.OperationError).Service() == "KMS" {
			KMSError := comamazonawskmssmithygenerated.Error_ToDafny(err)
			return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_ComAmazonawsKms_(KMSError)
		}
		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_Opaque_(err)

	case smithy.APIError:
		DynamoDBError := comamazonawsdynamodbsmithygenerated.Error_ToDafny(err)
		if !DynamoDBError.Is_OpaqueWithText() {
			return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_ComAmazonawsDynamodb_(DynamoDBError)
		}
		KMSError := comamazonawskmssmithygenerated.Error_ToDafny(err)
		if !KMSError.Is_OpaqueWithText() {
			return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_ComAmazonawsKms_(KMSError)
		}
		return AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_Opaque_(err)

	//Unmodelled Errors
	case awscryptographymaterialproviderssmithygeneratedtypes.CollectionOfErrors:
		return CollectionOfErrors_Input_ToDafny(err.(awscryptographymaterialproviderssmithygeneratedtypes.CollectionOfErrors))

	default:
		error, ok := err.(awscryptographymaterialproviderssmithygeneratedtypes.OpaqueError)
		if !ok {
			panic("Error is not an OpaqueError")
		}
		return OpaqueError_Input_ToDafny(error)
	}
}

func MaterialProvidersConfig_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.MaterialProvidersConfig) AwsCryptographyMaterialProvidersTypes.MaterialProvidersConfig {
	return func() AwsCryptographyMaterialProvidersTypes.MaterialProvidersConfig {

		return AwsCryptographyMaterialProvidersTypes.Companion_MaterialProvidersConfig_.Create_MaterialProvidersConfig_()
	}()

}

func Materials_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.Materials) AwsCryptographyMaterialProvidersTypes.Materials {
	return func() AwsCryptographyMaterialProvidersTypes.Materials {

		switch nativeInput.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberEncryption:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_Encryption_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberEncryption).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_Encryption_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.EncryptionMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberDecryption:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_Decryption_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberDecryption).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_Decryption_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DecryptionMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBranchKey:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_BranchKey_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBranchKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_BranchKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyKeyStoreTypes.BranchKeyMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBeaconKey:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_BeaconKey_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBeaconKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_BeaconKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyKeyStoreTypes.BeaconKeyMaterials))

		default:
			panic("Unhandled union type")
		}
	}()

}

func StaticConfigurations_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurations) AwsCryptographyMaterialProvidersTypes.StaticConfigurations {
	return func() AwsCryptographyMaterialProvidersTypes.StaticConfigurations {

		switch nativeInput.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberAWS_KMS_ECDH:
			var inputToConversion = Aws_cryptography_materialProviders_StaticConfigurations_AWS_KMS_ECDH_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberAWS_KMS_ECDH).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_StaticConfigurations_{}.Create_AWS__KMS__ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations))
		case *awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberRAW_ECDH:
			var inputToConversion = Aws_cryptography_materialProviders_StaticConfigurations_RAW_ECDH_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberRAW_ECDH).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_StaticConfigurations_{}.Create_RAW__ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations))

		default:
			panic("Unhandled union type")
		}
	}()

}

func KeyAgreementScheme_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.KeyAgreementScheme) AwsCryptographyMaterialProvidersTypes.KeyAgreementScheme {
	return func() AwsCryptographyMaterialProvidersTypes.KeyAgreementScheme {

		switch nativeInput.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.KeyAgreementSchemeMemberStaticConfiguration:
			var inputToConversion = Aws_cryptography_materialProviders_KeyAgreementScheme_StaticConfiguration_ToDafny(nativeInput.(*awscryptographymaterialproviderssmithygeneratedtypes.KeyAgreementSchemeMemberStaticConfiguration).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_KeyAgreementScheme_{}.Create_StaticConfiguration_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.StaticConfigurations))

		default:
			panic("Unhandled union type")
		}
	}()

}

func Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryKeyringInput_kmsClient_ToDafny(input *kms.Client) ComAmazonawsKmsTypes.IKMSClient {
	return &KMSwrapped.Shim{Client: input}
}

func Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryKeyringInput_discoveryFilter_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.DiscoveryFilter) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DiscoveryFilter_.Create_DiscoveryFilter_(Aws_cryptography_materialProviders_DiscoveryFilter_accountIds_ToDafny(input.AccountIds), Aws_cryptography_materialProviders_DiscoveryFilter_partition_ToDafny(input.Partition)))
	}()
}

func Aws_cryptography_materialProviders_DiscoveryFilter_accountIds_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_AccountIdList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_AccountIdList_member_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_DiscoveryFilter_partition_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryMultiKeyringInput_regions_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_RegionList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_RegionList_member_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryMultiKeyringInput_discoveryFilter_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.DiscoveryFilter) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DiscoveryFilter_.Create_DiscoveryFilter_(Aws_cryptography_materialProviders_DiscoveryFilter_accountIds_ToDafny(input.AccountIds), Aws_cryptography_materialProviders_DiscoveryFilter_partition_ToDafny(input.Partition)))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsDiscoveryMultiKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_KeyAgreementScheme_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurations) AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations {
	return func() AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPublicKeyDiscovery:
			var inputToConversion = Aws_cryptography_materialProviders_KmsEcdhStaticConfigurations_KmsPublicKeyDiscovery_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPublicKeyDiscovery).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_KmsEcdhStaticConfigurations_{}.Create_KmsPublicKeyDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.KmsPublicKeyDiscoveryInput))
		case *awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPrivateKeyToStaticPublicKey:
			var inputToConversion = Aws_cryptography_materialProviders_KmsEcdhStaticConfigurations_KmsPrivateKeyToStaticPublicKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPrivateKeyToStaticPublicKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_KmsEcdhStaticConfigurations_{}.Create_KmsPrivateKeyToStaticPublicKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.KmsPrivateKeyToStaticPublicKeyInput))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_KmsEcdhStaticConfigurations_KmsPublicKeyDiscovery_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.KmsPublicKeyDiscoveryInput) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_KmsPublicKeyDiscoveryInput_.Create_KmsPublicKeyDiscoveryInput_(Aws_cryptography_materialProviders_KmsPublicKeyDiscoveryInput_recipientKmsIdentifier_ToDafny(input.RecipientKmsIdentifier)))
	}()
}

func Aws_cryptography_materialProviders_KmsPublicKeyDiscoveryInput_recipientKmsIdentifier_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_KmsEcdhStaticConfigurations_KmsPrivateKeyToStaticPublicKey_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.KmsPrivateKeyToStaticPublicKeyInput) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_KmsPrivateKeyToStaticPublicKeyInput_.Create_KmsPrivateKeyToStaticPublicKeyInput_(Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_senderKmsIdentifier_ToDafny(input.SenderKmsIdentifier), Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_senderPublicKey_ToDafny(input.SenderPublicKey), Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_recipientPublicKey_ToDafny(input.RecipientPublicKey)))
	}()
}

func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_senderKmsIdentifier_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_senderPublicKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_recipientPublicKey_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_curveSpec_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec) AwsCryptographyPrimitivesTypes.ECDHCurveSpec {
	return func() AwsCryptographyPrimitivesTypes.ECDHCurveSpec {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyPrimitivesTypes.CompanionStruct_ECDHCurveSpec_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyPrimitivesTypes.ECDHCurveSpec)
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_kmsClient_ToDafny(input *kms.Client) ComAmazonawsKmsTypes.IKMSClient {
	return &KMSwrapped.Shim{Client: input}
}

func Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_branchKeyId_ToDafny(input *string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(*input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}())
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_keyStore_ToDafny(input *awscryptographykeystoresmithygenerated.Client) AwsCryptographyKeyStoreTypes.IKeyStoreClient {
	return input.DafnyClient
}

func Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_ttlSeconds_ToDafny(input int64) int64 {
	return func() int64 {

		return input
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_cache_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.CacheType) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberDefault:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_Default_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberDefault).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_Default_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DefaultCache)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberNo:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_No_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberNo).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_No_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.NoCache)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberSingleThreaded:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_SingleThreaded_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberSingleThreaded).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_SingleThreaded_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.SingleThreadedCache)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberMultiThreaded:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_MultiThreaded_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberMultiThreaded).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_MultiThreaded_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.MultiThreadedCache)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberStormTracking:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_StormTracking_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberStormTracking).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_StormTracking_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.StormTrackingCache)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberShared:
			var inputToConversion = func() Wrappers.Option {
				if (input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberShared).Value) == nil {
					return Wrappers.Companion_Option_.Create_None_()
				}
				return Wrappers.Companion_Option_.Create_Some_(CryptographicMaterialsCache_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberShared).Value))
			}()
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_Shared_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache)))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_CacheType_Default_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DefaultCache) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DefaultCache_.Create_DefaultCache_(Aws_cryptography_materialProviders_DefaultCache_entryCapacity_ToDafny(input.EntryCapacity)))
	}()
}

func Aws_cryptography_materialProviders_DefaultCache_entryCapacity_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_CacheType_No_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.NoCache) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_NoCache_.Create_NoCache_())
	}()
}

func Aws_cryptography_materialProviders_CacheType_SingleThreaded_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.SingleThreadedCache) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_SingleThreadedCache_.Create_SingleThreadedCache_(Aws_cryptography_materialProviders_SingleThreadedCache_entryCapacity_ToDafny(input.EntryCapacity), Aws_cryptography_materialProviders_SingleThreadedCache_entryPruningTailSize_ToDafny(input.EntryPruningTailSize)))
	}()
}

func Aws_cryptography_materialProviders_SingleThreadedCache_entryCapacity_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_SingleThreadedCache_entryPruningTailSize_ToDafny(input *int32) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_CacheType_MultiThreaded_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.MultiThreadedCache) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_MultiThreadedCache_.Create_MultiThreadedCache_(Aws_cryptography_materialProviders_MultiThreadedCache_entryCapacity_ToDafny(input.EntryCapacity), Aws_cryptography_materialProviders_MultiThreadedCache_entryPruningTailSize_ToDafny(input.EntryPruningTailSize)))
	}()
}

func Aws_cryptography_materialProviders_MultiThreadedCache_entryCapacity_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_MultiThreadedCache_entryPruningTailSize_ToDafny(input *int32) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_CacheType_StormTracking_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.StormTrackingCache) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_StormTrackingCache_.Create_StormTrackingCache_(Aws_cryptography_materialProviders_StormTrackingCache_entryCapacity_ToDafny(input.EntryCapacity), Aws_cryptography_materialProviders_StormTrackingCache_entryPruningTailSize_ToDafny(input.EntryPruningTailSize), Aws_cryptography_materialProviders_StormTrackingCache_gracePeriod_ToDafny(input.GracePeriod), Aws_cryptography_materialProviders_StormTrackingCache_graceInterval_ToDafny(input.GraceInterval), Aws_cryptography_materialProviders_StormTrackingCache_fanOut_ToDafny(input.FanOut), Aws_cryptography_materialProviders_StormTrackingCache_inFlightTTL_ToDafny(input.InFlightTTL), Aws_cryptography_materialProviders_StormTrackingCache_sleepMilli_ToDafny(input.SleepMilli), Aws_cryptography_materialProviders_StormTrackingCache_timeUnits_ToDafny(input.TimeUnits)))
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_entryCapacity_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_entryPruningTailSize_ToDafny(input *int32) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_gracePeriod_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_graceInterval_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_fanOut_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_inFlightTTL_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_sleepMilli_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_StormTrackingCache_timeUnits_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.TimeUnits) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == *input {
				break
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_TimeUnits_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.TimeUnits))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsHierarchicalKeyringInput_partitionId_ToDafny(input *string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(*input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}())
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsKeyringInput_kmsKeyId_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsKeyringInput_kmsClient_ToDafny(input *kms.Client) ComAmazonawsKmsTypes.IKMSClient {
	return &KMSwrapped.Shim{Client: input}
}

func Aws_cryptography_materialProviders_CreateAwsKmsKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_kmsClient_ToDafny(input *kms.Client) ComAmazonawsKmsTypes.IKMSClient {
	return &KMSwrapped.Shim{Client: input}
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_discoveryFilter_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.DiscoveryFilter) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DiscoveryFilter_.Create_DiscoveryFilter_(Aws_cryptography_materialProviders_DiscoveryFilter_accountIds_ToDafny(input.AccountIds), Aws_cryptography_materialProviders_DiscoveryFilter_partition_ToDafny(input.Partition)))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryKeyringInput_region_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryMultiKeyringInput_regions_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_RegionList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryMultiKeyringInput_discoveryFilter_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.DiscoveryFilter) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DiscoveryFilter_.Create_DiscoveryFilter_(Aws_cryptography_materialProviders_DiscoveryFilter_accountIds_ToDafny(input.AccountIds), Aws_cryptography_materialProviders_DiscoveryFilter_partition_ToDafny(input.Partition)))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkDiscoveryMultiKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkKeyringInput_kmsKeyId_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkKeyringInput_kmsClient_ToDafny(input *kms.Client) ComAmazonawsKmsTypes.IKMSClient {
	return &KMSwrapped.Shim{Client: input}
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkMultiKeyringInput_generator_ToDafny(input *string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(*input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}())
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkMultiKeyringInput_kmsKeyIds_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_KmsKeyIdList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_KmsKeyIdList_member_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMrkMultiKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMultiKeyringInput_generator_ToDafny(input *string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(*input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}())
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMultiKeyringInput_kmsKeyIds_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_KmsKeyIdList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsMultiKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_publicKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_kmsKeyId_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_encryptionAlgorithm_ToDafny(input kmstypes.EncryptionAlgorithmSpec) ComAmazonawsKmsTypes.EncryptionAlgorithmSpec {
	return func() ComAmazonawsKmsTypes.EncryptionAlgorithmSpec {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(ComAmazonawsKmsTypes.CompanionStruct_EncryptionAlgorithmSpec_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(ComAmazonawsKmsTypes.EncryptionAlgorithmSpec)
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_kmsClient_ToDafny(input *kms.Client) Wrappers.Option {
	return func() Wrappers.Option {
		if (input) == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(&KMSwrapped.Shim{Client: input})
	}()
}

func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_grantTokens_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_GrantTokenList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_CreateCryptographicMaterialsCacheInput_cache_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.CacheType) AwsCryptographyMaterialProvidersTypes.CacheType {
	return func() AwsCryptographyMaterialProvidersTypes.CacheType {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberDefault:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_Default_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberDefault).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_Default_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DefaultCache))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberNo:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_No_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberNo).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_No_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.NoCache))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberSingleThreaded:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_SingleThreaded_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberSingleThreaded).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_SingleThreaded_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.SingleThreadedCache))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberMultiThreaded:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_MultiThreaded_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberMultiThreaded).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_MultiThreaded_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.MultiThreadedCache))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberStormTracking:
			var inputToConversion = Aws_cryptography_materialProviders_CacheType_StormTracking_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberStormTracking).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_StormTracking_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.StormTrackingCache))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberShared:
			var inputToConversion = func() Wrappers.Option {
				if (input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberShared).Value) == nil {
					return Wrappers.Companion_Option_.Create_None_()
				}
				return Wrappers.Companion_Option_.Create_Some_(CryptographicMaterialsCache_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CacheTypeMemberShared).Value))
			}()
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CacheType_{}.Create_Shared_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_CreateMultiKeyringInput_childKeyrings_ToDafny(input []awscryptographymaterialproviderssmithygeneratedtypes.IKeyring) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Keyring_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_keyNamespace_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_keyName_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingKey_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingAlg_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AesWrappingAlg) AwsCryptographyMaterialProvidersTypes.AesWrappingAlg {
	return func() AwsCryptographyMaterialProvidersTypes.AesWrappingAlg {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_AesWrappingAlg_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyMaterialProvidersTypes.AesWrappingAlg)
	}()
}

func Aws_cryptography_materialProviders_CreateRawEcdhKeyringInput_KeyAgreementScheme_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurations) AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations {
	return func() AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberPublicKeyDiscovery:
			var inputToConversion = Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_PublicKeyDiscovery_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberPublicKeyDiscovery).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_RawEcdhStaticConfigurations_{}.Create_PublicKeyDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.PublicKeyDiscoveryInput))
		case *awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberRawPrivateKeyToStaticPublicKey:
			var inputToConversion = Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberRawPrivateKeyToStaticPublicKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_RawEcdhStaticConfigurations_{}.Create_RawPrivateKeyToStaticPublicKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.RawPrivateKeyToStaticPublicKeyInput))
		case *awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberEphemeralPrivateKeyToStaticPublicKey:
			var inputToConversion = Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_EphemeralPrivateKeyToStaticPublicKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberEphemeralPrivateKeyToStaticPublicKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_RawEcdhStaticConfigurations_{}.Create_EphemeralPrivateKeyToStaticPublicKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.EphemeralPrivateKeyToStaticPublicKeyInput))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_PublicKeyDiscovery_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.PublicKeyDiscoveryInput) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_PublicKeyDiscoveryInput_.Create_PublicKeyDiscoveryInput_(Aws_cryptography_materialProviders_PublicKeyDiscoveryInput_recipientStaticPrivateKey_ToDafny(input.RecipientStaticPrivateKey)))
	}()
}

func Aws_cryptography_materialProviders_PublicKeyDiscoveryInput_recipientStaticPrivateKey_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.RawPrivateKeyToStaticPublicKeyInput) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_RawPrivateKeyToStaticPublicKeyInput_.Create_RawPrivateKeyToStaticPublicKeyInput_(Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_senderStaticPrivateKey_ToDafny(input.SenderStaticPrivateKey), Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_recipientPublicKey_ToDafny(input.RecipientPublicKey)))
	}()
}

func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_senderStaticPrivateKey_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_recipientPublicKey_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_EphemeralPrivateKeyToStaticPublicKey_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EphemeralPrivateKeyToStaticPublicKeyInput) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_EphemeralPrivateKeyToStaticPublicKeyInput_.Create_EphemeralPrivateKeyToStaticPublicKeyInput_(Aws_cryptography_materialProviders_EphemeralPrivateKeyToStaticPublicKeyInput_recipientPublicKey_ToDafny(input.RecipientPublicKey)))
	}()
}

func Aws_cryptography_materialProviders_EphemeralPrivateKeyToStaticPublicKeyInput_recipientPublicKey_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_CreateRawEcdhKeyringInput_curveSpec_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec) AwsCryptographyPrimitivesTypes.ECDHCurveSpec {
	return func() AwsCryptographyPrimitivesTypes.ECDHCurveSpec {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyPrimitivesTypes.CompanionStruct_ECDHCurveSpec_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyPrimitivesTypes.ECDHCurveSpec)
	}()
}

func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_keyNamespace_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_keyName_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_paddingScheme_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.PaddingScheme) AwsCryptographyMaterialProvidersTypes.PaddingScheme {
	return func() AwsCryptographyMaterialProvidersTypes.PaddingScheme {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_PaddingScheme_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyMaterialProvidersTypes.PaddingScheme)
	}()
}

func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_publicKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_privateKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_CreateRequiredEncryptionContextCMMInput_requiredEncryptionContextKeys_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return dafny.SeqOf(func() []interface{} {
			if !utf8.ValidString(input) {
				panic("invalid utf8 input provided")
			}
			b := []byte(input)
			f := make([]interface{}, len(b))
			for i, v := range b {
				f[i] = v
			}
			return f
		}()...)
	}()
}

func Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteInfo) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo {

		return AwsCryptographyMaterialProvidersTypes.Companion_AlgorithmSuiteInfo_.Create_AlgorithmSuiteInfo_(Aws_cryptography_materialProviders_AlgorithmSuiteInfo_id_ToDafny(input.Id), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_binaryId_ToDafny(input.BinaryId), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_messageVersion_ToDafny(input.MessageVersion), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_encrypt_ToDafny(input.Encrypt), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_kdf_ToDafny(input.Kdf), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_commitment_ToDafny(input.Commitment), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_signature_ToDafny(input.Signature), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_symmetricSignature_ToDafny(input.SymmetricSignature), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_edkWrapping_ToDafny(input.EdkWrapping))
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_id_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) Wrappers.Option {
	return func() Wrappers.Option {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DBEAlgorithmSuiteId) Wrappers.Option {
	return func() Wrappers.Option {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_DBEAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_binaryId_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_messageVersion_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_encrypt_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.Encrypt) AwsCryptographyMaterialProvidersTypes.Encrypt {
	return func() AwsCryptographyMaterialProvidersTypes.Encrypt {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.EncryptMemberAES_GCM:
			var inputToConversion = Aws_cryptography_materialProviders_Encrypt_AES_GCM_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.EncryptMemberAES_GCM).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Encrypt_{}.Create_AES__GCM_(inputToConversion.UnwrapOr(nil).(AwsCryptographyPrimitivesTypes.AES__GCM))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_Encrypt_AES_GCM_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.AES_GCM) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyPrimitivesTypes.Companion_AES__GCM_.Create_AES__GCM_(awscryptographyprimitivessmithygenerated.Aws_cryptography_primitives_AES_GCM_keyLength_ToDafny(input.KeyLength), awscryptographyprimitivessmithygenerated.Aws_cryptography_primitives_AES_GCM_tagLength_ToDafny(input.TagLength), awscryptographyprimitivessmithygenerated.Aws_cryptography_primitives_AES_GCM_ivLength_ToDafny(input.IvLength)))
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_kdf_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithm) AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_HKDF_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_HKDF_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.HKDF))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_IDENTITY_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_IDENTITY_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IDENTITY))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_None_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_None_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.None))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_DerivationAlgorithm_HKDF_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.HKDF) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_HKDF_.Create_HKDF_(Aws_cryptography_materialProviders_HKDF_hmac_ToDafny(input.Hmac), Aws_cryptography_materialProviders_HKDF_saltLength_ToDafny(input.SaltLength), Aws_cryptography_materialProviders_HKDF_inputKeyLength_ToDafny(input.InputKeyLength), Aws_cryptography_materialProviders_HKDF_outputKeyLength_ToDafny(input.OutputKeyLength)))
	}()
}

func Aws_cryptography_materialProviders_HKDF_hmac_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm) AwsCryptographyPrimitivesTypes.DigestAlgorithm {
	return func() AwsCryptographyPrimitivesTypes.DigestAlgorithm {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyPrimitivesTypes.CompanionStruct_DigestAlgorithm_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyPrimitivesTypes.DigestAlgorithm)
	}()
}

func Aws_cryptography_materialProviders_HKDF_saltLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_HKDF_inputKeyLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_HKDF_outputKeyLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_DerivationAlgorithm_IDENTITY_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.IDENTITY) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_IDENTITY_.Create_IDENTITY_())
	}()
}

func Aws_cryptography_materialProviders_DerivationAlgorithm_None_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.None) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_None_.Create_None_())
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_commitment_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithm) AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_HKDF_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_HKDF_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.HKDF))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_IDENTITY_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_IDENTITY_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IDENTITY))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_None_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_None_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.None))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_signature_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.SignatureAlgorithm) AwsCryptographyMaterialProvidersTypes.SignatureAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.SignatureAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.SignatureAlgorithmMemberECDSA:
			var inputToConversion = Aws_cryptography_materialProviders_SignatureAlgorithm_ECDSA_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.SignatureAlgorithmMemberECDSA).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_SignatureAlgorithm_{}.Create_ECDSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ECDSA))
		case *awscryptographymaterialproviderssmithygeneratedtypes.SignatureAlgorithmMemberNone:
			var inputToConversion = Aws_cryptography_materialProviders_SignatureAlgorithm_None_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.SignatureAlgorithmMemberNone).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_SignatureAlgorithm_{}.Create_None_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.None))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_SignatureAlgorithm_ECDSA_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ECDSA) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_ECDSA_.Create_ECDSA_(Aws_cryptography_materialProviders_ECDSA_curve_ToDafny(input.Curve)))
	}()
}

func Aws_cryptography_materialProviders_ECDSA_curve_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECDSASignatureAlgorithm) AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm {
	return func() AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyPrimitivesTypes.CompanionStruct_ECDSASignatureAlgorithm_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm)
	}()
}

func Aws_cryptography_materialProviders_SignatureAlgorithm_None_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.None) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_None_.Create_None_())
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_symmetricSignature_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.SymmetricSignatureAlgorithm) AwsCryptographyMaterialProvidersTypes.SymmetricSignatureAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.SymmetricSignatureAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.SymmetricSignatureAlgorithmMemberHMAC:
			var inputToConversion = Aws_cryptography_materialProviders_SymmetricSignatureAlgorithm_HMAC_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.SymmetricSignatureAlgorithmMemberHMAC).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_SymmetricSignatureAlgorithm_{}.Create_HMAC_(inputToConversion.UnwrapOr(nil).(AwsCryptographyPrimitivesTypes.DigestAlgorithm))
		case *awscryptographymaterialproviderssmithygeneratedtypes.SymmetricSignatureAlgorithmMemberNone:
			var inputToConversion = Aws_cryptography_materialProviders_SymmetricSignatureAlgorithm_None_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.SymmetricSignatureAlgorithmMemberNone).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_SymmetricSignatureAlgorithm_{}.Create_None_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.None))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_SymmetricSignatureAlgorithm_HMAC_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm) Wrappers.Option {
	return func() Wrappers.Option {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyPrimitivesTypes.CompanionStruct_DigestAlgorithm_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyPrimitivesTypes.DigestAlgorithm))
	}()
}

func Aws_cryptography_materialProviders_SymmetricSignatureAlgorithm_None_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.None) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_None_.Create_None_())
	}()
}

func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_edkWrapping_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EdkWrappingAlgorithm) AwsCryptographyMaterialProvidersTypes.EdkWrappingAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.EdkWrappingAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.EdkWrappingAlgorithmMemberDIRECT_KEY_WRAPPING:
			var inputToConversion = Aws_cryptography_materialProviders_EdkWrappingAlgorithm_DIRECT_KEY_WRAPPING_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.EdkWrappingAlgorithmMemberDIRECT_KEY_WRAPPING).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_EdkWrappingAlgorithm_{}.Create_DIRECT__KEY__WRAPPING_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DIRECT__KEY__WRAPPING))
		case *awscryptographymaterialproviderssmithygeneratedtypes.EdkWrappingAlgorithmMemberIntermediateKeyWrapping:
			var inputToConversion = Aws_cryptography_materialProviders_EdkWrappingAlgorithm_IntermediateKeyWrapping_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.EdkWrappingAlgorithmMemberIntermediateKeyWrapping).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_EdkWrappingAlgorithm_{}.Create_IntermediateKeyWrapping_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IntermediateKeyWrapping))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_EdkWrappingAlgorithm_DIRECT_KEY_WRAPPING_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DIRECT_KEY_WRAPPING) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DIRECT__KEY__WRAPPING_.Create_DIRECT__KEY__WRAPPING_())
	}()
}

func Aws_cryptography_materialProviders_EdkWrappingAlgorithm_IntermediateKeyWrapping_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.IntermediateKeyWrapping) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_IntermediateKeyWrapping_.Create_IntermediateKeyWrapping_(Aws_cryptography_materialProviders_IntermediateKeyWrapping_keyEncryptionKeyKdf_ToDafny(input.KeyEncryptionKeyKdf), Aws_cryptography_materialProviders_IntermediateKeyWrapping_macKeyKdf_ToDafny(input.MacKeyKdf), Aws_cryptography_materialProviders_IntermediateKeyWrapping_pdkEncryptAlgorithm_ToDafny(input.PdkEncryptAlgorithm)))
	}()
}

func Aws_cryptography_materialProviders_IntermediateKeyWrapping_keyEncryptionKeyKdf_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithm) AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_HKDF_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_HKDF_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.HKDF))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_IDENTITY_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_IDENTITY_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IDENTITY))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_None_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_None_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.None))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_IntermediateKeyWrapping_macKeyKdf_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithm) AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {
	return func() AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_HKDF_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberHKDF).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_HKDF_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.HKDF))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_IDENTITY_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberIDENTITY).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_IDENTITY_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IDENTITY))
		case *awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone:
			var inputToConversion = Aws_cryptography_materialProviders_DerivationAlgorithm_None_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.DerivationAlgorithmMemberNone).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_DerivationAlgorithm_{}.Create_None_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.None))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_IntermediateKeyWrapping_pdkEncryptAlgorithm_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.Encrypt) AwsCryptographyMaterialProvidersTypes.Encrypt {
	return func() AwsCryptographyMaterialProvidersTypes.Encrypt {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.EncryptMemberAES_GCM:
			var inputToConversion = Aws_cryptography_materialProviders_Encrypt_AES_GCM_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.EncryptMemberAES_GCM).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Encrypt_{}.Create_AES__GCM_(inputToConversion.UnwrapOr(nil).(AwsCryptographyPrimitivesTypes.AES__GCM))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return dafny.SeqOf(func() []interface{} {
			if !utf8.ValidString(input) {
				panic("invalid utf8 input provided")
			}
			b := []byte(input)
			f := make([]interface{}, len(b))
			for i, v := range b {
				f[i] = v
			}
			return f
		}()...)
	}()
}

func Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return dafny.SeqOf(func() []interface{} {
			if !utf8.ValidString(input) {
				panic("invalid utf8 input provided")
			}
			b := []byte(input)
			f := make([]interface{}, len(b))
			for i, v := range b {
				f[i] = v
			}
			return f
		}()...)
	}()
}

func Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteInfo) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo {

		return AwsCryptographyMaterialProvidersTypes.Companion_AlgorithmSuiteInfo_.Create_AlgorithmSuiteInfo_(Aws_cryptography_materialProviders_AlgorithmSuiteInfo_id_ToDafny(input.Id), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_binaryId_ToDafny(input.BinaryId), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_messageVersion_ToDafny(input.MessageVersion), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_encrypt_ToDafny(input.Encrypt), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_kdf_ToDafny(input.Kdf), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_commitment_ToDafny(input.Commitment), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_signature_ToDafny(input.Signature), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_symmetricSignature_ToDafny(input.SymmetricSignature), Aws_cryptography_materialProviders_AlgorithmSuiteInfo_edkWrapping_ToDafny(input.EdkWrapping))
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input []awscryptographymaterialproviderssmithygeneratedtypes.EncryptedDataKey) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptedDataKeyList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_EncryptedDataKeyList_member_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptedDataKey) AwsCryptographyMaterialProvidersTypes.EncryptedDataKey {
	return func() AwsCryptographyMaterialProvidersTypes.EncryptedDataKey {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptedDataKey_.Create_EncryptedDataKey_(Aws_cryptography_materialProviders_EncryptedDataKey_keyProviderId_ToDafny(input.KeyProviderId), Aws_cryptography_materialProviders_EncryptedDataKey_keyProviderInfo_ToDafny(input.KeyProviderInfo), Aws_cryptography_materialProviders_EncryptedDataKey_ciphertext_ToDafny(input.Ciphertext))
	}()
}

func Aws_cryptography_materialProviders_EncryptedDataKey_keyProviderId_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return dafny.SeqOf(func() []interface{} {
			if !utf8.ValidString(input) {
				panic("invalid utf8 input provided")
			}
			b := []byte(input)
			f := make([]interface{}, len(b))
			for i, v := range b {
				f[i] = v
			}
			return f
		}()...)
	}()
}

func Aws_cryptography_materialProviders_EncryptedDataKey_keyProviderInfo_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_EncryptedDataKey_ciphertext_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input [][]byte) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_SymmetricSigningKeyList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_SymmetricSigningKeyList_member_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_GetAlgorithmSuiteInfoInput_binaryId_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_requiredEncryptionContextKeys_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_requiredEncryptionContextKeys_ToDafny(input []string) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_signingKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_verificationKey_ToDafny(input []byte) Wrappers.Option {
	return func() Wrappers.Option {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		for _, e := range input {
			v = append(v, e)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
	}()
}

func Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnDecryptInput_algorithm_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnDecryptInput_commitmentPolicy_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicy) AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {
	return func() AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBECommitmentPolicy))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_CommitmentPolicy_ESDK_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy) Wrappers.Option {
	return func() Wrappers.Option {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy))
	}()
}

func Aws_cryptography_materialProviders_CommitmentPolicy_DBE_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DBECommitmentPolicy) Wrappers.Option {
	return func() Wrappers.Option {

		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == input {
				break
			}
			if index == len(input.Values()) {
				panic("Input value did not found in enum values")
			}

		}
		var enum interface{}
		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_DBECommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.DBECommitmentPolicy))
	}()
}

func Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnEncryptInput_algorithm_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnEncryptInput_commitmentPolicy_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicy) AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {
	return func() AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBECommitmentPolicy))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_ValidDecryptionMaterialsTransitionInput_start_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input.SymmetricSigningKey))
	}()
}

func Aws_cryptography_materialProviders_ValidDecryptionMaterialsTransitionInput_stop_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input.SymmetricSigningKey))
	}()
}

func Aws_cryptography_materialProviders_ValidEncryptionMaterialsTransitionInput_start_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input.SymmetricSigningKeys))
	}()
}

func Aws_cryptography_materialProviders_ValidEncryptionMaterialsTransitionInput_stop_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input.SymmetricSigningKeys))
	}()
}

func Aws_cryptography_materialProviders_GetBranchKeyIdInput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_GetBranchKeyIdOutput_branchKeyId_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_GetClientInput_region_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_GetClientOutput_client_ToDafny(input *kms.Client) ComAmazonawsKmsTypes.IKMSClient {
	return &KMSwrapped.Shim{Client: input}
}

func Aws_cryptography_materialProviders_DeleteCacheEntryInput_identifier_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryInput_identifier_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryInput_bytesUsed_ToDafny(input *int64) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryOutput_materials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.Materials) AwsCryptographyMaterialProvidersTypes.Materials {
	return func() AwsCryptographyMaterialProvidersTypes.Materials {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberEncryption:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_Encryption_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberEncryption).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_Encryption_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.EncryptionMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberDecryption:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_Decryption_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberDecryption).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_Decryption_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DecryptionMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBranchKey:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_BranchKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBranchKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_BranchKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyKeyStoreTypes.BranchKeyMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBeaconKey:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_BeaconKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBeaconKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_BeaconKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyKeyStoreTypes.BeaconKeyMaterials))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_Materials_Encryption_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input.SymmetricSigningKeys)))
	}()
}

func Aws_cryptography_materialProviders_Materials_Decryption_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input.SymmetricSigningKey)))
	}()
}

func Aws_cryptography_materialProviders_Materials_BranchKey_ToDafny(input awscryptographykeystoresmithygeneratedtypes.BranchKeyMaterials) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyKeyStoreTypes.Companion_BranchKeyMaterials_.Create_BranchKeyMaterials_(awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BranchKeyMaterials_branchKeyIdentifier_ToDafny(input.BranchKeyIdentifier), awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BranchKeyMaterials_branchKeyVersion_ToDafny(input.BranchKeyVersion), awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BranchKeyMaterials_encryptionContext_ToDafny(input.EncryptionContext), awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BranchKeyMaterials_branchKey_ToDafny(input.BranchKey)))
	}()
}

func Aws_cryptography_materialProviders_Materials_BeaconKey_ToDafny(input awscryptographykeystoresmithygeneratedtypes.BeaconKeyMaterials) Wrappers.Option {
	return func() Wrappers.Option {

		return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyKeyStoreTypes.Companion_BeaconKeyMaterials_.Create_BeaconKeyMaterials_(awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BeaconKeyMaterials_beaconKeyIdentifier_ToDafny(input.BeaconKeyIdentifier), awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BeaconKeyMaterials_encryptionContext_ToDafny(input.EncryptionContext), awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BeaconKeyMaterials_beaconKey_ToDafny(input.BeaconKey), awscryptographykeystoresmithygenerated.Aws_cryptography_keyStore_BeaconKeyMaterials_hmacKeys_ToDafny(input.HmacKeys)))
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryOutput_creationTime_ToDafny(input int64) int64 {
	return func() int64 {

		return input
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryOutput_expiryTime_ToDafny(input int64) int64 {
	return func() int64 {

		return input
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryOutput_messagesUsed_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_GetCacheEntryOutput_bytesUsed_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_PutCacheEntryInput_identifier_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_PutCacheEntryInput_materials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.Materials) AwsCryptographyMaterialProvidersTypes.Materials {
	return func() AwsCryptographyMaterialProvidersTypes.Materials {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberEncryption:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_Encryption_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberEncryption).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_Encryption_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.EncryptionMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberDecryption:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_Decryption_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberDecryption).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_Decryption_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DecryptionMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBranchKey:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_BranchKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBranchKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_BranchKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyKeyStoreTypes.BranchKeyMaterials))
		case *awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBeaconKey:
			var inputToConversion = Aws_cryptography_materialProviders_Materials_BeaconKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.MaterialsMemberBeaconKey).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_Materials_{}.Create_BeaconKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyKeyStoreTypes.BeaconKeyMaterials))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_PutCacheEntryInput_creationTime_ToDafny(input int64) int64 {
	return func() int64 {

		return input
	}()
}

func Aws_cryptography_materialProviders_PutCacheEntryInput_expiryTime_ToDafny(input int64) int64 {
	return func() int64 {

		return input
	}()
}

func Aws_cryptography_materialProviders_PutCacheEntryInput_messagesUsed_ToDafny(input *int32) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_PutCacheEntryInput_bytesUsed_ToDafny(input *int32) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_UpdateUsageMetadataInput_identifier_ToDafny(input []byte) dafny.Sequence {
	return func() dafny.Sequence {
		v := make([]interface{}, 0, len(input))
		if input == nil {
			return nil
		}
		for _, e := range input {
			v = append(v, e)
		}
		return dafny.SeqFromArray(v, false)
	}()
}

func Aws_cryptography_materialProviders_UpdateUsageMetadataInput_bytesUsed_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_materialProviders_DecryptMaterialsInput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_DecryptMaterialsInput_commitmentPolicy_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicy) AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {
	return func() AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBECommitmentPolicy))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_DecryptMaterialsInput_encryptedDataKeys_ToDafny(input []awscryptographymaterialproviderssmithygeneratedtypes.EncryptedDataKey) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptedDataKeyList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_DecryptMaterialsInput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_DecryptMaterialsInput_reproducedEncryptionContext_ToDafny(input map[string]string) Wrappers.Option {
	return func() Wrappers.Option {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap())
	}()
}

func Aws_cryptography_materialProviders_DecryptMaterialsOutput_decryptionMaterials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input.SymmetricSigningKey))
	}()
}

func Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_commitmentPolicy_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicy) AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {
	return func() AwsCryptographyMaterialProvidersTypes.CommitmentPolicy {

		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberESDK).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy))
		case *awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_CommitmentPolicy_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.CommitmentPolicyMemberDBE).Value)
			return AwsCryptographyMaterialProvidersTypes.CompanionStruct_CommitmentPolicy_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBECommitmentPolicy))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_ESDK_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberESDK).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_ESDK_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE:
			var inputToConversion = Aws_cryptography_materialProviders_AlgorithmSuiteId_DBE_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteIdMemberDBE).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_AlgorithmSuiteId_{}.Create_DBE_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId)))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_maxPlaintextLength_ToDafny(input *int64) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		return Wrappers.Companion_Option_.Create_Some_(*input)
	}()
}

func Aws_cryptography_materialProviders_GetEncryptionMaterialsInput_requiredEncryptionContextKeys_ToDafny(input []string) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOf(fieldValue...))
	}()
}

func Aws_cryptography_materialProviders_GetEncryptionMaterialsOutput_encryptionMaterials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input.SymmetricSigningKeys))
	}()
}

func Aws_cryptography_materialProviders_OnDecryptInput_materials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input.SymmetricSigningKey))
	}()
}

func Aws_cryptography_materialProviders_OnDecryptInput_encryptedDataKeys_ToDafny(input []awscryptographymaterialproviderssmithygeneratedtypes.EncryptedDataKey) dafny.Sequence {
	return func() dafny.Sequence {

		var fieldValue []interface{} = make([]interface{}, 0, len(input))
		for _, val := range input {
			element := Aws_cryptography_materialProviders_EncryptedDataKeyList_member_ToDafny(val)
			fieldValue = append(fieldValue, element)
		}
		return dafny.SeqOf(fieldValue...)
	}()
}

func Aws_cryptography_materialProviders_OnDecryptOutput_materials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.DecryptionMaterials) AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.DecryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_DecryptionMaterials_.Create_DecryptionMaterials_(Aws_cryptography_materialProviders_DecryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_DecryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_DecryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_ToDafny(input.VerificationKey), Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_ToDafny(input.SymmetricSigningKey))
	}()
}

func Aws_cryptography_materialProviders_OnEncryptInput_materials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input.SymmetricSigningKeys))
	}()
}

func Aws_cryptography_materialProviders_OnEncryptOutput_materials_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.EncryptionMaterials) AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {
	return func() AwsCryptographyMaterialProvidersTypes.EncryptionMaterials {

		return AwsCryptographyMaterialProvidersTypes.Companion_EncryptionMaterials_.Create_EncryptionMaterials_(Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_ToDafny(input.AlgorithmSuite), Aws_cryptography_materialProviders_EncryptionMaterials_encryptionContext_ToDafny(input.EncryptionContext), Aws_cryptography_materialProviders_EncryptionMaterials_encryptedDataKeys_ToDafny(input.EncryptedDataKeys), Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys), Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_ToDafny(input.PlaintextDataKey), Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_ToDafny(input.SigningKey), Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_ToDafny(input.SymmetricSigningKeys))
	}()
}

func Aws_cryptography_materialProviders_AwsCryptographicMaterialProvidersException_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_EntryAlreadyExists_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_EntryDoesNotExist_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InFlightTTLExceeded_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidAlgorithmSuiteInfo_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidAlgorithmSuiteInfoOnDecrypt_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidAlgorithmSuiteInfoOnEncrypt_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidDecryptionMaterials_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidDecryptionMaterialsTransition_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidEncryptionMaterials_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_InvalidEncryptionMaterialsTransition_message_ToDafny(input string) dafny.Sequence {
	return func() dafny.Sequence {

		return func() dafny.Sequence {
			res, err := UTF8.DecodeFromNativeGoByteArray([]byte(input))
			if err != nil {
				panic("invalid utf8 input provided")
			}
			return res
		}()
	}()
}

func Aws_cryptography_materialProviders_StaticConfigurations_AWS_KMS_ECDH_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurations) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPublicKeyDiscovery:
			var inputToConversion = Aws_cryptography_materialProviders_KmsEcdhStaticConfigurations_KmsPublicKeyDiscovery_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPublicKeyDiscovery).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_KmsEcdhStaticConfigurations_{}.Create_KmsPublicKeyDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.KmsPublicKeyDiscoveryInput)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPrivateKeyToStaticPublicKey:
			var inputToConversion = Aws_cryptography_materialProviders_KmsEcdhStaticConfigurations_KmsPrivateKeyToStaticPublicKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.KmsEcdhStaticConfigurationsMemberKmsPrivateKeyToStaticPublicKey).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_KmsEcdhStaticConfigurations_{}.Create_KmsPrivateKeyToStaticPublicKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.KmsPrivateKeyToStaticPublicKeyInput)))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_StaticConfigurations_RAW_ECDH_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurations) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberPublicKeyDiscovery:
			var inputToConversion = Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_PublicKeyDiscovery_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberPublicKeyDiscovery).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_RawEcdhStaticConfigurations_{}.Create_PublicKeyDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.PublicKeyDiscoveryInput)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberRawPrivateKeyToStaticPublicKey:
			var inputToConversion = Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberRawPrivateKeyToStaticPublicKey).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_RawEcdhStaticConfigurations_{}.Create_RawPrivateKeyToStaticPublicKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.RawPrivateKeyToStaticPublicKeyInput)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberEphemeralPrivateKeyToStaticPublicKey:
			var inputToConversion = Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_EphemeralPrivateKeyToStaticPublicKey_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.RawEcdhStaticConfigurationsMemberEphemeralPrivateKeyToStaticPublicKey).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_RawEcdhStaticConfigurations_{}.Create_EphemeralPrivateKeyToStaticPublicKey_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.EphemeralPrivateKeyToStaticPublicKeyInput)))

		default:
			panic("Unhandled union type")
		}
	}()
}

func Aws_cryptography_materialProviders_KeyAgreementScheme_StaticConfiguration_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurations) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		switch input.(type) {
		case *awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberAWS_KMS_ECDH:
			var inputToConversion = Aws_cryptography_materialProviders_StaticConfigurations_AWS_KMS_ECDH_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberAWS_KMS_ECDH).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_StaticConfigurations_{}.Create_AWS__KMS__ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations)))
		case *awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberRAW_ECDH:
			var inputToConversion = Aws_cryptography_materialProviders_StaticConfigurations_RAW_ECDH_ToDafny(input.(*awscryptographymaterialproviderssmithygeneratedtypes.StaticConfigurationsMemberRAW_ECDH).Value)
			return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTypes.CompanionStruct_StaticConfigurations_{}.Create_RAW__ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations)))

		default:
			panic("Unhandled union type")
		}
	}()
}