Skip to content

Commit 0fb2be1

Browse files
committed
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
1 parent aebf397 commit 0fb2be1

File tree

237 files changed

+33350
-423
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

237 files changed

+33350
-423
lines changed
Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
# "Copyright Amazon.com Inc. or its affiliates. All Rights Reserved."
2+
# "SPDX-License-Identifier: CC-BY-SA-4.0"
3+
# This workflow runs any examples.
4+
name: Library Examples
5+
on:
6+
workflow_call:
7+
inputs:
8+
dafny:
9+
description: "The Dafny version to run"
10+
required: true
11+
type: string
12+
13+
jobs:
14+
java:
15+
runs-on: ubuntu-latest
16+
permissions:
17+
id-token: write
18+
contents: read
19+
defaults:
20+
run:
21+
shell: bash
22+
steps:
23+
- name: Support longpaths on Git checkout
24+
run: |
25+
git config --global core.longpaths true
26+
- name: Configure AWS Credentials for Tests
27+
uses: aws-actions/configure-aws-credentials@v4
28+
with:
29+
aws-region: us-west-2
30+
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
31+
role-session-name: JavaExampleTests
32+
33+
- uses: actions/checkout@v4
34+
- run: git submodule update --init libraries
35+
- run: git submodule update --init smithy-dafny
36+
37+
- name: Setup Dafny
38+
uses: dafny-lang/[email protected]
39+
with:
40+
dafny-version: ${{ inputs.dafny }}
41+
42+
- name: Setup Java 8
43+
uses: actions/setup-java@v3
44+
with:
45+
distribution: "corretto"
46+
java-version: 8
47+
48+
- name: Build AwsCryptographicMaterialProviders Java implementation
49+
working-directory: ./AwsCryptographicMaterialProviders
50+
run: |
51+
# This works because `node` is installed by default on GHA runners
52+
CORES=$(node -e 'console.log(os.cpus().length)')
53+
make build_java CORES=$CORES
54+
55+
- name: Test AwsCryptographicMaterialProviders Java Examples
56+
working-directory: ./AwsCryptographicMaterialProviders
57+
run: |
58+
make test_example_java

.github/workflows/pull.yml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,11 @@ jobs:
2929
uses: ./.github/workflows/library_java_tests.yml
3030
with:
3131
dafny: ${{needs.getVersion.outputs.version}}
32+
pr-ci-examples:
33+
needs: getVersion
34+
uses: ./.github/workflows/library_examples.yml
35+
with:
36+
dafny: ${{needs.getVersion.outputs.version}}
3237
pr-ci-net:
3338
needs: getVersion
3439
uses: ./.github/workflows/library_net_tests.yml
@@ -65,6 +70,7 @@ jobs:
6570
- pr-ci-java
6671
- pr-ci-net
6772
- pr-interop-test
73+
- pr-ci-examples
6874
runs-on: ubuntu-latest
6975
steps:
7076
- name: Verify all required jobs passed

AwsCryptographicMaterialProviders/Makefile

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,12 @@ include ../SharedMakefileV2.mk
99

1010
PROJECT_SERVICES := \
1111
AwsCryptographyKeyStore \
12-
AwsCryptographicMaterialProviders \
12+
AwsCryptographyKeyStoreAdmin \
13+
AwsCryptographicMaterialProviders
1314

1415
SERVICE_NAMESPACE_AwsCryptographicMaterialProviders=aws.cryptography.materialProviders
1516
SERVICE_NAMESPACE_AwsCryptographyKeyStore=aws.cryptography.keyStore
17+
SERVICE_NAMESPACE_AwsCryptographyKeyStoreAdmin=aws.cryptography.keyStoreAdmin
1618

1719
MAIN_SERVICE_FOR_RUST := AwsCryptographicMaterialProviders
1820

@@ -68,8 +70,15 @@ SERVICE_DEPS_AwsCryptographyKeyStore := \
6870
ComAmazonawsDynamodb \
6971
AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
7072

73+
SERVICE_DEPS_AwsCryptographyKeyStoreAdmin := \
74+
AwsCryptographyPrimitives \
75+
ComAmazonawsKms \
76+
ComAmazonawsDynamodb \
77+
AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
78+
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
7179
# Constants for languages that drop extern names (Python, Go)
7280

81+
7382
MPL_CORE_TYPES_FILE_PATH=dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
7483
MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.materialproviders.internaldafny.types\" } AwsCryptographyMaterialProvidersTypes"
7584
MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyMaterialProvidersTypes"
@@ -86,6 +95,14 @@ KEYSTORE_INDEX_FILE_PATH=dafny/AwsCryptographyKeyStore/src/Index.dfy
8695
KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystore.internaldafny\"} KeyStore refines AbstractAwsCryptographyKeyStoreService"
8796
KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING="module KeyStore refines AbstractAwsCryptographyKeyStoreService"
8897

