Merge branch 'mainline' into lucmcdon/hkeyring-vectors

.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

@@ -0,0 +1,21 @@
+#
+# This local action sets up code dependencies
+# to run Smithy-Dafny CI in GitHub Actions workflows.
+#
+
+name: "Install Smithy-Dafny codegen dependencies"
+description: "Install Java package dependencies required to run Smithy-Dafny codegen"
+runs:
+  using: "composite"
+  steps:
+    - name: Install smithy-dafny-codegen Rust dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+        build-root-directory: smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
+
+    - name: Install smithy-dafny-codegen Python dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :smithy-python-codegen:pTML
+        build-root-directory: smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen

.github/actions/polymorph_codegen/action.yml

@@ -61,7 +61,7 @@ runs:
       if: inputs.update-and-regenerate-mpl == 'true'
       shell: bash
       run: |
-        git submodule update --init --recursive --remote --merge mpl
+        git submodule update --remote --merge mpl
 
     - name: Don't regenerate dependencies unless requested
       id: dependencies
@@ -88,18 +88,20 @@ runs:
         make -C mpl/AwsCryptographicMaterialProviders setup_prettier
         make -C mpl/ComAmazonawsKms setup_prettier
         make -C mpl/ComAmazonawsDynamodb setup_prettier
-
-    - name: Regenerate Java code using smithy-dafny
-      # npx seems to be unavailable on Windows GHA runners,
-      # so we don't regenerate Java code on them either.
-      if: runner.os != 'Windows'
-      working-directory: ./${{ inputs.library }}
-      shell: bash
-      # smithy-dafny also formats generated code itself now,
-      # so prettier is a necessary dependency.
-      run: |
-        make setup_prettier
-        make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }}
+    
+    # In the ESDK Dafny it does not make sense to run smithy dafny for java code
+    # since the java esdk written natively and not through dafny
+    #- name: Regenerate Java code using smithy-dafny
+    #  # npx seems to be unavailable on Windows GHA runners,
+    #  # so we don't regenerate Java code on them either.
+    #  if: runner.os != 'Windows'
+    #  working-directory: ./${{ inputs.library }}
+    #  shell: bash
+    #  # smithy-dafny also formats generated code itself now,
+    #  # so prettier is a necessary dependency.
+    #  run: |
+    #    make setup_prettier
+    #    make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }}
 
     - name: Regenerate .NET code using smithy-dafny
       working-directory: ./${{ inputs.library }}

.github/workflows/check_only_keyword.yml

@@ -0,0 +1,40 @@
+# This workflow checks if you are checking in dafny code
+# with the keyword {:only}, it adds a message to the pull
+# request to remind you to remove it.
+name: Check {:only} decorator presence
+
+on:
+  pull_request:
+
+jobs:
+  grep-only-verification-keyword:
+    runs-on: ubuntu-latest
+    permissions:
+      issues: write
+      pull-requests: write
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+
+      - name: Check only keyword
+        id: only-keyword
+        shell: bash
+        run:
+          # checking in code with the dafny decorator {:only}
+          # will not verify the entire file or maybe the entire project depending on its configuration
+          # This action checks if you are either adding or removing the {:only} decorator and posting on the pr if you are.
+          echo "ONLY_KEYWORD=$(git diff origin/main origin/${GITHUB_HEAD_REF} **/*.dfy | grep -i {:only})" >> "$GITHUB_OUTPUT"
+
+      - name: Check if ONLY_KEYWORD is not empty
+        id: comment
+        env:
+          PR_NUMBER: ${{ github.event.number }}
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }}
+        if: ${{env.ONLY_KEYWORD != ''}}
+        run: |
+          COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?"
+          COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments"
+          curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}"
+          exit 1

.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}}