AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/awscryptographyprimitivessmithygenerated/to_dafny.go

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

package awscryptographyprimitivessmithygenerated

import (
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/AwsCryptographyPrimitivesTypes"
	"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/dafny-lang/DafnyRuntimeGo/v4/dafny"
)

func AESDecryptInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.AESDecryptInput) AwsCryptographyPrimitivesTypes.AESDecryptInput {

	return func() AwsCryptographyPrimitivesTypes.AESDecryptInput {

		return AwsCryptographyPrimitivesTypes.Companion_AESDecryptInput_.Create_AESDecryptInput_(Aws_cryptography_primitives_AESDecryptInput_encAlg_ToDafny(nativeInput.EncAlg), Aws_cryptography_primitives_AESDecryptInput_key_ToDafny(nativeInput.Key), Aws_cryptography_primitives_AESDecryptInput_cipherTxt_ToDafny(nativeInput.CipherTxt), Aws_cryptography_primitives_AESDecryptInput_authTag_ToDafny(nativeInput.AuthTag), Aws_cryptography_primitives_AESDecryptInput_iv_ToDafny(nativeInput.Iv), Aws_cryptography_primitives_AESDecryptInput_aad_ToDafny(nativeInput.Aad))
	}()

}

func AESEncryptInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.AESEncryptInput) AwsCryptographyPrimitivesTypes.AESEncryptInput {

	return func() AwsCryptographyPrimitivesTypes.AESEncryptInput {

		return AwsCryptographyPrimitivesTypes.Companion_AESEncryptInput_.Create_AESEncryptInput_(Aws_cryptography_primitives_AESEncryptInput_encAlg_ToDafny(nativeInput.EncAlg), Aws_cryptography_primitives_AESEncryptInput_iv_ToDafny(nativeInput.Iv), Aws_cryptography_primitives_AESEncryptInput_key_ToDafny(nativeInput.Key), Aws_cryptography_primitives_AESEncryptInput_msg_ToDafny(nativeInput.Msg), Aws_cryptography_primitives_AESEncryptInput_aad_ToDafny(nativeInput.Aad))
	}()

}

func AESEncryptOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.AESEncryptOutput) AwsCryptographyPrimitivesTypes.AESEncryptOutput {

	return func() AwsCryptographyPrimitivesTypes.AESEncryptOutput {

		return AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Create_AESEncryptOutput_(Aws_cryptography_primitives_AESEncryptOutput_cipherText_ToDafny(nativeOutput.CipherText), Aws_cryptography_primitives_AESEncryptOutput_authTag_ToDafny(nativeOutput.AuthTag))
	}()

}

func AesKdfCtrInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.AesKdfCtrInput) AwsCryptographyPrimitivesTypes.AesKdfCtrInput {

	return func() AwsCryptographyPrimitivesTypes.AesKdfCtrInput {

		return AwsCryptographyPrimitivesTypes.Companion_AesKdfCtrInput_.Create_AesKdfCtrInput_(Aws_cryptography_primitives_AesKdfCtrInput_ikm_ToDafny(nativeInput.Ikm), Aws_cryptography_primitives_AesKdfCtrInput_expectedLength_ToDafny(nativeInput.ExpectedLength), Aws_cryptography_primitives_AesKdfCtrInput_nonce_ToDafny(nativeInput.Nonce))
	}()

}

func CompressPublicKeyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.CompressPublicKeyInput) AwsCryptographyPrimitivesTypes.CompressPublicKeyInput {

	return func() AwsCryptographyPrimitivesTypes.CompressPublicKeyInput {

		return AwsCryptographyPrimitivesTypes.Companion_CompressPublicKeyInput_.Create_CompressPublicKeyInput_(Aws_cryptography_primitives_CompressPublicKeyInput_publicKey_ToDafny(nativeInput.PublicKey), Aws_cryptography_primitives_CompressPublicKeyInput_eccCurve_ToDafny(nativeInput.EccCurve))
	}()

}

func CompressPublicKeyOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.CompressPublicKeyOutput) AwsCryptographyPrimitivesTypes.CompressPublicKeyOutput {

	return func() AwsCryptographyPrimitivesTypes.CompressPublicKeyOutput {

		return AwsCryptographyPrimitivesTypes.Companion_CompressPublicKeyOutput_.Create_CompressPublicKeyOutput_(Aws_cryptography_primitives_CompressPublicKeyOutput_compressedPublicKey_ToDafny(nativeOutput.CompressedPublicKey))
	}()

}

func DecompressPublicKeyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.DecompressPublicKeyInput) AwsCryptographyPrimitivesTypes.DecompressPublicKeyInput {

	return func() AwsCryptographyPrimitivesTypes.DecompressPublicKeyInput {

		return AwsCryptographyPrimitivesTypes.Companion_DecompressPublicKeyInput_.Create_DecompressPublicKeyInput_(Aws_cryptography_primitives_DecompressPublicKeyInput_compressedPublicKey_ToDafny(nativeInput.CompressedPublicKey), Aws_cryptography_primitives_DecompressPublicKeyInput_eccCurve_ToDafny(nativeInput.EccCurve))
	}()

}

func DecompressPublicKeyOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.DecompressPublicKeyOutput) AwsCryptographyPrimitivesTypes.DecompressPublicKeyOutput {

	return func() AwsCryptographyPrimitivesTypes.DecompressPublicKeyOutput {

		return AwsCryptographyPrimitivesTypes.Companion_DecompressPublicKeyOutput_.Create_DecompressPublicKeyOutput_(Aws_cryptography_primitives_DecompressPublicKeyOutput_publicKey_ToDafny(nativeOutput.PublicKey))
	}()

}

func DeriveSharedSecretInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.DeriveSharedSecretInput) AwsCryptographyPrimitivesTypes.DeriveSharedSecretInput {

	return func() AwsCryptographyPrimitivesTypes.DeriveSharedSecretInput {

		return AwsCryptographyPrimitivesTypes.Companion_DeriveSharedSecretInput_.Create_DeriveSharedSecretInput_(Aws_cryptography_primitives_DeriveSharedSecretInput_eccCurve_ToDafny(nativeInput.EccCurve), Aws_cryptography_primitives_DeriveSharedSecretInput_privateKey_ToDafny(nativeInput.PrivateKey), Aws_cryptography_primitives_DeriveSharedSecretInput_publicKey_ToDafny(nativeInput.PublicKey))
	}()

}

func DeriveSharedSecretOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.DeriveSharedSecretOutput) AwsCryptographyPrimitivesTypes.DeriveSharedSecretOutput {

	return func() AwsCryptographyPrimitivesTypes.DeriveSharedSecretOutput {

		return AwsCryptographyPrimitivesTypes.Companion_DeriveSharedSecretOutput_.Create_DeriveSharedSecretOutput_(Aws_cryptography_primitives_DeriveSharedSecretOutput_sharedSecret_ToDafny(nativeOutput.SharedSecret))
	}()

}

func DigestInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.DigestInput) AwsCryptographyPrimitivesTypes.DigestInput {

	return func() AwsCryptographyPrimitivesTypes.DigestInput {

		return AwsCryptographyPrimitivesTypes.Companion_DigestInput_.Create_DigestInput_(Aws_cryptography_primitives_DigestInput_digestAlgorithm_ToDafny(nativeInput.DigestAlgorithm), Aws_cryptography_primitives_DigestInput_message_ToDafny(nativeInput.Message))
	}()

}

func ECDSASignInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.ECDSASignInput) AwsCryptographyPrimitivesTypes.ECDSASignInput {

	return func() AwsCryptographyPrimitivesTypes.ECDSASignInput {

		return AwsCryptographyPrimitivesTypes.Companion_ECDSASignInput_.Create_ECDSASignInput_(Aws_cryptography_primitives_ECDSASignInput_signatureAlgorithm_ToDafny(nativeInput.SignatureAlgorithm), Aws_cryptography_primitives_ECDSASignInput_signingKey_ToDafny(nativeInput.SigningKey), Aws_cryptography_primitives_ECDSASignInput_message_ToDafny(nativeInput.Message))
	}()

}

func ECDSAVerifyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.ECDSAVerifyInput) AwsCryptographyPrimitivesTypes.ECDSAVerifyInput {

	return func() AwsCryptographyPrimitivesTypes.ECDSAVerifyInput {

		return AwsCryptographyPrimitivesTypes.Companion_ECDSAVerifyInput_.Create_ECDSAVerifyInput_(Aws_cryptography_primitives_ECDSAVerifyInput_signatureAlgorithm_ToDafny(nativeInput.SignatureAlgorithm), Aws_cryptography_primitives_ECDSAVerifyInput_verificationKey_ToDafny(nativeInput.VerificationKey), Aws_cryptography_primitives_ECDSAVerifyInput_message_ToDafny(nativeInput.Message), Aws_cryptography_primitives_ECDSAVerifyInput_signature_ToDafny(nativeInput.Signature))
	}()

}

func GenerateECCKeyPairInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.GenerateECCKeyPairInput) AwsCryptographyPrimitivesTypes.GenerateECCKeyPairInput {

	return func() AwsCryptographyPrimitivesTypes.GenerateECCKeyPairInput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateECCKeyPairInput_.Create_GenerateECCKeyPairInput_(Aws_cryptography_primitives_GenerateECCKeyPairInput_eccCurve_ToDafny(nativeInput.EccCurve))
	}()

}

func GenerateECCKeyPairOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.GenerateECCKeyPairOutput) AwsCryptographyPrimitivesTypes.GenerateECCKeyPairOutput {

	return func() AwsCryptographyPrimitivesTypes.GenerateECCKeyPairOutput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateECCKeyPairOutput_.Create_GenerateECCKeyPairOutput_(Aws_cryptography_primitives_GenerateECCKeyPairOutput_eccCurve_ToDafny(nativeOutput.EccCurve), Aws_cryptography_primitives_GenerateECCKeyPairOutput_privateKey_ToDafny(nativeOutput.PrivateKey), Aws_cryptography_primitives_GenerateECCKeyPairOutput_publicKey_ToDafny(nativeOutput.PublicKey))
	}()

}

func GenerateECDSASignatureKeyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.GenerateECDSASignatureKeyInput) AwsCryptographyPrimitivesTypes.GenerateECDSASignatureKeyInput {

	return func() AwsCryptographyPrimitivesTypes.GenerateECDSASignatureKeyInput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateECDSASignatureKeyInput_.Create_GenerateECDSASignatureKeyInput_(Aws_cryptography_primitives_GenerateECDSASignatureKeyInput_signatureAlgorithm_ToDafny(nativeInput.SignatureAlgorithm))
	}()

}

func GenerateECDSASignatureKeyOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.GenerateECDSASignatureKeyOutput) AwsCryptographyPrimitivesTypes.GenerateECDSASignatureKeyOutput {

	return func() AwsCryptographyPrimitivesTypes.GenerateECDSASignatureKeyOutput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateECDSASignatureKeyOutput_.Create_GenerateECDSASignatureKeyOutput_(Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_signatureAlgorithm_ToDafny(nativeOutput.SignatureAlgorithm), Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_verificationKey_ToDafny(nativeOutput.VerificationKey), Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_signingKey_ToDafny(nativeOutput.SigningKey))
	}()

}

func GenerateRandomBytesInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.GenerateRandomBytesInput) AwsCryptographyPrimitivesTypes.GenerateRandomBytesInput {

	return func() AwsCryptographyPrimitivesTypes.GenerateRandomBytesInput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateRandomBytesInput_.Create_GenerateRandomBytesInput_(Aws_cryptography_primitives_GenerateRandomBytesInput_length_ToDafny(nativeInput.Length))
	}()

}

func GenerateRSAKeyPairInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.GenerateRSAKeyPairInput) AwsCryptographyPrimitivesTypes.GenerateRSAKeyPairInput {

	return func() AwsCryptographyPrimitivesTypes.GenerateRSAKeyPairInput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateRSAKeyPairInput_.Create_GenerateRSAKeyPairInput_(Aws_cryptography_primitives_GenerateRSAKeyPairInput_lengthBits_ToDafny(nativeInput.LengthBits))
	}()

}

func GenerateRSAKeyPairOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.GenerateRSAKeyPairOutput) AwsCryptographyPrimitivesTypes.GenerateRSAKeyPairOutput {

	return func() AwsCryptographyPrimitivesTypes.GenerateRSAKeyPairOutput {

		return AwsCryptographyPrimitivesTypes.Companion_GenerateRSAKeyPairOutput_.Create_GenerateRSAKeyPairOutput_(Aws_cryptography_primitives_GenerateRSAKeyPairOutput_publicKey_ToDafny(nativeOutput.PublicKey), Aws_cryptography_primitives_GenerateRSAKeyPairOutput_privateKey_ToDafny(nativeOutput.PrivateKey))
	}()

}

func GetPublicKeyFromPrivateKeyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.GetPublicKeyFromPrivateKeyInput) AwsCryptographyPrimitivesTypes.GetPublicKeyFromPrivateKeyInput {

	return func() AwsCryptographyPrimitivesTypes.GetPublicKeyFromPrivateKeyInput {

		return AwsCryptographyPrimitivesTypes.Companion_GetPublicKeyFromPrivateKeyInput_.Create_GetPublicKeyFromPrivateKeyInput_(Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyInput_eccCurve_ToDafny(nativeInput.EccCurve), Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyInput_privateKey_ToDafny(nativeInput.PrivateKey))
	}()

}

func GetPublicKeyFromPrivateKeyOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.GetPublicKeyFromPrivateKeyOutput) AwsCryptographyPrimitivesTypes.GetPublicKeyFromPrivateKeyOutput {

	return func() AwsCryptographyPrimitivesTypes.GetPublicKeyFromPrivateKeyOutput {

		return AwsCryptographyPrimitivesTypes.Companion_GetPublicKeyFromPrivateKeyOutput_.Create_GetPublicKeyFromPrivateKeyOutput_(Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_eccCurve_ToDafny(nativeOutput.EccCurve), Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_privateKey_ToDafny(nativeOutput.PrivateKey), Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_publicKey_ToDafny(nativeOutput.PublicKey))
	}()

}

func GetRSAKeyModulusLengthInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.GetRSAKeyModulusLengthInput) AwsCryptographyPrimitivesTypes.GetRSAKeyModulusLengthInput {

	return func() AwsCryptographyPrimitivesTypes.GetRSAKeyModulusLengthInput {

		return AwsCryptographyPrimitivesTypes.Companion_GetRSAKeyModulusLengthInput_.Create_GetRSAKeyModulusLengthInput_(Aws_cryptography_primitives_GetRSAKeyModulusLengthInput_publicKey_ToDafny(nativeInput.PublicKey))
	}()

}

func GetRSAKeyModulusLengthOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.GetRSAKeyModulusLengthOutput) AwsCryptographyPrimitivesTypes.GetRSAKeyModulusLengthOutput {

	return func() AwsCryptographyPrimitivesTypes.GetRSAKeyModulusLengthOutput {

		return AwsCryptographyPrimitivesTypes.Companion_GetRSAKeyModulusLengthOutput_.Create_GetRSAKeyModulusLengthOutput_(Aws_cryptography_primitives_GetRSAKeyModulusLengthOutput_length_ToDafny(nativeOutput.Length))
	}()

}

func HkdfInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.HkdfInput) AwsCryptographyPrimitivesTypes.HkdfInput {

	return func() AwsCryptographyPrimitivesTypes.HkdfInput {

		return AwsCryptographyPrimitivesTypes.Companion_HkdfInput_.Create_HkdfInput_(Aws_cryptography_primitives_HkdfInput_digestAlgorithm_ToDafny(nativeInput.DigestAlgorithm), Aws_cryptography_primitives_HkdfInput_salt_ToDafny(nativeInput.Salt), Aws_cryptography_primitives_HkdfInput_ikm_ToDafny(nativeInput.Ikm), Aws_cryptography_primitives_HkdfInput_info_ToDafny(nativeInput.Info), Aws_cryptography_primitives_HkdfInput_expectedLength_ToDafny(nativeInput.ExpectedLength))
	}()

}

func HkdfExpandInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.HkdfExpandInput) AwsCryptographyPrimitivesTypes.HkdfExpandInput {

	return func() AwsCryptographyPrimitivesTypes.HkdfExpandInput {

		return AwsCryptographyPrimitivesTypes.Companion_HkdfExpandInput_.Create_HkdfExpandInput_(Aws_cryptography_primitives_HkdfExpandInput_digestAlgorithm_ToDafny(nativeInput.DigestAlgorithm), Aws_cryptography_primitives_HkdfExpandInput_prk_ToDafny(nativeInput.Prk), Aws_cryptography_primitives_HkdfExpandInput_info_ToDafny(nativeInput.Info), Aws_cryptography_primitives_HkdfExpandInput_expectedLength_ToDafny(nativeInput.ExpectedLength))
	}()

}

func HkdfExtractInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.HkdfExtractInput) AwsCryptographyPrimitivesTypes.HkdfExtractInput {

	return func() AwsCryptographyPrimitivesTypes.HkdfExtractInput {

		return AwsCryptographyPrimitivesTypes.Companion_HkdfExtractInput_.Create_HkdfExtractInput_(Aws_cryptography_primitives_HkdfExtractInput_digestAlgorithm_ToDafny(nativeInput.DigestAlgorithm), Aws_cryptography_primitives_HkdfExtractInput_salt_ToDafny(nativeInput.Salt), Aws_cryptography_primitives_HkdfExtractInput_ikm_ToDafny(nativeInput.Ikm))
	}()

}

func HMacInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.HMacInput) AwsCryptographyPrimitivesTypes.HMacInput {

	return func() AwsCryptographyPrimitivesTypes.HMacInput {

		return AwsCryptographyPrimitivesTypes.Companion_HMacInput_.Create_HMacInput_(Aws_cryptography_primitives_HMacInput_digestAlgorithm_ToDafny(nativeInput.DigestAlgorithm), Aws_cryptography_primitives_HMacInput_key_ToDafny(nativeInput.Key), Aws_cryptography_primitives_HMacInput_message_ToDafny(nativeInput.Message))
	}()

}

func KdfCtrInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.KdfCtrInput) AwsCryptographyPrimitivesTypes.KdfCtrInput {

	return func() AwsCryptographyPrimitivesTypes.KdfCtrInput {

		return AwsCryptographyPrimitivesTypes.Companion_KdfCtrInput_.Create_KdfCtrInput_(Aws_cryptography_primitives_KdfCtrInput_digestAlgorithm_ToDafny(nativeInput.DigestAlgorithm), Aws_cryptography_primitives_KdfCtrInput_ikm_ToDafny(nativeInput.Ikm), Aws_cryptography_primitives_KdfCtrInput_expectedLength_ToDafny(nativeInput.ExpectedLength), Aws_cryptography_primitives_KdfCtrInput_purpose_ToDafny(nativeInput.Purpose), Aws_cryptography_primitives_KdfCtrInput_nonce_ToDafny(nativeInput.Nonce))
	}()

}

func ParsePublicKeyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.ParsePublicKeyInput) AwsCryptographyPrimitivesTypes.ParsePublicKeyInput {

	return func() AwsCryptographyPrimitivesTypes.ParsePublicKeyInput {

		return AwsCryptographyPrimitivesTypes.Companion_ParsePublicKeyInput_.Create_ParsePublicKeyInput_(Aws_cryptography_primitives_ParsePublicKeyInput_publicKey_ToDafny(nativeInput.PublicKey))
	}()

}

func ParsePublicKeyOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.ParsePublicKeyOutput) AwsCryptographyPrimitivesTypes.ParsePublicKeyOutput {

	return func() AwsCryptographyPrimitivesTypes.ParsePublicKeyOutput {

		return AwsCryptographyPrimitivesTypes.Companion_ParsePublicKeyOutput_.Create_ParsePublicKeyOutput_(Aws_cryptography_primitives_ParsePublicKeyOutput_publicKey_ToDafny(nativeOutput.PublicKey))
	}()

}

func RSADecryptInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.RSADecryptInput) AwsCryptographyPrimitivesTypes.RSADecryptInput {

	return func() AwsCryptographyPrimitivesTypes.RSADecryptInput {

		return AwsCryptographyPrimitivesTypes.Companion_RSADecryptInput_.Create_RSADecryptInput_(Aws_cryptography_primitives_RSADecryptInput_padding_ToDafny(nativeInput.Padding), Aws_cryptography_primitives_RSADecryptInput_privateKey_ToDafny(nativeInput.PrivateKey), Aws_cryptography_primitives_RSADecryptInput_cipherText_ToDafny(nativeInput.CipherText))
	}()

}

func RSAEncryptInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.RSAEncryptInput) AwsCryptographyPrimitivesTypes.RSAEncryptInput {

	return func() AwsCryptographyPrimitivesTypes.RSAEncryptInput {

		return AwsCryptographyPrimitivesTypes.Companion_RSAEncryptInput_.Create_RSAEncryptInput_(Aws_cryptography_primitives_RSAEncryptInput_padding_ToDafny(nativeInput.Padding), Aws_cryptography_primitives_RSAEncryptInput_publicKey_ToDafny(nativeInput.PublicKey), Aws_cryptography_primitives_RSAEncryptInput_plaintext_ToDafny(nativeInput.Plaintext))
	}()

}

func ValidatePublicKeyInput_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.ValidatePublicKeyInput) AwsCryptographyPrimitivesTypes.ValidatePublicKeyInput {

	return func() AwsCryptographyPrimitivesTypes.ValidatePublicKeyInput {

		return AwsCryptographyPrimitivesTypes.Companion_ValidatePublicKeyInput_.Create_ValidatePublicKeyInput_(Aws_cryptography_primitives_ValidatePublicKeyInput_eccCurve_ToDafny(nativeInput.EccCurve), Aws_cryptography_primitives_ValidatePublicKeyInput_publicKey_ToDafny(nativeInput.PublicKey))
	}()

}

