AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go

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

package awscryptographyencryptionsdksmithygenerated

import (
	"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/primitives/awscryptographyprimitivessmithygenerated"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/awscryptographyprimitivessmithygeneratedtypes"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/UTF8"
	"github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers"
	"github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk/AwsCryptographyEncryptionSdkTypes"
	"github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes"
	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
)

func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput {

	return func() AwsCryptographyEncryptionSdkTypes.DecryptInput {

		return AwsCryptographyEncryptionSdkTypes.Companion_DecryptInput_.Create_DecryptInput_(Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(nativeInput.Ciphertext), func() Wrappers.Option {
			if (nativeInput.MaterialsManager) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_ToDafny(nativeInput.MaterialsManager))
		}(), func() Wrappers.Option {
			if (nativeInput.Keyring) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.Keyring_ToDafny(nativeInput.Keyring))
		}(), Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext))
	}()

}

func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput {

	return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput {

		return AwsCryptographyEncryptionSdkTypes.Companion_DecryptOutput_.Create_DecryptOutput_(Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(nativeOutput.Plaintext), Aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(nativeOutput.EncryptionContext), Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(nativeOutput.AlgorithmSuiteId))
	}()

}

func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) AwsCryptographyEncryptionSdkTypes.EncryptInput {

	return func() AwsCryptographyEncryptionSdkTypes.EncryptInput {

		return AwsCryptographyEncryptionSdkTypes.Companion_EncryptInput_.Create_EncryptInput_(Aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(nativeInput.Plaintext), Aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), func() Wrappers.Option {
			if (nativeInput.MaterialsManager) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_ToDafny(nativeInput.MaterialsManager))
		}(), func() Wrappers.Option {
			if (nativeInput.Keyring) == nil {
				return Wrappers.Companion_Option_.Create_None_()
			}
			return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.Keyring_ToDafny(nativeInput.Keyring))
		}(), Aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), Aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(nativeInput.FrameLength))
	}()

}

func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput {

	return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput {

		return AwsCryptographyEncryptionSdkTypes.Companion_EncryptOutput_.Create_EncryptOutput_(Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(nativeOutput.Ciphertext), Aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(nativeOutput.EncryptionContext), Aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(nativeOutput.AlgorithmSuiteId))
	}()

}

func AwsEncryptionSdkException_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException) AwsCryptographyEncryptionSdkTypes.Error {
	return func() AwsCryptographyEncryptionSdkTypes.Error {

		return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(Aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(nativeInput.Message))
	}()

}

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

func Error_ToDafny(err error) AwsCryptographyEncryptionSdkTypes.Error {
	switch err.(type) {
	// Service Errors
	case awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException:
		return AwsEncryptionSdkException_ToDafny(err.(awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException))

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

	case awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersBaseException:
		return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(awscryptographymaterialproviderssmithygenerated.Error_ToDafny(err))

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

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

func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig) AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig {
	return func() AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig {

		return AwsCryptographyEncryptionSdkTypes.Companion_AwsEncryptionSdkConfig_.Create_AwsEncryptionSdkConfig_(Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy), Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_ToDafny(nativeInput.MaxEncryptedDataKeys), Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_ToDafny(nativeInput.NetV4_0_0_RetryPolicy))
	}()

}

func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy) AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy {
	return func() AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy {

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

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

}

func Aws_cryptography_encryptionSdk_DecryptInput_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_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input map[string]string) Wrappers.Option {
	return func() Wrappers.Option {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap())
	}()
}

func Aws_cryptography_encryptionSdk_DecryptOutput_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_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId {

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

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

func Aws_cryptography_encryptionSdk_EncryptInput_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_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input map[string]string) Wrappers.Option {
	return func() Wrappers.Option {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap())
	}()
}

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

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

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

func Aws_cryptography_encryptionSdk_EncryptOutput_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_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map {
	return func() dafny.Map {
		fieldValue := dafny.NewMapBuilder()
		for key, val := range input {
			fieldValue.Add(awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), awscryptographymaterialproviderssmithygenerated.Aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val))
		}
		return fieldValue.ToMap()
	}()
}

func Aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId {
	return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId {

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

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

func Aws_cryptography_encryptionSdk_AwsEncryptionSdkException_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_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy) Wrappers.Option {
	return func() Wrappers.Option {
		if input == nil {
			return Wrappers.Companion_Option_.Create_None_()
		}
		var index int
		for _, enumVal := range input.Values() {
			index++
			if enumVal == *input {
				break
			}

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

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

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

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