chore(dafny): Check for unique transformed keys on init mutation

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,7 +1,11 @@
-_Issue #, if available:_
+### Issue #, if available:
 
-_Description of changes:_
+### Description of changes:
 
-_Squash/merge commit message, if applicable:_
+### Squash/merge commit message, if applicable:
+
+```
+<message>
+```
 
 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

@@ -19,3 +19,14 @@ runs:
       with:
         arguments: :smithy-python-codegen:pTML
         build-root-directory: smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen
+
+    - name: Setup Python, black, and docformatter for code formatting
+      uses: actions/setup-python@v4
+      with:
+        python-version: ${{ matrix.python-version }}
+        architecture: x64
+    - shell: bash
+      run: |
+        python -m pip install --upgrade pip
+        python -m pip install --upgrade black
+        python -m pip install --upgrade docformatter

.github/actions/polymorph_codegen/action.yml

@@ -46,6 +46,15 @@ outputs:
 runs:
   using: "composite"
   steps:
+    - name: Setup Java 17 for codegen
+      uses: actions/setup-java@v3
+      with:
+        distribution: "corretto"
+        java-version: "17"
+
+    - name: Install Smithy-Dafny codegen dependencies
+      uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
     # Replace the project.properties file so that we pick up the right runtimes etc.,
     # in cases where inputs.dafny is different from the current value in that file.
     - name: Update top-level project.properties file

.github/actions/setup_dafny/action.yml

@@ -0,0 +1,30 @@
+#
+#
+# This local action consolidate all uses of dafny-lang/setup-dafny-action
+# as well as works around any dependencies or issues with setting up Dafny.
+# It can also be re-used by downstream projects such as the DB-ESDK and ESDK.
+#
+name: "Setup Dafny"
+description: "This uses the setup Dafny action."
+inputs:
+  dafny-version:
+    description: "The Dafny version to setup"
+    required: true
+    type: string
+runs:
+  using: "composite"
+  steps:
+    # The dotnet tool requires >= 9.0.202 to work on MacOS
+    # See: https://github.com/dotnet/sdk/issues/46857#issuecomment-2734338347
+    # Ideally this action would only install this on MacOS,
+    # but I do not want to keep track of the various values
+    # See: https://docs.github.com/en/actions/writing-workflows/choosing-what-your-workflow-does/store-information-in-variables#detecting-the-operating-system
+    - name: Setup .NET Core SDK '9.0.x'
+      uses: actions/setup-dotnet@v3
+      with:
+        dotnet-version: "9.0.x"
+
+    - name: Setup Dafny with setup-dafny action
+      uses: dafny-lang/[email protected]
+      with:
+        dafny-version: ${{ inputs.dafny-version }}

.github/workflows/library_codegen.yml

@@ -53,7 +53,7 @@ jobs:
       # and to translate version strings such as "nightly-latest"
       # to an actual DAFNY_VERSION.
       - name: Setup Dafny
-        uses: dafny-lang/[email protected]
+        uses: ./.github/actions/setup_dafny
         with:
           dafny-version: ${{ inputs.dafny }}
 
@@ -62,25 +62,16 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      # even though we just installed dotnet 6, maybe dotnet 8 is out there somewhere
+      - name: Create temporary global.json
+        run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json
+
       - name: Setup Java 17 for codegen
         uses: actions/setup-java@v3
         with:
           distribution: "corretto"
           java-version: "17"
 
-      - name: Install Smithy-Dafny codegen dependencies
-        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
-
-      - name: Setup Python, black, and docformatter for code formatting
-        uses: actions/setup-python@v4
-        with:
-          python-version: ${{ matrix.python-version }}
-          architecture: x64
-      - run: |
-          python -m pip install --upgrade pip
-          python -m pip install --upgrade black
-          python -m pip install --upgrade docformatter
-
       - name: Install Go
         uses: actions/setup-go@v5
         with:

.github/workflows/library_concurrency_tests.yml