func ValidatePublicKeyOutput_ToDafny(nativeOutput awscryptographyprimitivessmithygeneratedtypes.ValidatePublicKeyOutput) AwsCryptographyPrimitivesTypes.ValidatePublicKeyOutput {

	return func() AwsCryptographyPrimitivesTypes.ValidatePublicKeyOutput {

		return AwsCryptographyPrimitivesTypes.Companion_ValidatePublicKeyOutput_.Create_ValidatePublicKeyOutput_(Aws_cryptography_primitives_ValidatePublicKeyOutput_success_ToDafny(nativeOutput.Success))
	}()

}

func AwsCryptographicPrimitivesError_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.AwsCryptographicPrimitivesError) AwsCryptographyPrimitivesTypes.Error {
	return func() AwsCryptographyPrimitivesTypes.Error {

		return AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(Aws_cryptography_primitives_AwsCryptographicPrimitivesError_message_ToDafny(nativeInput.Message))
	}()

}

func CollectionOfErrors_Input_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.CollectionOfErrors) AwsCryptographyPrimitivesTypes.Error {
	var e []interface{}
	for _, i2 := range nativeInput.ListOfErrors {
		e = append(e, Error_ToDafny(i2))
	}
	return AwsCryptographyPrimitivesTypes.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 awscryptographyprimitivessmithygeneratedtypes.OpaqueError) AwsCryptographyPrimitivesTypes.Error {
	return AwsCryptographyPrimitivesTypes.Companion_Error_.Create_Opaque_(nativeInput.ErrObject)
}

func Error_ToDafny(err error) AwsCryptographyPrimitivesTypes.Error {
	switch err.(type) {
	// Service Errors
	case awscryptographyprimitivessmithygeneratedtypes.AwsCryptographicPrimitivesError:
		return AwsCryptographicPrimitivesError_ToDafny(err.(awscryptographyprimitivessmithygeneratedtypes.AwsCryptographicPrimitivesError))

	//DependentErrors

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

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

func CryptoConfig_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.CryptoConfig) AwsCryptographyPrimitivesTypes.CryptoConfig {
	return func() AwsCryptographyPrimitivesTypes.CryptoConfig {

		return AwsCryptographyPrimitivesTypes.Companion_CryptoConfig_.Create_CryptoConfig_()
	}()

}

func AES_CTR_ToDafny(nativeInput awscryptographyprimitivessmithygeneratedtypes.AES_CTR) AwsCryptographyPrimitivesTypes.AES__CTR {
	return func() AwsCryptographyPrimitivesTypes.AES__CTR {

		return AwsCryptographyPrimitivesTypes.Companion_AES__CTR_.Create_AES__CTR_(Aws_cryptography_primitives_AES_CTR_keyLength_ToDafny(nativeInput.KeyLength), Aws_cryptography_primitives_AES_CTR_nonceLength_ToDafny(nativeInput.NonceLength))
	}()

}

func Aws_cryptography_primitives_AESDecryptInput_encAlg_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.AES_GCM) AwsCryptographyPrimitivesTypes.AES__GCM {
	return func() AwsCryptographyPrimitivesTypes.AES__GCM {

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

func Aws_cryptography_primitives_AES_GCM_keyLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_AES_GCM_tagLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_AES_GCM_ivLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_AESDecryptInput_key_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_primitives_AESDecryptInput_cipherTxt_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_primitives_AESDecryptInput_authTag_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_primitives_AESDecryptInput_iv_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_primitives_AESDecryptInput_aad_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_primitives_AESDecryptOutput_plaintext_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_primitives_AESEncryptInput_encAlg_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.AES_GCM) AwsCryptographyPrimitivesTypes.AES__GCM {
	return func() AwsCryptographyPrimitivesTypes.AES__GCM {

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

func Aws_cryptography_primitives_AESEncryptInput_iv_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_primitives_AESEncryptInput_key_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_primitives_AESEncryptInput_msg_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_primitives_AESEncryptInput_aad_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_primitives_AESEncryptOutput_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_primitives_AESEncryptOutput_authTag_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_primitives_AesKdfCtrInput_ikm_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_primitives_AesKdfCtrInput_expectedLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_AesKdfCtrInput_nonce_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_primitives_AesKdfCtrOutput_okm_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_primitives_CompressPublicKeyInput_publicKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey) AwsCryptographyPrimitivesTypes.ECCPublicKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPublicKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(Aws_cryptography_primitives_ECCPublicKey_der_ToDafny(input.Der))
	}()
}

