diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy index ab851b1a8..736240c08 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy @@ -5,7 +5,7 @@ include "AwsEncryptionSdkOperations.dfy" module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } - EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService { + ESDK refines AbstractAwsCryptographyEncryptionSdkService { import Operations = AwsEncryptionSdkOperations import Primitives = AtomicPrimitives import MaterialProviders diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy index 7f8ec2943..dbd9bc181 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy @@ -6,7 +6,7 @@ include "../src/Index.dfy" module TestCreateEsdkClient { import Types = AwsCryptographyEncryptionSdkTypes import mplTypes = AwsCryptographyMaterialProvidersTypes - import EncryptionSdk + import ESDK import MaterialProviders import opened Wrappers import opened UInt = StandardLibrary.UInt @@ -50,11 +50,11 @@ module TestCreateEsdkClient { ]; method {:test} TestClientCreation() { - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); - var esdk: Types.IAwsEncryptionSdkClient :- expect EncryptionSdk.ESDK(config := defaultConfig); - expect esdk is EncryptionSdk.ESDKClient; - var esdkClient := esdk as EncryptionSdk.ESDKClient; + var esdk: Types.IAwsEncryptionSdkClient :- expect ESDK.ESDK(config := defaultConfig); + expect esdk is ESDK.ESDKClient; + var esdkClient := esdk as ESDK.ESDKClient; expect esdkClient.config.commitmentPolicy == defaultConfig.commitmentPolicy.value; expect esdkClient.config.maxEncryptedDataKeys == defaultConfig.maxEncryptedDataKeys; @@ -82,7 +82,7 @@ module TestCreateEsdkClient { netV4_0_0_RetryPolicy := Some(Types.NetV4_0_0_RetryPolicy.FORBID_RETRY) ); - var noRetryEsdk :- expect EncryptionSdk.ESDK(config := esdkConfig); + var noRetryEsdk :- expect ESDK.ESDK(config := esdkConfig); var expectFailureDecryptOutput := noRetryEsdk.Decrypt(Types.DecryptInput( ciphertext := ESDK_NET_V400_MESSAGE, @@ -95,8 +95,8 @@ module TestCreateEsdkClient { // Decrypt v4.0.0 message with the default configuration which is to retry // and expect decryption to pass - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var decryptOutput := esdk.Decrypt(Types.DecryptInput( ciphertext := ESDK_NET_V400_MESSAGE, diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestEncryptDecrypt.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestEncryptDecrypt.dfy index 58f5dc976..e195f96e8 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestEncryptDecrypt.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestEncryptDecrypt.dfy @@ -9,7 +9,7 @@ module TestEncryptDecrypt { import Types = AwsCryptographyEncryptionSdkTypes import mplTypes = AwsCryptographyMaterialProvidersTypes import MaterialProviders - import EncryptionSdk + import ESDK import opened Wrappers import Fixtures @@ -20,8 +20,8 @@ module TestEncryptDecrypt { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput); var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2")); diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy index ea074601d..c27eaa1db 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy @@ -9,7 +9,7 @@ module TestReproducedEncryptionContext { import Types = AwsCryptographyEncryptionSdkTypes import mplTypes = AwsCryptographyMaterialProvidersTypes import MaterialProviders - import EncryptionSdk + import ESDK import opened Wrappers import Fixtures @@ -20,8 +20,8 @@ module TestReproducedEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput); var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2")); @@ -67,8 +67,8 @@ module TestReproducedEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput); var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2")); @@ -113,8 +113,8 @@ module TestReproducedEncryptionContext { var asdf := [ 97, 115, 100, 102 ]; var namespace, name := Fixtures.NamespaceAndName(0); - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); var rawAESKeyring :- expect mpl.CreateRawAesKeyring(mplTypes.CreateRawAesKeyringInput( keyNamespace := namespace, diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy index f8b02fbc7..8c78050a2 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy @@ -16,7 +16,7 @@ module TestRequiredEncryptionContext { import KMS = Com.Amazonaws.Kms import DDB = Com.Amazonaws.Dynamodb import DDBTypes = ComAmazonawsDynamodbTypes - import EncryptionSdk + import ESDK import opened Wrappers import UTF8 @@ -35,8 +35,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -120,8 +120,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -229,8 +229,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -411,8 +411,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -586,8 +586,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -711,8 +711,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -814,8 +814,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -918,8 +918,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -1018,8 +1018,8 @@ module TestRequiredEncryptionContext { // The string "asdf" as bytes var asdf := [ 97, 115, 100, 102 ]; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); // get keyrings @@ -1133,8 +1133,8 @@ module TestRequiredEncryptionContext { ensures output.ValidState() && fresh(output) && fresh(output.History) && fresh(output.Modifies) { var kmsKey := Fixtures.keyArn; - var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); + var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); + var esdk :- expect ESDK.ESDK(config := defaultConfig); var mpl :- expect MaterialProviders.MaterialProviders(); var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput); var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2")); diff --git a/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy b/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy index 5a1da5c96..944874abf 100644 --- a/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy +++ b/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy @@ -7,7 +7,7 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.wrapped" } WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService { - import WrappedService = EncryptionSdk + import WrappedService = ESDK function method WrappedDefaultAwsEncryptionSdkConfig(): AwsEncryptionSdkConfig { diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy index 32b45ef0c..5e7fa11cb 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy @@ -7,7 +7,7 @@ module {:options "/functionSyntax:4"} AllEsdkV4NoReqEc { import Types = AwsCryptographyEncryptionSdkTypes import mplTypes = AwsCryptographyMaterialProvidersTypes import keyVectorKeyTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes - import EncryptionSdk + import ESDK import MaterialProviders import opened CompleteVectors import opened KeyDescription diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy index c74b1b460..f89a805c8 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy @@ -6,7 +6,7 @@ include "../LibraryIndex.dfy" module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc { import Types = AwsCryptographyEncryptionSdkTypes import mplTypes = AwsCryptographyMaterialProvidersTypes - import EncryptionSdk + import ESDK import MaterialProviders import opened CompleteVectors import opened KeyDescription diff --git a/TestVectors/dafny/TestVectors/src/WriteVectors.dfy b/TestVectors/dafny/TestVectors/src/WriteVectors.dfy index b56b87506..69bd11d68 100644 --- a/TestVectors/dafny/TestVectors/src/WriteVectors.dfy +++ b/TestVectors/dafny/TestVectors/src/WriteVectors.dfy @@ -9,7 +9,7 @@ include "WriteEsdkJsonManifests.dfy" module {:options "-functionSyntax:4"} WriteVectors { import Types = AwsCryptographyEncryptionSdkTypes import mplTypes = AwsCryptographyMaterialProvidersTypes - import EncryptionSdk + import ESDK import MaterialProviders import opened CompleteVectors import opened Wrappers