chore(test vectors): Add interop test in Go with CI (#731)

.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,22 @@ 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'
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          make purge_polymorph_code
 
       - name: Test Go
         working-directory: ${{ matrix.library }}

.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 }}
@@ -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'
@@ -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
@@ -122,26 +131,43 @@ 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'
           shell: bash
           working-directory: ./${{ matrix.library }}
           run: |
             make polymorph_rust
-
+        
         - name: Build ${{ matrix.library }} implementation in Rust
           if: matrix.language == 'rust'
           shell: bash
           working-directory: ./${{ matrix.library }}
           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
@@ -279,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'
@@ -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

TestVectors/Makefile

@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 CORES=2
-
+ENABLE_EXTERN_PROCESSING=1
 TRANSPILE_TESTS_IN_RUST=1
 
 include ../SharedMakefileV2.mk
@@ -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
@@ -109,9 +113,54 @@ 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
+transpile_implementation_go: _replace_main_method_name_go
+
+_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'
+	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
@@ -125,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)
@@ -150,6 +202,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 +220,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 +243,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=.. --manifest-name=decrypt-manifest.json
+
 _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"

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)
     )
   }
-}
+}

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)
+}

TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -0,0 +1,47 @@
+module github.com/aws/aws-encryption-sdk/testvectors
+
+go 1.23.2
+
+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 (
+	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
+)