feat(BKS & BKSA): Smithy Model for HV-2 #1350

texastony · 2025-03-23T01:16:30Z

Issue #, if available:

Smithy Model for HV-2

Description of changes:

Smithy (link to only Smithy Changes):

new KeyManageStrat AwsKmsSimple that will, eventually, support everything; we need this for customers to have an "idempotent" code path that works for HV-1 or HV-2; neither of the current strategies "always" work for HV-1 & HV-2
Various documentation fix ups

Dafny/Behavior changes (link to only Dafny Changes)

These changes prevent the execution of behaviors that have not been implemented yet;
as #1349 and #1342 land, some of these behaviors will become enabled.

on VersionKey, if an HV-2 is encountered, fail
on ApplyMutation, if an HV-2 is encountered, fail
on BKSA CreateKey, if HV-2 is requested, fail
on BKSA Initialize Mutation, if TerminalHV is 2, fail
on BKSA Initialize Mutation, if KeyManageStrat is AwsKmsSimple, fail
on BKSA Apply Mutation, if KeyManageStrat is AwsKmsSimple, fail

Dafny proof changes (link to only Dafny Changes)

refactored KmsUtils.dfy#keyManagerStrat to consolidate Modify expressions
^ let me quickly wire up the new AwsKmsSimple
AND reject it for various places

Squash/merge commit message, if applicable:

feat(BKS & BKSA): Smithy Model for HV-2

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

… Mutation

…nKey & Mutation

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy

...rialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/KmsUtils.dfy

github-actions · 2025-03-25T18:41:25Z

@texastony and @imabhichow, 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 · 2025-03-25T19:00:26Z

@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 · 2025-03-25T19:04:02Z

@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 · 2025-03-25T19:04:46Z

@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?

...rs/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyKeyStoreAdminService/shim.go

github-actions · 2025-03-25T19:57:37Z

@texastony and @imabhichow, 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?

See: https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/428a013170894c4cc2ecb2ded2662fa1de1b065e/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy#L224-L229

rishav-karanjit · 2025-03-25T22:58:44Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy

@@ -56,8 +57,7 @@ service KeyStoreAdmin {
    aws.cryptography.keyStore#KeyStorageException,
    aws.cryptography.keyStore#VersionRaceException,
    aws.cryptography.keyStore#BranchKeyCiphertextException,
-    aws.cryptography.keyStore#AlreadyExistsConditionFailed,
-    aws.cryptography.keyStore#NoLongerExistsConditionFailed,


Is AlreadyExistsConditionFailed and NoLongerExistsConditionFailed not in use anywhere?

My code search in hv-2/hv-2 tells me: "No its not used"

github-actions · 2025-03-25T23:03:40Z

@texastony and @rishav-karanjit, 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?

texastony temporarily deployed to Duvet CI March 23, 2025 01:16 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 01:54 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 19:05 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 19:36 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 20:56 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 21:01 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 22:12 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 23, 2025 23:26 — with GitHub Actions Inactive

texastony temporarily deployed to Duvet CI March 24, 2025 15:18 — with GitHub Actions Inactive

texastony added 16 commits March 24, 2025 17:25

feat: Smithy Model for HV-2

443c850

chore: revise HV-2 Smithy for PR Feedback

720f939

fix: enum names must start with a letter

51affe7

fix: typo = -> :

962b5a4

chore(BKS): polymorph

42d09c5

fix: WIP but some dafny resolve and verify issues

d73d29b

fix(BKS): revise KeyMangStrat for HV-2 as well as some docs

8ef7906

chore(BKS): polymorph

50fd5bd

WIP: BKS has a rsrc exhaustion problem; BKSA has 18+ errors

ad15aa9

chore(BKSA-Dafny): kmsSimple wiring

7e97172

chore(BKSA-Dafny): super happy with this keyManStrat abstraction

f22ed66

chore(BKSA-Dafny): almost done with model stubbing

4a57f9b

chore(BKSA-Dafny): almost done with model stubbing

853c9f4

chore(BKSA-Dafny): until completion of M1, reject HV-2 on CreateKey &…

282a130

… Mutation

chore(BKS/A-Dafny): until later, src & tests to reject HV-2 on Versio…

cb9347b

…nKey & Mutation

fix(BKSA): Mutations MUST NOT default to HV-1

dc4c03f

texastony force-pushed the hv-2/smithy-model-fixes branch from 887f4ef to dc4c03f Compare March 25, 2025 00:26

texastony added 2 commits March 24, 2025 17:31

chore: update smithy-dafny reference

1de9f7a

chore: update smithy-dafny reference

c35b553

texastony changed the base branch from hv-2/smithy-model to hv-2/hv-2 March 25, 2025 00:42

texastony commented Mar 25, 2025

View reviewed changes

texastony added 2 commits March 24, 2025 17:49

fix(BKSA-Smithy): VersionKey does not take an HV

2537147

fix(BKSA-Smithy): VersionKey does not take an HV

023372f

texastony temporarily deployed to Duvet CI March 25, 2025 00:53 — with GitHub Actions Inactive

texastony marked this pull request as ready for review March 25, 2025 00:54

texastony requested a review from a team as a code owner March 25, 2025 00:54

fix(BKSA-Smithy): VersionKey does not take an HV

23cb34f

texastony temporarily deployed to Duvet CI March 25, 2025 03:57 — with GitHub Actions Inactive

imabhichow reviewed Mar 25, 2025

View reviewed changes

...rs/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyKeyStoreAdminService/shim.go Outdated Show resolved Hide resolved

texastony added 2 commits March 25, 2025 14:03

fix(BKSA-Smithy): spelling and TODOs

a6e7e4f

chore: re-poly MPL but not TV

d7abe22

texastony temporarily deployed to Duvet CI March 25, 2025 21:53 — with GitHub Actions Inactive

Merge branch 'hv-2/hv-2' into hv-2/smithy-model-fixes

79eff98

texastony temporarily deployed to Duvet CI March 25, 2025 22:15 — with GitHub Actions Inactive

fix(BKS-Dafny): follow @ajewellamz solution for fresh Modifies

ec66d8d

See: https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/428a013170894c4cc2ecb2ded2662fa1de1b065e/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy#L224-L229

texastony temporarily deployed to Duvet CI March 25, 2025 22:22 — with GitHub Actions Inactive

texastony changed the title ~~fix(BKS): revise KeyMangStrat for HV-2 as well as some docs~~ feat(BKS & BKSA): Smithy Model for HV-2 Mar 25, 2025

rishav-karanjit approved these changes Mar 25, 2025

View reviewed changes

rishav-karanjit merged commit 23bf9cd into hv-2/hv-2 Mar 25, 2025
137 checks passed

rishav-karanjit deleted the hv-2/smithy-model-fixes branch March 25, 2025 23:06

imabhichow pushed a commit that referenced this pull request Mar 26, 2025

feat(BKS & BKSA): Smithy Model for HV-2 (#1350)

de26534

imabhichow pushed a commit that referenced this pull request Apr 8, 2025

feat(BKS & BKSA): Smithy Model for HV-2 (#1350)

e0022b3

texastony added a commit that referenced this pull request Apr 9, 2025

feat(BKS & BKSA): Smithy Model for HV-2 (#1350)

768cdca

texastony added a commit that referenced this pull request Apr 9, 2025

feat(BKS & BKSA): Smithy Model for HV-2 (#1350)

ce3fa8b

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(BKS & BKSA): Smithy Model for HV-2 #1350

feat(BKS & BKSA): Smithy Model for HV-2 #1350

texastony commented Mar 23, 2025 •

edited

Loading

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

rishav-karanjit Mar 25, 2025

rishav-karanjit Mar 25, 2025

github-actions bot commented Mar 25, 2025

feat(BKS & BKSA): Smithy Model for HV-2 #1350

feat(BKS & BKSA): Smithy Model for HV-2 #1350

Conversation

texastony commented Mar 23, 2025 • edited Loading

Issue #, if available:

Description of changes:

Smithy (link to only Smithy Changes):

Dafny/Behavior changes (link to only Dafny Changes)

Dafny proof changes (link to only Dafny Changes)

Squash/merge commit message, if applicable:

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

github-actions bot commented Mar 25, 2025

rishav-karanjit Mar 25, 2025

Choose a reason for hiding this comment

rishav-karanjit Mar 25, 2025

Choose a reason for hiding this comment

github-actions bot commented Mar 25, 2025

texastony commented Mar 23, 2025 •

edited

Loading