Merge pull request #732 from aws/Golang/dev

feat: polymorph_go check-in

.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

.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/[email protected]
+        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

.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,19 +122,19 @@ 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
@@ -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'

.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 }}

.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

.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:

.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:

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 {"

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