update verification

Author: josecorella

.github/workflows/library_dafny_verification.yml

@@ -13,8 +13,12 @@ on:
         required: false
         default: false
         type: boolean
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
       mpl-head:
-        description: "Using MPL HEAD"
+        description: "Running on MPL HEAD"
         required: false
         default: false
         type: boolean
@@ -52,11 +56,18 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
-      - uses: ./.github/actions/mpl-head
+      - name: Update MPL submodule if using MPL HEAD
         if: ${{ inputs.mpl-head == true }}
-        with:
-          dafny: ${{ env.DAFNY_VERSION }}
-          update-and-regenerate-mpl: true
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+
+      - 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
@@ -74,14 +85,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

@@ -12,19 +12,22 @@ jobs:
   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
+    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-head: true
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
   # mpl-head-ci-test-vector-verification:
   #   needs: getVerifyVersion
   #   uses: ./.github/workflows/test_vector_verification.yml

.github/workflows/mpl_head_version.yml

@@ -0,0 +1,34 @@
+# 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
+      - name: Update MPL submodule locally if requested
+        if: inputs.update-and-regenerate-mpl == 'true'
+        working-directory: submodules/MaterialProviders
+        shell: bash
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+
+      - name: Get the MPL version from the MPL submodule
+        id: read_property
+        uses: christian-draeger/read-properties@1.1.1
+        with:
+          path: "submodules/MaterialProviders/project.properties"
+          properties: "mplVersion"