chore: repolymorph with latest smithy-dafny

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy

@@ -1714,6 +1714,13 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
       // The Opaque error, used for native, extern, wrapped or unknown errors
     | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
+  // This dummy subset type is included to make sure Dafny
+  // always generates a _ExternBase___default.java class.
+  type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
+  predicate method IsDummySubsetType(x: int) {
+    0 < x
+  }
+
 }
 abstract module AbstractAwsCryptographyMaterialProvidersService
 {

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy

@@ -284,6 +284,13 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
       // The Opaque error, used for native, extern, wrapped or unknown errors
     | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
+  // This dummy subset type is included to make sure Dafny
+  // always generates a _ExternBase___default.java class.
+  type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
+  predicate method IsDummySubsetType(x: int) {
+    0 < x
+  }
+
 }
 abstract module AbstractAwsCryptographyKeyStoreService
 {

AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/keystore/types/__default.java

@@ -1,4 +1,4 @@
 package software.amazon.cryptography.keystore.internaldafny.types;
 
 public class __default
-  extends software.amazon.cryptography.keystore.internaldafny._ExternBase___default {}
+  extends software.amazon.cryptography.keystore.internaldafny.types._ExternBase___default {}

AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy

@@ -691,6 +691,13 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" }
       // The Opaque error, used for native, extern, wrapped or unknown errors
     | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
+  // This dummy subset type is included to make sure Dafny
+  // always generates a _ExternBase___default.java class.
+  type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
+  predicate method IsDummySubsetType(x: int) {
+    0 < x
+  }
+
 }
 abstract module AbstractAwsCryptographyPrimitivesService
 {

ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy

@@ -2905,6 +2905,13 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty
       // The Opaque error, used for native, extern, wrapped or unknown errors
     | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
+  // This dummy subset type is included to make sure Dafny
+  // always generates a _ExternBase___default.java class.
+  type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
+  predicate method IsDummySubsetType(x: int) {
+    0 < x
+  }
+
 }
 abstract module AbstractComAmazonawsDynamodbService {
   import opened Wrappers

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

@@ -0,0 +1,14 @@
+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 5c6364b2..7feacebc 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
+@@ -8670,9 +8670,6 @@ public class ToNative {
+     if (dafnyValue.is_InternalServerError()) {
+       return ToNative.Error((Error_InternalServerError) dafnyValue);
+     }
+-    if (dafnyValue.is_InvalidEndpointException()) {
+-      return ToNative.Error((Error_InvalidEndpointException) dafnyValue);
+-    }
+     if (dafnyValue.is_InvalidExportTimeException()) {
+       return ToNative.Error((Error_InvalidExportTimeException) dafnyValue);
+     }

ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java

@@ -354,6 +354,7 @@
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.DisableKinesisStreamingDestinationOutput;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.EnableKinesisStreamingDestinationInput;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.EnableKinesisStreamingDestinationOutput;
+import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_BackupInUseException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_BackupNotFoundException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException;
@@ -368,6 +369,7 @@
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ImportNotFoundException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_IndexNotFoundException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InternalServerError;
+import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidEndpointException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidExportTimeException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidRestoreTimeException;
 import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ItemCollectionSizeLimitExceededException;
@@ -8596,10 +8598,30 @@ public static TransactionInProgressException Error(
     return builder.build();
   }
 
-  // BEGIN MANUAL EDIT
-  public static RuntimeException Error(
-    software.amazon.cryptography.services.dynamodb.internaldafny.types.Error dafnyValue
-  ) {
+  public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) {
+    return ((Shim) dafnyValue).impl();
+  }
+
+  public static RuntimeException Error(Error_Opaque dafnyValue) {
+    // While the first two cases are logically identical,
+    // there is a semantic distinction.
+    // An un-modeled Service Error is different from a Java Heap Exhaustion error.
+    // In the future, Smithy-Dafny MAY allow for this distinction.
+    // Which would allow Dafny developers to treat the two differently.
+    if (dafnyValue.dtor_obj() instanceof DynamoDbException) {
+      return (DynamoDbException) dafnyValue.dtor_obj();
+    } else if (dafnyValue.dtor_obj() instanceof Exception) {
+      return (RuntimeException) dafnyValue.dtor_obj();
+    }
+    return new IllegalStateException(
+      String.format(
+        "Unknown error thrown while calling Amazon DynamoDB. %s",
+        dafnyValue
+      )
+    );
+  }
+
+  public static RuntimeException Error(Error dafnyValue) {
     if (dafnyValue.is_BackupInUseException()) {
       return ToNative.Error((Error_BackupInUseException) dafnyValue);
     }
@@ -8667,6 +8689,9 @@ public static RuntimeException Error(
         (Error_PointInTimeRecoveryUnavailableException) dafnyValue
       );
     }
+    if (dafnyValue.is_PolicyNotFoundException()) {
+      return ToNative.Error((Error_PolicyNotFoundException) dafnyValue);
+    }
     if (dafnyValue.is_ProvisionedThroughputExceededException()) {
       return ToNative.Error(
         (Error_ProvisionedThroughputExceededException) dafnyValue
@@ -8708,32 +8733,10 @@ public static RuntimeException Error(
     if (dafnyValue.is_Opaque()) {
       return ToNative.Error((Error_Opaque) dafnyValue);
     }
-    // TODO This should indicate a codegen bug
-    return new IllegalStateException(
-      String.format("Unknown error thrown while calling DDB. %s", dafnyValue)
-    );
-  }
-
-  // END MANUAL EDIT
-
-  public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) {
-    return ((Shim) dafnyValue).impl();
-  }
-
-  public static RuntimeException Error(Error_Opaque dafnyValue) {
-    // While the first two cases are logically identical,
-    // there is a semantic distinction.
-    // An un-modeled Service Error is different from a Java Heap Exhaustion error.
-    // In the future, Smithy-Dafny MAY allow for this distinction.
-    // Which would allow Dafny developers to treat the two differently.
-    if (dafnyValue.dtor_obj() instanceof DynamoDbException) {
-      return (DynamoDbException) dafnyValue.dtor_obj();
-    } else if (dafnyValue.dtor_obj() instanceof Exception) {
-      return (RuntimeException) dafnyValue.dtor_obj();
-    }
+    // 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 Amazon DynamoDB. %s",
+        "Unknown error thrown while calling service. %s",
         dafnyValue
       )
     );

ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy

@@ -1978,6 +1978,13 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"
       // The Opaque error, used for native, extern, wrapped or unknown errors
     | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
+  // This dummy subset type is included to make sure Dafny
+  // always generates a _ExternBase___default.java class.
+  type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
+  predicate method IsDummySubsetType(x: int) {
+    0 < x
+  }
+
 }
 abstract module AbstractComAmazonawsKmsService {
   import opened Wrappers