chore(smithy-dafny): changes to support Smithy-Dafny mainline (#643)

Co-authored-by: José Corella <[email protected]>

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

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.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/AwsCryptographyKeyStore/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(

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

@@ -1,8 +1,8 @@
 diff --git b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
-index 72738b20..83ba3510 100644
+index 43bf1a88..76f8023e 100644
 --- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
 +++ a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
-@@ -10809,7 +10809,13 @@ namespace Com.Amazonaws.Dynamodb
+@@ -11000,7 +11000,13 @@ namespace Com.Amazonaws.Dynamodb
          }
          public static Wrappers_Compile._IOption<Dafny.ISequence<Dafny.ISequence<char>>> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_Projection__M16_NonKeyAttributes(System.Collections.Generic.List<string> value)
          {

ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch

@@ -1,7 +1,7 @@
-diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
-index 171a36d3..3964b7cb 100644
---- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
-+++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
+diff --git a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
+index c30e7cdf..3964b7cb 100644
+--- a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
++++ b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
 @@ -8040,6 +8040,126 @@ public class ToNative {
      return builder.build();
    }
@@ -129,20 +129,9 @@ index 171a36d3..3964b7cb 100644
    public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) {
      return ((Shim) dafnyValue).impl();
    }
-@@ -8054,17 +8174,9 @@ public class ToNative {
-       return (DynamoDbException) dafnyValue.dtor_obj();
+@@ -8055,6 +8175,8 @@ public class ToNative {
      } else if (dafnyValue.dtor_obj() instanceof Exception) {
        return (RuntimeException) dafnyValue.dtor_obj();
--    } else if (dafnyValue.dtor_message().is_Some()) {
--      final String suffix = dafnyValue.dtor_obj() != null
--        ? String.format("  Unknown Object: %s", dafnyValue.dtor_obj())
--        : "";
--      final String message =
--        software.amazon.smithy.dafny.conversion.ToNative.Simple.String(
--          dafnyValue.dtor_message().dtor_value()
--        ) +
--        suffix;
--      return new RuntimeException(message);
      }
 +    // BEGIN MANUAL EDIT
 +    // END MANUAL EDIT

ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch

@@ -1,7 +1,7 @@
-diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java
+diff --git a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java
 index 52abd119..9d02d333 100644
---- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java
-+++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java
+--- a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java
++++ b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java
 @@ -2300,7 +2300,13 @@ public class ToDafny {
 
    public static DafnySequence<
@@ -50,10 +50,10 @@ index 52abd119..9d02d333 100644
          {
            return SigningAlgorithmSpec.create_SM2DSA();
          }
-diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java
-index 56979da2..59df5196 100644
---- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java
-+++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java
+diff --git a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java
+index e8eddd3c..59df5196 100644
+--- a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java
++++ b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java
 @@ -4542,6 +4542,196 @@ public class ToNative {
      return builder.build();
    }
@@ -251,20 +251,9 @@ index 56979da2..59df5196 100644
    public static KmsClient TrentService(IKMSClient dafnyValue) {
      return ((Shim) dafnyValue).impl();
    }
-@@ -4556,17 +4746,9 @@ public class ToNative {
-       return (KmsException) dafnyValue.dtor_obj();
+@@ -4557,6 +4747,8 @@ public class ToNative {
      } else if (dafnyValue.dtor_obj() instanceof Exception) {
        return (RuntimeException) dafnyValue.dtor_obj();
--    } else if (dafnyValue.dtor_message().is_Some()) {
--      final String suffix = dafnyValue.dtor_obj() != null
--        ? String.format("  Unknown Object: %s", dafnyValue.dtor_obj())
--        : "";
--      final String message =
--        software.amazon.smithy.dafny.conversion.ToNative.Simple.String(
--          dafnyValue.dtor_message().dtor_value()
--        ) +
--        suffix;
--      return new RuntimeException(message);
      }
 +    // BEGIN MANUAL EDIT
 +    // END MANUAL EDIT

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

@@ -1,8 +1,8 @@
 diff --git b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs
-index 87b39a81..e57de1dd 100644
+index 7b556e25..5cf59ac4 100644
 --- b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs
 +++ a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs
-@@ -3399,7 +3399,9 @@ namespace AWS.Cryptography.MaterialProviders.Wrapped
+@@ -3835,7 +3835,9 @@ namespace AWS.Cryptography.MaterialProviders.Wrapped
              dafnyVal._ComAmazonawsDynamodb
            );
          case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: