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

texastony · 2024-09-23T02:36:01Z

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

Verification failure is due to (just like in #751 ):

Key Store Admin's Index.dfy not proving Fresh, which has been a long standing issue with the Admin
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.

…ations

josecorella · 2024-09-24T22:29:01Z

...ptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy

-        itemIndex := 1 + itemIndex;
-      }
+      var lockItem: Option<Types.MutationLock> :-
+        MutationLockFromOptionalItem(ddbResponse.Responses.value[0].Item, input.Identifier);


imo; it is easier to reason about which response item you are handling if you break them out beforehand - it is more legible and I don't have to think too hard. future you would be thankful

var x := ddbResponse.Responses.value[0]; var y := ddbResponse.Responses.value[1]; ...

I can refactor this.
I even had it written this way,
but an earlier PR encouraged me to not have variables allocated that were not needed.

I took that feedback too far;
I agree that it would be a cleaner read to identify the three items.

Question: Is the cleanest implementation to assign each type an integer?

Because then we read:

MutationLockFromOptionalItem(ddbResponse.Responses.value[mLockIndex].Item, input.Identifier);

@seebees

…#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.

@seebees

…#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.

@seebees

* 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

@seebees

…#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.

@seebees

* 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

@seebees

…#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.

@seebees

* 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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

@seebees

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

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

9719343

…ations

texastony requested a review from a team as a code owner September 23, 2024 02:36

texastony had a problem deploying to Duvet CI September 23, 2024 02:36 — with GitHub Actions Failure

fix(Storage): .NET returns Some(empty map)

6d86551

texastony had a problem deploying to Duvet CI September 23, 2024 02:53 — with GitHub Actions Failure

fix(Storage): .NET returns Some(empty map)

333fa16

texastony had a problem deploying to Duvet CI September 23, 2024 03:02 — with GitHub Actions Failure

texastony merged commit 23bff65 into tony/test-mutations-java Sep 23, 2024
67 of 71 checks passed

texastony deleted the tony/refactor-storage-get-init-mut branch September 23, 2024 03:34

josecorella reviewed Sep 24, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

texastony commented Sep 23, 2024 •

edited

Loading

josecorella Sep 24, 2024

texastony Sep 25, 2024

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

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

Conversation

texastony commented Sep 23, 2024 • edited Loading

josecorella Sep 24, 2024

Choose a reason for hiding this comment

texastony Sep 25, 2024

Choose a reason for hiding this comment

texastony commented Sep 23, 2024 •

edited

Loading