merge

Author: lucasmcdonald3

.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/workflows/library_codegen.yml

@@ -42,7 +42,7 @@ 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
 
       # Only used to format generated code
       # and to translate version strings such as "nightly-latest"
@@ -57,6 +57,15 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      - 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
+
       - uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

.github/workflows/pull.yml

@@ -39,3 +39,20 @@ jobs:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-all-required:
+    if: always()
+    needs:
+      - getVersion
+      - getVerifyVersion
+      - pr-ci-format
+      - pr-ci-codegen
+      - pr-ci-verification
+      - pr-ci-java
+      - pr-ci-net
+      - pr-interop-test
+    runs-on: ubuntu-latest
+    steps:
+      - name: Verify all required jobs passed
+        uses: re-actors/alls-green@release/v1
+        with:
+          jobs: ${{ toJSON(needs) }}

.github/workflows/smithy-diff.yml

@@ -3,7 +3,8 @@
 name: Check Smithy Files
 
 on:
-  pull_request:
+  pull_request_review:
+    types: [submitted]
 
 jobs:
   require-approvals:
@@ -19,20 +20,22 @@ jobs:
       - name: Get Files changed
         id: file-changes
         shell: bash
+        env:
+          GITHUB_HEAD: ${{github.event.pull_request.head.ref}}
         run:
           # Checks to see if any of the smithy Models are being updated.
           # Doing this check allows us to catch things like, missing @javadoc trait documentation or bug in smithy dafny that has not be resolved.
-          echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD_REF} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
+          echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
 
       - name: Check if FILES is not empty
         id: comment
         env:
-          PR_NUMBER: ${{ github.event.number }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           FILES: ${{ steps.file-changes.outputs.FILES }}
         if: ${{env.FILES != ''}}
         run: |
           # TODO: If https://github.com/smithy-lang/smithy-dafny/issues/491 is resolved, remove comment about this issue.
-          COMMENT="@${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated javadoc trait documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?"
+          COMMENT="@${{github.event.pull_request.user.login}} and @${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated user documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?"
           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\"}"

.releaserc.cjs

@@ -20,9 +20,6 @@
 // We model all the files and the runtimes here in this structure
 const Runtimes = {
   java: {
-    "project.properties": {
-      dependencies: [],
-    },
     "AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts": {
       dependencies: [],
     },
@@ -84,13 +81,6 @@ module.exports = {
         replacements: [
           // Update the version for all Gradle Java projects
           // Does not update the dependencies
-          {
-            files: Object.keys(Runtimes.java),
-            from: 'mplVersion=".*"',
-            to: 'mplVersion="${nextRelease.version}"',
-            results: Object.keys(Runtimes.java).map(CheckResults),
-            countMatches: true,
-          },
           {
             files: Object.keys(Runtimes.java),
             from: 'version = ".*"',

AwsCryptographicMaterialProviders/.gitignore

@@ -1,6 +1,8 @@
 TestResults
 ImplementationFromDafny.cs
 TestsFromDafny.cs
+ImplementationFromDafny-cs.dtr
+TestsFromDafny-cs.dtr
 
 **/bin
 **/obj

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.3.0.patch

@@ -1,8 +1,8 @@
 diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
-index b10e603c..89561181 100644
+index e05ad66e..7b6ad3a7 100644
 --- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
 +++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
-@@ -3436,7 +3436,9 @@ namespace AWS.Cryptography.MaterialProviders
+@@ -3872,7 +3872,9 @@ namespace AWS.Cryptography.MaterialProviders
              dafnyVal._ComAmazonawsDynamodb
            );
          case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal:

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch

@@ -1,8 +1,8 @@
 diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
-index f5ef0458..f846a946 100644
+index 95c9eba1..bcd537fb 100644
 --- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
 +++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
-@@ -629,7 +629,9 @@ namespace AWS.Cryptography.KeyStore
+@@ -732,7 +732,9 @@ namespace AWS.Cryptography.KeyStore
              dafnyVal._ComAmazonawsDynamodb
            );
          case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
@@ -13,7 +13,7 @@ index f5ef0458..f846a946 100644
              dafnyVal._ComAmazonawsKms
            );
          case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal:
-@@ -652,7 +654,9 @@ namespace AWS.Cryptography.KeyStore
+@@ -755,7 +757,9 @@ namespace AWS.Cryptography.KeyStore
        {
          case "Com.Amazonaws.KMS":
            return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsKms(

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch

@@ -719,6 +719,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     | SingleThreaded(SingleThreaded: SingleThreadedCache)
     | MultiThreaded(MultiThreaded: MultiThreadedCache)
     | StormTracking(StormTracking: StormTrackingCache)
+    | Shared(Shared: ICryptographicMaterialsCache)
   class IClientSupplierCallHistory {
     ghost constructor() {
       GetClient := [];
@@ -823,7 +824,8 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly branchKeyIdSupplier: Option<IBranchKeyIdSupplier> := Option.None ,
     nameonly keyStore: AwsCryptographyKeyStoreTypes.IKeyStoreClient ,
     nameonly ttlSeconds: PositiveLong ,
-    nameonly cache: Option<CacheType> := Option.None
+    nameonly cache: Option<CacheType> := Option.None ,
+    nameonly partitionId: Option<string> := Option.None
   )
   datatype CreateAwsKmsKeyringInput = | CreateAwsKmsKeyringInput (
     nameonly kmsKeyId: KmsKeyId ,