auto commit

aws · Dec 10, 2024 · 5610c8b · 5610c8b
1 parent 6db9ace
commit 5610c8b
Show file tree

Hide file tree

Showing 9 changed files with 44 additions and 44 deletions.
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
@@ -3,7 +3,7 @@
 
 include "AwsEncryptionSdkOperations.dfy"
 
-module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService {
+module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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