TestVectorsAwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_dafny.go (861 lines of code) (raw):
// Code generated by smithy-go-codegen DO NOT EDIT.
package awscryptographymaterialproviderstestvectorkeyssmithygenerated
import (
"github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms/ComAmazonawsKmsTypes"
"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/AwsCryptographyMaterialProvidersTypes"
"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/awscryptographymaterialproviderssmithygenerated"
"github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl/awscryptographymaterialproviderssmithygeneratedtypes"
"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-cryptographic-material-providers-library/testvectors/AwsCryptographyMaterialProvidersTestVectorKeysTypes"
"github.com/aws/aws-cryptographic-material-providers-library/testvectors/awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes"
kmstypes "github.com/aws/aws-sdk-go-v2/service/kms/types"
"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
)
func TestVectorKeyringInput_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.TestVectorKeyringInput) AwsCryptographyMaterialProvidersTestVectorKeysTypes.TestVectorKeyringInput {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.TestVectorKeyringInput {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_TestVectorKeyringInput_.Create_TestVectorKeyringInput_(Aws_cryptography_materialProvidersTestVectorKeys_TestVectorKeyringInput_keyDescription_ToDafny(nativeInput.KeyDescription))
}()
}
func TestVectorCmmInput_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.TestVectorCmmInput) AwsCryptographyMaterialProvidersTestVectorKeysTypes.TestVectorCmmInput {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.TestVectorCmmInput {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_TestVectorCmmInput_.Create_TestVectorCmmInput_(Aws_cryptography_materialProvidersTestVectorKeys_TestVectorCmmInput_keyDescription_ToDafny(nativeInput.KeyDescription), Aws_cryptography_materialProvidersTestVectorKeys_TestVectorCmmInput_forOperation_ToDafny(nativeInput.ForOperation))
}()
}
func GetKeyDescriptionInput_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.GetKeyDescriptionInput) AwsCryptographyMaterialProvidersTestVectorKeysTypes.GetKeyDescriptionInput {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.GetKeyDescriptionInput {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_GetKeyDescriptionInput_.Create_GetKeyDescriptionInput_(Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionInput_json_ToDafny(nativeInput.Json))
}()
}
func GetKeyDescriptionOutput_ToDafny(nativeOutput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.GetKeyDescriptionOutput) AwsCryptographyMaterialProvidersTestVectorKeysTypes.GetKeyDescriptionOutput {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.GetKeyDescriptionOutput {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_GetKeyDescriptionOutput_.Create_GetKeyDescriptionOutput_(Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionOutput_keyDescription_ToDafny(nativeOutput.KeyDescription))
}()
}
func SerializeKeyDescriptionInput_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.SerializeKeyDescriptionInput) AwsCryptographyMaterialProvidersTestVectorKeysTypes.SerializeKeyDescriptionInput {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.SerializeKeyDescriptionInput {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_SerializeKeyDescriptionInput_.Create_SerializeKeyDescriptionInput_(Aws_cryptography_materialProvidersTestVectorKeys_SerializeKeyDescriptionInput_keyDescription_ToDafny(nativeInput.KeyDescription))
}()
}
func SerializeKeyDescriptionOutput_ToDafny(nativeOutput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.SerializeKeyDescriptionOutput) AwsCryptographyMaterialProvidersTestVectorKeysTypes.SerializeKeyDescriptionOutput {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.SerializeKeyDescriptionOutput {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_SerializeKeyDescriptionOutput_.Create_SerializeKeyDescriptionOutput_(Aws_cryptography_materialProvidersTestVectorKeys_SerializeKeyDescriptionOutput_json_ToDafny(nativeOutput.Json))
}()
}
func KeyVectorException_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyVectorException) AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_Error_.Create_KeyVectorException_(Aws_cryptography_materialProvidersTestVectorKeys_KeyVectorException_message_ToDafny(nativeInput.Message))
}()
}
func CollectionOfErrors_Input_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.CollectionOfErrors) AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error {
var e []interface{}
for _, i2 := range nativeInput.ListOfErrors {
e = append(e, Error_ToDafny(i2))
}
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.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 awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.OpaqueError) AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_Error_.Create_Opaque_(nativeInput.ErrObject)
}
func Error_ToDafny(err error) AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error {
switch err.(type) {
// Service Errors
case awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyVectorException:
return KeyVectorException_ToDafny(err.(awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyVectorException))
//DependentErrors
//Unmodelled Errors
case awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.CollectionOfErrors:
return CollectionOfErrors_Input_ToDafny(err.(awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.CollectionOfErrors))
default:
error, ok := err.(awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.OpaqueError)
if !ok {
panic("Error is not an OpaqueError")
}
return OpaqueError_Input_ToDafny(error)
}
}
func KeyVectorsConfig_ToDafny(nativeInput awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyVectorsConfig) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyVectorsConfig {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyVectorsConfig {
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_KeyVectorsConfig_.Create_KeyVectorsConfig_(Aws_cryptography_materialProvidersTestVectorKeys_KeyVectorsConfig_keyManifestPath_ToDafny(nativeInput.KeyManifestPath))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_TestVectorKeyringInput_keyDescription_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KMSInfo) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_KMSInfo_.Create_KMSInfo_(Aws_cryptography_materialProvidersTestVectorKeys_KMSInfo_keyId_ToDafny(input.KeyId)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KMSInfo_keyId_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_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KmsMrkAware) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_KmsMrkAware_.Create_KmsMrkAware_(Aws_cryptography_materialProvidersTestVectorKeys_KmsMrkAware_keyId_ToDafny(input.KeyId)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KmsMrkAware_keyId_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_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KmsMrkAwareDiscovery) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_KmsMrkAwareDiscovery_.Create_KmsMrkAwareDiscovery_(Aws_cryptography_materialProvidersTestVectorKeys_KmsMrkAwareDiscovery_keyId_ToDafny(input.KeyId), Aws_cryptography_materialProvidersTestVectorKeys_KmsMrkAwareDiscovery_defaultMrkRegion_ToDafny(input.DefaultMrkRegion), Aws_cryptography_materialProvidersTestVectorKeys_KmsMrkAwareDiscovery_awsKmsDiscoveryFilter_ToDafny(input.AwsKmsDiscoveryFilter)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KmsMrkAwareDiscovery_keyId_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_materialProvidersTestVectorKeys_KmsMrkAwareDiscovery_defaultMrkRegion_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_materialProvidersTestVectorKeys_KmsMrkAwareDiscovery_awsKmsDiscoveryFilter_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_(awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_DiscoveryFilter_accountIds_ToDafny(input.AccountIds), awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_DiscoveryFilter_partition_ToDafny(input.Partition)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.RawRSA) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_RawRSA_.Create_RawRSA_(Aws_cryptography_materialProvidersTestVectorKeys_RawRSA_keyId_ToDafny(input.KeyId), Aws_cryptography_materialProvidersTestVectorKeys_RawRSA_providerId_ToDafny(input.ProviderId), Aws_cryptography_materialProvidersTestVectorKeys_RawRSA_padding_ToDafny(input.Padding)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_RawRSA_keyId_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_materialProvidersTestVectorKeys_RawRSA_providerId_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_materialProvidersTestVectorKeys_RawRSA_padding_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_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.RawAES) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_RawAES_.Create_RawAES_(Aws_cryptography_materialProvidersTestVectorKeys_RawAES_keyId_ToDafny(input.KeyId), Aws_cryptography_materialProvidersTestVectorKeys_RawAES_providerId_ToDafny(input.ProviderId)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_RawAES_keyId_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_materialProvidersTestVectorKeys_RawAES_providerId_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_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.RawEcdh) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_RawEcdh_.Create_RawEcdh_(Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_senderKeyId_ToDafny(input.SenderKeyId), Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_recipientKeyId_ToDafny(input.RecipientKeyId), Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_senderPublicKey_ToDafny(input.SenderPublicKey), Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_recipientPublicKey_ToDafny(input.RecipientPublicKey), Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_providerId_ToDafny(input.ProviderId), Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_curveSpec_ToDafny(input.CurveSpec), Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_keyAgreementScheme_ToDafny(input.KeyAgreementScheme)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_RawEcdh_senderKeyId_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_materialProvidersTestVectorKeys_RawEcdh_recipientKeyId_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_materialProvidersTestVectorKeys_RawEcdh_senderPublicKey_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_materialProvidersTestVectorKeys_RawEcdh_recipientPublicKey_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_materialProvidersTestVectorKeys_RawEcdh_providerId_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_materialProvidersTestVectorKeys_RawEcdh_curveSpec_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_materialProvidersTestVectorKeys_RawEcdh_keyAgreementScheme_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_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.StaticKeyring) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_StaticKeyring_.Create_StaticKeyring_(Aws_cryptography_materialProvidersTestVectorKeys_StaticKeyring_keyId_ToDafny(input.KeyId)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_StaticKeyring_keyId_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_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KmsRsaKeyring) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_KmsRsaKeyring_.Create_KmsRsaKeyring_(Aws_cryptography_materialProvidersTestVectorKeys_KmsRsaKeyring_keyId_ToDafny(input.KeyId), Aws_cryptography_materialProvidersTestVectorKeys_KmsRsaKeyring_encryptionAlgorithm_ToDafny(input.EncryptionAlgorithm)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KmsRsaKeyring_keyId_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_materialProvidersTestVectorKeys_KmsRsaKeyring_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_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KmsEcdhKeyring) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_KmsEcdhKeyring_.Create_KmsEcdhKeyring_(Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_senderKeyId_ToDafny(input.SenderKeyId), Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_recipientKeyId_ToDafny(input.RecipientKeyId), Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_senderPublicKey_ToDafny(input.SenderPublicKey), Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_recipientPublicKey_ToDafny(input.RecipientPublicKey), Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_curveSpec_ToDafny(input.CurveSpec), Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_keyAgreementScheme_ToDafny(input.KeyAgreementScheme)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KmsEcdhKeyring_senderKeyId_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_materialProvidersTestVectorKeys_KmsEcdhKeyring_recipientKeyId_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_materialProvidersTestVectorKeys_KmsEcdhKeyring_senderPublicKey_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_materialProvidersTestVectorKeys_KmsEcdhKeyring_recipientPublicKey_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_materialProvidersTestVectorKeys_KmsEcdhKeyring_curveSpec_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_materialProvidersTestVectorKeys_KmsEcdhKeyring_keyAgreementScheme_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_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.HierarchyKeyring) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_HierarchyKeyring_.Create_HierarchyKeyring_(Aws_cryptography_materialProvidersTestVectorKeys_HierarchyKeyring_keyId_ToDafny(input.KeyId)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_HierarchyKeyring_keyId_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_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.MultiKeyring) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_MultiKeyring_.Create_MultiKeyring_(Aws_cryptography_materialProvidersTestVectorKeys_MultiKeyring_generator_ToDafny(input.Generator), Aws_cryptography_materialProvidersTestVectorKeys_MultiKeyring_childKeyrings_ToDafny(input.ChildKeyrings)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_MultiKeyring_generator_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) Wrappers.Option {
return func() Wrappers.Option {
if input == nil {
return Wrappers.Companion_Option_.Create_None_()
}
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring)))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM)))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.RequiredEncryptionContextCMM) Wrappers.Option {
return func() Wrappers.Option {
return Wrappers.Companion_Option_.Create_Some_(AwsCryptographyMaterialProvidersTestVectorKeysTypes.Companion_RequiredEncryptionContextCMM_.Create_RequiredEncryptionContextCMM_(Aws_cryptography_materialProvidersTestVectorKeys_RequiredEncryptionContextCMM_underlying_ToDafny(input.Underlying), Aws_cryptography_materialProvidersTestVectorKeys_RequiredEncryptionContextCMM_requiredEncryptionContextKeys_ToDafny(input.RequiredEncryptionContextKeys)))
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_RequiredEncryptionContextCMM_underlying_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_RequiredEncryptionContextCMM_requiredEncryptionContextKeys_ToDafny(input []string) dafny.Sequence {
return func() dafny.Sequence {
var fieldValue []interface{} = make([]interface{}, 0, len(input))
for _, val := range input {
element := awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContextKeys_member_ToDafny(val)
fieldValue = append(fieldValue, element)
}
return dafny.SeqOf(fieldValue...)
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_MultiKeyring_childKeyrings_ToDafny(input []awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) dafny.Sequence {
return func() dafny.Sequence {
var fieldValue []interface{} = make([]interface{}, 0, len(input))
for _, val := range input {
element := Aws_cryptography_materialProvidersTestVectorKeys_KeyDescriptionList_member_ToDafny(val)
fieldValue = append(fieldValue, element)
}
return dafny.SeqOf(fieldValue...)
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_KeyDescriptionList_member_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_TestVectorCmmInput_keyDescription_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_TestVectorCmmInput_forOperation_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.CmmOperation) AwsCryptographyMaterialProvidersTestVectorKeysTypes.CmmOperation {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.CmmOperation {
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(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_CmmOperation_{}.AllSingletonConstructors()), 0; i < index; i++ {
var ok bool
enum, ok = allEnums()
if !ok {
break
}
}
return enum.(AwsCryptographyMaterialProvidersTestVectorKeysTypes.CmmOperation)
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionInput_json_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_materialProvidersTestVectorKeys_GetKeyDescriptionOutput_keyDescription_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_SerializeKeyDescriptionInput_keyDescription_ToDafny(input awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription) AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
return func() AwsCryptographyMaterialProvidersTestVectorKeysTypes.KeyDescription {
switch input.(type) {
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Kms_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKms).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Kms_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KMSInfo))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrk_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrk).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrk_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAware))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsMrkDiscovery_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsMrkDiscovery).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsMrkDiscovery_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsMrkAwareDiscovery))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RSA_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRSA).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RSA_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawRSA))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_AES_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberAES).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_AES_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawAES))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_ECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_ECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RawEcdh))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Static_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberStatic).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Static_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.StaticKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsRsa_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsRsa).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsRsa_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsRsaKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_KmsECDH_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberKmsECDH).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_KmsECDH_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.KmsEcdhKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Hierarchy_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberHierarchy).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Hierarchy_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.HierarchyKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_Multi_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberMulti).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_Multi_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.MultiKeyring))
case *awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext:
var inputToConversion = Aws_cryptography_materialProvidersTestVectorKeys_KeyDescription_RequiredEncryptionContext_ToDafny(input.(*awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescriptionMemberRequiredEncryptionContext).Value)
return AwsCryptographyMaterialProvidersTestVectorKeysTypes.CompanionStruct_KeyDescription_{}.Create_RequiredEncryptionContext_(inputToConversion.UnwrapOr(nil).(AwsCryptographyMaterialProvidersTestVectorKeysTypes.RequiredEncryptionContextCMM))
default:
panic("Unhandled union type")
}
}()
}
func Aws_cryptography_materialProvidersTestVectorKeys_SerializeKeyDescriptionOutput_json_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_materialProvidersTestVectorKeys_KeyVectorException_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_materialProvidersTestVectorKeys_KeyVectorsConfig_keyManifestPath_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
}()
}()
}