From dc57046198cac6e89c7c5d68e52b3eb2b14e2787 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Tue, 14 Jan 2025 17:31:12 -0800 Subject: [PATCH 1/6] add diff --- .github/actions/polymorph_codegen/action.yml | 6 ++++++ .github/workflows/library_codegen.yml | 10 ++++++++++ 2 files changed, 16 insertions(+) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 66d0f7566..bd5fee546 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -116,6 +116,12 @@ runs: # run: | # make polymorph_rust ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} + - name: Regenerate Go code using smithy-dafny + working-directory: ./${{ inputs.library }} + shell: bash + run: | + make polymorph_go + - name: Check regenerated code against commited code # Composite action inputs seem to not actually support booleans properly for some reason if: inputs.diff-generated-code == 'true' diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index 90922d0fe..d534b5733 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -20,6 +20,7 @@ jobs: # Note dotnet is only used for formatting generated code # in this workflow dotnet-version: ["6.0.x"] + go-version: [1.23] os: [ubuntu-latest] runs-on: ${{ matrix.os }} defaults: @@ -61,6 +62,15 @@ jobs: - name: Install Smithy-Dafny codegen dependencies uses: ./.github/actions/install_smithy_dafny_codegen_dependencies + - name: Install Go + uses: actions/setup-go@v5 + with: + go-version: ${{ matrix.go-version }} + + - name: Install Go imports + run: | + go install golang.org/x/tools/cmd/goimports@latest + - uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} From 223ea3a698074c1454df7ec4c39f3ea9188e92bf Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Tue, 14 Jan 2025 17:58:58 -0800 Subject: [PATCH 2/6] bump mpl and check --- .github/actions/polymorph_codegen/action.yml | 5 +++ .../shim.go | 43 +++++++++++++++++++ .../enums.go | 17 ++++++++ mpl | 2 +- 4 files changed, 66 insertions(+), 1 deletion(-) create mode 100644 AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go create mode 100644 AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index bd5fee546..ab71effc7 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -122,6 +122,11 @@ runs: run: | make polymorph_go + - name: just print + shell: bash + run: | + cat AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go + - name: Check regenerated code against commited code # Composite action inputs seem to not actually support booleans properly for some reason if: inputs.diff-generated-code == 'true' diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go new file mode 100644 index 000000000..294d5c822 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go @@ -0,0 +1,43 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package WrappedAwsCryptographyEncryptionSdkService + +import ( + "context" + + "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygenerated" + "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" +) + +type Shim struct { + AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient + client *awscryptographyencryptionsdksmithygenerated.Client +} + +func (_static *CompanionStruct_Default___) WrappedESDK(inputConfig AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) Wrappers.Result { + var nativeConfig = awscryptographyencryptionsdksmithygenerated.AwsEncryptionSdkConfig_FromDafny(inputConfig) + var nativeClient, nativeError = awscryptographyencryptionsdksmithygenerated.NewClient(nativeConfig) + if nativeError != nil { + return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_Opaque_(nativeError)) + } + return Wrappers.Companion_Result_.Create_Success_(&Shim{client: nativeClient}) +} + +func (shim *Shim) Encrypt(input AwsCryptographyEncryptionSdkTypes.EncryptInput) Wrappers.Result { + var native_request = awscryptographyencryptionsdksmithygenerated.EncryptInput_FromDafny(input) + var native_response, native_error = shim.client.Encrypt(context.Background(), native_request) + if native_error != nil { + return Wrappers.Companion_Result_.Create_Failure_(awscryptographyencryptionsdksmithygenerated.Error_ToDafny(native_error)) + } + return Wrappers.Companion_Result_.Create_Success_(awscryptographyencryptionsdksmithygenerated.EncryptOutput_ToDafny(*native_response)) +} + +func (shim *Shim) Decrypt(input AwsCryptographyEncryptionSdkTypes.DecryptInput) Wrappers.Result { + var native_request = awscryptographyencryptionsdksmithygenerated.DecryptInput_FromDafny(input) + var native_response, native_error = shim.client.Decrypt(context.Background(), native_request) + if native_error != nil { + return Wrappers.Companion_Result_.Create_Failure_(awscryptographyencryptionsdksmithygenerated.Error_ToDafny(native_error)) + } + return Wrappers.Companion_Result_.Create_Success_(awscryptographyencryptionsdksmithygenerated.DecryptOutput_ToDafny(*native_response)) +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go new file mode 100644 index 000000000..0322a937c --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go @@ -0,0 +1,17 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +type NetV4_0_0_RetryPolicy string + +const ( + NetV4_0_0_RetryPolicyForbidRetry NetV4_0_0_RetryPolicy = "FORBID_RETRY" + NetV4_0_0_RetryPolicyAllowRetry NetV4_0_0_RetryPolicy = "ALLOW_RETRY" +) + +func (NetV4_0_0_RetryPolicy) Values() []NetV4_0_0_RetryPolicy { + return []NetV4_0_0_RetryPolicy{ + "FORBID_RETRY", + "ALLOW_RETRY", + } +} diff --git a/mpl b/mpl index 93798f13e..4508ab84b 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit 93798f13e64a9b83ed909d1ef27cafa3f00f3450 +Subproject commit 4508ab84bd6017e7db6f353d2195b93ac30761c9 From a4e937634ed04c67d10cf31935ada684ed1099f1 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Tue, 14 Jan 2025 18:11:32 -0800 Subject: [PATCH 3/6] 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] }() } From 3205033bc1198c2c16b95c44629d05d7aa4d2d52 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 15 Jan 2025 10:41:44 -0800 Subject: [PATCH 4/6] Revert "push polymorph code" This reverts commit a4e937634ed04c67d10cf31935ada684ed1099f1. --- .../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 edc7ce62e..294d5c822 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 613df60f7..084b4352f 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 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_() } @@ -30,25 +30,25 @@ 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)) }() } -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_() } @@ -58,16 +58,16 @@ 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)) }() } @@ -125,7 +125,14 @@ func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmit } -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { +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 { return func() dafny.Sequence { var v []interface{} if input == nil { @@ -138,6 +145,15 @@ func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_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() @@ -148,49 +164,6 @@ 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() @@ -201,38 +174,27 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(inpu }() } -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_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...) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) }() } @@ -246,15 +208,13 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input }() } -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_() - } +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 { + if enumVal == input { break } } @@ -266,16 +226,7 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input 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) + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) }() } @@ -292,6 +243,15 @@ 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() @@ -302,36 +262,59 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(inpu }() } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { +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_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_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 enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy)) }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(input string) dafny.Sequence { +func aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence { return func() dafny.Sequence { - return dafny.SeqOfChars([]dafny.Char(input)...) + 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_commitmentPolicy_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy) Wrappers.Option { +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_() @@ -344,46 +327,63 @@ func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDa } } 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 Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId)) }() } -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_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_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_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...) }() } diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go index 733d2f842..65f1830e5 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -12,9 +12,10 @@ import ( "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) -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 @@ -27,24 +28,24 @@ 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()), } } -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 @@ -57,17 +58,16 @@ 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()), } } @@ -140,7 +140,20 @@ func AwsEncryptionSdkConfig_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTy } -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { +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 { return func() []byte { var b []byte if input == nil { @@ -156,6 +169,16 @@ func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input inte } }() } +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 { @@ -171,60 +194,6 @@ 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 { @@ -240,38 +209,25 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(in return m } -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_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)) - } - } + return &u.Values()[index] }() } func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -289,12 +245,9 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(inp return m } -func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { +func aws_cryptography_encryptionSdk_EncryptOutput_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()); ; { @@ -307,17 +260,7 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(inpu } } - 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 + return u.Values()[index] }() } func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { @@ -336,6 +279,16 @@ 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 { @@ -351,25 +304,44 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(in return m } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) +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) 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 } } } - return u.Values()[index] + return &u.Values()[index] }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(input interface{}) string { +func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input interface{}) string { return func() string { var s string for i := dafny.Iterate(input); ; { @@ -377,24 +349,30 @@ func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny( if !ok { return s } else { - s = s + string(val.(dafny.Char)) + // 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_commitmentPolicy_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy +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.ESDKCommitmentPolicy) + 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 } } @@ -403,34 +381,56 @@ func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_From return &u.Values()[index] }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(input interface{}) *int64 { - return func() *int64 { - var b int64 - if input == nil { - return nil +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) + + } } - b = input.(int64) - return &b }() } -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_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)) + } + } }() } diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go index edc7ce62e..294d5c822 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 613df60f7..084b4352f 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 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_() } @@ -30,25 +30,25 @@ 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)) }() } -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_() } @@ -58,16 +58,16 @@ 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)) }() } @@ -125,7 +125,14 @@ func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmit } -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { +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 { return func() dafny.Sequence { var v []interface{} if input == nil { @@ -138,6 +145,15 @@ func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_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() @@ -148,49 +164,6 @@ 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() @@ -201,38 +174,27 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(inpu }() } -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_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...) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) }() } @@ -246,15 +208,13 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input }() } -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_() - } +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 { + if enumVal == input { break } } @@ -266,16 +226,7 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input 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) + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) }() } @@ -292,6 +243,15 @@ 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() @@ -302,36 +262,59 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(inpu }() } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { - return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { +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_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_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 enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy)) }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(input string) dafny.Sequence { +func aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(input string) dafny.Sequence { return func() dafny.Sequence { - return dafny.SeqOfChars([]dafny.Char(input)...) + 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_commitmentPolicy_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy) Wrappers.Option { +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_() @@ -344,46 +327,63 @@ func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDa } } 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 Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId)) }() } -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_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_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_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...) }() } diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go index 733d2f842..65f1830e5 100644 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -12,9 +12,10 @@ import ( "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) -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 @@ -27,24 +28,24 @@ 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()), } } -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 @@ -57,17 +58,16 @@ 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()), } } @@ -140,7 +140,20 @@ func AwsEncryptionSdkConfig_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTy } -func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { +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 { return func() []byte { var b []byte if input == nil { @@ -156,6 +169,16 @@ func aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input inte } }() } +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 { @@ -171,60 +194,6 @@ 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 { @@ -240,38 +209,25 @@ func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(in return m } -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_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)) - } - } + return &u.Values()[index] }() } func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -289,12 +245,9 @@ func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(inp return m } -func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { +func aws_cryptography_encryptionSdk_EncryptOutput_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()); ; { @@ -307,17 +260,7 @@ func aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_FromDafny(inpu } } - 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 + return u.Values()[index] }() } func aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { @@ -336,6 +279,16 @@ 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 { @@ -351,25 +304,44 @@ func aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(in return m } -func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - return func() awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId - inputEnum := input.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) +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) 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 } } } - return u.Values()[index] + return &u.Values()[index] }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(input interface{}) string { +func aws_cryptography_materialProviders_EncryptionContext_key_FromDafny(input interface{}) string { return func() string { var s string for i := dafny.Iterate(input); ; { @@ -377,24 +349,30 @@ func aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny( if !ok { return s } else { - s = s + string(val.(dafny.Char)) + // 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_commitmentPolicy_FromDafny(input interface{}) *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - return func() *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy { - var u awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy +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.ESDKCommitmentPolicy) + 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 } } @@ -403,34 +381,56 @@ func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_From return &u.Values()[index] }() } -func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(input interface{}) *int64 { - return func() *int64 { - var b int64 - if input == nil { - return nil +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) + + } } - b = input.(int64) - return &b }() } -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_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)) + } + } }() } From c17eda1786d7968bbf046796178ecd5915d607ab Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 15 Jan 2025 10:41:56 -0800 Subject: [PATCH 5/6] Revert "bump mpl and check" This reverts commit 223ea3a698074c1454df7ec4c39f3ea9188e92bf. --- .github/actions/polymorph_codegen/action.yml | 5 --- .../shim.go | 43 ------------------- .../enums.go | 17 -------- mpl | 2 +- 4 files changed, 1 insertion(+), 66 deletions(-) delete mode 100644 AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go delete mode 100644 AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index ab71effc7..bd5fee546 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -122,11 +122,6 @@ runs: run: | make polymorph_go - - name: just print - shell: bash - run: | - cat AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go - - name: Check regenerated code against commited code # Composite action inputs seem to not actually support booleans properly for some reason if: inputs.diff-generated-code == 'true' diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go deleted file mode 100644 index 294d5c822..000000000 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go +++ /dev/null @@ -1,43 +0,0 @@ -// Code generated by smithy-go-codegen DO NOT EDIT. - -package WrappedAwsCryptographyEncryptionSdkService - -import ( - "context" - - "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" - "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygenerated" - "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" -) - -type Shim struct { - AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient - client *awscryptographyencryptionsdksmithygenerated.Client -} - -func (_static *CompanionStruct_Default___) WrappedESDK(inputConfig AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) Wrappers.Result { - var nativeConfig = awscryptographyencryptionsdksmithygenerated.AwsEncryptionSdkConfig_FromDafny(inputConfig) - var nativeClient, nativeError = awscryptographyencryptionsdksmithygenerated.NewClient(nativeConfig) - if nativeError != nil { - return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_Opaque_(nativeError)) - } - return Wrappers.Companion_Result_.Create_Success_(&Shim{client: nativeClient}) -} - -func (shim *Shim) Encrypt(input AwsCryptographyEncryptionSdkTypes.EncryptInput) Wrappers.Result { - var native_request = awscryptographyencryptionsdksmithygenerated.EncryptInput_FromDafny(input) - var native_response, native_error = shim.client.Encrypt(context.Background(), native_request) - if native_error != nil { - return Wrappers.Companion_Result_.Create_Failure_(awscryptographyencryptionsdksmithygenerated.Error_ToDafny(native_error)) - } - return Wrappers.Companion_Result_.Create_Success_(awscryptographyencryptionsdksmithygenerated.EncryptOutput_ToDafny(*native_response)) -} - -func (shim *Shim) Decrypt(input AwsCryptographyEncryptionSdkTypes.DecryptInput) Wrappers.Result { - var native_request = awscryptographyencryptionsdksmithygenerated.DecryptInput_FromDafny(input) - var native_response, native_error = shim.client.Decrypt(context.Background(), native_request) - if native_error != nil { - return Wrappers.Companion_Result_.Create_Failure_(awscryptographyencryptionsdksmithygenerated.Error_ToDafny(native_error)) - } - return Wrappers.Companion_Result_.Create_Success_(awscryptographyencryptionsdksmithygenerated.DecryptOutput_ToDafny(*native_response)) -} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go deleted file mode 100644 index 0322a937c..000000000 --- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go +++ /dev/null @@ -1,17 +0,0 @@ -// Code generated by smithy-go-codegen DO NOT EDIT. - -package awscryptographyencryptionsdksmithygeneratedtypes - -type NetV4_0_0_RetryPolicy string - -const ( - NetV4_0_0_RetryPolicyForbidRetry NetV4_0_0_RetryPolicy = "FORBID_RETRY" - NetV4_0_0_RetryPolicyAllowRetry NetV4_0_0_RetryPolicy = "ALLOW_RETRY" -) - -func (NetV4_0_0_RetryPolicy) Values() []NetV4_0_0_RetryPolicy { - return []NetV4_0_0_RetryPolicy{ - "FORBID_RETRY", - "ALLOW_RETRY", - } -} diff --git a/mpl b/mpl index 4508ab84b..93798f13e 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit 4508ab84bd6017e7db6f353d2195b93ac30761c9 +Subproject commit 93798f13e64a9b83ed909d1ef27cafa3f00f3450 From caa1c41b1862f5a77ab78fc5ff0f94970df31bff Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 15 Jan 2025 13:49:49 -0800 Subject: [PATCH 6/6] auto commit --- .../shim.go | 43 +++++++++++++++++++ .../enums.go | 17 ++++++++ AwsEncryptionSDK/runtimes/go/examples/main.go | 2 +- 3 files changed, 61 insertions(+), 1 deletion(-) create mode 100644 AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go create mode 100644 AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go new file mode 100644 index 000000000..13b92b3a1 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go @@ -0,0 +1,43 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +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-dafny/releases/go/encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated" +) + +type Shim struct { + AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient + client *awscryptographyencryptionsdksmithygenerated.Client +} + +func (_static *CompanionStruct_Default___) WrappedESDK(inputConfig AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) Wrappers.Result { + var nativeConfig = awscryptographyencryptionsdksmithygenerated.AwsEncryptionSdkConfig_FromDafny(inputConfig) + var nativeClient, nativeError = awscryptographyencryptionsdksmithygenerated.NewClient(nativeConfig) + if nativeError != nil { + return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_Opaque_(nativeError)) + } + return Wrappers.Companion_Result_.Create_Success_(&Shim{client: nativeClient}) +} + +func (shim *Shim) Encrypt(input AwsCryptographyEncryptionSdkTypes.EncryptInput) Wrappers.Result { + var native_request = awscryptographyencryptionsdksmithygenerated.EncryptInput_FromDafny(input) + var native_response, native_error = shim.client.Encrypt(context.Background(), native_request) + if native_error != nil { + return Wrappers.Companion_Result_.Create_Failure_(awscryptographyencryptionsdksmithygenerated.Error_ToDafny(native_error)) + } + return Wrappers.Companion_Result_.Create_Success_(awscryptographyencryptionsdksmithygenerated.EncryptOutput_ToDafny(*native_response)) +} + +func (shim *Shim) Decrypt(input AwsCryptographyEncryptionSdkTypes.DecryptInput) Wrappers.Result { + var native_request = awscryptographyencryptionsdksmithygenerated.DecryptInput_FromDafny(input) + var native_response, native_error = shim.client.Decrypt(context.Background(), native_request) + if native_error != nil { + return Wrappers.Companion_Result_.Create_Failure_(awscryptographyencryptionsdksmithygenerated.Error_ToDafny(native_error)) + } + return Wrappers.Companion_Result_.Create_Success_(awscryptographyencryptionsdksmithygenerated.DecryptOutput_ToDafny(*native_response)) +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go new file mode 100644 index 000000000..0322a937c --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go @@ -0,0 +1,17 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +type NetV4_0_0_RetryPolicy string + +const ( + NetV4_0_0_RetryPolicyForbidRetry NetV4_0_0_RetryPolicy = "FORBID_RETRY" + NetV4_0_0_RetryPolicyAllowRetry NetV4_0_0_RetryPolicy = "ALLOW_RETRY" +) + +func (NetV4_0_0_RetryPolicy) Values() []NetV4_0_0_RetryPolicy { + return []NetV4_0_0_RetryPolicy{ + "FORBID_RETRY", + "ALLOW_RETRY", + } +} diff --git a/AwsEncryptionSDK/runtimes/go/examples/main.go b/AwsEncryptionSDK/runtimes/go/examples/main.go index aa8ee08e9..c7a5a2abe 100644 --- a/AwsEncryptionSDK/runtimes/go/examples/main.go +++ b/AwsEncryptionSDK/runtimes/go/examples/main.go @@ -22,8 +22,8 @@ import ( "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/keyring/multikeyring" "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/keyring/rawaeskeyring" "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/keyring/rawrsakeyring" - "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/multithreading" "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/misc" + "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/multithreading" "github.com/aws/aws-encryption-sdk-dafny/releases/go/encryption-sdk/examples/utils" )