feat(KeyStoreAdmin):

.github/workflows/library_concurrency_tests.yml

@@ -0,0 +1,116 @@
+# This workflow performs Concurrency tests of the MPL in Java.
+name: Library Concurrency Tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  generateEncryptVectors:
+    strategy:
+      matrix:
+        library: [AwsCryptographicMaterialProviders]
+        os: [
+            # https://taskei.amazon.dev/tasks/CrypTool-5283
+            # windows-latest,
+            ubuntu-latest,
+            macos-13,
+          ]
+        language: [
+            java,
+            # net,
+            # python,
+            # rust
+          ]
+        # https://taskei.amazon.dev/tasks/CrypTool-5284
+        java-versions: [8, 17]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+
+      # Test Vectors need to call KMS
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: ConcurrencyTests
+
+      - uses: actions/checkout@v3
+      #  Not all submodules are needed.
+      # We manually pull the submodule we DO need.
+      - run: git submodule update --init libraries
+      - run: git submodule update --init --recursive smithy-dafny
+
+      # Setup Java in Rust is needed for running polymorph
+      - name: Setup Java 17
+        if: matrix.language == 'java' || matrix.language == 'rust'
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 17
+
+      - name: Setup .NET Core SDK '6.0.x'
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: "6.0.x"
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ inputs.dafny }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+
+      # Build implementation for each runtime
+      - name: Build ${{ matrix.library }} implementation in Java
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_java CORES=$CORES
+
+      - name: Setup gradle
+        if: matrix.language == 'java'
+        uses: gradle/gradle-build-action@v2
+        with:
+          gradle-version: 7.2
+
+      - name: Setup Java ${{matrix.java-versions}}
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: ${{matrix.java-versions}}
+
+      - name: Compile Java
+        uses: gradle/gradle-build-action@v3
+        with:
+          arguments: build
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Test Java
+        uses: gradle/gradle-build-action@v3
+        with:
+          arguments: testConcurrentExamples
+          build-root-directory: ./${{ matrix.library }}/runtimes/java

.github/workflows/library_examples.yml

@@ -0,0 +1,58 @@
+# "Copyright Amazon.com Inc. or its affiliates. All Rights Reserved."
+# "SPDX-License-Identifier: CC-BY-SA-4.0"
+# This workflow runs any examples.
+name: Library Examples
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+
+jobs:
+  java:
+    runs-on: ubuntu-latest
+    permissions:
+      id-token: write
+      contents: read
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: JavaExampleTests
+
+      - uses: actions/checkout@v4
+      - run: git submodule update --init libraries
+      - run: git submodule update --init smithy-dafny
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Setup Java 8
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 8
+
+      - name: Build AwsCryptographicMaterialProviders Java implementation
+        working-directory: ./AwsCryptographicMaterialProviders
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_java CORES=$CORES
+
+      - name: Test AwsCryptographicMaterialProviders Java Examples
+        working-directory: ./AwsCryptographicMaterialProviders
+        run: |
+          make test_example_java

.github/workflows/pull.yml

@@ -29,6 +29,11 @@ jobs:
     uses: ./.github/workflows/library_java_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-examples:
+    needs: getVersion
+    uses: ./.github/workflows/library_examples.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
   pr-ci-net:
     needs: getVersion
     uses: ./.github/workflows/library_net_tests.yml
@@ -65,6 +70,7 @@ jobs:
       - pr-ci-java
       - pr-ci-net
       - pr-interop-test
+      - pr-ci-examples
     runs-on: ubuntu-latest
     steps:
       - name: Verify all required jobs passed

AwsCryptographicMaterialProviders/Makefile

@@ -9,10 +9,15 @@ include ../SharedMakefileV2.mk
 
 PROJECT_SERVICES := \
 	AwsCryptographyKeyStore \
-	AwsCryptographicMaterialProviders \
+	AwsCryptographyKeyStoreAdmin \
+	AwsCryptographicMaterialProviders
 
 SERVICE_NAMESPACE_AwsCryptographicMaterialProviders=aws.cryptography.materialProviders
 SERVICE_NAMESPACE_AwsCryptographyKeyStore=aws.cryptography.keyStore
+SERVICE_NAMESPACE_AwsCryptographyKeyStoreAdmin=aws.cryptography.keyStoreAdmin
+
+# 90_000_000 or 9e7
+MAX_RESOURCE_COUNT=90000000
 
 MAIN_SERVICE_FOR_RUST := AwsCryptographicMaterialProviders
 
