From b8296015e154e914dbf53210690537696ac87ba0 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Mon, 30 Dec 2024 11:12:57 -0800 Subject: [PATCH 01/14] Bring from my Go branch --- .../library_interop_test_vectors.yml | 58 +++++++++++++++++- TestVectors/Makefile | 60 +++++++++++++++++++ .../WrappedESDK/extern.go | 11 ++++ .../go/ImplementationFromDafny-go/go.mod | 49 +++++++++++++++ .../TestWrappedESDKMain/extern.go | 19 ++++++ .../runtimes/go/TestsFromDafny-go/go.mod | 51 ++++++++++++++++ 6 files changed, 245 insertions(+), 3 deletions(-) create mode 100644 TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go create mode 100644 TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod create mode 100644 TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go create mode 100644 TestVectors/runtimes/go/TestsFromDafny-go/go.mod diff --git a/.github/workflows/library_interop_test_vectors.yml b/.github/workflows/library_interop_test_vectors.yml index 2a2ef05a2..36f83068e 100644 --- a/.github/workflows/library_interop_test_vectors.yml +++ b/.github/workflows/library_interop_test_vectors.yml @@ -25,7 +25,7 @@ jobs: ubuntu-latest, macos-13, ] - language: [java, net, rust] + language: [java, net, rust, go] # https://taskei.amazon.dev/tasks/CrypTool-5284 dotnet-version: ["6.0.x"] runs-on: ${{ matrix.os }} @@ -87,6 +87,15 @@ jobs: sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' mpl/smithy-dafny/SmithyDafnyMakefile.mk fi + - name: Setup Go + uses: actions/setup-go@v5 + with: + go-version: "1.23" + + - name: Install Go imports + run: | + go install golang.org/x/tools/cmd/goimports@latest + - name: Setup NASM for Windows in Rust (aws-lc-sys) if: matrix.language == 'rust' && matrix.os == 'windows-latest' uses: ilammy/setup-nasm@v1 @@ -142,6 +151,23 @@ jobs: run: | CORES=$(node -e 'console.log(os.cpus().length)') make transpile_rust CORES=$CORES + + - name: Build ${{ matrix.library }} implementation in Go + if: matrix.language == 'go' + 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 + + # TODO: Remove this after Go polymorph does not generate unwanted duplicate code. + - name: Purge polymorph code in Go + if: matrix.language == 'go' + shell: bash + working-directory: ./${{ matrix.library }} + run: | + make purge_polymorph_code - name: Setup gradle if: matrix.language == 'java' @@ -177,8 +203,8 @@ jobs: ubuntu-latest, macos-13, ] - encrypting_language: [java, net, rust] - decrypting_language: [java, net, rust] + encrypting_language: [java, net, rust, go] + decrypting_language: [java, net, rust, go] # https://taskei.amazon.dev/tasks/CrypTool-5284 dotnet-version: ["6.0.x"] runs-on: ${{ matrix.os }} @@ -240,6 +266,15 @@ jobs: sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' mpl/smithy-dafny/SmithyDafnyMakefile.mk fi + - name: Setup Go + uses: actions/setup-go@v5 + with: + go-version: "1.23" + + - name: Install Go imports + run: | + go install golang.org/x/tools/cmd/goimports@latest + - name: Setup NASM for Windows in Rust (aws-lc-sys) if: matrix.decrypting_language == 'rust' && matrix.os == 'windows-latest' uses: ilammy/setup-nasm@v1 @@ -295,6 +330,23 @@ jobs: run: | CORES=$(node -e 'console.log(os.cpus().length)') make transpile_rust CORES=$CORES + + - name: Build ${{ matrix.library }} implementation in Go + if: matrix.decrypting_language == 'go' + 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 + + # TODO: Remove this after Go polymorph does not generate unwanted duplicate code. + - name: Purge polymorph code in Go + if: matrix.decrypting_language == 'go' + shell: bash + working-directory: ./${{ matrix.library }} + run: | + make purge_polymorph_code - name: Download Encrypt Manifest Artifact uses: actions/download-artifact@v4 diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 6dade7a48..ae8ae3d14 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 TRANSPILE_TESTS_IN_RUST=1 include ../SharedMakefileV2.mk @@ -109,10 +110,48 @@ REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;' REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;' REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;' +# Go + +GO_MODULE_NAME="github.com/aws/aws-encryption-sdk/testvectors" + +GO_DEPENDENCY_MODULE_NAMES := \ + --dependency-library-name=aws.cryptography.encryptionSdk=github.com/aws/aws-encryption-sdk \ + --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 := \ + AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \ + 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 \ + mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr + +# Constants for languages that drop extern names (Go) + +WRAPPED_INDEX_FILE_PATH=dafny/TestVectors/src/LibraryIndex.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.encryptionsdk.internaldafny.wrapped\" } WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService" + transpile_implementation_java: _replace_main_method_name_java transpile_implementation_net: _replace_main_method_name_net transpile_implementation_rust: _replace_main_method_name_rust +_polymorph_go: purge_polymorph_code + +# Smithy-dafny generated shim needs a long term fix. +# TODO: Remove this commands once smithy-dafny is fixed +# This commands does not work on windows +# https://taskei.amazon.dev/tasks/CrypTool-5283 +purge_polymorph_code: + find .. -name "shim.go" | xargs sed -i $(SED_PARAMETER) 's/(_static \*CompanionStruct_Default___)//g' + # TODO: Remove after wrapped client issue is fixed in Rust _polymorph_rust: _remove_wrapped_client_rust @@ -150,6 +189,10 @@ test_generate_vectors_rust: cd ../../ cp dafny/TestVectors/test/keys.json runtimes/rust/ +test_generate_vectors_go: + go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go encrypt-manifest --encrypt-manifest-output ../ + cp dafny/TestVectors/test/keys.json runtimes/go + test_encrypt_vectors_java: gradle -p runtimes/java run --args="encrypt --manifest-path . --decrypt-manifest-path ." @@ -164,6 +207,9 @@ test_encrypt_vectors_rust: cargo run --bin test-vectors --features="wrapped-client" --release -- encrypt --manifest-path . --decrypt-manifest-path . && \ cd ../../ +test_encrypt_vectors_go: + go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go encrypt --manifest-path=.. --decrypt-manifest-path=.. + test_decrypt_encrypt_vectors_java: gradle -p runtimes/java run --args="decrypt --manifest-path . --manifest-name decrypt-manifest.json" @@ -184,6 +230,20 @@ test_decrypt_encrypt_vectors_rust: cargo run --bin test-vectors --features="wrapped-client" --release -- decrypt --manifest-path . --manifest-name decrypt-manifest.json && \ cd ../../ +test_decrypt_encrypt_vectors_go: + go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. + _polymorph_dependencies: @echo "No polymorphing of dependency" +_sed_types_file_remove_extern: + @echo "No extern to process for ESDK TestVectors" + +_sed_index_file_remove_extern: + @echo "No extern to process for ESDK TestVectors" + +_sed_types_file_add_extern: + @echo "No extern to process for ESDK TestVectors" + +_sed_index_file_add_extern: + @echo "No extern to process for ESDK TestVectors" \ No newline at end of file diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go b/TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go new file mode 100644 index 000000000..f7c876b96 --- /dev/null +++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go @@ -0,0 +1,11 @@ +package WrappedESDK + +import ( + "github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes" + "github.com/aws/aws-encryption-sdk/test/WrappedAwsCryptographyEncryptionSdkService" + "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" +) + +func (_static CompanionStruct_Default___) WrappedESDK(config AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) Wrappers.Result { + return WrappedAwsCryptographyEncryptionSdkService.WrappedESDK(config) +} diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod new file mode 100644 index 000000000..be16b875a --- /dev/null +++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod @@ -0,0 +1,49 @@ +module github.com/aws/aws-encryption-sdk/testvectors + +go 1.23.2 + +replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + +replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ + +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/ + github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 => ../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-encryption-sdk v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-encryption-sdk/test v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/TestsFromDafny-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-cryptographic-material-providers-library/testvectors v0.0.0 + github.com/aws/aws-encryption-sdk v0.0.0 + github.com/aws/aws-encryption-sdk/test v0.0.0 + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 + github.com/dafny-lang/DafnyStandardLibGo v0.0.0 +) + +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 +) \ No newline at end of file diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go b/TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go new file mode 100644 index 000000000..d670fc2ac --- /dev/null +++ b/TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go @@ -0,0 +1,19 @@ +package TestWrappedESDKMain + +import ( + os "os" + + "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" +) + +// TODO: Remove this once Dafny bug is fixed. +// Dafny bug: https://t.corp.amazon.com/9a9028fd-2711-4843-b8f0-09965f7e61a7/communication#f03694be-7410-47f9-866d-e43093b018f9 +var m_TestWrappedESDKMain = CompanionStruct_Default___{} + +func (CompanionStruct_Default___) GetTestVectorExecutionDirectory() dafny.Sequence { + cwd, err := os.Getwd() + if err != nil { + panic(err) + } + return dafny.SeqOfString(cwd + "/../../../") +} diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod new file mode 100644 index 000000000..17de7878f --- /dev/null +++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod @@ -0,0 +1,51 @@ +module github.com/aws/aws-encryption-sdk/testvectors/test + +go 1.23.2 + +replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + +replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../aws-cryptographic-material-providers-library/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ + +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/ + github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 => ../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-encryption-sdk v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-encryption-sdk/test v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/TestsFromDafny-go + github.com/aws/aws-encryption-sdk/testvectors 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-cryptographic-material-providers-library/testvectors v0.0.0 + github.com/aws/aws-encryption-sdk v0.0.0 + github.com/aws/aws-encryption-sdk/testvectors v0.0.0 + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 + github.com/dafny-lang/DafnyStandardLibGo v0.0.0 +) + +require ( + github.com/aws/aws-encryption-sdk/test v0.0.0 // indirect + 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 +) \ No newline at end of file From d76eb9d98d4e511af0bda137e35145ad0a6ae839 Mon Sep 17 00:00:00 2001 From: Rishav karanjit Date: Tue, 31 Dec 2024 13:33:47 -0800 Subject: [PATCH 02/14] Update Makefile --- TestVectors/Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 2ddeae58e..23131cae0 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -2,7 +2,6 @@ # SPDX-License-Identifier: Apache-2.0 CORES=2 - ENABLE_EXTERN_PROCESSING=1 TRANSPILE_TESTS_IN_RUST=1 @@ -246,4 +245,4 @@ _sed_types_file_add_extern: @echo "No extern to process for ESDK TestVectors" _sed_index_file_add_extern: - @echo "No extern to process for ESDK TestVectors" \ No newline at end of file + @echo "No extern to process for ESDK TestVectors" From 052acf2c0d56f16bcdc1beed00526b3c6db99983 Mon Sep 17 00:00:00 2001 From: Rishav karanjit Date: Tue, 31 Dec 2024 13:37:51 -0800 Subject: [PATCH 03/14] Update LibraryIndex.dfy --- TestVectors/dafny/TestVectors/src/LibraryIndex.dfy | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy b/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy index 7097ff992..57d7f92f7 100644 --- a/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy +++ b/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy @@ -3,9 +3,7 @@ include "../Model/AwsCryptographyEncryptionSdkTypesWrapped.dfy" -module - {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.wrapped" } - WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService +module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.wrapped" } WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService { import WrappedService = ESDK @@ -51,4 +49,4 @@ module netV4_0_0_RetryPolicy := Some(netV4_0_0_RetryPolicy) ) } -} \ No newline at end of file +} From 7e9a366e51a317ec3918ab2d62d43cf46865f888 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 10:25:03 -0800 Subject: [PATCH 04/14] auto commit --- TestVectors/Makefile | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 23131cae0..31c5bb6d0 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -150,6 +150,12 @@ _polymorph_go: purge_polymorph_code # https://taskei.amazon.dev/tasks/CrypTool-5283 purge_polymorph_code: find .. -name "shim.go" | xargs sed -i $(SED_PARAMETER) 's/(_static \*CompanionStruct_Default___)//g' + rm -rf runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated \ + runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes \ + runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService \ + runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated \ + runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes \ + runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService # TODO: Remove after wrapped client issue is fixed in Rust _polymorph_rust: _remove_wrapped_client_rust From a584264a851ef8c05f9f2f6b17da7d7c684ed4c2 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 10:31:13 -0800 Subject: [PATCH 05/14] auto commit --- .../go/ImplementationFromDafny-go/go.mod | 2 +- .../go/ImplementationFromDafny-go/go.sum | 48 +++++++++++++++++++ .../runtimes/go/TestsFromDafny-go/go.mod | 2 +- .../runtimes/go/TestsFromDafny-go/go.sum | 48 +++++++++++++++++++ 4 files changed, 98 insertions(+), 2 deletions(-) create mode 100644 TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum create mode 100644 TestVectors/runtimes/go/TestsFromDafny-go/go.sum diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod index be16b875a..dac0bd281 100644 --- a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod +++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod @@ -46,4 +46,4 @@ require ( 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 -) \ No newline at end of file +) diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum new file mode 100644 index 000000000..3f00f4e18 --- /dev/null +++ b/TestVectors/runtimes/go/ImplementationFromDafny-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.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/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/TestVectors/runtimes/go/TestsFromDafny-go/go.mod b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod index 17de7878f..bf78320ae 100644 --- a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod +++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod @@ -48,4 +48,4 @@ require ( 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 -) \ No newline at end of file +) diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.sum b/TestVectors/runtimes/go/TestsFromDafny-go/go.sum new file mode 100644 index 000000000..3f00f4e18 --- /dev/null +++ b/TestVectors/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.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/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= From d50d3f37c19749c0188521ed7ede1c5f71e7495e Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 10:54:35 -0800 Subject: [PATCH 06/14] Update go test workflow --- .github/workflows/library_go_tests.yml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml index f38c5363e..1b8a9b62f 100644 --- a/.github/workflows/library_go_tests.yml +++ b/.github/workflows/library_go_tests.yml @@ -19,7 +19,7 @@ jobs: strategy: fail-fast: false matrix: - library: [AwsEncryptionSDK] + library: [AwsEncryptionSDK, TestVectors] go-version: [ "1.23" ] os: [ # Sed script doesn't work properly on windows @@ -74,6 +74,14 @@ jobs: # This works because `node` is installed by default on GHA runners CORES=$(node -e 'console.log(os.cpus().length)') make transpile_go CORES=$CORES + + # TODO: Remove this after Go polymorph does not generate unwanted duplicate code. + - name: Purge polymorph code in Go + if: matrix.library == 'TestVectorsAwsCryptographicMaterialProviders' + working-directory: ./${{ matrix.library }} + shell: bash + run: | + make purge_polymorph_code - name: Test Go working-directory: ${{ matrix.library }} From 10462faf0776500f01d1b11e301300ef06aa44f4 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 11:11:07 -0800 Subject: [PATCH 07/14] auto commit --- .github/workflows/library_go_tests.yml | 2 +- .github/workflows/library_interop_test_vectors.yml | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml index 1b8a9b62f..90ccfbf18 100644 --- a/.github/workflows/library_go_tests.yml +++ b/.github/workflows/library_go_tests.yml @@ -77,7 +77,7 @@ jobs: # TODO: Remove this after Go polymorph does not generate unwanted duplicate code. - name: Purge polymorph code in Go - if: matrix.library == 'TestVectorsAwsCryptographicMaterialProviders' + if: matrix.library == 'TestVectors' working-directory: ./${{ matrix.library }} shell: bash run: | diff --git a/.github/workflows/library_interop_test_vectors.yml b/.github/workflows/library_interop_test_vectors.yml index e47ee678f..36f83068e 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' @@ -131,11 +131,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' @@ -143,7 +143,7 @@ jobs: working-directory: ./${{ matrix.library }} run: | make polymorph_rust - + - name: Build ${{ matrix.library }} implementation in Rust if: matrix.language == 'rust' shell: bash @@ -314,7 +314,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' From 59216fc97e30877e56453f33999c5e3fd21f1aa8 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 12:27:18 -0800 Subject: [PATCH 08/14] auto commit --- TestVectors/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 31c5bb6d0..b458aba97 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -236,6 +236,7 @@ test_decrypt_encrypt_vectors_rust: cd ../../ test_decrypt_encrypt_vectors_go: + ls runtimes/go/ && \ go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. _polymorph_dependencies: From 77a454cefb6188706b1161805e9f9b571de29022 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 12:34:38 -0800 Subject: [PATCH 09/14] auto commit --- TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod | 6 ++---- TestVectors/runtimes/go/TestsFromDafny-go/go.mod | 6 ++---- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod index dac0bd281..b4ecbc1fd 100644 --- a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod +++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod @@ -2,17 +2,15 @@ module github.com/aws/aws-encryption-sdk/testvectors go 1.23.2 -replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ - -replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ - 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/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 => ../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-encryption-sdk v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-encryption-sdk/test v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/ + github.com/dafny-lang/DafnyStandardLibGo v0.0.0 => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ ) require ( diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod index bf78320ae..afed1f510 100644 --- a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod +++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod @@ -2,18 +2,16 @@ module github.com/aws/aws-encryption-sdk/testvectors/test go 1.23.2 -replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ - -replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../aws-cryptographic-material-providers-library/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ - 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/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 => ../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-encryption-sdk v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-encryption-sdk/test v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/TestsFromDafny-go github.com/aws/aws-encryption-sdk/testvectors v0.0.0 => ../ImplementationFromDafny-go/ + github.com/dafny-lang/DafnyStandardLibGo v0.0.0 => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ ) require ( From 69a79c286eed264e91e712b62c4f86eed00bd4c7 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 13:03:12 -0800 Subject: [PATCH 10/14] auto commit --- .github/workflows/library_go_tests.yml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml index 90ccfbf18..8f31e011f 100644 --- a/.github/workflows/library_go_tests.yml +++ b/.github/workflows/library_go_tests.yml @@ -74,7 +74,15 @@ jobs: # 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: Unzip .NET Retry Flag Manifests + shell: bash + working-directory: TestVectors/dafny/TestVectors/test/ + run: | + unzip invalid-Net-4.0.0.zip -d invalid-Net-4.0.0 + unzip v4-Net-4.0.1.zip -d v4-Net-4.0.1 + unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0 + # TODO: Remove this after Go polymorph does not generate unwanted duplicate code. - name: Purge polymorph code in Go if: matrix.library == 'TestVectors' From a2b8e14cef9f7a9b7dce89f21798104404f1afbc Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 13:04:07 -0800 Subject: [PATCH 11/14] auto commit --- TestVectors/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index b458aba97..897362cc0 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -237,7 +237,7 @@ test_decrypt_encrypt_vectors_rust: test_decrypt_encrypt_vectors_go: ls runtimes/go/ && \ - go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. + go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. --manifest-name decrypt-manifest.json _polymorph_dependencies: @echo "No polymorphing of dependency" From 97292d24e23bd64d3a895592022c2654bc751854 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 13:08:48 -0800 Subject: [PATCH 12/14] auto commit --- TestVectors/Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 897362cc0..e0af17d84 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -236,7 +236,6 @@ test_decrypt_encrypt_vectors_rust: cd ../../ test_decrypt_encrypt_vectors_go: - ls runtimes/go/ && \ go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. --manifest-name decrypt-manifest.json _polymorph_dependencies: From f37693f2bb50bc14fa4245dd289c64e869eceeb7 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 2 Jan 2025 15:24:16 -0800 Subject: [PATCH 13/14] auto commit --- TestVectors/Makefile | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index e0af17d84..4537bc851 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -101,6 +101,10 @@ IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN= \ let dafny_args = dafny_runtime::Sequence::from_array_owned(dafny_strings);\ r\#_WrappedESDKMain_Compile::_default::Main2(\&dafny_args);" +IMPLEMENTATION_FROM_DAFNY_TV_GO_FILE=runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny.go +IMPLEMENTATION_FROM_DAFNY_TV_GO_MPL_MAIN="m_WrappedMaterialProvidersMain.Companion_Default___.Main(_dafny.FromMainArguments(os.Args))" +IMPLEMENTATION_FROM_DAFNY_TV_GO_ESDK_MAIN="m_WrappedESDKMain.Companion_Default___.Main2(_dafny.FromMainArguments(os.Args))" + # TODO: Remove after wrapped client issue is fixed in Rust REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs @@ -141,6 +145,7 @@ WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedESDK refines WrappedAbst transpile_implementation_java: _replace_main_method_name_java transpile_implementation_net: _replace_main_method_name_net transpile_implementation_rust: _replace_main_method_name_rust +transpile_implementation_go: _replace_main_method_name_go _polymorph_go: purge_polymorph_code @@ -169,6 +174,9 @@ _replace_main_method_name_net: _replace_main_method_name_rust: $(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN) +_replace_main_method_name_go: + $(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_GO_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_GO_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_GO_ESDK_MAIN) + # TODO: Remove after wrapped client issue is fixed in Rust _remove_wrapped_client_rust: $(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1) @@ -236,7 +244,7 @@ test_decrypt_encrypt_vectors_rust: cd ../../ test_decrypt_encrypt_vectors_go: - go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. --manifest-name decrypt-manifest.json + go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. --manifest-name=decrypt-manifest.json _polymorph_dependencies: @echo "No polymorphing of dependency" From 47323dbc697c19f0e42d0a8a0c5ba6fa11dbeca6 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 3 Jan 2025 09:43:11 -0800 Subject: [PATCH 14/14] auto commit --- TestVectors/Makefile | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 4537bc851..ad4bc090a 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -129,11 +129,11 @@ GO_DEPENDENCY_MODULE_NAMES := \ TRANSLATION_RECORD_GO := \ AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \ - 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 \ + 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 \ mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr # Constants for languages that drop extern names (Go)