dafny-4.2.0.patch

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
--- 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<
     ? extends KeyAgreementAlgorithmSpec
-  > KeyAgreementAlgorithmSpecList(List<String> nativeValue) {
+    // BEGIN MANUAL EDIT
+  > KeyAgreementAlgorithmSpecList(
+    List<
+      software.amazon.awssdk.services.kms.model.KeyAgreementAlgorithmSpec
+    > nativeValue
+  ) {
+    // END MANUAL EDIT
     return software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence(
       nativeValue,
       software.amazon.cryptography.services.kms.internaldafny.ToDafny::KeyAgreementAlgorithmSpec,
@@ -2890,7 +2896,9 @@ public class ToDafny {
   }
 
   public static DafnySequence<? extends MacAlgorithmSpec> MacAlgorithmSpecList(
-    List<String> nativeValue
+    // BEGIN MANUAL EDIT
+    List<software.amazon.awssdk.services.kms.model.MacAlgorithmSpec> nativeValue
+    // END MANUAL EDIT
   ) {
     return software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence(
       nativeValue,
@@ -4641,7 +4649,9 @@ public class ToDafny {
         {
           return AlgorithmSpec.create_RSA__AES__KEY__WRAP__SHA__256();
         }
-      case SM2PKE:
+      // BEGIN MANUAL EDIT
+      case SM2_PKE:
+        // END MANUAL EDIT
         {
           return AlgorithmSpec.create_SM2PKE();
         }
@@ -5448,7 +5458,9 @@ public class ToDafny {
         {
           return SigningAlgorithmSpec.create_ECDSA__SHA__512();
         }
-      case SM2DSA:
+      // BEGIN MANUAL EDIT
+      case SM2_DSA:
+        // END MANUAL EDIT
         {
           return SigningAlgorithmSpec.create_SM2DSA();
         }
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();
   }
 
+  // BEGIN MANUAL EDIT
+  public static RuntimeException Error(
+    software.amazon.cryptography.services.kms.internaldafny.types.Error dafnyValue
+  ) {
+    if (dafnyValue.is_AlreadyExistsException()) {
+      return ToNative.Error((Error_AlreadyExistsException) dafnyValue);
+    }
+    if (dafnyValue.is_CloudHsmClusterInUseException()) {
+      return ToNative.Error((Error_CloudHsmClusterInUseException) dafnyValue);
+    }
+    if (dafnyValue.is_CloudHsmClusterInvalidConfigurationException()) {
+      return ToNative.Error(
+        (Error_CloudHsmClusterInvalidConfigurationException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_CloudHsmClusterNotActiveException()) {
+      return ToNative.Error(
+        (Error_CloudHsmClusterNotActiveException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_CloudHsmClusterNotFoundException()) {
+      return ToNative.Error(
+        (Error_CloudHsmClusterNotFoundException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_CloudHsmClusterNotRelatedException()) {
+      return ToNative.Error(
+        (Error_CloudHsmClusterNotRelatedException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_ConflictException()) {
+      return ToNative.Error((Error_ConflictException) dafnyValue);
+    }
+    if (dafnyValue.is_CustomKeyStoreHasCMKsException()) {
+      return ToNative.Error((Error_CustomKeyStoreHasCMKsException) dafnyValue);
+    }
+    if (dafnyValue.is_CustomKeyStoreInvalidStateException()) {
+      return ToNative.Error(
+        (Error_CustomKeyStoreInvalidStateException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_CustomKeyStoreNameInUseException()) {
+      return ToNative.Error(
+        (Error_CustomKeyStoreNameInUseException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_CustomKeyStoreNotFoundException()) {
+      return ToNative.Error((Error_CustomKeyStoreNotFoundException) dafnyValue);
+    }
+    if (dafnyValue.is_DependencyTimeoutException()) {
+      return ToNative.Error((Error_DependencyTimeoutException) dafnyValue);
+    }
+    if (dafnyValue.is_DisabledException()) {
+      return ToNative.Error((Error_DisabledException) dafnyValue);
+    }
+    if (dafnyValue.is_DryRunOperationException()) {
+      return ToNative.Error((Error_DryRunOperationException) dafnyValue);
+    }
+    if (dafnyValue.is_ExpiredImportTokenException()) {
+      return ToNative.Error((Error_ExpiredImportTokenException) dafnyValue);
+    }
+    if (dafnyValue.is_IncorrectKeyException()) {
+      return ToNative.Error((Error_IncorrectKeyException) dafnyValue);
+    }
+    if (dafnyValue.is_IncorrectKeyMaterialException()) {
+      return ToNative.Error((Error_IncorrectKeyMaterialException) dafnyValue);
+    }
+    if (dafnyValue.is_IncorrectTrustAnchorException()) {
+      return ToNative.Error((Error_IncorrectTrustAnchorException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidAliasNameException()) {
+      return ToNative.Error((Error_InvalidAliasNameException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidArnException()) {
+      return ToNative.Error((Error_InvalidArnException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidCiphertextException()) {
+      return ToNative.Error((Error_InvalidCiphertextException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidGrantIdException()) {
+      return ToNative.Error((Error_InvalidGrantIdException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidGrantTokenException()) {
+      return ToNative.Error((Error_InvalidGrantTokenException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidImportTokenException()) {
+      return ToNative.Error((Error_InvalidImportTokenException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidKeyUsageException()) {
+      return ToNative.Error((Error_InvalidKeyUsageException) dafnyValue);
+    }
+    if (dafnyValue.is_InvalidMarkerException()) {
+      return ToNative.Error((Error_InvalidMarkerException) dafnyValue);
+    }
+    if (dafnyValue.is_KeyUnavailableException()) {
+      return ToNative.Error((Error_KeyUnavailableException) dafnyValue);
+    }
+    if (dafnyValue.is_KMSInternalException()) {
+      return ToNative.Error((Error_KMSInternalException) dafnyValue);
+    }
+    if (dafnyValue.is_KMSInvalidMacException()) {
+      return ToNative.Error((Error_KMSInvalidMacException) dafnyValue);
+    }
+    if (dafnyValue.is_KMSInvalidSignatureException()) {
+      return ToNative.Error((Error_KMSInvalidSignatureException) dafnyValue);
+    }
+    if (dafnyValue.is_KMSInvalidStateException()) {
+      return ToNative.Error((Error_KMSInvalidStateException) dafnyValue);
+    }
+    if (dafnyValue.is_LimitExceededException()) {
+      return ToNative.Error((Error_LimitExceededException) dafnyValue);
+    }
+    if (dafnyValue.is_MalformedPolicyDocumentException()) {
+      return ToNative.Error(
+        (Error_MalformedPolicyDocumentException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_NotFoundException()) {
+      return ToNative.Error((Error_NotFoundException) dafnyValue);
+    }
+    if (dafnyValue.is_TagException()) {
+      return ToNative.Error((Error_TagException) dafnyValue);
+    }
+    if (dafnyValue.is_UnsupportedOperationException()) {
+      return ToNative.Error((Error_UnsupportedOperationException) dafnyValue);
+    }
+    if (dafnyValue.is_XksKeyAlreadyInUseException()) {
+      return ToNative.Error((Error_XksKeyAlreadyInUseException) dafnyValue);
+    }
+    if (dafnyValue.is_XksKeyInvalidConfigurationException()) {
+      return ToNative.Error(
+        (Error_XksKeyInvalidConfigurationException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_XksKeyNotFoundException()) {
+      return ToNative.Error((Error_XksKeyNotFoundException) dafnyValue);
+    }
+    if (dafnyValue.is_XksProxyIncorrectAuthenticationCredentialException()) {
+      return ToNative.Error(
+        (Error_XksProxyIncorrectAuthenticationCredentialException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_XksProxyInvalidConfigurationException()) {
+      return ToNative.Error(
+        (Error_XksProxyInvalidConfigurationException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_XksProxyInvalidResponseException()) {
+      return ToNative.Error(
+        (Error_XksProxyInvalidResponseException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_XksProxyUriEndpointInUseException()) {
+      return ToNative.Error(
+        (Error_XksProxyUriEndpointInUseException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_XksProxyUriInUseException()) {
+      return ToNative.Error((Error_XksProxyUriInUseException) dafnyValue);
+    }
+    if (dafnyValue.is_XksProxyUriUnreachableException()) {
+      return ToNative.Error((Error_XksProxyUriUnreachableException) dafnyValue);
+    }
+    if (dafnyValue.is_XksProxyVpcEndpointServiceInUseException()) {
+      return ToNative.Error(
+        (Error_XksProxyVpcEndpointServiceInUseException) dafnyValue
+      );
+    }
+    if (
+      dafnyValue.is_XksProxyVpcEndpointServiceInvalidConfigurationException()
+    ) {
+      return ToNative.Error(
+        (Error_XksProxyVpcEndpointServiceInvalidConfigurationException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_XksProxyVpcEndpointServiceNotFoundException()) {
+      return ToNative.Error(
+        (Error_XksProxyVpcEndpointServiceNotFoundException) dafnyValue
+      );
+    }
+    if (dafnyValue.is_Opaque()) {
+      return ToNative.Error((Error_Opaque) dafnyValue);
+    }
+    // TODO This should indicate a codegen bug; every error Should have been taken care of.
+    return new IllegalStateException(
+      String.format("Unknown error thrown while calling KMS. %s", dafnyValue)
+    );
+  }
+
+  // END MANUAL EDIT
   public static KmsClient TrentService(IKMSClient dafnyValue) {
     return ((Shim) dafnyValue).impl();
   }