From a4e937634ed04c67d10cf31935ada684ed1099f1 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Tue, 14 Jan 2025 18:11:32 -0800 Subject: [PATCH] push polymorph code --- .../shim.go | 2 +- .../to_dafny.go | 236 +++++++-------- .../to_native.go | 284 +++++++++--------- .../shim.go | 2 +- .../to_dafny.go | 236 +++++++-------- .../to_native.go | 284 +++++++++--------- 6 files changed, 522 insertions(+), 522 deletions(-) diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go index 294d5c822..edc7ce62e 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go @@ -5,9 +5,9 @@ package WrappedAwsCryptographyEncryptionSdkService import ( "context" + "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers" "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygenerated" - "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" ) type Shim struct { diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go index 084b4352f..613df60f7 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -10,17 +10,17 @@ import ( "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygeneratedtypes" "github.com/aws/aws-cryptographic-material-providers-library/primitives/awscryptographyprimitivessmithygenerated" "github.com/aws/aws-cryptographic-material-providers-library/primitives/awscryptographyprimitivessmithygeneratedtypes" + "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers" "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes" "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" - "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" ) -func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) AwsCryptographyEncryptionSdkTypes.EncryptInput { +func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput { - return func() AwsCryptographyEncryptionSdkTypes.EncryptInput { + return func() AwsCryptographyEncryptionSdkTypes.DecryptInput { - 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 { + 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_() } @@ -30,25 +30,25 @@ func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygenerate 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)) + }(), aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext)) }() } -func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput { +func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput { - return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput { + return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput { - 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)) + 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 DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput { +func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) AwsCryptographyEncryptionSdkTypes.EncryptInput { - return func() AwsCryptographyEncryptionSdkTypes.DecryptInput { + return func() AwsCryptographyEncryptionSdkTypes.EncryptInput { - return AwsCryptographyEncryptionSdkTypes.Companion_DecryptInput_.Create_DecryptInput_(aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(nativeInput.Ciphertext), func() Wrappers.Option { + 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_() } @@ -58,16 +58,16 @@ func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygenerate 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)) + }(), aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(nativeInput.FrameLength)) }() } -func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput { +func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput { - return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput { + return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput { - 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)) + 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)) }() } @@ -125,14 +125,7 @@ func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmit } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(input string) dafny.Sequence { - return func() dafny.Sequence { - - return dafny.SeqOfChars([]dafny.Char(input)...) - }() -} - -func aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { +func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { var v []interface{} if input == nil { @@ -145,15 +138,6 @@ func aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) }() } -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_DecryptInput_encryptionContext_ToDafny(input map[string]string) Wrappers.Option { return func() Wrappers.Option { fieldValue := dafny.NewMapBuilder() @@ -164,6 +148,49 @@ func aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input }() } +func aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence { + return func() dafny.Sequence { + + return dafny.SeqOf(func() []interface{} { + utf8.ValidString(input) + b := []byte(input) + f := make([]interface{}, len(b)) + for i, v := range b { + f[i] = v + } + return f + }()...) + }() +} + +func aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(input string) dafny.Sequence { + return func() dafny.Sequence { + + return dafny.SeqOf(func() []interface{} { + utf8.ValidString(input) + b := []byte(input) + f := make([]interface{}, len(b)) + for i, v := range b { + f[i] = v + } + return f + }()...) + }() +} + +func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { + return func() dafny.Sequence { + var v []interface{} + if input == nil { + return nil + } + for _, e := range input { + v = append(v, e) + } + return dafny.SeqOf(v...) + }() +} + func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map { return func() dafny.Map { fieldValue := dafny.NewMapBuilder() @@ -174,27 +201,38 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(inpu }() } -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_() - } +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 { + if enumVal == input { break } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + }() +} + +func aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { + return func() dafny.Sequence { + var v []interface{} + if input == nil { + return nil + } + for _, e := range input { + v = append(v, e) + } + return dafny.SeqOf(v...) }() } @@ -208,13 +246,15 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input }() } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - +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 { + if enumVal == *input { break } } @@ -226,7 +266,16 @@ func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input break } } - return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + 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) }() } @@ -243,15 +292,6 @@ func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(input []byt }() } -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_EncryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map { return func() dafny.Map { fieldValue := dafny.NewMapBuilder() @@ -262,59 +302,36 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(inpu }() } -func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { - return func() dafny.Sequence { - var v []interface{} - if input == nil { - return nil - } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqOf(v...) - }() -} +func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { -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 { + if enumVal == input { break } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.ESDKCommitmentPolicy)) + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) }() } -func aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence { +func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(input string) dafny.Sequence { return func() dafny.Sequence { - return dafny.SeqOf(func() []interface{} { - utf8.ValidString(input) - b := []byte(input) - f := make([]interface{}, len(b)) - for i, v := range b { - f[i] = v - } - return f - }()...) + return dafny.SeqOfChars([]dafny.Char(input)...) }() } -func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) Wrappers.Option { +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_() @@ -327,63 +344,46 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.ESDKAlgorithmSuiteId)) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy)) }() } -func aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(input string) dafny.Sequence { - return func() dafny.Sequence { - - return dafny.SeqOf(func() []interface{} { - utf8.ValidString(input) - b := []byte(input) - f := make([]interface{}, len(b)) - for i, v := range b { - f[i] = v - } - return f - }()...) +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_DecryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - +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 { + if enumVal == *input { break } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) - }() -} - -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { - return func() dafny.Sequence { - var v []interface{} - if input == nil { - return nil - } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqOf(v...) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) }() } diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go index 65f1830e5..733d2f842 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -12,10 +12,9 @@ import ( "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) -func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.EncryptInput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput { +func DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.DecryptInput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput { - return awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput{Plaintext: aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(dafnyInput.Dtor_plaintext()), - EncryptionContext: aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), + return awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput{Ciphertext: aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(dafnyInput.Dtor_ciphertext()), MaterialsManager: func() awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { if dafnyInput.Dtor_materialsManager().UnwrapOr(nil) == nil { return nil @@ -28,24 +27,24 @@ func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.Encrypt } return awscryptographymaterialproviderssmithygenerated.Keyring_FromDafny(dafnyInput.Dtor_keyring().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IKeyring)) }(), - AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(dafnyInput.Dtor_algorithmSuiteId().UnwrapOr(nil)), - FrameLength: aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(dafnyInput.Dtor_frameLength().UnwrapOr(nil)), + EncryptionContext: aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), } } -func EncryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.EncryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput { +func DecryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.DecryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput { - return awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput{Ciphertext: aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(dafnyOutput.Dtor_ciphertext()), - EncryptionContext: aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), - AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), + return awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput{Plaintext: aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(dafnyOutput.Dtor_plaintext()), + EncryptionContext: aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), + AlgorithmSuiteId: aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), } } -func DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.DecryptInput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput { +func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.EncryptInput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput { - return awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput{Ciphertext: aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(dafnyInput.Dtor_ciphertext()), + return awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput{Plaintext: aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(dafnyInput.Dtor_plaintext()), + EncryptionContext: aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), MaterialsManager: func() awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { if dafnyInput.Dtor_materialsManager().UnwrapOr(nil) == nil { return nil @@ -58,16 +57,17 @@ func DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.Decrypt } return awscryptographymaterialproviderssmithygenerated.Keyring_FromDafny(dafnyInput.Dtor_keyring().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IKeyring)) }(), - EncryptionContext: aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), + AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(dafnyInput.Dtor_algorithmSuiteId().UnwrapOr(nil)), + FrameLength: aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(dafnyInput.Dtor_frameLength().UnwrapOr(nil)), } } -func DecryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.DecryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput { +func EncryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.EncryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput { - return awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput{Plaintext: aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(dafnyOutput.Dtor_plaintext()), - EncryptionContext: aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), - AlgorithmSuiteId: aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), + return awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput{Ciphertext: aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(dafnyOutput.Dtor_ciphertext()), + EncryptionContext: aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), + AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), } } @@ -140,20 +140,7 @@ func AwsEncryptionSdkConfig_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTy } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(input interface{}) string { - return func() string { - var s string - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return s - } else { - s = s + string(val.(dafny.Char)) - } - } - }() -} -func aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { +func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { var b []byte if input == nil { @@ -169,16 +156,6 @@ func aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input inter } }() } -func aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input interface{}) *int64 { - return func() *int64 { - var b int64 - if input == nil { - return nil - } - b = input.(int64) - return &b - }() -} func aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { var m map[string]string = make(map[string]string) if input == nil { @@ -194,6 +171,60 @@ func aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(inp return m } +func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input interface{}) string { + return func() string { + var s string + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return s + } else { + // UTF bytes should be always converted from bytes to string in go + // Otherwise go treats the string as a unicode codepoint + + var valUint, _ = val.(uint8) + var byteSlice = []byte{valUint} + s = s + string(byteSlice) + + } + } + }() +} +func aws_cryptography_materialProviders_EncryptionContext_value_FromDafny(input interface{}) string { + return func() string { + var s string + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return s + } else { + // UTF bytes should be always converted from bytes to string in go + // Otherwise go treats the string as a unicode codepoint + + var valUint, _ = val.(uint8) + var byteSlice = []byte{valUint} + s = s + string(byteSlice) + + } + } + }() +} +func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { + return func() []byte { + var b []byte + if input == nil { + return nil + } + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return b + } else { + b = append(b, val.(byte)) + } + } + }() +} func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { var m map[string]string = make(map[string]string) if input == nil { @@ -209,25 +240,38 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(in return m } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_FromDafny(input interface{}) *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { - return func() *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { - var u awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy - if input == nil { - return nil - } - inputEnum := input.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy) +func aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy).Equals(inputEnum) { + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { break } } } - return &u.Values()[index] + return u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { + return func() []byte { + var b []byte + if input == nil { + return nil + } + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return b + } else { + b = append(b, val.(byte)) + } + } }() } func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -245,9 +289,12 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(inp return m } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { +func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + if input == nil { + return nil + } inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) index := -1 for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { @@ -260,7 +307,17 @@ func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(inp } } - return u.Values()[index] + return &u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input interface{}) *int64 { + return func() *int64 { + var b int64 + if input == nil { + return nil + } + b = input.(int64) + return &b }() } func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { @@ -279,16 +336,6 @@ func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input int } }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(input interface{}) *int64 { - return func() *int64 { - var b int64 - if input == nil { - return nil - } - b = input.(int64) - return &b - }() -} func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { var m map[string]string = make(map[string]string) if input == nil { @@ -304,44 +351,25 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(in return m } -func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { - return func() []byte { - var b []byte - if input == nil { - return nil - } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } - } - }() -} -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy - if input == nil { - return nil - } - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy) +func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy).Equals(inputEnum) { + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { break } } } - return &u.Values()[index] + return u.Values()[index] }() } -func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input interface{}) string { +func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(input interface{}) string { return func() string { var s string for i := dafny.Iterate(input); ; { @@ -349,30 +377,24 @@ func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input in if !ok { return s } else { - // UTF bytes should be always converted from bytes to string in go - // Otherwise go treats the string as a unicode codepoint - - var valUint, _ = val.(uint8) - var byteSlice = []byte{valUint} - s = s + string(byteSlice) - + s = s + string(val.(dafny.Char)) } } }() } -func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { + return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { + var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy if input == nil { return nil } - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy).Equals(inputEnum) { break } } @@ -381,56 +403,34 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(inpu return &u.Values()[index] }() } -func aws_cryptography_materialProviders_EncryptionContext_value_FromDafny(input interface{}) string { - return func() string { - var s string - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return s - } else { - // UTF bytes should be always converted from bytes to string in go - // Otherwise go treats the string as a unicode codepoint - - var valUint, _ = val.(uint8) - var byteSlice = []byte{valUint} - s = s + string(byteSlice) - - } +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(input interface{}) *int64 { + return func() *int64 { + var b int64 + if input == nil { + return nil } + b = input.(int64) + return &b }() } -func aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_FromDafny(input interface{}) *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { + return func() *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { + var u awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy + if input == nil { + return nil + } + inputEnum := input.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + if enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy).Equals(inputEnum) { break } } } - return u.Values()[index] - }() -} -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { - return func() []byte { - var b []byte - if input == nil { - return nil - } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } - } + return &u.Values()[index] }() } diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go index 294d5c822..edc7ce62e 100644 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go @@ -5,9 +5,9 @@ package WrappedAwsCryptographyEncryptionSdkService import ( "context" + "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers" "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygenerated" - "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" ) type Shim struct { diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go index 084b4352f..613df60f7 100644 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -10,17 +10,17 @@ import ( "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygeneratedtypes" "github.com/aws/aws-cryptographic-material-providers-library/primitives/awscryptographyprimitivessmithygenerated" "github.com/aws/aws-cryptographic-material-providers-library/primitives/awscryptographyprimitivessmithygeneratedtypes" + "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers" "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes" "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" - "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" ) -func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) AwsCryptographyEncryptionSdkTypes.EncryptInput { +func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput { - return func() AwsCryptographyEncryptionSdkTypes.EncryptInput { + return func() AwsCryptographyEncryptionSdkTypes.DecryptInput { - 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 { + 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_() } @@ -30,25 +30,25 @@ func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygenerate 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)) + }(), aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext)) }() } -func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput { +func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput { - return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput { + return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput { - 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)) + 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 DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput { +func EncryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) AwsCryptographyEncryptionSdkTypes.EncryptInput { - return func() AwsCryptographyEncryptionSdkTypes.DecryptInput { + return func() AwsCryptographyEncryptionSdkTypes.EncryptInput { - return AwsCryptographyEncryptionSdkTypes.Companion_DecryptInput_.Create_DecryptInput_(aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(nativeInput.Ciphertext), func() Wrappers.Option { + 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_() } @@ -58,16 +58,16 @@ func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygenerate 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)) + }(), aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(nativeInput.FrameLength)) }() } -func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput { +func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput { - return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput { + return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput { - 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)) + 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)) }() } @@ -125,14 +125,7 @@ func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmit } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(input string) dafny.Sequence { - return func() dafny.Sequence { - - return dafny.SeqOfChars([]dafny.Char(input)...) - }() -} - -func aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { +func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { var v []interface{} if input == nil { @@ -145,15 +138,6 @@ func aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) }() } -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_DecryptInput_encryptionContext_ToDafny(input map[string]string) Wrappers.Option { return func() Wrappers.Option { fieldValue := dafny.NewMapBuilder() @@ -164,6 +148,49 @@ func aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input }() } +func aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence { + return func() dafny.Sequence { + + return dafny.SeqOf(func() []interface{} { + utf8.ValidString(input) + b := []byte(input) + f := make([]interface{}, len(b)) + for i, v := range b { + f[i] = v + } + return f + }()...) + }() +} + +func aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(input string) dafny.Sequence { + return func() dafny.Sequence { + + return dafny.SeqOf(func() []interface{} { + utf8.ValidString(input) + b := []byte(input) + f := make([]interface{}, len(b)) + for i, v := range b { + f[i] = v + } + return f + }()...) + }() +} + +func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { + return func() dafny.Sequence { + var v []interface{} + if input == nil { + return nil + } + for _, e := range input { + v = append(v, e) + } + return dafny.SeqOf(v...) + }() +} + func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map { return func() dafny.Map { fieldValue := dafny.NewMapBuilder() @@ -174,27 +201,38 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(inpu }() } -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_() - } +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 { + if enumVal == input { break } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + }() +} + +func aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { + return func() dafny.Sequence { + var v []interface{} + if input == nil { + return nil + } + for _, e := range input { + v = append(v, e) + } + return dafny.SeqOf(v...) }() } @@ -208,13 +246,15 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input }() } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - +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 { + if enumVal == *input { break } } @@ -226,7 +266,16 @@ func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input break } } - return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + 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) }() } @@ -243,15 +292,6 @@ func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(input []byt }() } -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_EncryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map { return func() dafny.Map { fieldValue := dafny.NewMapBuilder() @@ -262,59 +302,36 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(inpu }() } -func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { - return func() dafny.Sequence { - var v []interface{} - if input == nil { - return nil - } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqOf(v...) - }() -} +func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { -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 { + if enumVal == input { break } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.ESDKCommitmentPolicy)) + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) }() } -func aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence { +func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(input string) dafny.Sequence { return func() dafny.Sequence { - return dafny.SeqOf(func() []interface{} { - utf8.ValidString(input) - b := []byte(input) - f := make([]interface{}, len(b)) - for i, v := range b { - f[i] = v - } - return f - }()...) + return dafny.SeqOfChars([]dafny.Char(input)...) }() } -func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) Wrappers.Option { +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_() @@ -327,63 +344,46 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.ESDKAlgorithmSuiteId)) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy)) }() } -func aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(input string) dafny.Sequence { - return func() dafny.Sequence { - - return dafny.SeqOf(func() []interface{} { - utf8.ValidString(input) - b := []byte(input) - f := make([]interface{}, len(b)) - for i, v := range b { - f[i] = v - } - return f - }()...) +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_DecryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - +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 { + if enumVal == *input { break } } var enum interface{} - for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + 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.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) - }() -} - -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { - return func() dafny.Sequence { - var v []interface{} - if input == nil { - return nil - } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqOf(v...) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) }() } diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go index 65f1830e5..733d2f842 100644 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -12,10 +12,9 @@ import ( "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) -func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.EncryptInput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput { +func DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.DecryptInput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput { - return awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput{Plaintext: aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(dafnyInput.Dtor_plaintext()), - EncryptionContext: aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), + return awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput{Ciphertext: aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(dafnyInput.Dtor_ciphertext()), MaterialsManager: func() awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { if dafnyInput.Dtor_materialsManager().UnwrapOr(nil) == nil { return nil @@ -28,24 +27,24 @@ func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.Encrypt } return awscryptographymaterialproviderssmithygenerated.Keyring_FromDafny(dafnyInput.Dtor_keyring().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IKeyring)) }(), - AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(dafnyInput.Dtor_algorithmSuiteId().UnwrapOr(nil)), - FrameLength: aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(dafnyInput.Dtor_frameLength().UnwrapOr(nil)), + EncryptionContext: aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), } } -func EncryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.EncryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput { +func DecryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.DecryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput { - return awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput{Ciphertext: aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(dafnyOutput.Dtor_ciphertext()), - EncryptionContext: aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), - AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), + return awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput{Plaintext: aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(dafnyOutput.Dtor_plaintext()), + EncryptionContext: aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), + AlgorithmSuiteId: aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), } } -func DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.DecryptInput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput { +func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.EncryptInput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput { - return awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput{Ciphertext: aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(dafnyInput.Dtor_ciphertext()), + return awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput{Plaintext: aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(dafnyInput.Dtor_plaintext()), + EncryptionContext: aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), MaterialsManager: func() awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { if dafnyInput.Dtor_materialsManager().UnwrapOr(nil) == nil { return nil @@ -58,16 +57,17 @@ func DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.Decrypt } return awscryptographymaterialproviderssmithygenerated.Keyring_FromDafny(dafnyInput.Dtor_keyring().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IKeyring)) }(), - EncryptionContext: aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), + AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(dafnyInput.Dtor_algorithmSuiteId().UnwrapOr(nil)), + FrameLength: aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(dafnyInput.Dtor_frameLength().UnwrapOr(nil)), } } -func DecryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.DecryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput { +func EncryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.EncryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput { - return awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput{Plaintext: aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(dafnyOutput.Dtor_plaintext()), - EncryptionContext: aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), - AlgorithmSuiteId: aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), + return awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput{Ciphertext: aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(dafnyOutput.Dtor_ciphertext()), + EncryptionContext: aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(dafnyOutput.Dtor_encryptionContext()), + AlgorithmSuiteId: aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(dafnyOutput.Dtor_algorithmSuiteId()), } } @@ -140,20 +140,7 @@ func AwsEncryptionSdkConfig_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTy } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(input interface{}) string { - return func() string { - var s string - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return s - } else { - s = s + string(val.(dafny.Char)) - } - } - }() -} -func aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { +func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { var b []byte if input == nil { @@ -169,16 +156,6 @@ func aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input inter } }() } -func aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input interface{}) *int64 { - return func() *int64 { - var b int64 - if input == nil { - return nil - } - b = input.(int64) - return &b - }() -} func aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { var m map[string]string = make(map[string]string) if input == nil { @@ -194,6 +171,60 @@ func aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(inp return m } +func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input interface{}) string { + return func() string { + var s string + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return s + } else { + // UTF bytes should be always converted from bytes to string in go + // Otherwise go treats the string as a unicode codepoint + + var valUint, _ = val.(uint8) + var byteSlice = []byte{valUint} + s = s + string(byteSlice) + + } + } + }() +} +func aws_cryptography_materialProviders_EncryptionContext_value_FromDafny(input interface{}) string { + return func() string { + var s string + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return s + } else { + // UTF bytes should be always converted from bytes to string in go + // Otherwise go treats the string as a unicode codepoint + + var valUint, _ = val.(uint8) + var byteSlice = []byte{valUint} + s = s + string(byteSlice) + + } + } + }() +} +func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { + return func() []byte { + var b []byte + if input == nil { + return nil + } + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return b + } else { + b = append(b, val.(byte)) + } + } + }() +} func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { var m map[string]string = make(map[string]string) if input == nil { @@ -209,25 +240,38 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(in return m } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_FromDafny(input interface{}) *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { - return func() *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { - var u awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy - if input == nil { - return nil - } - inputEnum := input.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy) +func aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy).Equals(inputEnum) { + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { break } } } - return &u.Values()[index] + return u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { + return func() []byte { + var b []byte + if input == nil { + return nil + } + for i := dafny.Iterate(input); ; { + val, ok := i() + if !ok { + return b + } else { + b = append(b, val.(byte)) + } + } }() } func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -245,9 +289,12 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(inp return m } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { +func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + if input == nil { + return nil + } inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) index := -1 for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { @@ -260,7 +307,17 @@ func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(inp } } - return u.Values()[index] + return &u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input interface{}) *int64 { + return func() *int64 { + var b int64 + if input == nil { + return nil + } + b = input.(int64) + return &b }() } func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { @@ -279,16 +336,6 @@ func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input int } }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(input interface{}) *int64 { - return func() *int64 { - var b int64 - if input == nil { - return nil - } - b = input.(int64) - return &b - }() -} func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { var m map[string]string = make(map[string]string) if input == nil { @@ -304,44 +351,25 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(in return m } -func aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { - return func() []byte { - var b []byte - if input == nil { - return nil - } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } - } - }() -} -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy - if input == nil { - return nil - } - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy) +func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { + var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy).Equals(inputEnum) { + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { break } } } - return &u.Values()[index] + return u.Values()[index] }() } -func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input interface{}) string { +func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(input interface{}) string { return func() string { var s string for i := dafny.Iterate(input); ; { @@ -349,30 +377,24 @@ func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input in if !ok { return s } else { - // UTF bytes should be always converted from bytes to string in go - // Otherwise go treats the string as a unicode codepoint - - var valUint, _ = val.(uint8) - var byteSlice = []byte{valUint} - s = s + string(byteSlice) - + s = s + string(val.(dafny.Char)) } } }() } -func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { + return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { + var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy if input == nil { return nil } - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy).Equals(inputEnum) { break } } @@ -381,56 +403,34 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(inpu return &u.Values()[index] }() } -func aws_cryptography_materialProviders_EncryptionContext_value_FromDafny(input interface{}) string { - return func() string { - var s string - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return s - } else { - // UTF bytes should be always converted from bytes to string in go - // Otherwise go treats the string as a unicode codepoint - - var valUint, _ = val.(uint8) - var byteSlice = []byte{valUint} - s = s + string(byteSlice) - - } +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(input interface{}) *int64 { + return func() *int64 { + var b int64 + if input == nil { + return nil } + b = input.(int64) + return &b }() } -func aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_FromDafny(input interface{}) *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { + return func() *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy { + var u awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy + if input == nil { + return nil + } + inputEnum := input.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy) index := -1 - for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + for allEnums := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()); ; { enum, ok := allEnums() if ok { index++ - if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + if enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy).Equals(inputEnum) { break } } } - return u.Values()[index] - }() -} -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { - return func() []byte { - var b []byte - if input == nil { - return nil - } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } - } + return &u.Values()[index] }() }