chore(CI): add backwards compatability tests for nightly

.github/workflows/dafny_interop.yml

@@ -4,6 +4,21 @@
 name: Dafny Interoperability Test
 
 on:
+  workflow_call:
+    inputs:
+      mpl-dafny:
+        description: "The Dafny version to compile the MPL with (4.2.0, nightly-latest, etc..)"
+        required: true
+        type: string
+      mpl-commit:
+        description: "The MPL branch/commit to use"
+        required: false
+        default: "main"
+        type: string
+      esdk-dafny:
+        description: "The Dafny version to compile the DBESDK with (4.2.0, nightly-latest, etc..)"
+        required: true
+        type: string
   workflow_dispatch:
     inputs:
       mpl-dafny:
@@ -33,3 +48,9 @@ jobs:
       mpl-dafny: ${{inputs.mpl-dafny}}
       mpl-commit: ${{inputs.mpl-commit}}
       esdk-dafny: ${{inputs.esdk-dafny}}
+  dafny-nightly-go:
+    uses: ./.github/workflows/dafny_interop_library_go_tests.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      esdk-dafny: ${{inputs.esdk-dafny}}

.github/workflows/dafny_interop_library_go_tests.yml

@@ -0,0 +1,108 @@
+# This workflow performs tests in Go with nightly latest versions for mpl or esdk.
+name: Library Go Backwards Interop Tests
+
+on:
+  workflow_call:
+    inputs:
+      mpl-dafny:
+        description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)"
+        required: true
+        type: string
+      mpl-commit:
+        description: "The MPL commit to use"
+        required: false
+        default: "main"
+        type: string
+      esdk-dafny:
+        description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
+        required: true
+        type: string
+
+jobs:
+  testGo:
+    strategy:
+      fail-fast: false
+      matrix:
+        library: [TestVectors]
+        go-version: ["1.23"]
+        os: [
+            # Sed script doesn't work properly on windows
+            # windows-latest,
+            ubuntu-22.04,
+            # TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
+            # 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 MPL Dafny
+        uses: ./mpl/.github/actions/setup_dafny
+        with:
+          dafny-version: ${{ inputs.mpl-dafny }}
+
+      - name: Update MPL submodule
+        working-directory: mpl
+        run: |
+          git fetch
+          git checkout ${{inputs.mpl-commit}}
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      - name: Install Go
+        uses: actions/setup-go@v5
+        with:
+          go-version: ${{ matrix.go-version }}
+
+      - name: Install Go imports
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
+      - name: Compile MPL with Dafny ${{inputs.mpl-dafny}}
+        shell: bash
+        working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders
+        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: Setup ESDK Dafny
+        uses: ./mpl/.github/actions/setup_dafny
+        with:
+          dafny-version: ${{ inputs.esdk-dafny}}
+
+      - name: Build ESDK 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/dafny_interop_test_vector_net.yml

@@ -235,7 +235,7 @@ jobs:
         uses: actions/upload-artifact@v4
         if: matrix.os != 'windows-latest'
         with:
-          name: ${{matrix.os}}_vector_artifact
+          name: ${{matrix.os}}_mpl-${{inputs.mpl-dafny}}_esdk-${{inputs.esdk-dafny}}_vectors
           path: AwsEncryptionSDK/net41/vectors/*.zip
 
   decrypt_net_vectors_with_js:
@@ -274,7 +274,7 @@ jobs:
       - name: Download Encrypt Manifest Artifact
         uses: actions/download-artifact@v4
         with:
-          name: ${{matrix.os}}_vector_artifact
+          name: ${{matrix.os}}_mpl-${{inputs.mpl-dafny}}_esdk-${{inputs.esdk-dafny}}_vectors
           path: AwsEncryptionSDK/net41/vectors
 
       - uses: actions/setup-node@v4

.github/workflows/nighly_dafny.yml

@@ -43,13 +43,38 @@ jobs:
     with:
       dafny: "nightly-latest"
       regenerate-code: true
+  getVersion:
+    uses: ./.github/workflows/dafny_version.yaml
+  dafny_nightly_backwards_interop_esdk:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    needs: getVersion
+    uses: ./.github/workflows/dafny_interop.yml
+    with:
+      mpl-dafny: ${{needs.getVersion.outputs.version}}
+      mpl-commit: "main"
+      esdk-dafny: "nightly-latest"
+  dafny_nightly_backwards_interop_mpl:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    needs: getVersion
+    uses: ./.github/workflows/dafny_interop.yml
+    with:
+      mpl-dafny: "nightly-latest"
+      mpl-commit: "main"
+      esdk-dafny: ${{needs.getVersion.outputs.version}}
 
   cut-issue-on-failure:
     runs-on: ubuntu-22.04
     permissions:
       id-token: write
       contents: read
-    needs: [dafny-nightly-verification, dafny-nightly-net]
+    needs:
+      [
+        dafny-nightly-verification,
+        dafny-nightly-net,
+        dafny-nightly-go,
+        dafny_nightly_backwards_interop_esdk,
+        dafny_nightly_backwards_interop_mpl,
+      ]
     if: ${{ always() && contains(needs.*.result, 'failure') }}
     steps:
       # We need access to the role that is able to get CI Bot Creds