98+
KEYSTORE_ADMIN_TYPES_FILE_PATH=dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
99+
KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystoreadmin.internaldafny.types\" } AwsCryptographyKeyStoreAdminTypes"
100+
KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyKeyStoreAdminTypes"
101+
102+
KEYSTORE_ADMIN_INDEX_FILE_PATH=dafny/AwsCryptographyKeyStoreAdmin/src/Index.dfy
103+
KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystoreadmin.internaldafny\"} KeyStoreAdmin refines AbstractAwsCryptographyKeyStoreAdminService"
104+
KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING="module KeyStoreAdmin refines AbstractAwsCryptographyKeyStoreAdminService"
105+
89106
SYNCHRONIZED_LOCAL_CMC_FILE_PATH=dafny/AwsCryptographicMaterialProviders/src/CMCs/SynchronizedLocalCMC.dfy
90107
SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } {:extern \"software.amazon.cryptography.internaldafny.SynchronizedLocalCMC\" } SynchronizedLocalCMC {"
91108
SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } SynchronizedLocalCMC {"
@@ -97,20 +114,24 @@ STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\
97114
_sed_types_file_remove_extern:
98115
$(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)
99116
$(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)
117+
$(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)
100118

101119
_sed_index_file_remove_extern:
102120
$(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)
103121
$(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)
122+
$(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)
104123
$(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)
105124
$(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)
106125

107126
_sed_types_file_add_extern:
108127
$(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)
109128
$(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)
129+
$(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)
110130

111131
_sed_index_file_add_extern:
112132
$(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)
113133
$(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)
134+
$(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)
114135
$(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)
115136
$(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)
116137

@@ -130,3 +151,7 @@ PYTHON_DEPENDENCY_MODULE_NAMES := \
130151
--dependency-library-name=com.amazonaws.dynamodb=aws_cryptography_internal_dynamodb \
131152
--dependency-library-name=aws.cryptography.materialProviders=aws_cryptographic_material_providers \
132153
--dependency-library-name=aws.cryptography.keyStore=aws_cryptographic_material_providers \
154+
--dependency-library-name=aws.cryptography.keyStoreAdmin=aws_cryptographic_material_providers \
155+
156+
test_example_java:
157+
$(GRADLEW) -p runtimes/java testExamples
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
2+
index 0b153802b..56aef9ec6 100644
3+
--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
4+
+++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
5+
@@ -3903,7 +3903,9 @@ namespace AWS.Cryptography.MaterialProviders
6+
dafnyVal._ComAmazonawsDynamodb
7+
);
8+
case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
9+
- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
10+
+ // BEGIN MANUAL EDIT
11+
+ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
12+
+ // END MANUAL EDIT
13+
dafnyVal._ComAmazonawsKms
14+
);
15+
case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal:
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
2+
index 5764797e..4310b660 100644
3+
--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
4+
+++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
5+
@@ -794,7 +794,7 @@ abstract module AbstractAwsCryptographyKeyStoreService
6+
import opened Types = AwsCryptographyKeyStoreTypes
7+
import Operations : AbstractAwsCryptographyKeyStoreOperations
8+
function method DefaultKeyStoreConfig(): KeyStoreConfig
9+
- method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
10+
+ method {:vcs_split_on_every_assert} {:rlimit 90500000} KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
11+
returns (res: Result<KeyStoreClient, Error>)
12+
requires config.ddbClient.Some? ==>
13+
config.ddbClient.value.ValidState()

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch

Lines changed: 0 additions & 26 deletions
This file was deleted.
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,22 @@
11
diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
2-
index f5ef0458..f846a946 100644
2+
index 2804c8f21..868d600b3 100644
33
--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
44
+++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs
5-
@@ -629,7 +629,9 @@ namespace AWS.Cryptography.KeyStore
5+
@@ -1875,7 +1875,7 @@ namespace AWS.Cryptography.KeyStore
66
dafnyVal._ComAmazonawsDynamodb
77
);
88
case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
99
- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
10-
+ // BEGIN MANUAL EDIT
11-
+ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
12-
+ // END MANUAL EDIT
10+
+ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( // Manual edit KMS. -> Kms.
1311
dafnyVal._ComAmazonawsKms
1412
);
15-
case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal:
16-
@@ -652,7 +654,9 @@ namespace AWS.Cryptography.KeyStore
13+
case software.amazon.cryptography.keystore.internaldafny.types.Error_AlreadyExistsConditionFailed dafnyVal:
14+
@@ -1910,7 +1910,7 @@ namespace AWS.Cryptography.KeyStore
1715
{
1816
case "Com.Amazonaws.KMS":
1917
return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsKms(
2018
- Com.Amazonaws.KMS.TypeConversion.ToDafny_CommonError(value)
21-
+ // BEGIN MANUAL EDIT
22-
+ Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value)
23-
+ // END MANUAL EDIT
19+
+ Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value) // Manual edit KMS. -> Kms.
2420
);
2521
case "Com.Amazonaws.Dynamodb":
2622
return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsDynamodb(
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
2+
index 2122e39c..2d12b29f 100644
3+
--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
4+
+++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
5+
@@ -833,7 +833,8 @@ namespace AWS.Cryptography.KeyStoreAdmin
6+
dafnyVal._ComAmazonawsDynamodb
7+
);
8+
case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
9+
- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
10+
+ // MANUAL EDIT KMS -> Kms
11+
+ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
12+
dafnyVal._ComAmazonawsKms
13+
);
14+
case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_KeyStoreAdminException dafnyVal:
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
2+
index fa79a35cd..97802ad43 100644
3+
--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
4+
+++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStoreAdmin/TypeConversion.cs
5+
@@ -963,7 +963,8 @@ namespace AWS.Cryptography.KeyStoreAdmin
6+
dafnyVal._ComAmazonawsDynamodb
7+
);
8+
case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
9+
- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
10+
+ // MANUAL EDIT KMS -> Kms
11+
+ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
12+
dafnyVal._ComAmazonawsKms
13+
);
14+
case software.amazon.cryptography.keystoreadmin.internaldafny.types.Error_KeyStoreAdminException dafnyVal:

0 commit comments

Comments
 (0)