func Aws_cryptography_primitives_ECCPublicKey_der_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_primitives_CompressPublicKeyInput_eccCurve_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_primitives_CompressPublicKeyOutput_compressedPublicKey_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_primitives_DecompressPublicKeyInput_compressedPublicKey_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_primitives_DecompressPublicKeyInput_eccCurve_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_primitives_DecompressPublicKeyOutput_publicKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey) AwsCryptographyPrimitivesTypes.ECCPublicKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPublicKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(Aws_cryptography_primitives_ECCPublicKey_der_ToDafny(input.Der))
	}()
}

func Aws_cryptography_primitives_DeriveSharedSecretInput_eccCurve_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_primitives_DeriveSharedSecretInput_privateKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPrivateKey) AwsCryptographyPrimitivesTypes.ECCPrivateKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPrivateKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_(Aws_cryptography_primitives_ECCPrivateKey_pem_ToDafny(input.Pem))
	}()
}

func Aws_cryptography_primitives_ECCPrivateKey_pem_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_primitives_DeriveSharedSecretInput_publicKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey) AwsCryptographyPrimitivesTypes.ECCPublicKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPublicKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(Aws_cryptography_primitives_ECCPublicKey_der_ToDafny(input.Der))
	}()
}

func Aws_cryptography_primitives_DeriveSharedSecretOutput_sharedSecret_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_primitives_DigestInput_digestAlgorithm_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_primitives_DigestInput_message_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_primitives_DigestOutput_digest_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_primitives_ECDSASignInput_signatureAlgorithm_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_primitives_ECDSASignInput_signingKey_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_primitives_ECDSASignInput_message_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_primitives_ECDSASignOutput_signature_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_primitives_ECDSAVerifyInput_signatureAlgorithm_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_primitives_ECDSAVerifyInput_verificationKey_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_primitives_ECDSAVerifyInput_message_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_primitives_ECDSAVerifyInput_signature_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_primitives_ECDSAVerifyOutput_success_ToDafny(input bool) bool {
	return func() bool {

		return input
	}()
}

func Aws_cryptography_primitives_GenerateECCKeyPairInput_eccCurve_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_primitives_GenerateECCKeyPairOutput_eccCurve_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_primitives_GenerateECCKeyPairOutput_privateKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPrivateKey) AwsCryptographyPrimitivesTypes.ECCPrivateKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPrivateKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_(Aws_cryptography_primitives_ECCPrivateKey_pem_ToDafny(input.Pem))
	}()
}

func Aws_cryptography_primitives_GenerateECCKeyPairOutput_publicKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey) AwsCryptographyPrimitivesTypes.ECCPublicKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPublicKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(Aws_cryptography_primitives_ECCPublicKey_der_ToDafny(input.Der))
	}()
}

func Aws_cryptography_primitives_GenerateECDSASignatureKeyInput_signatureAlgorithm_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_primitives_GenerateECDSASignatureKeyOutput_signatureAlgorithm_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_primitives_GenerateECDSASignatureKeyOutput_verificationKey_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_primitives_GenerateECDSASignatureKeyOutput_signingKey_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_primitives_GenerateRandomBytesInput_length_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_GenerateRandomBytesOutput_data_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_primitives_GenerateRSAKeyPairInput_lengthBits_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_GenerateRSAKeyPairOutput_publicKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.RSAPublicKey) AwsCryptographyPrimitivesTypes.RSAPublicKey {
	return func() AwsCryptographyPrimitivesTypes.RSAPublicKey {

		return AwsCryptographyPrimitivesTypes.Companion_RSAPublicKey_.Create_RSAPublicKey_(Aws_cryptography_primitives_RSAPublicKey_lengthBits_ToDafny(input.LengthBits), Aws_cryptography_primitives_RSAPublicKey_pem_ToDafny(input.Pem))
	}()
}

func Aws_cryptography_primitives_RSAPublicKey_lengthBits_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_RSAPublicKey_pem_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_primitives_GenerateRSAKeyPairOutput_privateKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.RSAPrivateKey) AwsCryptographyPrimitivesTypes.RSAPrivateKey {
	return func() AwsCryptographyPrimitivesTypes.RSAPrivateKey {

		return AwsCryptographyPrimitivesTypes.Companion_RSAPrivateKey_.Create_RSAPrivateKey_(Aws_cryptography_primitives_RSAPrivateKey_lengthBits_ToDafny(input.LengthBits), Aws_cryptography_primitives_RSAPrivateKey_pem_ToDafny(input.Pem))
	}()
}

func Aws_cryptography_primitives_RSAPrivateKey_lengthBits_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_RSAPrivateKey_pem_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_primitives_GetPublicKeyFromPrivateKeyInput_eccCurve_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_primitives_GetPublicKeyFromPrivateKeyInput_privateKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPrivateKey) AwsCryptographyPrimitivesTypes.ECCPrivateKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPrivateKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_(Aws_cryptography_primitives_ECCPrivateKey_pem_ToDafny(input.Pem))
	}()
}

func Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_eccCurve_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_primitives_GetPublicKeyFromPrivateKeyOutput_privateKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPrivateKey) AwsCryptographyPrimitivesTypes.ECCPrivateKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPrivateKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_(Aws_cryptography_primitives_ECCPrivateKey_pem_ToDafny(input.Pem))
	}()
}

func Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_publicKey_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_primitives_GetRSAKeyModulusLengthInput_publicKey_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_primitives_GetRSAKeyModulusLengthOutput_length_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_HkdfInput_digestAlgorithm_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_primitives_HkdfInput_salt_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_primitives_HkdfInput_ikm_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_primitives_HkdfInput_info_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_primitives_HkdfInput_expectedLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_HkdfOutput_okm_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_primitives_HkdfExpandInput_digestAlgorithm_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_primitives_HkdfExpandInput_prk_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_primitives_HkdfExpandInput_info_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_primitives_HkdfExpandInput_expectedLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_HkdfExpandOutput_okm_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_primitives_HkdfExtractInput_digestAlgorithm_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_primitives_HkdfExtractInput_salt_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_primitives_HkdfExtractInput_ikm_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_primitives_HkdfExtractOutput_prk_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_primitives_HMacInput_digestAlgorithm_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_primitives_HMacInput_key_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_primitives_HMacInput_message_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_primitives_HMacOutput_digest_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_primitives_KdfCtrInput_digestAlgorithm_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_primitives_KdfCtrInput_ikm_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_primitives_KdfCtrInput_expectedLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_KdfCtrInput_purpose_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_primitives_KdfCtrInput_nonce_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_primitives_KdfCtrOutput_okm_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_primitives_ParsePublicKeyInput_publicKey_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_primitives_ParsePublicKeyOutput_publicKey_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey) AwsCryptographyPrimitivesTypes.ECCPublicKey {
	return func() AwsCryptographyPrimitivesTypes.ECCPublicKey {

		return AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(Aws_cryptography_primitives_ECCPublicKey_der_ToDafny(input.Der))
	}()
}

func Aws_cryptography_primitives_RSADecryptInput_padding_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.RSAPaddingMode) AwsCryptographyPrimitivesTypes.RSAPaddingMode {
	return func() AwsCryptographyPrimitivesTypes.RSAPaddingMode {

		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_RSAPaddingMode_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyPrimitivesTypes.RSAPaddingMode)
	}()
}

func Aws_cryptography_primitives_RSADecryptInput_privateKey_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_primitives_RSADecryptInput_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_primitives_RSADecryptOutput_plaintext_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_primitives_RSAEncryptInput_padding_ToDafny(input awscryptographyprimitivessmithygeneratedtypes.RSAPaddingMode) AwsCryptographyPrimitivesTypes.RSAPaddingMode {
	return func() AwsCryptographyPrimitivesTypes.RSAPaddingMode {

		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_RSAPaddingMode_{}.AllSingletonConstructors()), 0; i < index; i++ {
			var ok bool
			enum, ok = allEnums()
			if !ok {
				break
			}
		}
		return enum.(AwsCryptographyPrimitivesTypes.RSAPaddingMode)
	}()
}

func Aws_cryptography_primitives_RSAEncryptInput_publicKey_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_primitives_RSAEncryptInput_plaintext_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_primitives_RSAEncryptOutput_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_primitives_ValidatePublicKeyInput_eccCurve_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_primitives_ValidatePublicKeyInput_publicKey_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_primitives_ValidatePublicKeyOutput_success_ToDafny(input bool) bool {
	return func() bool {

		return input
	}()
}

func Aws_cryptography_primitives_AwsCryptographicPrimitivesError_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_primitives_AES_CTR_keyLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}

func Aws_cryptography_primitives_AES_CTR_nonceLength_ToDafny(input int32) int32 {
	return func() int32 {

		return input
	}()
}