diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index 3985007b5..effd77843 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -33,19 +33,24 @@ jobs: uses: ./.github/workflows/library_rust_tests.yml with: dafny: '4.9.0' + daily-ci-go: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_go_tests.yml + with: + dafny: '4.9.0' daily-ci-interop-tests: if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/library_interop_tests.yml with: dafny: '4.9.0' - + daily-dafny-test-vectors: if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/library_interop_test_vectors.yml with: dafny: '4.9.0' - + daily-dafny-legacy-test-vectors: if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/library_legacy_interop_test_vectors.yml diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml new file mode 100644 index 000000000..f38c5363e --- /dev/null +++ b/.github/workflows/library_go_tests.yml @@ -0,0 +1,82 @@ +# This workflow performs tests in Go. +name: Library Go tests + +on: + workflow_call: + inputs: + dafny: + description: 'The Dafny version to run' + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean + +jobs: + testGo: + strategy: + fail-fast: false + matrix: + library: [AwsEncryptionSDK] + go-version: [ "1.23" ] + os: [ + # Sed script doesn't work properly on windows + # windows-latest, + ubuntu-latest, + macos-13, + ] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + - name: Init Submodules + shell: bash + run: | + git submodule update --init libraries + git submodule update --init --recursive mpl + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v2 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: GoTests + + - name: Setup Dafny + uses: dafny-lang/setup-dafny-action@v1.7.0 + with: + dafny-version: ${{ inputs.dafny }} + + - name: Setup NASM for Windows (aws-lc-sys) + if: matrix.os == 'windows-latest' + uses: ilammy/setup-nasm@v1 + + - 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 + + - name: Compile ${{ matrix.library }} implementation + shell: bash + working-directory: ${{ matrix.library }} + run: | + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_go CORES=$CORES + + - name: Test Go + working-directory: ${{ matrix.library }} + shell: bash + run: | + make test_go \ No newline at end of file diff --git a/.github/workflows/library_interop_test_vectors.yml b/.github/workflows/library_interop_test_vectors.yml index 2a2ef05a2..e384bdfe9 100644 --- a/.github/workflows/library_interop_test_vectors.yml +++ b/.github/workflows/library_interop_test_vectors.yml @@ -43,7 +43,7 @@ jobs: uses: aws-actions/configure-aws-credentials@v2 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 role-session-name: InterOpTests - uses: actions/checkout@v3 @@ -75,7 +75,7 @@ jobs: # TODO - uncomment this after Rust formatter works # - name: Rustfmt Check # uses: actions-rust-lang/rustfmt@v1 - + # TODO: Remove this after the formatting in Rust starts working - name: smithy-dafny Rust hacks if: matrix.language == 'rust' @@ -122,11 +122,11 @@ jobs: # This works because `node` is installed by default on GHA runners CORES=$(node -e 'console.log(os.cpus().length)') make transpile_net - + - name: Install Smithy-Dafny codegen dependencies if: matrix.language == 'rust' uses: ./.github/actions/install_smithy_dafny_codegen_dependencies - + # TODO: Remove this after checking in Rust polymorph code - name: Run make polymorph_rust if: matrix.language == 'rust' @@ -134,7 +134,7 @@ jobs: working-directory: ./${{ matrix.library }} run: | make polymorph_rust - + - name: Build ${{ matrix.library }} implementation in Rust if: matrix.language == 'rust' shell: bash @@ -279,7 +279,7 @@ jobs: - name: Install Smithy-Dafny codegen dependencies if: matrix.decrypting_language == 'rust' uses: ./.github/actions/install_smithy_dafny_codegen_dependencies - + # TODO: Remove this after checking in Rust polymorph code - name: Run make polymorph_rust if: matrix.decrypting_language == 'rust' diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml index 3d4dec075..41d221b19 100644 --- a/.github/workflows/manual.yml +++ b/.github/workflows/manual.yml @@ -37,3 +37,8 @@ jobs: with: dafny: ${{ inputs.dafny }} regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-go: + uses: ./.github/workflows/library_go_tests.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} \ No newline at end of file diff --git a/.github/workflows/nighly_dafny.yml b/.github/workflows/nighly_dafny.yml index de10f6510..fb8ea0f89 100644 --- a/.github/workflows/nighly_dafny.yml +++ b/.github/workflows/nighly_dafny.yml @@ -37,6 +37,12 @@ jobs: with: dafny: 'nightly-latest' regenerate-code: true + dafny-nightly-go: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_go_tests.yml + with: + dafny: 'nightly-latest' + regenerate-code: true cut-issue-on-failure: runs-on: ubuntu-latest diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 5b7f925fa..2eb130b8c 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -25,6 +25,10 @@ jobs: uses: ./.github/workflows/library_rust_tests.yml with: dafny: '4.9.0' + pr-ci-go: + uses: ./.github/workflows/library_go_tests.yml + with: + dafny: '4.9.0' pr-test-vectors: uses: ./.github/workflows/library_interop_tests.yml with: diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 78204dcd0..a0a084d3a 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -27,6 +27,10 @@ jobs: uses: ./.github/workflows/library_rust_tests.yml with: dafny: '4.9.0' + push-ci-go: + uses: ./.github/workflows/library_go_tests.yml + with: + dafny: '4.9.0' pr-test-vectors: uses: ./.github/workflows/library_interop_tests.yml with: diff --git a/AwsEncryptionSDK/Makefile b/AwsEncryptionSDK/Makefile index 1421a931f..a7b4437cd 100644 --- a/AwsEncryptionSDK/Makefile +++ b/AwsEncryptionSDK/Makefile @@ -1,6 +1,7 @@ # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: Apache-2.0 CORES=2 +ENABLE_EXTERN_PROCESSING=1 TRANSPILE_TESTS_IN_RUST := 1 @@ -64,3 +65,30 @@ SERVICE_DEPS_AwsEncryptionSdk := \ mpl/ComAmazonawsDynamodb \ mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \ mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore + +GO_MODULE_NAME="github.com/aws/aws-encryption-sdk" + +GO_DEPENDENCY_MODULE_NAMES := \ + --dependency-library-name=com.amazonaws.dynamodb=github.com/aws/aws-cryptographic-material-providers-library/dynamodb \ + --dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/kms \ + --dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/mpl \ + --dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/primitives \ + --dependency-library-name=aws.cryptography.materialProviders=github.com/aws/aws-cryptographic-material-providers-library/mpl \ + --dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \ + --dependency-library-name=sdk.com.amazonaws.kms=github.com/aws/aws-sdk-go-v2/service/kms + + +TRANSLATION_RECORD_GO := \ + mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \ + mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \ + mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \ + mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \ + mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr + +TYPES_FILE_PATH=dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.encryptionsdk.internaldafny.types\" } AwsCryptographyEncryptionSdkTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyEncryptionSdkTypes" + +INDEX_FILE_PATH=dafny/AwsEncryptionSdk/src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.encryptionsdk.internaldafny\" } ESDK refines AbstractAwsCryptographyEncryptionSdkService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module ESDK refines AbstractAwsCryptographyEncryptionSdkService {" diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy index 736240c08..bdb79f323 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy @@ -3,9 +3,7 @@ include "AwsEncryptionSdkOperations.dfy" -module - {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } - ESDK refines AbstractAwsCryptographyEncryptionSdkService { +module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } ESDK refines AbstractAwsCryptographyEncryptionSdkService { import Operations = AwsEncryptionSdkOperations import Primitives = AtomicPrimitives import MaterialProviders diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/api_client.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/api_client.go new file mode 100644 index 000000000..0ebe3337e --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/api_client.go @@ -0,0 +1,68 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygenerated + +import ( + "context" + + "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk/ESDK" + "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes" +) + +type Client struct { + DafnyClient AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient +} + +func NewClient(clientConfig awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig) (*Client, error) { + var dafnyConfig = AwsEncryptionSdkConfig_ToDafny(clientConfig) + var dafny_response = ESDK.Companion_Default___.ESDK(dafnyConfig) + if dafny_response.Is_Failure() { + panic("Client construction failed. This should never happen") + } + var dafnyClient = dafny_response.Extract().(AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient) + client := &Client{dafnyClient} + return client, nil +} + +func (client *Client) Encrypt(ctx context.Context, params awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) (*awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput, error) { + err := params.Validate() + if err != nil { + opaqueErr := awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError{ + ErrObject: err, + } + return nil, opaqueErr + } + + var dafny_request AwsCryptographyEncryptionSdkTypes.EncryptInput = EncryptInput_ToDafny(params) + var dafny_response = client.DafnyClient.Encrypt(dafny_request) + + if dafny_response.Is_Failure() { + err := dafny_response.Dtor_error().(AwsCryptographyEncryptionSdkTypes.Error) + return nil, Error_FromDafny(err) + } + var native_response = EncryptOutput_FromDafny(dafny_response.Dtor_value().(AwsCryptographyEncryptionSdkTypes.EncryptOutput)) + return &native_response, nil + +} + +func (client *Client) Decrypt(ctx context.Context, params awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) (*awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput, error) { + err := params.Validate() + if err != nil { + opaqueErr := awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError{ + ErrObject: err, + } + return nil, opaqueErr + } + + var dafny_request AwsCryptographyEncryptionSdkTypes.DecryptInput = DecryptInput_ToDafny(params) + var dafny_response = client.DafnyClient.Decrypt(dafny_request) + + if dafny_response.Is_Failure() { + err := dafny_response.Dtor_error().(AwsCryptographyEncryptionSdkTypes.Error) + return nil, Error_FromDafny(err) + } + var native_response = DecryptOutput_FromDafny(dafny_response.Dtor_value().(AwsCryptographyEncryptionSdkTypes.DecryptOutput)) + return &native_response, nil + +} diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go new file mode 100644 index 000000000..084b4352f --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -0,0 +1,389 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygenerated + +import ( + "unicode/utf8" + + "github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes" + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygenerated" + "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-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 { + + return func() AwsCryptographyEncryptionSdkTypes.EncryptInput { + + return AwsCryptographyEncryptionSdkTypes.Companion_EncryptInput_.Create_EncryptInput_(aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(nativeInput.Plaintext), aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), func() Wrappers.Option { + if (nativeInput.MaterialsManager) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_ToDafny(nativeInput.MaterialsManager)) + }(), func() Wrappers.Option { + if (nativeInput.Keyring) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.Keyring_ToDafny(nativeInput.Keyring)) + }(), aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(nativeInput.FrameLength)) + }() + +} + +func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput { + + return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput { + + return AwsCryptographyEncryptionSdkTypes.Companion_EncryptOutput_.Create_EncryptOutput_(aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(nativeOutput.Ciphertext), aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(nativeOutput.EncryptionContext), aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(nativeOutput.AlgorithmSuiteId)) + }() + +} + +func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput { + + return func() AwsCryptographyEncryptionSdkTypes.DecryptInput { + + return AwsCryptographyEncryptionSdkTypes.Companion_DecryptInput_.Create_DecryptInput_(aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(nativeInput.Ciphertext), func() Wrappers.Option { + if (nativeInput.MaterialsManager) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_ToDafny(nativeInput.MaterialsManager)) + }(), func() Wrappers.Option { + if (nativeInput.Keyring) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.Keyring_ToDafny(nativeInput.Keyring)) + }(), aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext)) + }() + +} + +func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput { + + return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput { + + return AwsCryptographyEncryptionSdkTypes.Companion_DecryptOutput_.Create_DecryptOutput_(aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(nativeOutput.Plaintext), aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(nativeOutput.EncryptionContext), aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(nativeOutput.AlgorithmSuiteId)) + }() + +} + +func AwsEncryptionSdkException_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException) AwsCryptographyEncryptionSdkTypes.Error { + return func() AwsCryptographyEncryptionSdkTypes.Error { + + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(nativeInput.Message)) + }() + +} + +func CollectionOfErrors_Input_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors) AwsCryptographyEncryptionSdkTypes.Error { + var e []interface{} + for _, i2 := range nativeInput.ListOfErrors { + e = append(e, Error_ToDafny(i2)) + } + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_CollectionOfErrors_(dafny.SeqOf(e...), dafny.SeqOfChars([]dafny.Char(nativeInput.Message)...)) +} +func OpaqueError_Input_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError) AwsCryptographyEncryptionSdkTypes.Error { + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_Opaque_(nativeInput.ErrObject) +} + +func Error_ToDafny(err error) AwsCryptographyEncryptionSdkTypes.Error { + switch err.(type) { + // Service Errors + case awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException: + return AwsEncryptionSdkException_ToDafny(err.(awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException)) + + //DependentErrors + case awscryptographyprimitivessmithygeneratedtypes.AwsCryptographicPrimitivesBaseException: + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(awscryptographyprimitivessmithygenerated.Error_ToDafny(err)) + + case awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersBaseException: + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(awscryptographymaterialproviderssmithygenerated.Error_ToDafny(err)) + + //Unmodelled Errors + case awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors: + return CollectionOfErrors_Input_ToDafny(err.(awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors)) + + default: + error, ok := err.(awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError) + if !ok { + panic("Error is not an OpaqueError") + } + return OpaqueError_Input_ToDafny(error) + } +} + +func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig) AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig { + return func() AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig { + + return AwsCryptographyEncryptionSdkTypes.Companion_AwsEncryptionSdkConfig_.Create_AwsEncryptionSdkConfig_(aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy), aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_ToDafny(nativeInput.MaxEncryptedDataKeys), aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_ToDafny(nativeInput.NetV4_0_0_RetryPolicy)) + }() + +} + +func 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 { + return nil + } + for _, e := range input { + v = append(v, e) + } + return dafny.SeqOf(v...) + }() +} + +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() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap()) + }() +} + +func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map { + return func() dafny.Map { + fieldValue := dafny.NewMapBuilder() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return fieldValue.ToMap() + }() +} + +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_ToDafny(input *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy) Wrappers.Option { + return func() Wrappers.Option { + if input == nil { + return Wrappers.Companion_Option_.Create_None_() + } + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == *input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) + }() +} + +func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input map[string]string) Wrappers.Option { + return func() Wrappers.Option { + fieldValue := dafny.NewMapBuilder() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap()) + }() +} + +func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + }() +} + +func aws_cryptography_encryptionSdk_EncryptOutput_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...) + }() +} + +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() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return fieldValue.ToMap() + }() +} + +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 { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy)) + }() +} + +func aws_cryptography_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_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) Wrappers.Option { + return func() Wrappers.Option { + if input == nil { + return Wrappers.Companion_Option_.Create_None_() + } + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == *input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId)) + }() +} + +func aws_cryptography_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_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return 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 new file mode 100644 index 000000000..65f1830e5 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -0,0 +1,436 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygenerated + +import ( + "github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes" + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygenerated" + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygeneratedtypes" + "github.com/aws/aws-cryptographic-material-providers-library/primitives/awscryptographyprimitivessmithygenerated" + "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes" + "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" +) + +func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.EncryptInput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput { + + 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 + } + return awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_FromDafny(dafnyInput.Dtor_materialsManager().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager)) + }(), + Keyring: func() awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { + if dafnyInput.Dtor_keyring().UnwrapOr(nil) == nil { + return nil + } + 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)), + } + +} + +func EncryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.EncryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput { + + 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 DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.DecryptInput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput { + + 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 + } + return awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_FromDafny(dafnyInput.Dtor_materialsManager().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager)) + }(), + Keyring: func() awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { + if dafnyInput.Dtor_keyring().UnwrapOr(nil) == nil { + return nil + } + return awscryptographymaterialproviderssmithygenerated.Keyring_FromDafny(dafnyInput.Dtor_keyring().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IKeyring)) + }(), + EncryptionContext: aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), + } + +} + +func DecryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.DecryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput { + + 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 AwsEncryptionSdkException_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.Error) awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException { + return awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException{Message: aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(dafnyOutput.Dtor_message())} + +} + +func CollectionOfErrors_Output_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.Error) awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors { + listOfErrors := dafnyOutput.Dtor_list() + message := dafnyOutput.Dtor_message() + t := awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors{} + for i := dafny.Iterate(listOfErrors); ; { + val, ok := i() + if !ok { + break + } + err := val.(AwsCryptographyEncryptionSdkTypes.Error) + t.ListOfErrors = append(t.ListOfErrors, Error_FromDafny(err)) + + } + t.Message = func() string { + var s string + for i := dafny.Iterate(message); ; { + val, ok := i() + if !ok { + return s + } else { + s = s + string(val.(dafny.Char)) + } + } + }() + return t +} +func OpaqueError_Output_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.Error) awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError { + return awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError{ + ErrObject: dafnyOutput.Dtor_obj(), + } +} + +func Error_FromDafny(err AwsCryptographyEncryptionSdkTypes.Error) error { + // Service Errors + if err.Is_AwsEncryptionSdkException() { + return AwsEncryptionSdkException_FromDafny(err) + } + + //DependentErrors + if err.Is_AwsCryptographyPrimitives() { + return awscryptographyprimitivessmithygenerated.Error_FromDafny(err.Dtor_AwsCryptographyPrimitives()) + } + + if err.Is_AwsCryptographyMaterialProviders() { + return awscryptographymaterialproviderssmithygenerated.Error_FromDafny(err.Dtor_AwsCryptographyMaterialProviders()) + } + + //Unmodelled Errors + if err.Is_CollectionOfErrors() { + return CollectionOfErrors_Output_FromDafny(err) + } + + return OpaqueError_Output_FromDafny(err) +} + +func AwsEncryptionSdkConfig_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig { + return awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig{CommitmentPolicy: aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_FromDafny(dafnyOutput.Dtor_commitmentPolicy().UnwrapOr(nil)), + MaxEncryptedDataKeys: aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(dafnyOutput.Dtor_maxEncryptedDataKeys().UnwrapOr(nil)), + NetV4_0_0_RetryPolicy: aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_FromDafny(dafnyOutput.Dtor_netV4__0__0__RetryPolicy().UnwrapOr(nil)), + } + +} + +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 { + 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_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 { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + return m + +} +func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { + var m map[string]string = make(map[string]string) + if input == nil { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + 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) + index := -1 + for allEnums := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy).Equals(inputEnum) { + break + } + } + } + + return &u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { + var m map[string]string = make(map[string]string) + if input == nil { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + 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) + index := -1 + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + break + } + } + } + + return u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptOutput_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)) + } + } + }() +} +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 { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + 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) + index := -1 + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy).Equals(inputEnum) { + break + } + } + } + + return &u.Values()[index] + }() +} +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_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()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + break + } + } + } + + 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_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(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).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)) + } + } + }() +} diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/enums.go new file mode 100644 index 000000000..0322a937c --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-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/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/errors.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/errors.go new file mode 100644 index 000000000..aa73b8a30 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/errors.go @@ -0,0 +1,17 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +import ( + "fmt" +) + +type AwsEncryptionSdkException struct { + AwsEncryptionSdkBaseException + Message string + ErrorCodeOverride *string +} + +func (e AwsEncryptionSdkException) Error() string { + return fmt.Sprintf("%s: %s", e.ErrorCodeOverride, e.Message) +} diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/types.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/types.go new file mode 100644 index 000000000..ca87e8b27 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/types.go @@ -0,0 +1,189 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +import ( + "fmt" + "unicode/utf8" + + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygeneratedtypes" +) + +type DecryptInput struct { + Ciphertext []byte + + EncryptionContext map[string]string + + Keyring awscryptographymaterialproviderssmithygeneratedtypes.IKeyring + + MaterialsManager awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager +} + +func (input DecryptInput) Validate() error { + if input.aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_Validate() + } + + return nil +} + +func (input DecryptInput) aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type DecryptOutput struct { + AlgorithmSuiteId awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + + EncryptionContext map[string]string + + Plaintext []byte +} + +func (input DecryptOutput) Validate() error { + if input.EncryptionContext == nil { + return fmt.Errorf("input.EncryptionContext is required but has a nil value.") + } + if input.aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_Validate() + } + + return nil +} + +func (input DecryptOutput) aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type EncryptInput struct { + Plaintext []byte + + AlgorithmSuiteId *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + + EncryptionContext map[string]string + + FrameLength *int64 + + Keyring awscryptographymaterialproviderssmithygeneratedtypes.IKeyring + + MaterialsManager awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager +} + +func (input EncryptInput) Validate() error { + if input.aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_Validate() + } + if input.FrameLength != nil { + if *input.FrameLength < 1 { + return fmt.Errorf("FrameLength has a minimum of 1 but has the value of %d.", *input.FrameLength) + } + if *input.FrameLength > 4294967296 { + return fmt.Errorf("FrameLength has a maximum of 4294967296 but has the value of %d.", *input.FrameLength) + } + } + + return nil +} + +func (input EncryptInput) aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type EncryptOutput struct { + AlgorithmSuiteId awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + + Ciphertext []byte + + EncryptionContext map[string]string +} + +func (input EncryptOutput) Validate() error { + if input.EncryptionContext == nil { + return fmt.Errorf("input.EncryptionContext is required but has a nil value.") + } + if input.aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_Validate() + } + + return nil +} + +func (input EncryptOutput) aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type AtomicPrimitivesReference struct { +} + +func (input AtomicPrimitivesReference) Validate() error { + + return nil +} + +type AwsEncryptionSdkConfig struct { + CommitmentPolicy *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy + + MaxEncryptedDataKeys *int64 + + NetV4_0_0_RetryPolicy *NetV4_0_0_RetryPolicy +} + +func (input AwsEncryptionSdkConfig) Validate() error { + if input.MaxEncryptedDataKeys != nil { + if *input.MaxEncryptedDataKeys < 1 { + return fmt.Errorf("CountingNumbers has a minimum of 1 but has the value of %d.", *input.MaxEncryptedDataKeys) + } + } + + return nil +} + +type MaterialProvidersReference struct { +} + +func (input MaterialProvidersReference) Validate() error { + + return nil +} + +type AwsEncryptionSdkBaseException interface { + // This is a dummy method to allow type assertion since Go empty interfaces + // aren't useful for type assertion checks. No concrete class is expected to implement + // this method. This is also not exported. + interfaceBindingMethod() +} diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/unmodelled_errors.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/unmodelled_errors.go new file mode 100644 index 000000000..d6f21280b --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/unmodelled_errors.go @@ -0,0 +1,26 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +import ( + "fmt" +) + +type CollectionOfErrors struct { + AwsEncryptionSdkBaseException + ListOfErrors []error + Message string +} + +func (e CollectionOfErrors) Error() string { + return fmt.Sprintf("message: %s\n err %v", e.Message, e.ListOfErrors) +} + +type OpaqueError struct { + AwsEncryptionSdkBaseException + ErrObject interface{} +} + +func (e OpaqueError) Error() string { + return fmt.Sprintf("message: %v", e.ErrObject) +} diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod new file mode 100644 index 000000000..bccec04e3 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod @@ -0,0 +1,46 @@ +module github.com/aws/aws-encryption-sdk + +go 1.23.0 + +require github.com/dafny-lang/DafnyStandardLibGo v0.0.0 + +replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../../aws-cryptographic-material-providers-library/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + +require ( + github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 + github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 + github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 + github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1 + +) + +require ( + github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect + github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect + github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect + github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect + github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect + github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect + github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect + github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect + github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 // indirect + github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect + github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect + github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect + github.com/aws/smithy-go v1.21.0 // indirect + github.com/google/uuid v1.6.0 // indirect + github.com/jmespath/go-jmespath v0.4.0 // indirect +) + +replace ( + github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ + +) + +replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.sum b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.sum new file mode 100644 index 000000000..2b40218dd --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.sum @@ -0,0 +1,49 @@ +github.com/aws/aws-sdk-go-v2 v1.31.0 h1:3V05LbxTSItI5kUqNwhJrrrY1BAXxXt0sN0l72QmG5U= +github.com/aws/aws-sdk-go-v2 v1.31.0/go.mod h1:ztolYtaEUtdpf9Wftr31CJfLVjOnD/CVRkKOOYgF8hA= +github.com/aws/aws-sdk-go-v2/config v1.27.37 h1:xaoIwzHVuRWRHFI0jhgEdEGc8xE1l91KaeRDsWEIncU= +github.com/aws/aws-sdk-go-v2/config v1.27.37/go.mod h1:S2e3ax9/8KnMSyRVNd3sWTKs+1clJ2f1U6nE0lpvQRg= +github.com/aws/aws-sdk-go-v2/credentials v1.17.35 h1:7QknrZhYySEB1lEXJxGAmuD5sWwys5ZXNr4m5oEz0IE= +github.com/aws/aws-sdk-go-v2/credentials v1.17.35/go.mod h1:8Vy4kk7at4aPSmibr7K+nLTzG6qUQAUO4tW49fzUV4E= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 h1:C/d03NAmh8C4BZXhuRNboF/DqhBkBCeDiJDcaqIT5pA= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14/go.mod h1:7I0Ju7p9mCIdlrfS+JCgqcYD0VXz/N4yozsox+0o078= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 h1:kYQ3H1u0ANr9KEKlGs/jTLrBFPo8P8NaH/w7A01NeeM= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18/go.mod h1:r506HmK5JDUh9+Mw4CfGJGSSoqIiLCndAuqXuhbv67Y= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 h1:Z7IdFUONvTcvS7YuhtVxN99v2cCoHRXOS4mTr0B/pUc= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18/go.mod h1:DkKMmksZVVyat+Y+r1dEOgJEfUeA7UngIHWeKsi0yNc= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 h1:DDN8yqYzFUDy2W5zk3tLQNKaO/1t0h3fNixPJacu264= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1/go.mod h1:k5XW8MoMxsNZ20RJmsokakvENUwQyjv69R9GqrI4xdQ= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 h1:QFASJGfT8wMXtuP3D5CRmMjARHv9ZmzFUMJznHDOY3w= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5/go.mod h1:QdZ3OmoIjSX+8D1OPAzPxDfjXASbBMDsz9qvtyIhtik= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 h1:dOxqOlOEa2e2heC/74+ZzcJOa27+F1aXFZpYgY/4QfA= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19/go.mod h1:aV6U1beLFvk3qAgognjS3wnGGoDId8hlPEiBsLHXVZE= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 h1:Xbwbmk44URTiHNx6PNo0ujDE6ERlsCKJD3u1zfnzAPg= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20/go.mod h1:oAfOFzUB14ltPZj1rWwRc3d/6OgD76R8KlvU3EqM9Fg= +github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 h1:jwWMpQ/1obJRdHaix9k10zWSnSMZGdDTZIDiS5CGzq8= +github.com/aws/aws-sdk-go-v2/service/kms v1.36.0/go.mod h1:OHmlX4+o0XIlJAQGAHPIy0N9yZcYS/vNG+T7geSNcFw= +github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 h1:2jrVsMHqdLD1+PA4BA6Nh1eZp0Gsy3mFSB5MxDvcJtU= +github.com/aws/aws-sdk-go-v2/service/sso v1.23.1/go.mod h1:XRlMvmad0ZNL+75C5FYdMvbbLkd6qiqz6foR1nA1PXY= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 h1:0L7yGCg3Hb3YQqnSgBTZM5wepougtL1aEccdcdYhHME= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1/go.mod h1:FnvDM4sfa+isJ3kDXIzAB9GAwVSzFzSy97uZ3IsHo4E= +github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 h1:8K0UNOkZiK9Uh3HIF6Bx0rcNCftqGCeKmOaR7Gp5BSo= +github.com/aws/aws-sdk-go-v2/service/sts v1.31.1/go.mod h1:yMWe0F+XG0DkRZK5ODZhG7BEFYhLXi2dqGsv6tX0cgI= +github.com/aws/smithy-go v1.21.0 h1:H7L8dtDRk0P1Qm6y0ji7MCYMQObJ5R9CRpyPhRUkLYA= +github.com/aws/smithy-go v1.21.0/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0 h1:ttdCpTQKspK9A/tqE1qnipvjp9IrURS1kC2w47we6GM= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= +github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= +github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= +github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= +github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo= +github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg= +github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo= +github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8= +github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U= +github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM= +github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4= +github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME= +gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0= +gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10= +gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI= diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go new file mode 100644 index 000000000..294d5c822 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-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/awscryptographyencryptionsdksmithygenerated/api_client.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/api_client.go new file mode 100644 index 000000000..0ebe3337e --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/api_client.go @@ -0,0 +1,68 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygenerated + +import ( + "context" + + "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk/ESDK" + "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes" +) + +type Client struct { + DafnyClient AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient +} + +func NewClient(clientConfig awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig) (*Client, error) { + var dafnyConfig = AwsEncryptionSdkConfig_ToDafny(clientConfig) + var dafny_response = ESDK.Companion_Default___.ESDK(dafnyConfig) + if dafny_response.Is_Failure() { + panic("Client construction failed. This should never happen") + } + var dafnyClient = dafny_response.Extract().(AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient) + client := &Client{dafnyClient} + return client, nil +} + +func (client *Client) Encrypt(ctx context.Context, params awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput) (*awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput, error) { + err := params.Validate() + if err != nil { + opaqueErr := awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError{ + ErrObject: err, + } + return nil, opaqueErr + } + + var dafny_request AwsCryptographyEncryptionSdkTypes.EncryptInput = EncryptInput_ToDafny(params) + var dafny_response = client.DafnyClient.Encrypt(dafny_request) + + if dafny_response.Is_Failure() { + err := dafny_response.Dtor_error().(AwsCryptographyEncryptionSdkTypes.Error) + return nil, Error_FromDafny(err) + } + var native_response = EncryptOutput_FromDafny(dafny_response.Dtor_value().(AwsCryptographyEncryptionSdkTypes.EncryptOutput)) + return &native_response, nil + +} + +func (client *Client) Decrypt(ctx context.Context, params awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) (*awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput, error) { + err := params.Validate() + if err != nil { + opaqueErr := awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError{ + ErrObject: err, + } + return nil, opaqueErr + } + + var dafny_request AwsCryptographyEncryptionSdkTypes.DecryptInput = DecryptInput_ToDafny(params) + var dafny_response = client.DafnyClient.Decrypt(dafny_request) + + if dafny_response.Is_Failure() { + err := dafny_response.Dtor_error().(AwsCryptographyEncryptionSdkTypes.Error) + return nil, Error_FromDafny(err) + } + var native_response = DecryptOutput_FromDafny(dafny_response.Dtor_value().(AwsCryptographyEncryptionSdkTypes.DecryptOutput)) + return &native_response, nil + +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go new file mode 100644 index 000000000..084b4352f --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -0,0 +1,389 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygenerated + +import ( + "unicode/utf8" + + "github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes" + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygenerated" + "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-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 { + + return func() AwsCryptographyEncryptionSdkTypes.EncryptInput { + + return AwsCryptographyEncryptionSdkTypes.Companion_EncryptInput_.Create_EncryptInput_(aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(nativeInput.Plaintext), aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext), func() Wrappers.Option { + if (nativeInput.MaterialsManager) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_ToDafny(nativeInput.MaterialsManager)) + }(), func() Wrappers.Option { + if (nativeInput.Keyring) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.Keyring_ToDafny(nativeInput.Keyring)) + }(), aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(nativeInput.AlgorithmSuiteId), aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(nativeInput.FrameLength)) + }() + +} + +func EncryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput) AwsCryptographyEncryptionSdkTypes.EncryptOutput { + + return func() AwsCryptographyEncryptionSdkTypes.EncryptOutput { + + return AwsCryptographyEncryptionSdkTypes.Companion_EncryptOutput_.Create_EncryptOutput_(aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(nativeOutput.Ciphertext), aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_ToDafny(nativeOutput.EncryptionContext), aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(nativeOutput.AlgorithmSuiteId)) + }() + +} + +func DecryptInput_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput) AwsCryptographyEncryptionSdkTypes.DecryptInput { + + return func() AwsCryptographyEncryptionSdkTypes.DecryptInput { + + return AwsCryptographyEncryptionSdkTypes.Companion_DecryptInput_.Create_DecryptInput_(aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(nativeInput.Ciphertext), func() Wrappers.Option { + if (nativeInput.MaterialsManager) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_ToDafny(nativeInput.MaterialsManager)) + }(), func() Wrappers.Option { + if (nativeInput.Keyring) == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(awscryptographymaterialproviderssmithygenerated.Keyring_ToDafny(nativeInput.Keyring)) + }(), aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(nativeInput.EncryptionContext)) + }() + +} + +func DecryptOutput_ToDafny(nativeOutput awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput) AwsCryptographyEncryptionSdkTypes.DecryptOutput { + + return func() AwsCryptographyEncryptionSdkTypes.DecryptOutput { + + return AwsCryptographyEncryptionSdkTypes.Companion_DecryptOutput_.Create_DecryptOutput_(aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(nativeOutput.Plaintext), aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(nativeOutput.EncryptionContext), aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(nativeOutput.AlgorithmSuiteId)) + }() + +} + +func AwsEncryptionSdkException_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException) AwsCryptographyEncryptionSdkTypes.Error { + return func() AwsCryptographyEncryptionSdkTypes.Error { + + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_ToDafny(nativeInput.Message)) + }() + +} + +func CollectionOfErrors_Input_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors) AwsCryptographyEncryptionSdkTypes.Error { + var e []interface{} + for _, i2 := range nativeInput.ListOfErrors { + e = append(e, Error_ToDafny(i2)) + } + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_CollectionOfErrors_(dafny.SeqOf(e...), dafny.SeqOfChars([]dafny.Char(nativeInput.Message)...)) +} +func OpaqueError_Input_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError) AwsCryptographyEncryptionSdkTypes.Error { + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_Opaque_(nativeInput.ErrObject) +} + +func Error_ToDafny(err error) AwsCryptographyEncryptionSdkTypes.Error { + switch err.(type) { + // Service Errors + case awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException: + return AwsEncryptionSdkException_ToDafny(err.(awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException)) + + //DependentErrors + case awscryptographyprimitivessmithygeneratedtypes.AwsCryptographicPrimitivesBaseException: + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(awscryptographyprimitivessmithygenerated.Error_ToDafny(err)) + + case awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersBaseException: + return AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(awscryptographymaterialproviderssmithygenerated.Error_ToDafny(err)) + + //Unmodelled Errors + case awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors: + return CollectionOfErrors_Input_ToDafny(err.(awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors)) + + default: + error, ok := err.(awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError) + if !ok { + panic("Error is not an OpaqueError") + } + return OpaqueError_Input_ToDafny(error) + } +} + +func AwsEncryptionSdkConfig_ToDafny(nativeInput awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig) AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig { + return func() AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig { + + return AwsCryptographyEncryptionSdkTypes.Companion_AwsEncryptionSdkConfig_.Create_AwsEncryptionSdkConfig_(aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDafny(nativeInput.CommitmentPolicy), aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_ToDafny(nativeInput.MaxEncryptedDataKeys), aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_ToDafny(nativeInput.NetV4_0_0_RetryPolicy)) + }() + +} + +func 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 { + return nil + } + for _, e := range input { + v = append(v, e) + } + return dafny.SeqOf(v...) + }() +} + +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() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap()) + }() +} + +func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_ToDafny(input map[string]string) dafny.Map { + return func() dafny.Map { + fieldValue := dafny.NewMapBuilder() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return fieldValue.ToMap() + }() +} + +func aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_ToDafny(input *awscryptographyencryptionsdksmithygeneratedtypes.NetV4_0_0_RetryPolicy) Wrappers.Option { + return func() Wrappers.Option { + if input == nil { + return Wrappers.Companion_Option_.Create_None_() + } + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == *input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy)) + }() +} + +func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_ToDafny(input map[string]string) Wrappers.Option { + return func() Wrappers.Option { + fieldValue := dafny.NewMapBuilder() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return Wrappers.Companion_Option_.Create_Some_(fieldValue.ToMap()) + }() +} + +func aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId) + }() +} + +func aws_cryptography_encryptionSdk_EncryptOutput_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...) + }() +} + +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() + for key, val := range input { + fieldValue.Add(aws_cryptography_materialProviders_EncryptionContext_key_ToDafny(key), aws_cryptography_materialProviders_EncryptionContext_value_ToDafny(val)) + } + return fieldValue.ToMap() + }() +} + +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 { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy)) + }() +} + +func aws_cryptography_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_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) Wrappers.Option { + return func() Wrappers.Option { + if input == nil { + return Wrappers.Companion_Option_.Create_None_() + } + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == *input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return Wrappers.Companion_Option_.Create_Some_(enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId)) + }() +} + +func aws_cryptography_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_algorithmSuiteId_ToDafny(input awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId) AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + return func() AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId { + + var index int + for _, enumVal := range input.Values() { + index++ + if enumVal == input { + break + } + } + var enum interface{} + for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { + var ok bool + enum, ok = allEnums() + if !ok { + break + } + } + return 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 new file mode 100644 index 000000000..65f1830e5 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -0,0 +1,436 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygenerated + +import ( + "github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes" + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygenerated" + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygeneratedtypes" + "github.com/aws/aws-cryptographic-material-providers-library/primitives/awscryptographyprimitivessmithygenerated" + "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk/awscryptographyencryptionsdksmithygeneratedtypes" + "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" +) + +func EncryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.EncryptInput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptInput { + + 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 + } + return awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_FromDafny(dafnyInput.Dtor_materialsManager().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager)) + }(), + Keyring: func() awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { + if dafnyInput.Dtor_keyring().UnwrapOr(nil) == nil { + return nil + } + 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)), + } + +} + +func EncryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.EncryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.EncryptOutput { + + 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 DecryptInput_FromDafny(dafnyInput AwsCryptographyEncryptionSdkTypes.DecryptInput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptInput { + + 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 + } + return awscryptographymaterialproviderssmithygenerated.CryptographicMaterialsManager_FromDafny(dafnyInput.Dtor_materialsManager().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager)) + }(), + Keyring: func() awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { + if dafnyInput.Dtor_keyring().UnwrapOr(nil) == nil { + return nil + } + return awscryptographymaterialproviderssmithygenerated.Keyring_FromDafny(dafnyInput.Dtor_keyring().UnwrapOr(nil).(AwsCryptographyMaterialProvidersTypes.IKeyring)) + }(), + EncryptionContext: aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext().UnwrapOr(nil)), + } + +} + +func DecryptOutput_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.DecryptOutput) awscryptographyencryptionsdksmithygeneratedtypes.DecryptOutput { + + 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 AwsEncryptionSdkException_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.Error) awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException { + return awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkException{Message: aws_cryptography_encryptionSdk_AwsEncryptionSdkException_message_FromDafny(dafnyOutput.Dtor_message())} + +} + +func CollectionOfErrors_Output_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.Error) awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors { + listOfErrors := dafnyOutput.Dtor_list() + message := dafnyOutput.Dtor_message() + t := awscryptographyencryptionsdksmithygeneratedtypes.CollectionOfErrors{} + for i := dafny.Iterate(listOfErrors); ; { + val, ok := i() + if !ok { + break + } + err := val.(AwsCryptographyEncryptionSdkTypes.Error) + t.ListOfErrors = append(t.ListOfErrors, Error_FromDafny(err)) + + } + t.Message = func() string { + var s string + for i := dafny.Iterate(message); ; { + val, ok := i() + if !ok { + return s + } else { + s = s + string(val.(dafny.Char)) + } + } + }() + return t +} +func OpaqueError_Output_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.Error) awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError { + return awscryptographyencryptionsdksmithygeneratedtypes.OpaqueError{ + ErrObject: dafnyOutput.Dtor_obj(), + } +} + +func Error_FromDafny(err AwsCryptographyEncryptionSdkTypes.Error) error { + // Service Errors + if err.Is_AwsEncryptionSdkException() { + return AwsEncryptionSdkException_FromDafny(err) + } + + //DependentErrors + if err.Is_AwsCryptographyPrimitives() { + return awscryptographyprimitivessmithygenerated.Error_FromDafny(err.Dtor_AwsCryptographyPrimitives()) + } + + if err.Is_AwsCryptographyMaterialProviders() { + return awscryptographymaterialproviderssmithygenerated.Error_FromDafny(err.Dtor_AwsCryptographyMaterialProviders()) + } + + //Unmodelled Errors + if err.Is_CollectionOfErrors() { + return CollectionOfErrors_Output_FromDafny(err) + } + + return OpaqueError_Output_FromDafny(err) +} + +func AwsEncryptionSdkConfig_FromDafny(dafnyOutput AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig { + return awscryptographyencryptionsdksmithygeneratedtypes.AwsEncryptionSdkConfig{CommitmentPolicy: aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_FromDafny(dafnyOutput.Dtor_commitmentPolicy().UnwrapOr(nil)), + MaxEncryptedDataKeys: aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_maxEncryptedDataKeys_FromDafny(dafnyOutput.Dtor_maxEncryptedDataKeys().UnwrapOr(nil)), + NetV4_0_0_RetryPolicy: aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy_FromDafny(dafnyOutput.Dtor_netV4__0__0__RetryPolicy().UnwrapOr(nil)), + } + +} + +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 { + 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_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 { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + return m + +} +func aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { + var m map[string]string = make(map[string]string) + if input == nil { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + 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) + index := -1 + for allEnums := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy).Equals(inputEnum) { + break + } + } + } + + return &u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { + var m map[string]string = make(map[string]string) + if input == nil { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + 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) + index := -1 + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + break + } + } + } + + return u.Values()[index] + }() +} +func aws_cryptography_encryptionSdk_EncryptOutput_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)) + } + } + }() +} +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 { + return nil + } + for i := dafny.Iterate(input.(dafny.Map).Items()); ; { + val, ok := i() + if !ok { + break + } + m[aws_cryptography_materialProviders_EncryptionContext_key_FromDafny((*val.(dafny.Tuple).IndexInt(0)))] = aws_cryptography_materialProviders_EncryptionContext_value_FromDafny((*val.(dafny.Tuple).IndexInt(1))) + } + 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) + index := -1 + for allEnums := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy).Equals(inputEnum) { + break + } + } + } + + return &u.Values()[index] + }() +} +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_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()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).Equals(inputEnum) { + break + } + } + } + + 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_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(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()); ; { + enum, ok := allEnums() + if ok { + index++ + if enum.(AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId).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)) + } + } + }() +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/errors.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/errors.go new file mode 100644 index 000000000..aa73b8a30 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/errors.go @@ -0,0 +1,17 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +import ( + "fmt" +) + +type AwsEncryptionSdkException struct { + AwsEncryptionSdkBaseException + Message string + ErrorCodeOverride *string +} + +func (e AwsEncryptionSdkException) Error() string { + return fmt.Sprintf("%s: %s", e.ErrorCodeOverride, e.Message) +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/types.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/types.go new file mode 100644 index 000000000..ca87e8b27 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/types.go @@ -0,0 +1,189 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +import ( + "fmt" + "unicode/utf8" + + "github.com/aws/aws-cryptographic-material-providers-library/mpl/awscryptographymaterialproviderssmithygeneratedtypes" +) + +type DecryptInput struct { + Ciphertext []byte + + EncryptionContext map[string]string + + Keyring awscryptographymaterialproviderssmithygeneratedtypes.IKeyring + + MaterialsManager awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager +} + +func (input DecryptInput) Validate() error { + if input.aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_Validate() + } + + return nil +} + +func (input DecryptInput) aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type DecryptOutput struct { + AlgorithmSuiteId awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + + EncryptionContext map[string]string + + Plaintext []byte +} + +func (input DecryptOutput) Validate() error { + if input.EncryptionContext == nil { + return fmt.Errorf("input.EncryptionContext is required but has a nil value.") + } + if input.aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_Validate() + } + + return nil +} + +func (input DecryptOutput) aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type EncryptInput struct { + Plaintext []byte + + AlgorithmSuiteId *awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + + EncryptionContext map[string]string + + FrameLength *int64 + + Keyring awscryptographymaterialproviderssmithygeneratedtypes.IKeyring + + MaterialsManager awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager +} + +func (input EncryptInput) Validate() error { + if input.aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_Validate() + } + if input.FrameLength != nil { + if *input.FrameLength < 1 { + return fmt.Errorf("FrameLength has a minimum of 1 but has the value of %d.", *input.FrameLength) + } + if *input.FrameLength > 4294967296 { + return fmt.Errorf("FrameLength has a maximum of 4294967296 but has the value of %d.", *input.FrameLength) + } + } + + return nil +} + +func (input EncryptInput) aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type EncryptOutput struct { + AlgorithmSuiteId awscryptographymaterialproviderssmithygeneratedtypes.ESDKAlgorithmSuiteId + + Ciphertext []byte + + EncryptionContext map[string]string +} + +func (input EncryptOutput) Validate() error { + if input.EncryptionContext == nil { + return fmt.Errorf("input.EncryptionContext is required but has a nil value.") + } + if input.aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_Validate() != nil { + return input.aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_Validate() + } + + return nil +} + +func (input EncryptOutput) aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_Validate() error { + for key, value := range input.EncryptionContext { + if !utf8.ValidString(key) { + return fmt.Errorf("Invalid UTF bytes %s ", key) + } + if !utf8.ValidString(value) { + return fmt.Errorf("Invalid UTF bytes %s ", value) + } + } + + return nil +} + +type AtomicPrimitivesReference struct { +} + +func (input AtomicPrimitivesReference) Validate() error { + + return nil +} + +type AwsEncryptionSdkConfig struct { + CommitmentPolicy *awscryptographymaterialproviderssmithygeneratedtypes.ESDKCommitmentPolicy + + MaxEncryptedDataKeys *int64 + + NetV4_0_0_RetryPolicy *NetV4_0_0_RetryPolicy +} + +func (input AwsEncryptionSdkConfig) Validate() error { + if input.MaxEncryptedDataKeys != nil { + if *input.MaxEncryptedDataKeys < 1 { + return fmt.Errorf("CountingNumbers has a minimum of 1 but has the value of %d.", *input.MaxEncryptedDataKeys) + } + } + + return nil +} + +type MaterialProvidersReference struct { +} + +func (input MaterialProvidersReference) Validate() error { + + return nil +} + +type AwsEncryptionSdkBaseException interface { + // This is a dummy method to allow type assertion since Go empty interfaces + // aren't useful for type assertion checks. No concrete class is expected to implement + // this method. This is also not exported. + interfaceBindingMethod() +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/unmodelled_errors.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/unmodelled_errors.go new file mode 100644 index 000000000..d6f21280b --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes/unmodelled_errors.go @@ -0,0 +1,26 @@ +// Code generated by smithy-go-codegen DO NOT EDIT. + +package awscryptographyencryptionsdksmithygeneratedtypes + +import ( + "fmt" +) + +type CollectionOfErrors struct { + AwsEncryptionSdkBaseException + ListOfErrors []error + Message string +} + +func (e CollectionOfErrors) Error() string { + return fmt.Sprintf("message: %s\n err %v", e.Message, e.ListOfErrors) +} + +type OpaqueError struct { + AwsEncryptionSdkBaseException + ErrObject interface{} +} + +func (e OpaqueError) Error() string { + return fmt.Sprintf("message: %v", e.ErrObject) +} diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/go.mod b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/go.mod new file mode 100644 index 000000000..dd7a9eaf4 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/go.mod @@ -0,0 +1,49 @@ +module github.com/aws/aws-encryption-sdk/test + +go 1.23.0 + +require github.com/dafny-lang/DafnyStandardLibGo v0.0.0 + +replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + +replace github.com/aws/aws-encryption-sdk v0.0.0 => ../ImplementationFromDafny-go + +require ( + github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 + github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 + github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 + github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 + github.com/aws/aws-encryption-sdk v0.0.0 + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1 + +) + +require ( + github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect + github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect + github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect + github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect + github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect + github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect + github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect + github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect + github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 // indirect + github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect + github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect + github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect + github.com/aws/smithy-go v1.21.0 // indirect + github.com/google/uuid v1.6.0 // indirect + github.com/jmespath/go-jmespath v0.4.0 // indirect +) + +replace ( + github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ + +) + +replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/go.sum b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/go.sum new file mode 100644 index 000000000..55861093d --- /dev/null +++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/go.sum @@ -0,0 +1,48 @@ +github.com/aws/aws-sdk-go-v2 v1.31.0 h1:3V05LbxTSItI5kUqNwhJrrrY1BAXxXt0sN0l72QmG5U= +github.com/aws/aws-sdk-go-v2 v1.31.0/go.mod h1:ztolYtaEUtdpf9Wftr31CJfLVjOnD/CVRkKOOYgF8hA= +github.com/aws/aws-sdk-go-v2/config v1.27.37 h1:xaoIwzHVuRWRHFI0jhgEdEGc8xE1l91KaeRDsWEIncU= +github.com/aws/aws-sdk-go-v2/config v1.27.37/go.mod h1:S2e3ax9/8KnMSyRVNd3sWTKs+1clJ2f1U6nE0lpvQRg= +github.com/aws/aws-sdk-go-v2/credentials v1.17.35 h1:7QknrZhYySEB1lEXJxGAmuD5sWwys5ZXNr4m5oEz0IE= +github.com/aws/aws-sdk-go-v2/credentials v1.17.35/go.mod h1:8Vy4kk7at4aPSmibr7K+nLTzG6qUQAUO4tW49fzUV4E= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 h1:C/d03NAmh8C4BZXhuRNboF/DqhBkBCeDiJDcaqIT5pA= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14/go.mod h1:7I0Ju7p9mCIdlrfS+JCgqcYD0VXz/N4yozsox+0o078= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 h1:kYQ3H1u0ANr9KEKlGs/jTLrBFPo8P8NaH/w7A01NeeM= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18/go.mod h1:r506HmK5JDUh9+Mw4CfGJGSSoqIiLCndAuqXuhbv67Y= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 h1:Z7IdFUONvTcvS7YuhtVxN99v2cCoHRXOS4mTr0B/pUc= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18/go.mod h1:DkKMmksZVVyat+Y+r1dEOgJEfUeA7UngIHWeKsi0yNc= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 h1:DDN8yqYzFUDy2W5zk3tLQNKaO/1t0h3fNixPJacu264= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1/go.mod h1:k5XW8MoMxsNZ20RJmsokakvENUwQyjv69R9GqrI4xdQ= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 h1:QFASJGfT8wMXtuP3D5CRmMjARHv9ZmzFUMJznHDOY3w= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5/go.mod h1:QdZ3OmoIjSX+8D1OPAzPxDfjXASbBMDsz9qvtyIhtik= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 h1:dOxqOlOEa2e2heC/74+ZzcJOa27+F1aXFZpYgY/4QfA= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19/go.mod h1:aV6U1beLFvk3qAgognjS3wnGGoDId8hlPEiBsLHXVZE= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 h1:Xbwbmk44URTiHNx6PNo0ujDE6ERlsCKJD3u1zfnzAPg= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20/go.mod h1:oAfOFzUB14ltPZj1rWwRc3d/6OgD76R8KlvU3EqM9Fg= +github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 h1:jwWMpQ/1obJRdHaix9k10zWSnSMZGdDTZIDiS5CGzq8= +github.com/aws/aws-sdk-go-v2/service/kms v1.36.0/go.mod h1:OHmlX4+o0XIlJAQGAHPIy0N9yZcYS/vNG+T7geSNcFw= +github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 h1:2jrVsMHqdLD1+PA4BA6Nh1eZp0Gsy3mFSB5MxDvcJtU= +github.com/aws/aws-sdk-go-v2/service/sso v1.23.1/go.mod h1:XRlMvmad0ZNL+75C5FYdMvbbLkd6qiqz6foR1nA1PXY= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 h1:0L7yGCg3Hb3YQqnSgBTZM5wepougtL1aEccdcdYhHME= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1/go.mod h1:FnvDM4sfa+isJ3kDXIzAB9GAwVSzFzSy97uZ3IsHo4E= +github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 h1:8K0UNOkZiK9Uh3HIF6Bx0rcNCftqGCeKmOaR7Gp5BSo= +github.com/aws/aws-sdk-go-v2/service/sts v1.31.1/go.mod h1:yMWe0F+XG0DkRZK5ODZhG7BEFYhLXi2dqGsv6tX0cgI= +github.com/aws/smithy-go v1.21.0 h1:H7L8dtDRk0P1Qm6y0ji7MCYMQObJ5R9CRpyPhRUkLYA= +github.com/aws/smithy-go v1.21.0/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1 h1:dOgaw3i0I9nWKPjfXYzEfgWsVRJykL6FA18DErvQiJQ= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= +github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= +github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= +github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= +github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo= +github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg= +github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo= +github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8= +github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U= +github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM= +github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4= +github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME= +gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0= +gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10= +gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI= diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java index c24a0e9ec..2fb2fd638 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java @@ -10,8 +10,14 @@ public class OpaqueError extends RuntimeException { */ private final Object obj; + /** + * A best effort text representation of obj. + */ + private final String altText; + protected OpaqueError(BuilderImpl builder) { super(messageFromBuilder(builder), builder.cause()); + this.altText = builder.altText(); this.obj = builder.obj(); } @@ -46,6 +52,13 @@ public Object obj() { return this.obj; } + /** + * @return A best effort text representation of obj. + */ + public String altText() { + return this.altText; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -85,6 +98,16 @@ public interface Builder { */ Object obj(); + /** + * @param altText A best effort text representation of obj. + */ + Builder altText(String altText); + + /** + * @return A best effort text representation of obj. + */ + String altText(); + OpaqueError build(); } @@ -96,6 +119,8 @@ static class BuilderImpl implements Builder { protected Object obj; + protected String altText; + protected BuilderImpl() {} protected BuilderImpl(OpaqueError model) { @@ -131,6 +156,15 @@ public Object obj() { return this.obj; } + public Builder altText(String altText) { + this.altText = altText; + return this; + } + + public String altText() { + return this.altText; + } + public OpaqueError build() { if ( this.obj != null && this.cause == null && this.obj instanceof Throwable diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 6dade7a48..81d595c2e 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -54,7 +54,7 @@ PROJECT_DEPENDENCIES := \ AwsEncryptionSDK \ # Since we are packaging projects differently, we cannot make assumptions -# about where the files are located. +# about where the files are located. # This is here to get unblocked but should be removed once we have migrated packages # to the new packaging format. PROJECT_INDEX := \ diff --git a/mpl b/mpl index 1915a11bb..93798f13e 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit 1915a11bb84d3d9135b89d2a46ec9d6dff27b493 +Subproject commit 93798f13e64a9b83ed909d1ef27cafa3f00f3450