@@ -36,7 +41,6 @@ RUST_OTHER_FILES := \
 	runtimes/rust/src/time.rs \
 	runtimes/rust/src/uuid.rs
 
-MAX_RESOURCE_COUNT=90000000
 # Order is important
 # In java they MUST be built
 # in the order they depend on each other
@@ -68,8 +72,15 @@ SERVICE_DEPS_AwsCryptographyKeyStore := \
 	ComAmazonawsDynamodb \
 	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
 
+SERVICE_DEPS_AwsCryptographyKeyStoreAdmin := \
+	AwsCryptographyPrimitives \
+	ComAmazonawsKms \
+	ComAmazonawsDynamodb \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
 # Constants for languages that drop extern names (Python, Go)
 
+
 MPL_CORE_TYPES_FILE_PATH=dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
 MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.materialproviders.internaldafny.types\" } AwsCryptographyMaterialProvidersTypes"
 MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyMaterialProvidersTypes"
@@ -86,6 +97,14 @@ KEYSTORE_INDEX_FILE_PATH=dafny/AwsCryptographyKeyStore/src/Index.dfy
 KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystore.internaldafny\"} KeyStore refines AbstractAwsCryptographyKeyStoreService"
 KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING="module KeyStore refines AbstractAwsCryptographyKeyStoreService"
 
+KEYSTORE_ADMIN_TYPES_FILE_PATH=dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
+KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystoreadmin.internaldafny.types\" } AwsCryptographyKeyStoreAdminTypes"
+KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyKeyStoreAdminTypes"
+
+KEYSTORE_ADMIN_INDEX_FILE_PATH=dafny/AwsCryptographyKeyStoreAdmin/src/Index.dfy
+KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystoreadmin.internaldafny\"} KeyStoreAdmin refines AbstractAwsCryptographyKeyStoreAdminService"
+KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING="module KeyStoreAdmin refines AbstractAwsCryptographyKeyStoreAdminService"
+
 SYNCHRONIZED_LOCAL_CMC_FILE_PATH=dafny/AwsCryptographicMaterialProviders/src/CMCs/SynchronizedLocalCMC.dfy
 SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } {:extern \"software.amazon.cryptography.internaldafny.SynchronizedLocalCMC\" } SynchronizedLocalCMC {"
 SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } SynchronizedLocalCMC {"
@@ -97,20 +116,24 @@ STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\
 _sed_types_file_remove_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_TYPES_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING)
 
 _sed_index_file_remove_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_INDEX_FILE_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(SYNCHRONIZED_LOCAL_CMC_FILE_PATH) SED_BEFORE_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING) SED_AFTER_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(STORM_TRACKING_CMC_FILE_PATH) SED_BEFORE_STRING=$(STORM_TRACKING_CMC_WITH_EXTERN_STRING) SED_AFTER_STRING=$(STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING)
 
 _sed_types_file_add_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_TYPES_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING)
 
 _sed_index_file_add_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_INDEX_FILE_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(SYNCHRONIZED_LOCAL_CMC_FILE_PATH) SED_BEFORE_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(STORM_TRACKING_CMC_FILE_PATH) SED_BEFORE_STRING=$(STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(STORM_TRACKING_CMC_WITH_EXTERN_STRING)
 
@@ -130,3 +153,7 @@ PYTHON_DEPENDENCY_MODULE_NAMES := \
 	--dependency-library-name=com.amazonaws.dynamodb=aws_cryptography_internal_dynamodb \
 	--dependency-library-name=aws.cryptography.materialProviders=aws_cryptographic_material_providers \
 	--dependency-library-name=aws.cryptography.keyStore=aws_cryptographic_material_providers \
+	--dependency-library-name=aws.cryptography.keyStoreAdmin=aws_cryptographic_material_providers \
+
+test_example_java:
+	$(GRADLEW) -p runtimes/java cleanTestExamples testExamples

AwsCryptographicMaterialProviders/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 0b153802b..56aef9ec6 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:

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.8.0.patch

@@ -0,0 +1,13 @@
+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
+@@ -794,7 +794,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()

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch → AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.8.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
+index 2804c8f21..868d600b3 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
+@@ -1875,7 +1875,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_AlreadyExistsConditionFailed dafnyVal:
+@@ -1910,7 +1910,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(

AwsCryptographicMaterialProviders/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: