chore(KSA-Model): more Mutation Operation changes (#955)

Explicitly:
- Change InitializeMutationFlag from a union to an enum for ToString reasons
- Model `DoNotVersion` flag for Initialize Mutation
- Refactor Describe Mutation output to detail Input so resume can be done
- Refactor System Key to be optional, detailing that TrustStorage is the default
- More errors
- Smithy changes from PR feedback on #854
- Correction of spelling mistakes
- Mutation Token's UUID is required

Why change the flag to an enum?

Dafny/Smithy-Dafny's support for Union's results in structures that do not print well.
The intention of the  `InitializeMutationFlag` is to inform customers
about the result of their request.

Such information may,
possibly even should,
be logged.

Initialize Mutation and Apply Mutation MUST
ensure that the UUID of the Index and Commitment agree.
Apply MUST ensure that the UUID of the Commitment and Token agree.
The Mutation Token's UUID is REQUIRED.
It is how we track a mutation,
much like how CFN tracks a change set.

Fixed bug where UUID is a reserved word in DDB.

Refactored some of the error messages.
Utilize Java Example to demonstrate resume and restart.
Finally, addressed some of the feedback on PR #854.

feat(Mutations): Idempotent Resume (#854)

Refactor Storage:
- Rename Mutation Lock to Mutation Commitment
- Introduce Mutation Index to describe what items of a Branch Key have been mutated
- Add Input field to Mutation Commitment
- Add Ciphertext field to Mutation Commitment
- When Mutating an item, always write with an optimistic lock
- Allow Initialize Mutation to over write a Version, instead of only creating a version
- When Overwriting a Mutation Index, ensure it has not changed
- Whenever writing for Mutation, ensure the Mutation Commitment's ENC is as expected (along with original and terminal)

Refactor Storage to contain operations that:
1. Allow for Atomic Mutations (maybe cut later)
2. Allow for Deleting a Mutation
3. Allow for Creating a Mutation Index

Refactor KeyStoreAdmin:
- Support a System Key for Mutations
- Stub out the System Key
- Logic for handling Mutation Index

Refactor Initialize Mutation:
- If Commitment & Index already exist and match Input, write nothing and return token
- If Commitment already exists and matches input, write index, and return token
- If Commitment already exists and does not match input, fail
- If no commitment, Initialize Mutation

Refactor Apply Mutation:
- Write an update Page Index.

fix: Dafny intendation formatting

chore: fix Java test examples

chore: more fomratting for CI

feat(Mutations): Native test for Loose access in-flight

feat(Mutations): Example In Flight Mutation Scanner

feat(Mutations-TODO): Some Terminal KMS Exceptions (#795)

If the KMS Call, for mutating the Beacon, fails,
it MAY indicate the MPL Consumer does not have access to the
terminal KMS Key.

If the KMS call for verifying a terminal version fails,
it MAY indicate the MPL Consumer does not have access to the
terminal KMS Key.

Also fix some Dafny tests failing verification.

feat(KS+): More modeled errors (#754)

* refactor(Storage): Use TransactGet instead of BatchGet for GetInitMut (#753)

This resolves feedback from both @seebees  and @josecorella
on Mutations branch.

* chore(Mutations): address #754\#discussion_r1775676091

#754 (comment)

* chore(Mutations): Address feedback from #750

See #750

* chore(Mutations): address feedback on #742

See #742

refactor(Storage): Use TransactGet instead of BatchGet for GetInitMut (#753)

This resolves feedback from both @seebees  and @josecorella
on Mutations branch.

Verification failure is due to (just like in #751 ):
1. Key Store Admin's Index.dfy not proving Fresh, which has been a long standing issue with the Admin
2. In `AwsCryptographyKeyStore/test/Storage/TestGetItemsForInitializeMutation.dfy`, the test assumes `type` is in the Encryption Context. It is, but Structure.dfy does not prove that, so it must be proven else where.

A .NET MPL job failed due to .NET 48 Sig V4 Auth bug.

test(Mutations): additional testing for Mutations

feat(Mutations): more clean up

feat(Mutations): log statements for ApplyMutation

fix(Storage): typo

fix(Storage): ensure KmsArn is valid

chore(Mutations): respond to comments on PR #720

test(GHW): Run Java Examples for PR CI (#749)

chore(Java): Examples for Mutations (#742)

chore(Mutations): comment out non-GA Mutations (#750)

Crypto Tools, at this time, intends to release Branch Key Mutations
without some operations useful for recovering a dropped Mutation Token
or dealing with the disagreement of a Mutation Token and a Mutation Lock.

Additionally,
we intend to release the Key Store Admin with only support for
one Key Management Strategy.

All checks are green except for Verification.
Verification is failing for the Key Store Admin's Index.dfy.

Verification for the Key Store Admin's Index.dfy
has been failing for a long time.

feat: Mutations BETA (#720)

Beta build of Mutations with several substantial gaps

Author: texastony

.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
@@ -69,7 +74,8 @@ jobs:
       # - pr-ci-go
       # - pr-ci-rust
       - pr-interop-test
-    runs-on: ubuntu-22.04
+      - pr-ci-examples
+    runs-on: ubuntu--22.04
     steps:
       - name: Verify all required jobs passed
         uses: re-actors/alls-green@release/v1

AwsCryptographicMaterialProviders/Makefile

@@ -8,10 +8,12 @@ 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
 
 MAIN_SERVICE_FOR_RUST := AwsCryptographicMaterialProviders
 
@@ -84,8 +86,15 @@ TRANSLATION_RECORD_GO := \
     ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
     AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
 
+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"
@@ -102,6 +111,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 {"
@@ -113,20 +130,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)
 
@@ -146,3 +167,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 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.2.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/AwsCryptographyKeyStore/dotnet/dafny-4.1.0.patch renamed to AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/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 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:

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 fa79a35cd..97802ad43 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
+@@ -963,7 +963,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: