feat(Mutations): Idempotent Resume #854

texastony · 2024-10-11T14:56:29Z

Issue #, if available:

Description of changes:
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:

Allow for Atomic Mutations (maybe cut later)
Allow for Deleting a Mutation
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.

Squash/merge commit message, if applicable:

feat(Mutations): Idempotent Resume

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

github-actions · 2024-10-31T21:47:53Z

Detected changes to the release files or to the check-files action

github-actions · 2024-10-31T21:47:54Z

Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy

github-actions · 2024-11-07T21:42:11Z

@texastony and @josecorella, I noticed you are updating the smithy model files.
Does this update need new or updated user documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

josecorella

looking good

github-actions · 2024-11-07T21:43:18Z

@texastony and @josecorella, I noticed you are updating the smithy model files.
Does this update need new or updated user documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

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

This reverts commit 82e501d.

github-actions · 2024-11-07T23:33:12Z

@texastony and @texastony, I noticed you are updating the smithy model files.
Does this update need new or updated user documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

github-actions · 2024-11-07T23:46:07Z

@texastony and @texastony, I noticed you are updating the smithy model files.
Does this update need new or updated user documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

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. Refactored some of the error messages. Utilize Java Example to demonstrate resume and restart. Finally, addressed some of the feedback on PR #854.

This reverts commit 4b54cbc. Instead, these suggestions were consumed in PR #955.

This reverts commit 620f96e. Instead, these suggestions were consumed in PR #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. Refactored some of the error messages. Utilize Java Example to demonstrate resume and restart. Finally, addressed some of the feedback on PR #854.

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.

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.

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.

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.

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.

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.

@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

texastony temporarily deployed to Duvet CI October 11, 2024 14:56 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 15, 2024 19:14 — with GitHub Actions Inactive

texastony force-pushed the tony/mutations-idempotent branch from 0fcd93a to 8e288a7 Compare October 15, 2024 19:16

texastony temporarily deployed to Duvet CI October 15, 2024 19:16 — with GitHub Actions Inactive

texastony force-pushed the tony/mutations-idempotent branch from 8e288a7 to d6ddff4 Compare October 17, 2024 16:10

texastony temporarily deployed to Duvet CI October 17, 2024 16:11 — with GitHub Actions Inactive

texastony force-pushed the tony/mutations-idempotent branch from d6ddff4 to 2578b47 Compare October 17, 2024 17:52

texastony temporarily deployed to Duvet CI October 17, 2024 17:52 — with GitHub Actions Inactive

texastony force-pushed the tony/mutations-idempotent branch from 2578b47 to ab94d23 Compare October 18, 2024 17:53

texastony temporarily deployed to Duvet CI October 18, 2024 17:53 — with GitHub Actions Inactive

texastony force-pushed the tony/mutations-idempotent branch from ab94d23 to cb41489 Compare October 18, 2024 17:54

texastony temporarily deployed to Duvet CI October 18, 2024 17:54 — with GitHub Actions Inactive

texastony marked this pull request as ready for review October 18, 2024 22:57

texastony requested a review from a team as a code owner October 18, 2024 22:57

texastony marked this pull request as draft October 18, 2024 22:57

texastony temporarily deployed to Duvet CI October 19, 2024 17:27 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 21, 2024 20:48 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 21, 2024 22:07 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 22, 2024 16:11 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 29, 2024 03:17 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 29, 2024 19:45 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 29, 2024 20:23 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 30, 2024 18:08 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 30, 2024 18:37 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 30, 2024 18:59 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 31, 2024 17:36 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 31, 2024 21:47 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI October 31, 2024 23:06 — with GitHub Actions Inactive

josecorella reviewed Nov 7, 2024

View reviewed changes

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy Show resolved Hide resolved

josecorella reviewed Nov 7, 2024

View reviewed changes

Revert "chore: non-breaking PR suggestions [skip ci]"

123f317

This reverts commit 82e501d.

texastony added 2 commits November 7, 2024 17:35

Revert "chore: non-breaking PR suggestions [skip ci]"

46e342b

This reverts commit 4b54cbc. Instead, these suggestions were consumed in PR #955.

Revert "chore: non-breaking PR suggestions [skip-ci] "

8159730

This reverts commit 620f96e. Instead, these suggestions were consumed in PR #955.

texastony temporarily deployed to Duvet CI November 8, 2024 01:38 — with GitHub Actions Inactive

texastony merged commit f6b42b9 into rc-1.8.0 Nov 8, 2024
95 checks passed

texastony deleted the tony/mutations-idempotent branch November 8, 2024 03:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Mutations): Idempotent Resume #854

feat(Mutations): Idempotent Resume #854

texastony commented Oct 11, 2024 •

edited

Loading

github-actions bot commented Oct 31, 2024

github-actions bot commented Oct 31, 2024

github-actions bot commented Nov 7, 2024

josecorella left a comment

github-actions bot commented Nov 7, 2024

github-actions bot commented Nov 7, 2024

github-actions bot commented Nov 7, 2024

feat(Mutations): Idempotent Resume #854

feat(Mutations): Idempotent Resume #854

Conversation

texastony commented Oct 11, 2024 • edited Loading

github-actions bot commented Oct 31, 2024

github-actions bot commented Oct 31, 2024

github-actions bot commented Nov 7, 2024

josecorella left a comment

Choose a reason for hiding this comment

github-actions bot commented Nov 7, 2024

github-actions bot commented Nov 7, 2024

github-actions bot commented Nov 7, 2024

texastony commented Oct 11, 2024 •

edited

Loading