@@ -0,0 +1,116 @@
+# This workflow performs Concurrency tests of the MPL in Java.
+name: Library Concurrency Tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  generateEncryptVectors:
+    strategy:
+      matrix:
+        library: [AwsCryptographicMaterialProviders]
+        os: [
+            # https://taskei.amazon.dev/tasks/CrypTool-5283
+            # windows-latest,
+            ubuntu-latest,
+            macos-13,
+          ]
+        language: [
+            java,
+            # net,
+            # python,
+            # rust
+          ]
+        # https://taskei.amazon.dev/tasks/CrypTool-5284
+        java-versions: [8, 17]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+
+      # Test Vectors need to call KMS
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: ConcurrencyTests
+
+      - uses: actions/checkout@v3
+      #  Not all submodules are needed.
+      # We manually pull the submodule we DO need.
+      - run: git submodule update --init libraries
+      - run: git submodule update --init --recursive smithy-dafny
+
+      # Setup Java in Rust is needed for running polymorph
+      - name: Setup Java 17
+        if: matrix.language == 'java' || matrix.language == 'rust'
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 17
+
+      - name: Setup .NET Core SDK '6.0.x'
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: "6.0.x"
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ inputs.dafny }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+
+      # Build implementation for each runtime
+      - name: Build ${{ matrix.library }} implementation in Java
+        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 build_java CORES=$CORES
+
+      - name: Setup gradle
+        if: matrix.language == 'java'
+        uses: gradle/gradle-build-action@v2
+        with:
+          gradle-version: 7.2
+
+      - name: Setup Java ${{matrix.java-versions}}
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: ${{matrix.java-versions}}
+
+      - name: Compile Java
+        uses: gradle/gradle-build-action@v3
+        with:
+          arguments: build
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Test Java
+        uses: gradle/gradle-build-action@v3
+        with:
+          arguments: testConcurrentExamples
+          build-root-directory: ./${{ matrix.library }}/runtimes/java

.github/workflows/library_dafny_verification.yml

@@ -45,20 +45,13 @@ jobs:
       # The specification submodule is private so we don't have access, but we don't need
       # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
       - run: git submodule update --init libraries
-      - run: git submodule update --init smithy-dafny
+      - run: git submodule update --init --recursive smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/[email protected]
+        uses: ./.github/actions/setup_dafny
         with:
           dafny-version: ${{ inputs.dafny }}
 
-      # dafny-reportgenerator requires next6
-      # but only 7.0 is installed on macos-13-large
-      - name: Setup .NET Core SDK '6.0.x'
-        uses: actions/setup-dotnet@v3
-        with:
-          dotnet-version: "6.0.x"
-
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/library_examples.yml

@@ -0,0 +1,58 @@
+# "Copyright Amazon.com Inc. or its affiliates. All Rights Reserved."
+# "SPDX-License-Identifier: CC-BY-SA-4.0"
+# This workflow runs any examples.
+name: Library Examples
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+
+jobs:
+  java:
+    runs-on: ubuntu-22.04
+    permissions:
+      id-token: write
+      contents: read
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: JavaExampleTests
+
+      - uses: actions/checkout@v4
+      - run: git submodule update --init libraries
+      - run: git submodule update --init smithy-dafny
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Setup Java 8
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 8
+
+      - name: Build AwsCryptographicMaterialProviders Java implementation
+        working-directory: ./AwsCryptographicMaterialProviders
+        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: Test AwsCryptographicMaterialProviders Java Examples
+        working-directory: ./AwsCryptographicMaterialProviders
+        run: |
+          make test_example_java

.github/workflows/library_format.yml

@@ -46,10 +46,10 @@ jobs:
       # The specification submodule is private so we don't have access, but we don't need
       # it to verify the Dafny code. Instead we manually pull the submodule we DO need.
       - run: git submodule update --init libraries
-      - run: git submodule update --init smithy-dafny
+      - run: git submodule update --init --recursive smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/[email protected]
+        uses: ./.github/actions/setup_dafny
         with:
           dafny-version: ${{ inputs.dafny }}
 
@@ -61,6 +61,10 @@ jobs:
           library: ${{ matrix.library }}
           diff-generated-code: false
 
+      # make sure we always format for dotnet 6
+      - name: Create temporary global.json
+        run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json
+
       - name: Check format of ${{ matrix.library }} Dafny code
         working-directory: ./${{ matrix.library }}
         run: |

.github/workflows/library_go_tests.yml

@@ -61,10 +61,10 @@ jobs:
       # The specification submodule is private so we don't have access, but we don't need
       # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
       - run: git submodule update --init libraries
-      - run: git submodule update --init smithy-dafny
+      - run: git submodule update --init --recursive smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/[email protected]
+        uses: ./.github/actions/setup_dafny
         with:
           dafny-version: ${{ inputs.dafny }}