From 13124933913caba4ac3e923bffb41d6c86a3dfd3 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Fri, 8 Nov 2024 14:59:53 -0500 Subject: [PATCH] chore: repolymorph with latest smithy-dafny (#968) * chore: repolymorph for latest smithy-dafny --- .../AwsCryptographyMaterialProvidersTypes.dfy | 7 + .../Model/AwsCryptographyKeyStoreTypes.dfy | 7 + .../keystore/types/__default.java | 2 +- .../Model/AwsCryptographyPrimitivesTypes.dfy | 7 + .../Model/ComAmazonawsDynamodbTypes.dfy | 7 + .../codegen-patches/java/dafny-4.2.0.patch | 131 ---------- .../codegen-patches/java/dafny-4.8.0.patch | 14 ++ .../dynamodb/internaldafny/ToNative.java | 59 ++--- .../Model/ComAmazonawsKmsTypes.dfy | 7 + .../codegen-patches/java/dafny-4.8.0.patch | 226 +----------------- .../services/kms/internaldafny/ToDafny.java | 4 - .../services/kms/internaldafny/ToNative.java | 52 ++-- ...hyMaterialProvidersTestVectorKeysTypes.dfy | 7 + .../internaldafny/types/__default.java | 3 + smithy-dafny | 2 +- 15 files changed, 119 insertions(+), 416 deletions(-) delete mode 100644 ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch create mode 100644 ComAmazonawsDynamodb/codegen-patches/java/dafny-4.8.0.patch create mode 100644 TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/types/__default.java diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy index 7f34a93d7..0790e276f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +++ b/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 { diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy index 92eead3ec..b16e75d07 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +++ b/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 { diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/keystore/types/__default.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/keystore/types/__default.java index 35abb0265..3c8bbba4c 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/keystore/types/__default.java +++ b/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 {} diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy index 35ad66284..485871afc 100644 --- a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy +++ b/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 { diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy index c26daf579..8c808cfd6 100644 --- a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy +++ b/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 diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch deleted file mode 100644 index c601737ae..000000000 --- a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch +++ /dev/null @@ -1,131 +0,0 @@ -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 c30e7cdf..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 -@@ -8040,6 +8040,126 @@ public class ToNative { - return builder.build(); - } - -+ // BEGIN MANUAL EDIT -+ public static RuntimeException Error( -+ software.amazon.cryptography.services.dynamodb.internaldafny.types.Error dafnyValue -+ ) { -+ if (dafnyValue.is_BackupInUseException()) { -+ return ToNative.Error((Error_BackupInUseException) dafnyValue); -+ } -+ if (dafnyValue.is_BackupNotFoundException()) { -+ return ToNative.Error((Error_BackupNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_ConditionalCheckFailedException()) { -+ return ToNative.Error((Error_ConditionalCheckFailedException) dafnyValue); -+ } -+ if (dafnyValue.is_ContinuousBackupsUnavailableException()) { -+ return ToNative.Error( -+ (Error_ContinuousBackupsUnavailableException) dafnyValue -+ ); -+ } -+ if (dafnyValue.is_DuplicateItemException()) { -+ return ToNative.Error((Error_DuplicateItemException) dafnyValue); -+ } -+ if (dafnyValue.is_ExportConflictException()) { -+ return ToNative.Error((Error_ExportConflictException) dafnyValue); -+ } -+ if (dafnyValue.is_ExportNotFoundException()) { -+ return ToNative.Error((Error_ExportNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_GlobalTableAlreadyExistsException()) { -+ return ToNative.Error( -+ (Error_GlobalTableAlreadyExistsException) dafnyValue -+ ); -+ } -+ if (dafnyValue.is_GlobalTableNotFoundException()) { -+ return ToNative.Error((Error_GlobalTableNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_IdempotentParameterMismatchException()) { -+ return ToNative.Error( -+ (Error_IdempotentParameterMismatchException) dafnyValue -+ ); -+ } -+ if (dafnyValue.is_ImportConflictException()) { -+ return ToNative.Error((Error_ImportConflictException) dafnyValue); -+ } -+ if (dafnyValue.is_ImportNotFoundException()) { -+ return ToNative.Error((Error_ImportNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_IndexNotFoundException()) { -+ return ToNative.Error((Error_IndexNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_InternalServerError()) { -+ return ToNative.Error((Error_InternalServerError) dafnyValue); -+ } -+ if (dafnyValue.is_InvalidExportTimeException()) { -+ return ToNative.Error((Error_InvalidExportTimeException) dafnyValue); -+ } -+ if (dafnyValue.is_InvalidRestoreTimeException()) { -+ return ToNative.Error((Error_InvalidRestoreTimeException) dafnyValue); -+ } -+ if (dafnyValue.is_ItemCollectionSizeLimitExceededException()) { -+ return ToNative.Error( -+ (Error_ItemCollectionSizeLimitExceededException) dafnyValue -+ ); -+ } -+ if (dafnyValue.is_LimitExceededException()) { -+ return ToNative.Error((Error_LimitExceededException) dafnyValue); -+ } -+ if (dafnyValue.is_PointInTimeRecoveryUnavailableException()) { -+ return ToNative.Error( -+ (Error_PointInTimeRecoveryUnavailableException) dafnyValue -+ ); -+ } -+ if (dafnyValue.is_ProvisionedThroughputExceededException()) { -+ return ToNative.Error( -+ (Error_ProvisionedThroughputExceededException) dafnyValue -+ ); -+ } -+ if (dafnyValue.is_ReplicaAlreadyExistsException()) { -+ return ToNative.Error((Error_ReplicaAlreadyExistsException) dafnyValue); -+ } -+ if (dafnyValue.is_ReplicaNotFoundException()) { -+ return ToNative.Error((Error_ReplicaNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_RequestLimitExceeded()) { -+ return ToNative.Error((Error_RequestLimitExceeded) dafnyValue); -+ } -+ if (dafnyValue.is_ResourceInUseException()) { -+ return ToNative.Error((Error_ResourceInUseException) dafnyValue); -+ } -+ if (dafnyValue.is_ResourceNotFoundException()) { -+ return ToNative.Error((Error_ResourceNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_TableAlreadyExistsException()) { -+ return ToNative.Error((Error_TableAlreadyExistsException) dafnyValue); -+ } -+ if (dafnyValue.is_TableInUseException()) { -+ return ToNative.Error((Error_TableInUseException) dafnyValue); -+ } -+ if (dafnyValue.is_TableNotFoundException()) { -+ return ToNative.Error((Error_TableNotFoundException) dafnyValue); -+ } -+ if (dafnyValue.is_TransactionCanceledException()) { -+ return ToNative.Error((Error_TransactionCanceledException) dafnyValue); -+ } -+ if (dafnyValue.is_TransactionConflictException()) { -+ return ToNative.Error((Error_TransactionConflictException) dafnyValue); -+ } -+ if (dafnyValue.is_TransactionInProgressException()) { -+ return ToNative.Error((Error_TransactionInProgressException) dafnyValue); -+ } -+ 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(); - } diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.8.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.8.0.patch new file mode 100644 index 000000000..193233bc7 --- /dev/null +++ b/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); + } 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 89b16d3aa..7feacebc6 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 @@ -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 ) ); diff --git a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy index 3dc44f3bf..54f8f6bde 100644 --- a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy +++ b/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 diff --git a/ComAmazonawsKms/codegen-patches/java/dafny-4.8.0.patch b/ComAmazonawsKms/codegen-patches/java/dafny-4.8.0.patch index 1c2310cd7..90ef7642d 100644 --- a/ComAmazonawsKms/codegen-patches/java/dafny-4.8.0.patch +++ b/ComAmazonawsKms/codegen-patches/java/dafny-4.8.0.patch @@ -4494,7 +4494,7 @@ index 5e894e4e..9d02d333 100644 return new Error_XksProxyVpcEndpointServiceInvalidConfigurationException( message ); -@@ -5641,14 +4617,11 @@ public class ToDafny { +@@ -5641,13 +4617,10 @@ public class ToDafny { message = Objects.nonNull(nativeValue.getMessage()) ? Option.create_Some( @@ -4509,227 +4509,3 @@ index 5e894e4e..9d02d333 100644 + : Option.create_None(); return new Error_XksProxyVpcEndpointServiceNotFoundException(message); } - -@@ -5676,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(); - } -@@ -6483,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..399865e7 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(); - } 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 d8dc6c8f0..d8767cd0f 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 @@ -4645,9 +4645,7 @@ public static AlgorithmSpec AlgorithmSpec( { return AlgorithmSpec.create_RSA__AES__KEY__WRAP__SHA__256(); } - // BEGIN MANUAL EDIT case SM2_PKE: - // END MANUAL EDIT { return AlgorithmSpec.create_SM2PKE(); } @@ -5454,9 +5452,7 @@ public static SigningAlgorithmSpec SigningAlgorithmSpec( { return SigningAlgorithmSpec.create_ECDSA__SHA__512(); } - // 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 399865e76..d4e598f82 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 @@ -190,6 +190,7 @@ import software.amazon.awssdk.services.kms.model.XksProxyVpcEndpointServiceInUseException; import software.amazon.awssdk.services.kms.model.XksProxyVpcEndpointServiceInvalidConfigurationException; import software.amazon.awssdk.services.kms.model.XksProxyVpcEndpointServiceNotFoundException; +import software.amazon.cryptography.services.kms.internaldafny.types.Error; import software.amazon.cryptography.services.kms.internaldafny.types.Error_AlreadyExistsException; import software.amazon.cryptography.services.kms.internaldafny.types.Error_CloudHsmClusterInUseException; import software.amazon.cryptography.services.kms.internaldafny.types.Error_CloudHsmClusterInvalidConfigurationException; @@ -4542,10 +4543,30 @@ public static XksProxyVpcEndpointServiceNotFoundException Error( return builder.build(); } - // BEGIN MANUAL EDIT - public static RuntimeException Error( - software.amazon.cryptography.services.kms.internaldafny.types.Error dafnyValue - ) { + public static KmsClient TrentService(IKMSClient 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 KmsException) { + return (KmsException) 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 AWS Key Management Service. %s", + dafnyValue + ) + ); + } + + public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_AlreadyExistsException()) { return ToNative.Error((Error_AlreadyExistsException) dafnyValue); } @@ -4726,30 +4747,9 @@ public static RuntimeException Error( 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(); - } - - 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 KmsException) { - return (KmsException) 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 AWS Key Management Service. %s", + "Unknown error thrown while calling service. %s", dafnyValue ) ); diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy index bc931fdbc..26615f621 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy @@ -262,6 +262,13 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in // 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 AbstractAwsCryptographyMaterialProvidersTestVectorKeysService { diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/types/__default.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/types/__default.java new file mode 100644 index 000000000..92a8f3b0c --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/types/__default.java @@ -0,0 +1,3 @@ +package software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types; + +public class __default extends _ExternBase___default {} diff --git a/smithy-dafny b/smithy-dafny index c47e0832b..465b91697 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit c47e0832b9dfafaa112593dd493728823804cc9b +Subproject commit 465b916975ac71938774a47069cdbcc478f403f4