aws · texastony · Sep 18, 2024 · Sep 11, 2024 · Sep 12, 2024 · Sep 13, 2024
diff --git a/.github/workflows/block_main.yml b/.github/workflows/block_main.yml
diff --git a/.github/workflows/library_interop_tests.yml b/.github/workflows/library_interop_tests.yml
@@ -25,10 +25,7 @@ jobs:
             ubuntu-latest,
             macos-12,
           ]
-        # language: [java, net]
-        # Cutting .NET tests for rc-1.7.0
-        # We MUST restore these before going GA
-        language: [java]
+        language: [java, net]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -131,12 +128,8 @@ jobs:
             ubuntu-latest,
             macos-12,
           ]
-        # Cutting .NET tests for rc-1.7.0
-        # We MUST restore these before going GA
-        # encrypting_language: [java, net]
-        # decrypting_language: [java, net]
-        encrypting_language: [java]
-        decrypting_language: [java]
+        encrypting_language: [java, net]
+        decrypting_language: [java, net]
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
     permissions:

diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml
@@ -19,15 +19,14 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        library: [
+        library:
+          [
             StandardLibrary,
             AwsCryptographyPrimitives,
             ComAmazonawsKms,
             ComAmazonawsDynamodb,
-            # Cutting .NET tests for rc-1.7.0
-            # We MUST restore these before going GA
-            # AwsCryptographicMaterialProviders,
-            # TestVectorsAwsCryptographicMaterialProviders,
+            AwsCryptographicMaterialProviders,
+            TestVectorsAwsCryptographicMaterialProviders,
           ]
         dotnet-version: ["6.0.x"]
         os: [windows-latest, ubuntu-latest, macos-12]

diff --git a/.gitignore b/.gitignore
@@ -6,6 +6,7 @@ build/*
 test/**/Output/*
 /package-lock.json
 /node_modules
+*.log
 
 # Duvet output
 specification_compliance_report.html

diff --git a/AwsCryptographicMaterialProviders/Makefile b/AwsCryptographicMaterialProviders/Makefile
@@ -8,9 +8,11 @@ include ../SharedMakefileV2.mk
 PROJECT_SERVICES := \
 	AwsCryptographicMaterialProviders \
 	AwsCryptographyKeyStore \
+	AwsCryptographyKeyStoreAdmin \
 
 SERVICE_NAMESPACE_AwsCryptographicMaterialProviders=aws.cryptography.materialProviders
 SERVICE_NAMESPACE_AwsCryptographyKeyStore=aws.cryptography.keyStore
+SERVICE_NAMESPACE_AwsCryptographyKeyStoreAdmin=aws.cryptography.keyStoreAdmin
 
 MAX_RESOURCE_COUNT=90000000
 # Order is important
@@ -44,3 +46,9 @@ SERVICE_DEPS_AwsCryptographyKeyStore := \
 	ComAmazonawsDynamodb \
 	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
 
+SERVICE_DEPS_AwsCryptographyKeyStoreAdmin := \
+	AwsCryptographyPrimitives \
+	ComAmazonawsKms \
+	ComAmazonawsDynamodb \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
diff --git a/...terialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.8.0.patch b/...terialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.8.0.patch
@@ -0,0 +1,21 @@
+diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
+index ba2a2324..39a4a4e7 100644
+--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
+@@ -1,11 +1,11 @@
+ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+ // SPDX-License-Identifier: Apache-2.0
+ // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/StandardLibrary/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/AwsCryptographyPrimitives/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/ComAmazonawsDynamodb/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/ComAmazonawsKms/src/Index.dfy"
++include "../../../../StandardLibrary/src/Index.dfy"
++include "../../../../AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
++include "../../../../AwsCryptographyPrimitives/src/Index.dfy"
++include "../../../../ComAmazonawsDynamodb/src/Index.dfy"
++include "../../../../ComAmazonawsKms/src/Index.dfy"
+ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.types" } AwsCryptographyMaterialProvidersTypes
+ {
+   import opened Wrappers
diff --git a/...erialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.8.0.patch b/...erialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.8.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 0b153802..56aef9ec 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
+@@ -3903,7 +3903,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/...tographyKeyStore/dotnet/dafny-4.1.0.patch → ...AwsCryptographyKeyStore/dafny-4.7.0.patch b/...tographyKeyStore/dotnet/dafny-4.1.0.patch → ...AwsCryptographyKeyStore/dafny-4.7.0.patch
@@ -1,26 +1,22 @@
-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
+diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
+index c10f4e45..8e563bf5 100644
+--- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
++++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
+@@ -1773,7 +1773,7 @@ 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
++          return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( // Manual edit KMS. -> Kms.
              dafnyVal._ComAmazonawsKms
            );
-         case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal:
-@@ -652,7 +654,9 @@ namespace AWS.Cryptography.KeyStore
+         case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStorageException dafnyVal:
+@@ -1800,7 +1800,7 @@ 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
++            Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value) // Manual edit KMS. -> Kms.
            );
          case "Com.Amazonaws.Dynamodb":
            return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsDynamodb(
diff --git a/...ographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.8.0.patch b/...ographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.8.0.patch
@@ -0,0 +1,26 @@
+diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+index 5764797e..4310b660 100644
+--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+@@ -1,9 +1,9 @@
+ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+ // SPDX-License-Identifier: Apache-2.0
+ // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/StandardLibrary/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/ComAmazonawsDynamodb/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/ComAmazonawsKms/src/Index.dfy"
++include "../../../../StandardLibrary/src/Index.dfy"
++include "../../../../ComAmazonawsDynamodb/src/Index.dfy"
++include "../../../../ComAmazonawsKms/src/Index.dfy"
+ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } AwsCryptographyKeyStoreTypes
+ {
+   import opened Wrappers
+@@ -785,7 +785,7 @@ abstract module AbstractAwsCryptographyKeyStoreService
+   import opened Types = AwsCryptographyKeyStoreTypes
+   import Operations : AbstractAwsCryptographyKeyStoreOperations
+   function method DefaultKeyStoreConfig(): KeyStoreConfig
+-  method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
++  method {:vcs_split_on_every_assert} {:rlimit 90500000} KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
+     returns (res: Result<KeyStoreClient, Error>)
+     requires config.ddbClient.Some? ==>
+                config.ddbClient.value.ValidState()
diff --git a/...tographyKeyStore/dotnet/dafny-4.2.0.patch → ...tographyKeyStore/dotnet/dafny-4.8.0.patch b/...tographyKeyStore/dotnet/dafny-4.2.0.patch → ...tographyKeyStore/dotnet/dafny-4.8.0.patch
@@ -1,26 +1,35 @@
 diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
-index 95c9eba1..bcd537fb 100644
+index cc3dc4cd..63100b40 100644
 --- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
 +++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
-@@ -732,7 +732,9 @@ namespace AWS.Cryptography.KeyStore
+@@ -1727,7 +1727,7 @@ 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
++          return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( // Manual edit KMS. -> Kms.
              dafnyVal._ComAmazonawsKms
            );
-         case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal:
-@@ -755,7 +757,9 @@ namespace AWS.Cryptography.KeyStore
+         case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStorageException dafnyVal:
+@@ -1754,7 +1754,7 @@ 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
++            Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value) // Manual edit KMS. -> Kms.
            );
          case "Com.Amazonaws.Dynamodb":
            return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsDynamodb(
+diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/WriteMutatedVersionsInput.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/WriteMutatedVersionsInput.cs
+index 16da0962..9607f4a4 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/WriteMutatedVersionsInput.cs
++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/WriteMutatedVersionsInput.cs
+@@ -11,7 +11,7 @@ namespace AWS.Cryptography.KeyStore
+     private string _identifier;
+     private System.IO.MemoryStream _original;
+     private System.IO.MemoryStream _terminal;
+-    private bool? _completeMutation;
++    private bool? _completeMutation = false; // Manual edit to default false
+     public System.Collections.Generic.List<AWS.Cryptography.KeyStore.EncryptedHierarchicalKey> Items
+     {
+       get { return this._items; }
diff --git a/...tographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.8.0.patch b/...tographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/java/dafny-4.8.0.patch
@@ -0,0 +1,13 @@
+diff --git b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/WriteMutatedVersionsInput.java a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/WriteMutatedVersionsInput.java
+index 16acf434..d72c36c3 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/WriteMutatedVersionsInput.java
++++ a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/WriteMutatedVersionsInput.java
+@@ -149,7 +149,7 @@ public class WriteMutatedVersionsInput {
+
+     protected ByteBuffer Terminal;
+
+-    protected Boolean CompleteMutation;
++    protected Boolean CompleteMutation = false; // Manual Edit to default to false
+
+     protected BuilderImpl() {}
+
diff --git a/...hicMaterialProviders/codegen-patches/AwsCryptographyKeyStoreAdmin/dafny/dafny-4.8.0.patch b/...hicMaterialProviders/codegen-patches/AwsCryptographyKeyStoreAdmin/dafny/dafny-4.8.0.patch
@@ -0,0 +1,19 @@
+diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
+index 75dcc28b..455a38f8 100644
+--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
+@@ -1,10 +1,10 @@
+ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+ // SPDX-License-Identifier: Apache-2.0
+ // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/StandardLibrary/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/ComAmazonawsDynamodb/src/Index.dfy"
+-include "../../../../../../../../Volumes/workplace/aws-cryptographic-material-providers-library/ComAmazonawsKms/src/Index.dfy"
++include "../../../../StandardLibrary/src/Index.dfy"
++include "../../../../AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
++include "../../../../ComAmazonawsDynamodb/src/Index.dfy"
++include "../../../../ComAmazonawsKms/src/Index.dfy"
+ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types" } AwsCryptographyKeyStoreAdminTypes
+ {
+   import opened Wrappers
diff --git a/...icMaterialProviders/codegen-patches/AwsCryptographyKeyStoreAdmin/dotnet/dafny-4.2.0.patch b/...icMaterialProviders/codegen-patches/AwsCryptographyKeyStoreAdmin/dotnet/dafny-4.2.0.patch
@@ -0,0 +1,14 @@
+diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
+index 2122e39c..2d12b29f 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
+@@ -833,7 +833,8 @@ namespace AWS.Cryptography.KeyStoreAdmin
+             dafnyVal._ComAmazonawsDynamodb
+           );
+         case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
+-          return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
++          // MANUAL EDIT KMS -> Kms
++          return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
+             dafnyVal._ComAmazonawsKms
+           );
+         case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_KeyStoreAdminException dafnyVal:
diff --git a/...icMaterialProviders/codegen-patches/AwsCryptographyKeyStoreAdmin/dotnet/dafny-4.8.0.patch b/...icMaterialProviders/codegen-patches/AwsCryptographyKeyStoreAdmin/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,14 @@
+diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
+index b8ad30a5..4904d73b 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
+@@ -1056,7 +1056,8 @@ namespace AWS.Cryptography.KeyStoreAdmin
+             dafnyVal._ComAmazonawsDynamodb
+           );
+         case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
+-          return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
++          // MANUAL EDIT KMS -> Kms
++          return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
+             dafnyVal._ComAmazonawsKms
+           );
+         case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_KeyStoreAdminException dafnyVal:
diff --git a/...s/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/...s/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
 include "../../../../StandardLibrary/src/Index.dfy"
-include "../../AwsCryptographyKeyStore/src/Index.dfy"
+include "../../../../AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
 include "../../../../AwsCryptographyPrimitives/src/Index.dfy"
 include "../../../../ComAmazonawsDynamodb/src/Index.dfy"
 include "../../../../ComAmazonawsKms/src/Index.dfy"