chore(GHA): add action for testing against MPL HEAD

.github/workflows/ci_examples_java.yml

@@ -13,6 +13,15 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   testJava:
@@ -48,6 +57,20 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Update project.properties if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_examples_net.yml

@@ -13,6 +13,11 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   dotNetExamples:
@@ -45,6 +50,15 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_java.yml

@@ -13,6 +13,15 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   testJava:
@@ -42,6 +51,20 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Update project.properties if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_net.yml

@@ -13,6 +13,11 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   testDotNet:
@@ -46,6 +51,15 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_vector_java.yml

@@ -13,6 +13,15 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   testJava:
@@ -51,6 +60,20 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Update project.properties if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_vector_net.yml

@@ -13,6 +13,11 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   testDotNet:
@@ -51,6 +56,15 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/daily_ci.yml

@@ -36,6 +36,11 @@ jobs:
     uses: ./.github/workflows/test_vector_verification.yml
     with:
       dafny: ${{needs.getVerifyVersion.outputs.version}}
+  daily-ci-java:
+    needs: getVersion
+    uses: ./.github/workflows/ci_test_java.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
   daily-ci-java-test-vectors:
     needs: getVersion
     uses: ./.github/workflows/ci_test_vector_java.yml

.github/workflows/library_dafny_verification.yml

@@ -13,6 +13,15 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   verification:
@@ -47,6 +56,20 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Update project.properties if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
       # dafny-reportgenerator requires next6
       # but only 7.0 is installed on macos-12-large
       - name: Setup .NET Core SDK '6.0.x'
@@ -63,14 +86,14 @@ jobs:
           diff-generated-code: false
 
       - name: Verify ${{ matrix.library }} Dafny code
-        working-directory: ./DynamoDbEncryption
+        working-directory: DynamoDbEncryption
         run: |
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make verify_service CORES=$CORES SERVICE=${{ matrix.library }}
 
       - name: Check solver resource use
         if: success() || failure()
-        working-directory: ./DynamoDbEncryption
+        working-directory: DynamoDbEncryption
         run: |
           make dafny-reportgenerator

.github/workflows/mpl-head.yml

@@ -0,0 +1,78 @@
+# This workflow invokes other workflows with the latest MPL head at 14:00 UTC (7am PDT)
+name: CI MPL HEAD
+
+on:
+  schedule:
+    - cron: "00 14 * * 1-5"
+
+jobs:
+  getVersion:
+    # Don't run the cron builds on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/dafny_version.yml
+  getVerifyVersion:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/dafny_verify_version.yml
+  getMplHeadVersion:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/mpl_head_version.yml
+  mpl-head-ci-format:
+    needs: getVersion
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_format.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+  mpl-head-ci-verification:
+    needs: [getVerifyVersion, getMplHeadVersion]
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_dafny_verification.yml
+    with:
+      dafny: ${{needs.getVerifyVersion.outputs.version}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-test-vector-verification:
+    needs: [getVerifyVersion, getMplHeadVersion]
+    uses: ./.github/workflows/test_vector_verification.yml
+    with:
+      dafny: ${{needs.getVerifyVersion.outputs.version}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-java:
+    needs: [getVersion, getMplHeadVersion]
+    uses: ./.github/workflows/ci_test_java.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-java-test-vectors:
+    needs: [getVersion, getMplHeadVersion]
+    uses: ./.github/workflows/ci_test_vector_java.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-java-examples:
+    needs: [getVersion, getMplHeadVersion]
+    uses: ./.github/workflows/ci_examples_java.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-net:
+    needs: getVersion
+    uses: ./.github/workflows/ci_test_net.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-net-test-vectors:
+    needs: getVersion
+    uses: ./.github/workflows/ci_test_vector_net.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+      mpl-head: true
+  mpl-head-ci-net-examples:
+    needs: getVersion
+    uses: ./.github/workflows/ci_examples_net.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
+      mpl-head: true

.github/workflows/mpl_head_version.yml

@@ -0,0 +1,36 @@
+# This workflow reads the project.properties
+# into the environment variables
+# and then creates an output variable for `dafnyVerifyVersion `
+name: MPL HEAD Version
+
+on:
+  workflow_call:
+    outputs:
+      version:
+        description: "The dafny version for verify"
+        value: ${{ jobs.getMplHeadVersion.outputs.version }}
+
+jobs:
+  getMplHeadVersion:
+    runs-on: ubuntu-latest
+    outputs:
+      version: ${{ steps.read_property.outputs.mplVersion }}
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Update MPL submodule locally if requested
+        working-directory: submodules/MaterialProviders
+        shell: bash
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Get the MPL version from the MPL submodule
+        id: read_property
+        uses: christian-draeger/[email protected]
+        with:
+          path: "submodules/MaterialProviders/project.properties"
+          properties: "mplVersion"