-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(dafny): Local Service Constructors MUST return concrete
- Loading branch information
Showing
30 changed files
with
788 additions
and
32 deletions.
There are no files selected for viewing
32 changes: 32 additions & 0 deletions
32
...terialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.1.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<IAwsCryptographicMaterialProvidersClient, Error>) | ||
| + // BEGIN MANUAL FIX | ||
| + returns (res: Result<MaterialProvidersClient, Error>) | ||
| + // 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<IAwsCryptographicMaterialProvidersClient, Error> { | ||
| + // BEGIN MANUAL FIX | ||
| + function method CreateSuccessOfClient(client: MaterialProvidersClient): Result<MaterialProvidersClient, Error> { | ||
| + // 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<IAwsCryptographicMaterialProvidersClient, Error> { | ||
| + // BEGIN MANUAL FIX | ||
| + function method CreateFailureOfError(error: Error): Result<MaterialProvidersClient, Error> { | ||
| + // END MANUAL FIX | ||
| Failure(error) | ||
| } | ||
| class MaterialProvidersClient extends IAwsCryptographicMaterialProvidersClient |
15 changes: 15 additions & 0 deletions
15
...erialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.1.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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: |
25 changes: 25 additions & 0 deletions
25
...aterialProviders/codegen-patches/AwsCryptographicMaterialProviders/java/dafny-4.1.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<IAwsCryptographicMaterialProvidersClient, Error> result = | ||
| + //BEGIN MANUAL FIX | ||
| + Result<MaterialProvidersClient, Error> result = | ||
| + //END MANUAL FIX | ||
| __default.MaterialProviders(dafnyValue); | ||
| if (result.is_Failure()) { | ||
| throw ToNative.Error(result.dtor_error()); |
32 changes: 32 additions & 0 deletions
32
...ographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.1.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<IKeyStoreClient, Error>) | ||
| + // BEGIN MANUAL FIX | ||
| + returns (res: Result<KeyStoreClient, Error>) | ||
| + // 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<IKeyStoreClient, Error> { | ||
| + // BEGIN MANUAL FIX | ||
| + function method CreateSuccessOfClient(client: KeyStoreClient): Result<KeyStoreClient, Error> { | ||
| + // 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<IKeyStoreClient, Error> { | ||
| + // BEGIN MANUAL FIX | ||
| + function method CreateFailureOfError(error: Error): Result<KeyStoreClient, Error> { | ||
| + // END MANUAL FIX | ||
| Failure(error) | ||
| } | ||
| class KeyStoreClient extends IKeyStoreClient |
26 changes: 26 additions & 0 deletions
26
...graphicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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( |
25 changes: 25 additions & 0 deletions
25
...tographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.1.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<IKeyStoreClient, Error> result = __default.KeyStore(dafnyValue); | ||
| + // BEGIN MANUAL FIX | ||
| + Result<KeyStoreClient, Error> result = __default.KeyStore(dafnyValue); | ||
| + // END MANUAL FIX | ||
| if (result.is_Failure()) { | ||
| throw ToNative.Error(result.dtor_error()); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.