chore(GHA): update nightlies for interop and interop action

.github/workflows/dafny-interop.yml

@@ -27,33 +27,33 @@ jobs:
       mpl-dafny: ${{inputs.mpl-dafny}}
       mpl-commit: ${{inputs.mpl-commit}}
       dbesdk-dafny: ${{inputs.dbesdk-dafny}}
-  # dafny-interop-java-test-vectors:
-  #   uses: ./.github/workflows/ci_test_vector_java.yml
-  #   with:
-  #     mpl-dafny: ${{inputs.mpl-dafny}}
-  #     mpl-commit: ${{inputs.mpl-commit}}
-  #     dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
-  # dafny-interop-java-examples:
-  #   uses: ./.github/workflows/ci_examples_java.yml
-  #   with:
-  #     mpl-dafny: ${{inputs.mpl-dafny}}
-  #     mpl-commit: ${{inputs.mpl-commit}}
-  #     dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
-  # dafny-interop-net:
-  #   uses: ./.github/workflows/ci_test_net.yml
-  #   with:
-  #     mpl-dafny: ${{inputs.mpl-dafny}}
-  #     mpl-commit: ${{inputs.mpl-commit}}
-  #     dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
-  # dafny-interop-net-test-vectors:
-  #   uses: ./.github/workflows/ci_test_vector_net.yml
-  #   with:
-  #     mpl-dafny: ${{inputs.mpl-dafny}}
-  #     mpl-commit: ${{inputs.mpl-commit}}
-  #     dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
-  # dafny-interop-net-examples:
-  #   uses: ./.github/workflows/ci_examples_net.yml
-  #   with:
-  #     mpl-dafny: ${{inputs.mpl-dafny}}
-  #     mpl-commit: ${{inputs.mpl-commit}}
-  #     dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
+  dafny-interop-java-test-vectors:
+    uses: ./.github/workflows/dafny_interop_test_vector_java.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      dbesdk-dafny: ${{inputs.dbesdk-dafny}}
+  dafny-interop-java-examples:
+    uses: ./.github/workflows/dafny_interop_examples_java.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      dbesdk-dafny: ${{inputs.dbesdk-dafny}}
+  dafny-interop-net:
+    uses: ./.github/workflows/dafny_interop_test_net.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      dbesdk-dafny: ${{inputs.dbesdk-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}}
+      dbesdk-dafny: ${{inputs.dbesdk-dafny}}
+  dafny-interop-net-examples:
+    uses: ./.github/workflows/dafny_interop_examples_net.yml
+    with:
+      mpl-dafny: ${{inputs.mpl-dafny}}
+      mpl-commit: ${{inputs.mpl-commit}}
+      dbesdk-dafny: ${{inputs.dbesdk-dafny}}

.github/workflows/dafny_interop_examples_java.yml

@@ -0,0 +1,92 @@
+# This workflow performs tests in Java with MPL nightly latest.
+name: Library Java Backwards Example 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
+      dbesdk-dafny:
+        description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
+        required: true
+        type: string
+
+jobs:
+  testExamplesJava:
+    strategy:
+      max-parallel: 1
+      matrix:
+        java-version: [8, 11, 16, 17]
+        os: [macos-12]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - 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-Java-Tests
+
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          fetch-depth: 0
+
+      - 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: Setup Java ${{ matrix.java-version }}
+        uses: actions/setup-java@v4
+        with:
+          distribution: "corretto"
+          java-version: ${{ matrix.java-version }}
+
+      - name: Build MPL with Dafny ${{inputs.mpl-dafny}}
+        working-directory: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_java CORES=$CORES
+
+      - name: Setup DBESDK Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dbesdk-dafny}}
+
+      - name: Build implementation
+        shell: bash
+        working-directory: ./DynamoDbEncryption
+        run: |
+          make transpile_implementation_java
+          make transpile_test_java
+          make mvn_local_deploy
+
+      - name: Test Examples
+        working-directory: ./Examples
+        run: |
+          # Run simple examples
+          gradle -p runtimes/java/DynamoDbEncryption test 
+          # Run migration examples
+          gradle -p runtimes/java/Migration/PlaintextToAWSDBE test
+          gradle -p runtimes/java/Migration/DDBECToAWSDBE test

.github/workflows/dafny_interop_examples_net.yml

@@ -0,0 +1,100 @@
+# This workflow performs tests in DotNet with MPL nightly latest.
+name: Library DotNet Backwards Interop Example 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
+      dbesdk-dafny:
+        description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
+        required: true
+        type: string
+
+jobs:
+  dotNetExamples:
+    strategy:
+      matrix:
+        library: [DynamoDbEncryption]
+        dotnet-version: ["6.0.x"]
+        os: [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 ${{ matrix.dotnet-version }}
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: ${{ matrix.dotnet-version }}
+
+      - 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: ./${{ matrix.library }}
+        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: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders
+        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 DBESDK Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dbesdk-dafny}}
+
+      - 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_implementation_net CORES=$CORES
+          make transpile_test_net CORES=$CORES
+      - name: Run Examples
+        working-directory: ./Examples/runtimes/net
+        shell: bash
+        run: |
+          dotnet run

.github/workflows/dafny_interop_java.yml

@@ -1,5 +1,5 @@
-# This workflow performs tests in Java.
-name: Library Java tests
+# This workflow performs tests in Java with MPL nightly latest.
+name: Library Java Backwards Interop Tests
 
 on:
   workflow_call:
@@ -47,7 +47,7 @@ jobs:
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
-      - name: Update MPL submodule if using MPL HEAD
+      - name: Update MPL submodule
         working-directory: submodules/MaterialProviders
         run: |
           git fetch

.github/workflows/dafny_interop_test_net.yml

@@ -0,0 +1,124 @@
+# 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
+      dbesdk-dafny:
+        description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
+        required: true
+        type: string
+
+jobs:
+  testDotNet:
+    strategy:
+      matrix:
+        library: [DynamoDbEncryption]
+        dotnet-version: ["6.0.x"]
+        os: [macos-12, ubuntu-latest, windows-latest]
+    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 ${{ matrix.dotnet-version }}
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: ${{ matrix.dotnet-version }}
+
+      - 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: ./${{ matrix.library }}
+        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: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders
+        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 DBESDK Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dbesdk-dafny}}
+
+      - 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_implementation_net CORES=$CORES
+          make transpile_test_net CORES=$CORES
+
+      - name: Test ${{ matrix.library }} net48
+        if: matrix.os == 'windows-latest'
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          dotnet restore runtimes/net/tests
+          dotnet build runtimes/net/tests
+          make test_net FRAMEWORK=net48
+
+      - name: Test ${{ matrix.library }} net6.0
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          dotnet restore runtimes/net/tests
+          dotnet build runtimes/net/tests
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            make test_net_mac_intel
+          else
+            make test_net FRAMEWORK=net6.0
+          fi
+
+      - name: Test Build and Pack ${{ matrix.library}}
+        shell: bash
+        if: matrix.os != 'windows-latest'
+        working-directory: ./${{ matrix.library }}
+        run: |
+          dotnet build runtimes/net /p:Configuration=Release -nowarn:CS0162,CS0168
+          dotnet pack runtimes/net/DynamoDbEncryption.csproj --no-build /p:Configuration=Release --output build