chore(GHA): add dafny interoperability action

.github/workflows/dafny_interop.yml

@@ -0,0 +1,35 @@
+# This workflow is for testing backwards compatibility of a dafny version
+# and tests if a project that consumes the mpl will be backwards compatible with
+# a newer version of Dafny
+name: Dafny Interoperability Test
+
+on:
+  workflow_dispatch:
+    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
+
+jobs:
+  dafny-interop-net:
+    uses: ./.github/workflows/dafny_interop_test_net.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      esdk-dafny: ${{inputs.esdk-dafny}}
+  dafny-interop-net-test-vectors:
+    uses: ./.github/workflows/dafny_interop_test_vector_net.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      esdk-dafny: ${{inputs.esdk-dafny}}

.github/workflows/dafny_interop_test_net.yml

@@ -0,0 +1,253 @@
+# This workflow performs tests in DotNet with MPL nightly latest.
+name: Library DotNet 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:
+  testDotNet:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [
+          windows-latest,
+          ubuntu-latest,
+          macos-12,
+        ]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          fetch-depth: 0
+
+      - name: Setup .NET Core SDK 6
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: '6.0.x'
+
+      - name: Setup MPL Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.mpl-dafny }}
+
+      - name: Update MPL submodule
+        working-directory: submodules/MaterialProviders
+        run: |
+          git fetch
+          git checkout ${{inputs.mpl-commit}}
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Download Dependencies
+        working-directory: AwsEncryptionSDK
+        run: make setup_net
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
+          role-session-name: DDBEC-Dafny-Net-Tests
+
+      - name: Compile MPL with Dafny ${{inputs.mpl-dafny}}
+        shell: bash
+        working-directory: mpl 
+        run: |
+          make setup_net
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_net CORES=$CORES
+
+      - name: Setup ESDK Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.esdk-dafny}}
+
+      - name: Build ESDK implementation
+        shell: bash
+        working-directory: AwsEncryptionSDK
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          make transpile_implementation_net 
+          make transpile_test_net
+
+      - name: Test .NET Framework net48
+        working-directory: ./AwsEncryptionSDK
+        if: matrix.os == 'windows-latest' 
+        shell: bash
+        run: |
+          make test_net FRAMEWORK=net48
+
+      - name: Test .NET net6.0
+        working-directory: ./AwsEncryptionSDK
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            make test_net_mac_intel FRAMEWORK=net6.0
+          else
+            make test_net FRAMEWORK=net6.0
+          fi
+
+      - name: Test Examples on .NET Framework net48
+        working-directory: ./AwsEncryptionSDK
+        if: matrix.os == 'windows-latest' 
+        shell: bash
+        run: |
+          dotnet test \
+            runtimes/net/Examples \
+            --framework net48
+
+      - name: Test Examples on .NET net6.0
+        working-directory: ./AwsEncryptionSDK
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" 
+            dotnet test \
+              runtimes/net/Examples \
+              --framework net6.0
+          else
+            dotnet test \
+              runtimes/net/Examples \
+              --framework net6.0
+          fi
+
+      - name: Unzip ESDK-NET @ v4.0.0 Valid Vectors
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
+        shell: bash
+        run: |
+          NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors
+          mkdir -p $NET_400_VALID_VECTORS
+          DOWNLOAD_NAME=valid-Net-4.0.0.zip
+          unzip -o -qq $DOWNLOAD_NAME -d $NET_400_VALID_VECTORS
+
+      - name: Run ESDK-NET @ v4.0.0 Valid Vectors expect success
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+        continue-on-error: true
+        shell: bash
+        run: |
+          NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors
+          ESDK_NET_V400_POLICY="forbid" \
+          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \
+          dotnet test --framework net48
+          ESDK_NET_V400_POLICY="forbid" \
+          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \
+          dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+
+      - name: Unzip ESDK-NET @ v4.0.0 Invalid Vectors
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
+        shell: bash
+        run: |
+          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
+          mkdir -p $NET_400_INVALID_VECTORS
+          DOWNLOAD_NAME=invalid-Net-4.0.0.zip
+          unzip -o -qq $DOWNLOAD_NAME -d $NET_400_INVALID_VECTORS
+
+      - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 48 expect failure
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+        continue-on-error: true
+        shell: bash
+        run: |
+          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
+          ESDK_NET_V400_POLICY="forbid" \
+          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
+          dotnet test --framework net48
+          # Dotnet test returns 1 for failure.
+          TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi;
+          # We want this to fail, so if it returned 1, step passes, else it fails
+          # TODO Post-#619: Refactor Test Vectors to expect failure,
+          # as I doubt this true false logic works
+
+      - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 6.0 expect failure
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+        continue-on-error: true
+        shell: bash
+        run: |
+          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            ESDK_NET_V400_POLICY="forbid" \
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
+            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
+            dotnet test --framework net6.0
+          else
+            ESDK_NET_V400_POLICY="forbid" \
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
+            dotnet test --framework net6.0
+          fi
+          # Dotnet test returns 1 for failure.
+          TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi;
+          # We want this to fail, so if it returned 1, step passes, else it fails
+          # TODO Post-#619: Refactor Test Vectors to expect failure,
+          # as I doubt this true false logic works
+
+      - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET expect Success
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+        shell: bash
+        run: |
+          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
+          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
+          dotnet test --framework net48 --logger "console;verbosity=quiet"
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
+            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
+            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+          else
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
+            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+          fi
+
+      - name: Unzip ESDK-NET @ v4.0.1 Vectors
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
+        shell: bash
+        run: |
+          NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors
+          mkdir -p $NET_401_VECTORS
+          DOWNLOAD_NAME=v4-Net-4.0.1.zip
+          unzip -o -qq $DOWNLOAD_NAME -d $NET_401_VECTORS
+
+      - name: Run ESDK-NET @ v4.0.1 Vectors expect success
+        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+        shell: bash
+        run: |
+          NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors
+          # We expect net48 to run only for Windows
+          if [ "$RUNNER_OS" == "Windows" ]; then
+            ESDK_NET_V400_POLICY="forbid" \
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
+            dotnet test --framework net48
+          fi
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
+            ESDK_NET_V400_POLICY="forbid" \
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
+            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+          else
+            ESDK_NET_V400_POLICY="forbid" \
+            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
+            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+          fi