From 64f72c121fef31a83bcf3a5346d7efc1e84ab25f Mon Sep 17 00:00:00 2001 From: Tony Knapp <5892063+texastony@users.noreply.github.com> Date: Fri, 29 Mar 2024 14:09:57 -0500 Subject: [PATCH] fix(dafny): Local Service Constructors MUST return concrete --- .../dafny/dafny-4.1.0.patch | 32 +++ .../dotnet/dafny-4.1.0.patch | 15 ++ .../java/dafny-4.1.0.patch | 25 +++ .../dafny/dafny-4.1.0.patch | 32 +++ .../dotnet/dafny-4.1.0.patch | 26 +++ .../java/dafny-4.1.0.patch | 25 +++ .../AwsCryptographyMaterialProvidersTypes.dfy | 12 +- .../src/Index.dfy | 4 +- .../Model/AwsCryptographyKeyStoreTypes.dfy | 12 +- .../AwsCryptographyKeyStore/src/Index.dfy | 4 +- .../cryptography/keystore/KeyStore.java | 7 +- .../materialproviders/MaterialProviders.java | 7 +- .../Model/AwsCryptographyPrimitivesTypes.dfy | 12 +- .../codegen-patches/dafny/dafny-4.1.0.patch | 32 +++ .../codegen-patches/java/dafny-4.1.0.patch | 28 +++ .../primitives/AtomicPrimitives.java | 10 +- AwsCryptographyPrimitives/src/Index.dfy | 8 +- .../codegen-patches/dotnet/dafny-4.1.0.patch | 19 ++ .../codegen-patches/java/dafny-4.1.0.patch | 193 +++++++++++++++++ .../codegen-patches/java/dafny-4.2.0.patch | 4 +- .../codegen-patches/java/dafny-4.1.0.patch | 202 ++++++++++++++++++ .../KeyVectors/dafny/dafny-4.1.0.patch | 32 +++ .../KeyVectors/java/dafny-4.1.0.patch | 25 +++ .../dotnet/dafny-4.1.0.patch | 15 ++ ...hyMaterialProvidersTestVectorKeysTypes.dfy | 12 +- .../dafny/KeyVectors/src/Index.dfy | 8 +- .../src/TestManifests.dfy | 4 +- .../internaldafny/wrapped/__default.java | 6 +- .../internaldafny/__default.java | 2 + .../KeyVectors.java | 7 +- 30 files changed, 788 insertions(+), 32 deletions(-) create mode 100644 AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.1.0.patch create mode 100644 AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch create mode 100644 AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/java/dafny-4.1.0.patch create mode 100644 AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.1.0.patch create mode 100644 AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch create mode 100644 AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.1.0.patch create mode 100644 AwsCryptographyPrimitives/codegen-patches/dafny/dafny-4.1.0.patch create mode 100644 AwsCryptographyPrimitives/codegen-patches/java/dafny-4.1.0.patch create mode 100644 ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.1.0.patch create mode 100644 ComAmazonawsDynamodb/codegen-patches/java/dafny-4.1.0.patch create mode 100644 ComAmazonawsKms/codegen-patches/java/dafny-4.1.0.patch create mode 100644 TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/dafny/dafny-4.1.0.patch create mode 100644 TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/java/dafny-4.1.0.patch create mode 100644 TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.1.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.1.0.patch new file mode 100644 index 000000000..51765dfa2 --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.1.0.patch @@ -0,0 +1,32 @@ +diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +index 7fc594a1..7a5be522 100644 +--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy ++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +@@ -1529,7 +1529,9 @@ abstract module AbstractAwsCryptographyMaterialProvidersService + import Operations : AbstractAwsCryptographyMaterialProvidersOperations + function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig + method MaterialProviders(config: MaterialProvidersConfig := DefaultMaterialProvidersConfig()) +- returns (res: Result) ++ // BEGIN MANUAL FIX ++ returns (res: Result) ++ // END MANUAL FIX + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) +@@ -1537,10 +1539,14 @@ abstract module AbstractAwsCryptographyMaterialProvidersService + && res.value.ValidState() + + // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals +- function method CreateSuccessOfClient(client: IAwsCryptographicMaterialProvidersClient): Result { ++ // BEGIN MANUAL FIX ++ function method CreateSuccessOfClient(client: MaterialProvidersClient): Result { ++ // END MANUAL FIX + Success(client) + } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals +- function method CreateFailureOfError(error: Error): Result { ++ // BEGIN MANUAL FIX ++ function method CreateFailureOfError(error: Error): Result { ++ // END MANUAL FIX + Failure(error) + } + class MaterialProvidersClient extends IAwsCryptographicMaterialProvidersClient diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch new file mode 100644 index 000000000..27a455a72 --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch @@ -0,0 +1,15 @@ +diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +index b10e603c..89561181 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 + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: +- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError( ++ // BEGIN MANUAL EDIT ++ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( ++ // END MANUAL EDIT + dafnyVal._ComAmazonawsKms + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal: diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/java/dafny-4.1.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/java/dafny-4.1.0.patch new file mode 100644 index 000000000..08dd3f2de --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/java/dafny-4.1.0.patch @@ -0,0 +1,25 @@ +diff --git b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java +index ac695b97..290bcfc0 100644 +--- b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java ++++ a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java +@@ -10,6 +10,9 @@ import java.lang.Byte; + import java.lang.IllegalArgumentException; + import java.nio.ByteBuffer; + import java.util.Objects; ++//BEGIN MANUAL FIX ++import software.amazon.cryptography.materialproviders.internaldafny.MaterialProvidersClient; ++//END MANUAL FIX + import software.amazon.cryptography.materialproviders.internaldafny.__default; + import software.amazon.cryptography.materialproviders.internaldafny.types.Error; + import software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient; +@@ -49,7 +52,9 @@ public class MaterialProviders { + MaterialProvidersConfig input = builder.MaterialProvidersConfig(); + software.amazon.cryptography.materialproviders.internaldafny.types.MaterialProvidersConfig dafnyValue = + ToDafny.MaterialProvidersConfig(input); +- Result result = ++ //BEGIN MANUAL FIX ++ Result result = ++ //END MANUAL FIX + __default.MaterialProviders(dafnyValue); + if (result.is_Failure()) { + throw ToNative.Error(result.dtor_error()); diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.1.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.1.0.patch new file mode 100644 index 000000000..4a3c957ff --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.1.0.patch @@ -0,0 +1,32 @@ +diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +index 26600cfa..a3d5c6c9 100644 +--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy ++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +@@ -285,7 +285,9 @@ abstract module AbstractAwsCryptographyKeyStoreService + import Operations : AbstractAwsCryptographyKeyStoreOperations + function method DefaultKeyStoreConfig(): KeyStoreConfig + method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig()) +- returns (res: Result) ++ // BEGIN MANUAL FIX ++ returns (res: Result) ++ // END MANUAL FIX + requires config.ddbClient.Some? ==> + config.ddbClient.value.ValidState() + requires config.kmsClient.Some? ==> +@@ -314,10 +316,14 @@ abstract module AbstractAwsCryptographyKeyStoreService + config.kmsClient.value.ValidState() + + // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals +- function method CreateSuccessOfClient(client: IKeyStoreClient): Result { ++ // BEGIN MANUAL FIX ++ function method CreateSuccessOfClient(client: KeyStoreClient): Result { ++ // END MANUAL FIX + Success(client) + } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals +- function method CreateFailureOfError(error: Error): Result { ++ // BEGIN MANUAL FIX ++ function method CreateFailureOfError(error: Error): Result { ++ // END MANUAL FIX + Failure(error) + } + class KeyStoreClient extends IKeyStoreClient diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch new file mode 100644 index 000000000..f9ee0bc55 --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch @@ -0,0 +1,26 @@ +diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs +index f5ef0458..f846a946 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 + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsKms dafnyVal: +- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError( ++ // BEGIN MANUAL EDIT ++ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( ++ // END MANUAL EDIT + dafnyVal._ComAmazonawsKms + ); + case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal: +@@ -652,7 +654,9 @@ namespace AWS.Cryptography.KeyStore + { + case "Com.Amazonaws.KMS": + return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsKms( +- Com.Amazonaws.KMS.TypeConversion.ToDafny_CommonError(value) ++ // BEGIN MANUAL EDIT ++ Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value) ++ // END MANUAL EDIT + ); + case "Com.Amazonaws.Dynamodb": + return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsDynamodb( diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.1.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.1.0.patch new file mode 100644 index 000000000..cf621cc62 --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.1.0.patch @@ -0,0 +1,25 @@ +diff --git b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java +index 68bf0666..7efec786 100644 +--- b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java ++++ a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java +@@ -6,6 +6,9 @@ package software.amazon.cryptography.keystore; + import Wrappers_Compile.Result; + import java.lang.IllegalArgumentException; + import java.util.Objects; ++// BEGIN MANUAL FIX ++import software.amazon.cryptography.keystore.internaldafny.KeyStoreClient; ++// END MANUAL FIX + import software.amazon.cryptography.keystore.internaldafny.__default; + import software.amazon.cryptography.keystore.internaldafny.types.Error; + import software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient; +@@ -32,7 +35,9 @@ public class KeyStore { + KeyStoreConfig input = builder.KeyStoreConfig(); + software.amazon.cryptography.keystore.internaldafny.types.KeyStoreConfig dafnyValue = + ToDafny.KeyStoreConfig(input); +- Result result = __default.KeyStore(dafnyValue); ++ // BEGIN MANUAL FIX ++ Result result = __default.KeyStore(dafnyValue); ++ // END MANUAL FIX + if (result.is_Failure()) { + throw ToNative.Error(result.dtor_error()); + } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy index 7fc594a12..7a5be522a 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy @@ -1529,7 +1529,9 @@ abstract module AbstractAwsCryptographyMaterialProvidersService import Operations : AbstractAwsCryptographyMaterialProvidersOperations function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig method MaterialProviders(config: MaterialProvidersConfig := DefaultMaterialProvidersConfig()) - returns (res: Result) + // BEGIN MANUAL FIX + returns (res: Result) + // END MANUAL FIX ensures res.Success? ==> && fresh(res.value) && fresh(res.value.Modifies) @@ -1537,10 +1539,14 @@ abstract module AbstractAwsCryptographyMaterialProvidersService && res.value.ValidState() // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals - function method CreateSuccessOfClient(client: IAwsCryptographicMaterialProvidersClient): Result { + // BEGIN MANUAL FIX + function method CreateSuccessOfClient(client: MaterialProvidersClient): Result { + // END MANUAL FIX Success(client) } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals - function method CreateFailureOfError(error: Error): Result { + // BEGIN MANUAL FIX + function method CreateFailureOfError(error: Error): Result { + // END MANUAL FIX Failure(error) } class MaterialProvidersClient extends IAwsCryptographicMaterialProvidersClient diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy index c773f284a..db4e0df6c 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy @@ -18,7 +18,7 @@ module } method MaterialProviders(config: MaterialProvidersConfig) - returns (res: Result) + returns (res: Result) ensures res.Success? ==> && res.value is MaterialProvidersClient { @@ -29,7 +29,7 @@ module var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient; var client := new MaterialProvidersClient(Operations.Config( crypto := cryptoPrimitives )); - return Success(client as IAwsCryptographicMaterialProvidersClient); + return Success(client); } class MaterialProvidersClient... { diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy index 26600cfa3..a3d5c6c95 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy @@ -285,7 +285,9 @@ abstract module AbstractAwsCryptographyKeyStoreService import Operations : AbstractAwsCryptographyKeyStoreOperations function method DefaultKeyStoreConfig(): KeyStoreConfig method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig()) - returns (res: Result) + // BEGIN MANUAL FIX + returns (res: Result) + // END MANUAL FIX requires config.ddbClient.Some? ==> config.ddbClient.value.ValidState() requires config.kmsClient.Some? ==> @@ -314,10 +316,14 @@ abstract module AbstractAwsCryptographyKeyStoreService config.kmsClient.value.ValidState() // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals - function method CreateSuccessOfClient(client: IKeyStoreClient): Result { + // BEGIN MANUAL FIX + function method CreateSuccessOfClient(client: KeyStoreClient): Result { + // END MANUAL FIX Success(client) } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals - function method CreateFailureOfError(error: Error): Result { + // BEGIN MANUAL FIX + function method CreateFailureOfError(error: Error): Result { + // END MANUAL FIX Failure(error) } class KeyStoreClient extends IKeyStoreClient diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy index d40d4689f..f00cd67dc 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy @@ -32,7 +32,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny"} } method KeyStore(config: KeyStoreConfig) - returns (res: Result) + returns (res: Result) ensures res.Success? ==> && res.value is KeyStoreClient && var rconfig := (res.value as KeyStoreClient).config; @@ -123,7 +123,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny"} ddbClient := ddbClient ) ); - return Success(client as IKeyStoreClient); + return Success(client); } class KeyStoreClient... { diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java index 68bf0666d..7efec7861 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java @@ -6,6 +6,9 @@ import Wrappers_Compile.Result; import java.lang.IllegalArgumentException; import java.util.Objects; +// BEGIN MANUAL FIX +import software.amazon.cryptography.keystore.internaldafny.KeyStoreClient; +// END MANUAL FIX import software.amazon.cryptography.keystore.internaldafny.__default; import software.amazon.cryptography.keystore.internaldafny.types.Error; import software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient; @@ -32,7 +35,9 @@ protected KeyStore(BuilderImpl builder) { KeyStoreConfig input = builder.KeyStoreConfig(); software.amazon.cryptography.keystore.internaldafny.types.KeyStoreConfig dafnyValue = ToDafny.KeyStoreConfig(input); - Result result = __default.KeyStore(dafnyValue); + // BEGIN MANUAL FIX + Result result = __default.KeyStore(dafnyValue); + // END MANUAL FIX if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java index ac695b974..290bcfc01 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java @@ -10,6 +10,9 @@ import java.lang.IllegalArgumentException; import java.nio.ByteBuffer; import java.util.Objects; +//BEGIN MANUAL FIX +import software.amazon.cryptography.materialproviders.internaldafny.MaterialProvidersClient; +//END MANUAL FIX import software.amazon.cryptography.materialproviders.internaldafny.__default; import software.amazon.cryptography.materialproviders.internaldafny.types.Error; import software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient; @@ -49,7 +52,9 @@ protected MaterialProviders(BuilderImpl builder) { MaterialProvidersConfig input = builder.MaterialProvidersConfig(); software.amazon.cryptography.materialproviders.internaldafny.types.MaterialProvidersConfig dafnyValue = ToDafny.MaterialProvidersConfig(input); - Result result = + //BEGIN MANUAL FIX + Result result = + //END MANUAL FIX __default.MaterialProviders(dafnyValue); if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy index acd5a3466..6bd1c1e2f 100644 --- a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy +++ b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy @@ -519,7 +519,9 @@ abstract module AbstractAwsCryptographyPrimitivesService import Operations : AbstractAwsCryptographyPrimitivesOperations function method DefaultCryptoConfig(): CryptoConfig method AtomicPrimitives(config: CryptoConfig := DefaultCryptoConfig()) - returns (res: Result) + // BEGIN MANUAL FIX + returns (res: Result) + // END MANUAL FIX ensures res.Success? ==> && fresh(res.value) && fresh(res.value.Modifies) @@ -527,10 +529,14 @@ abstract module AbstractAwsCryptographyPrimitivesService && res.value.ValidState() // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals - function method CreateSuccessOfClient(client: IAwsCryptographicPrimitivesClient): Result { + // BEGIN MANUAL FIX + function method CreateSuccessOfClient(client: AtomicPrimitivesClient): Result { + // END MANUAL FIX Success(client) } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals - function method CreateFailureOfError(error: Error): Result { + // BEGIN MANUAL FIX + function method CreateFailureOfError(error: Error): Result { + // END MANUAL FIX Failure(error) } class AtomicPrimitivesClient extends IAwsCryptographicPrimitivesClient diff --git a/AwsCryptographyPrimitives/codegen-patches/dafny/dafny-4.1.0.patch b/AwsCryptographyPrimitives/codegen-patches/dafny/dafny-4.1.0.patch new file mode 100644 index 000000000..80b689bbc --- /dev/null +++ b/AwsCryptographyPrimitives/codegen-patches/dafny/dafny-4.1.0.patch @@ -0,0 +1,32 @@ +diff --git b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy +index acd5a346..6bd1c1e2 100644 +--- b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy ++++ a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy +@@ -519,7 +519,9 @@ abstract module AbstractAwsCryptographyPrimitivesService + import Operations : AbstractAwsCryptographyPrimitivesOperations + function method DefaultCryptoConfig(): CryptoConfig + method AtomicPrimitives(config: CryptoConfig := DefaultCryptoConfig()) +- returns (res: Result) ++ // BEGIN MANUAL FIX ++ returns (res: Result) ++ // END MANUAL FIX + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) +@@ -527,10 +529,14 @@ abstract module AbstractAwsCryptographyPrimitivesService + && res.value.ValidState() + + // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals +- function method CreateSuccessOfClient(client: IAwsCryptographicPrimitivesClient): Result { ++ // BEGIN MANUAL FIX ++ function method CreateSuccessOfClient(client: AtomicPrimitivesClient): Result { ++ // END MANUAL FIX + Success(client) + } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals +- function method CreateFailureOfError(error: Error): Result { ++ // BEGIN MANUAL FIX ++ function method CreateFailureOfError(error: Error): Result { ++ // END MANUAL FIX + Failure(error) + } + class AtomicPrimitivesClient extends IAwsCryptographicPrimitivesClient diff --git a/AwsCryptographyPrimitives/codegen-patches/java/dafny-4.1.0.patch b/AwsCryptographyPrimitives/codegen-patches/java/dafny-4.1.0.patch new file mode 100644 index 000000000..7d1d0d51b --- /dev/null +++ b/AwsCryptographyPrimitives/codegen-patches/java/dafny-4.1.0.patch @@ -0,0 +1,28 @@ +diff --git b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java +index 2652f9bb..bcaa2894 100644 +--- b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java ++++ a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java +@@ -10,6 +10,9 @@ import java.lang.Byte; + import java.lang.IllegalArgumentException; + import java.nio.ByteBuffer; + import java.util.Objects; ++// BEGIN MANUAL FIX ++import software.amazon.cryptography.primitives.internaldafny.AtomicPrimitivesClient; ++// END MANUAL FIX + import software.amazon.cryptography.primitives.internaldafny.__default; + import software.amazon.cryptography.primitives.internaldafny.types.Error; + import software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient; +@@ -44,8 +47,11 @@ public class AtomicPrimitives { + CryptoConfig input = builder.CryptoConfig(); + software.amazon.cryptography.primitives.internaldafny.types.CryptoConfig dafnyValue = + ToDafny.CryptoConfig(input); +- Result result = +- __default.AtomicPrimitives(dafnyValue); ++ // BEGIN MANUAL FIX ++ Result result = __default.AtomicPrimitives( ++ dafnyValue ++ ); ++ // END MANUAL FIX + if (result.is_Failure()) { + throw ToNative.Error(result.dtor_error()); + } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java index 2652f9bb9..bcaa2894c 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/AtomicPrimitives.java @@ -10,6 +10,9 @@ import java.lang.IllegalArgumentException; import java.nio.ByteBuffer; import java.util.Objects; +// BEGIN MANUAL FIX +import software.amazon.cryptography.primitives.internaldafny.AtomicPrimitivesClient; +// END MANUAL FIX import software.amazon.cryptography.primitives.internaldafny.__default; import software.amazon.cryptography.primitives.internaldafny.types.Error; import software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient; @@ -44,8 +47,11 @@ protected AtomicPrimitives(BuilderImpl builder) { CryptoConfig input = builder.CryptoConfig(); software.amazon.cryptography.primitives.internaldafny.types.CryptoConfig dafnyValue = ToDafny.CryptoConfig(input); - Result result = - __default.AtomicPrimitives(dafnyValue); + // BEGIN MANUAL FIX + Result result = __default.AtomicPrimitives( + dafnyValue + ); + // END MANUAL FIX if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } diff --git a/AwsCryptographyPrimitives/src/Index.dfy b/AwsCryptographyPrimitives/src/Index.dfy index 46f3bfab3..40a672ece 100644 --- a/AwsCryptographyPrimitives/src/Index.dfy +++ b/AwsCryptographyPrimitives/src/Index.dfy @@ -12,12 +12,16 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny" } Aws.Cr } method AtomicPrimitives(config: CryptoConfig) - returns (res: Result) + // BEGIN MANUAL FIX + returns (res: Result) + // END MANUAL FIX ensures res.Success? ==> && res.value is AtomicPrimitivesClient { var client := new AtomicPrimitivesClient(Operations.Config); - return Success(client as IAwsCryptographicPrimitivesClient); + // BEGIN MANUAL FIX + return Success(client); + // END MANUAL FIX } class AtomicPrimitivesClient... { diff --git a/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.1.0.patch b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.1.0.patch new file mode 100644 index 000000000..10981d791 --- /dev/null +++ b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.1.0.patch @@ -0,0 +1,19 @@ +diff --git b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +index 72738b20..83ba3510 100644 +--- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs ++++ a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +@@ -10809,7 +10809,13 @@ namespace Com.Amazonaws.Dynamodb + } + public static Wrappers_Compile._IOption>> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_Projection__M16_NonKeyAttributes(System.Collections.Generic.List value) + { +- return value == null ? Wrappers_Compile.Option>>.create_None() : Wrappers_Compile.Option>>.create_Some(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NonKeyAttributeNameList((System.Collections.Generic.List)value)); ++ // BEGIN MANUAL EDIT ++ if (value == null || value.Count == 0) ++ { ++ return Wrappers_Compile.Option>>.create_None(); ++ } ++ return Wrappers_Compile.Option>>.create_Some(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NonKeyAttributeNameList((System.Collections.Generic.List)value)); ++ // END MANUAL EDIT + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S30_LocalSecondaryIndexDescription__M9_IndexName(Wrappers_Compile._IOption> value) + { diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.1.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.1.0.patch new file mode 100644 index 000000000..e28782cea --- /dev/null +++ b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.1.0.patch @@ -0,0 +1,193 @@ +diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +index 04e0401a..c2f87875 100644 +--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java ++++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +@@ -10489,16 +10489,9 @@ public class ToDafny { + } + + public static Error Error(DynamoDbException nativeValue) { +- Option> message; +- message = +- Objects.nonNull(nativeValue.getMessage()) +- ? Option.create_Some( +- software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( +- nativeValue.getMessage() +- ) +- ) +- : Option.create_None(); +- return new Error_Opaque(message); ++ // BEGIN MANUAL EDIT ++ return new Error_Opaque(nativeValue); ++ // END MANUAL EDIT + } + + public static IDynamoDBClient DynamoDB_20120810(DynamoDbClient nativeValue) { +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 e3fa41d0..80bf84d1 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 +@@ -109,6 +109,9 @@ import software.amazon.awssdk.services.dynamodb.model.DestinationStatus; + import software.amazon.awssdk.services.dynamodb.model.DisableKinesisStreamingDestinationRequest; + import software.amazon.awssdk.services.dynamodb.model.DisableKinesisStreamingDestinationResponse; + import software.amazon.awssdk.services.dynamodb.model.DuplicateItemException; ++// BEGIN MANUAL EDIT ++import software.amazon.awssdk.services.dynamodb.model.DynamoDbException; ++// END MANUAL EDIT + import software.amazon.awssdk.services.dynamodb.model.EnableKinesisStreamingDestinationRequest; + import software.amazon.awssdk.services.dynamodb.model.EnableKinesisStreamingDestinationResponse; + import software.amazon.awssdk.services.dynamodb.model.Endpoint; +@@ -349,6 +352,9 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidRestoreTimeException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ItemCollectionSizeLimitExceededException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_LimitExceededException; ++// BEGIN MANUAL EDIT ++import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_Opaque; ++// END MANUAL EDIT + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_PointInTimeRecoveryUnavailableException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ProvisionedThroughputExceededException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ReplicaAlreadyExistsException; +@@ -422,6 +428,19 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Update + + public class ToNative { + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error(Error_Opaque dafnyValue) { ++ if (dafnyValue.dtor_obj() instanceof DynamoDbException) { ++ return (DynamoDbException) dafnyValue.dtor_obj(); ++ } ++ // Because we only ever put `DynamoDbException` into `Error_Opaque`, ++ // recieving any other type here indicates a bug with the codegen. ++ // Bubble up some error to indicate this failure state. ++ return new IllegalStateException("Unknown error recieved from DynamoDb."); ++ } ++ ++ // END MANUAL EDIT ++ + public static ArchivalSummary ArchivalSummary( + software.amazon.cryptography.services.dynamodb.internaldafny.types.ArchivalSummary dafnyValue + ) { +@@ -8035,6 +8054,124 @@ 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("Unknown error recieved from DynamoDb."); ++ } ++ ++ // END MANUAL EDIT ++ + public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) { + return ((Shim) dafnyValue).impl(); + } diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch index 3b6150cf1..e28782cea 100644 --- a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch +++ b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch @@ -1,5 +1,5 @@ diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java -index 04e0401..c2f8787 100644 +index 04e0401a..c2f87875 100644 --- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java @@ -10489,16 +10489,9 @@ public class ToDafny { @@ -23,7 +23,7 @@ index 04e0401..c2f8787 100644 public static IDynamoDBClient DynamoDB_20120810(DynamoDbClient nativeValue) { 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 e3fa41d..80bf84d 100644 +index e3fa41d0..80bf84d1 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 @@ -109,6 +109,9 @@ import software.amazon.awssdk.services.dynamodb.model.DestinationStatus; diff --git a/ComAmazonawsKms/codegen-patches/java/dafny-4.1.0.patch b/ComAmazonawsKms/codegen-patches/java/dafny-4.1.0.patch new file mode 100644 index 000000000..15d5e519e --- /dev/null +++ b/ComAmazonawsKms/codegen-patches/java/dafny-4.1.0.patch @@ -0,0 +1,202 @@ +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 +index 9084fae1..880ddcae 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 +@@ -4179,16 +4179,9 @@ public class ToDafny { + } + + public static Error Error(KmsException nativeValue) { +- Option> message; +- message = +- Objects.nonNull(nativeValue.getMessage()) +- ? Option.create_Some( +- software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( +- nativeValue.getMessage() +- ) +- ) +- : Option.create_None(); +- return new Error_Opaque(message); ++ // BEGIN MANUAL EDIT ++ return new Error_Opaque(nativeValue); ++ // END MANUAL EDIT + } + + public static IKMSClient TrentService(KmsClient nativeValue) { +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 b4cc1964..98e53314 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 +@@ -103,6 +103,9 @@ import software.amazon.awssdk.services.kms.model.KeySpec; + import software.amazon.awssdk.services.kms.model.KeyState; + import software.amazon.awssdk.services.kms.model.KeyUnavailableException; + import software.amazon.awssdk.services.kms.model.KeyUsageType; ++// BEGIN MANUAL EDIT ++import software.amazon.awssdk.services.kms.model.KmsException; ++// END MANUAL EDIT + import software.amazon.awssdk.services.kms.model.KmsInternalException; + import software.amazon.awssdk.services.kms.model.KmsInvalidSignatureException; + import software.amazon.awssdk.services.kms.model.KmsInvalidStateException; +@@ -178,12 +181,30 @@ import software.amazon.cryptography.services.kms.internaldafny.types.Error_KeyUn + import software.amazon.cryptography.services.kms.internaldafny.types.Error_LimitExceededException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_MalformedPolicyDocumentException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_NotFoundException; ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; ++// END MANUAL EDIT ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; ++// BEGIN MANUAL EDIT + import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient; + + public class ToNative { + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error(Error_Opaque dafnyValue) { ++ if (dafnyValue.dtor_obj() instanceof KmsException) { ++ return (KmsException) dafnyValue.dtor_obj(); ++ } ++ // Because we only ever put `KmsException` into `Error_Opaque`, ++ // recieving any other type here indicates a bug with the codegen. ++ // Bubble up some error to indicate this failure state. ++ return new IllegalStateException("Unknown error recieved from KMS."); ++ } ++ ++ // END MANUAL EDIT ++ + public static AlgorithmSpec AlgorithmSpec( + software.amazon.cryptography.services.kms.internaldafny.types.AlgorithmSpec dafnyValue + ) { +@@ -3339,6 +3360,132 @@ 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_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_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_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_Opaque()) { ++ return ToNative.Error((Error_Opaque) dafnyValue); ++ } ++ // TODO This should indicate a codegen bug ++ return new IllegalStateException("Unknown error recieved from KMS."); ++ } ++ ++ // END MANUAL EDIT ++ + public static KmsClient TrentService(IKMSClient dafnyValue) { + return ((Shim) dafnyValue).impl(); + } diff --git a/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/dafny/dafny-4.1.0.patch b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/dafny/dafny-4.1.0.patch new file mode 100644 index 000000000..61ab71a7a --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/dafny/dafny-4.1.0.patch @@ -0,0 +1,32 @@ +diff --git b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy +index 47fc0d23..0e6e4b7f 100644 +--- b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy ++++ a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy +@@ -250,7 +250,9 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService + import Operations : AbstractAwsCryptographyMaterialProvidersTestVectorKeysOperations + function method DefaultKeyVectorsConfig(): KeyVectorsConfig + method KeyVectors(config: KeyVectorsConfig := DefaultKeyVectorsConfig()) +- returns (res: Result) ++ // BEGIN MANUAL FIX ++ returns (res: Result) ++ // END MANUAL FIX + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) +@@ -258,10 +260,14 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService + && res.value.ValidState() + + // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals +- function method CreateSuccessOfClient(client: IKeyVectorsClient): Result { ++ // BEGIN MANUAL FIX ++ function method CreateSuccessOfClient(client: KeyVectorsClient): Result { ++ // END MANUAL FIX + Success(client) + } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals +- function method CreateFailureOfError(error: Error): Result { ++ // BEGIN MANUAL FIX ++ function method CreateFailureOfError(error: Error): Result { ++ // END MANUAL FIX + Failure(error) + } + class KeyVectorsClient extends IKeyVectorsClient diff --git a/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/java/dafny-4.1.0.patch b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/java/dafny-4.1.0.patch new file mode 100644 index 000000000..20f508012 --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/KeyVectors/java/dafny-4.1.0.patch @@ -0,0 +1,25 @@ +diff --git b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java +index 50632855..e9a071c5 100644 +--- b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java ++++ a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java +@@ -10,6 +10,9 @@ import software.amazon.cryptography.materialproviders.CryptographicMaterialsMana + import software.amazon.cryptography.materialproviders.ICryptographicMaterialsManager; + import software.amazon.cryptography.materialproviders.IKeyring; + import software.amazon.cryptography.materialproviders.Keyring; ++// BEGIN MANUAL FIX ++import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.KeyVectorsClient; ++// END MANUAL FIX + import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.__default; + import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error; + import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.IKeyVectorsClient; +@@ -29,7 +32,9 @@ public class KeyVectors { + KeyVectorsConfig input = builder.KeyVectorsConfig(); + software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.KeyVectorsConfig dafnyValue = + ToDafny.KeyVectorsConfig(input); +- Result result = __default.KeyVectors(dafnyValue); ++ // BEGIN MANUAL FIX ++ Result result = __default.KeyVectors(dafnyValue); ++ // END MANUAL FIX + if (result.is_Failure()) { + throw ToNative.Error(result.dtor_error()); + } diff --git a/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch new file mode 100644 index 000000000..e55782a7a --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch @@ -0,0 +1,15 @@ +diff --git b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +index 87b39a81..e57de1dd 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 + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: +- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError( ++ // BEGIN MANUAL EDIT ++ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( ++ // END MANUAL EDIT + dafnyVal._ComAmazonawsKms + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal: diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy index 47fc0d230..0e6e4b7fb 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy @@ -250,7 +250,9 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService import Operations : AbstractAwsCryptographyMaterialProvidersTestVectorKeysOperations function method DefaultKeyVectorsConfig(): KeyVectorsConfig method KeyVectors(config: KeyVectorsConfig := DefaultKeyVectorsConfig()) - returns (res: Result) + // BEGIN MANUAL FIX + returns (res: Result) + // END MANUAL FIX ensures res.Success? ==> && fresh(res.value) && fresh(res.value.Modifies) @@ -258,10 +260,14 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService && res.value.ValidState() // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals - function method CreateSuccessOfClient(client: IKeyVectorsClient): Result { + // BEGIN MANUAL FIX + function method CreateSuccessOfClient(client: KeyVectorsClient): Result { + // END MANUAL FIX Success(client) } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals - function method CreateFailureOfError(error: Error): Result { + // BEGIN MANUAL FIX + function method CreateFailureOfError(error: Error): Result { + // END MANUAL FIX Failure(error) } class KeyVectorsClient extends IKeyVectorsClient diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy index acb6c1e45..83543c3c7 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy @@ -21,7 +21,9 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in } method KeyVectors(config: KeyVectorsConfig) - returns (res: Result) + // BEGIN MANUAL FIX + returns (res: Result) + // END MANUAL FIX ensures res.Success? ==> res.value is KeyVectorsClient { @@ -49,7 +51,9 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in ); var client := new KeyVectorsClient(config); - res := Success(client as IKeyVectorsClient); + // BEGIN MANUAL FIX + res := Success(client); + // END MANUAL FIX } class KeyVectorsClient... { diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy index 34076485a..3674c06a9 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy @@ -186,13 +186,13 @@ module {:options "-functionSyntax:4"} TestManifests { datatype ManifestData = | DecryptManifest( version: nat, - keys: KeyVectorsTypes.IKeyVectorsClient, + keys: KeyVectors.KeyVectorsClient, client: Values.JSON, jsonTests: seq<(string, Values.JSON)> ) | EncryptManifest( version: nat, - keys: KeyVectorsTypes.IKeyVectorsClient, + keys: KeyVectors.KeyVectorsClient, jsonTests: seq<(string, Values.JSON)> ) diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java index 6f8c75567..220646025 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java @@ -1,3 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 package software.amazon.cryptography.materialproviders.internaldafny.wrapped; import Wrappers_Compile.Result; @@ -25,8 +27,6 @@ > WrappedMaterialProviders(MaterialProvidersConfig config) { .builder() .impl(impl) .build(); - return software.amazon.cryptography.materialproviders.internaldafny.__default.CreateSuccessOfClient( - wrappedClient - ); + return Result.create_Success(wrappedClient); } } diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/__default.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/__default.java index 728c26e88..1e8fd3307 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/__default.java +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviderstestvectorkeys/internaldafny/__default.java @@ -1,3 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 package software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny; public class __default extends _ExternBase___default {} diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java index 506328556..e9a071c58 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/KeyVectors.java @@ -10,6 +10,9 @@ import software.amazon.cryptography.materialproviders.ICryptographicMaterialsManager; import software.amazon.cryptography.materialproviders.IKeyring; import software.amazon.cryptography.materialproviders.Keyring; +// BEGIN MANUAL FIX +import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.KeyVectorsClient; +// END MANUAL FIX import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.__default; import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error; import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.IKeyVectorsClient; @@ -29,7 +32,9 @@ protected KeyVectors(BuilderImpl builder) { KeyVectorsConfig input = builder.KeyVectorsConfig(); software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.KeyVectorsConfig dafnyValue = ToDafny.KeyVectorsConfig(input); - Result result = __default.KeyVectors(dafnyValue); + // BEGIN MANUAL FIX + Result result = __default.KeyVectors(dafnyValue); + // END MANUAL FIX if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); }