Apply suggestions from code review

Co-authored-by: José Corella <[email protected]>
aws · Nov 7, 2024 · 0518af8 · 0518af8
1 parent d4ba279
commit 0518af8
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 13 deletions.
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/Storage.smithy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/Storage.smithy
@@ -138,14 +138,14 @@ structure MutationCommitment {
   Terminal: Blob
 
   @required
-  @documentation("Description of the input to Initizlize Mutation.")
+  @documentation("Description of the input to initialize a Mutation.")
   Input: Blob 
 
   @required
   CiphertextBlob: Blob
 }
 
-@documentation("Information on an in-flight Mutation of a Branch Key.")
+@documentation("Information of an in-flight Mutation of a Branch Key.")
 structure MutationIndex {
   @required
   @documentation("The Branch Key under Mutation.")
@@ -330,7 +330,7 @@ in the terminal state of a Mutation,
 a page of version (decrypt only) items,
 conditioned on:
 - every version already exsisting
-- every version's enc has not changed
+- every version's cipher-text had not changed
 - the Mutation Commitment has not changed
 ")
 operation WriteMutatedVersions {

diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy
@@ -542,7 +542,8 @@ module {:options "/functionSyntax:4" } CreateKeys {
     );
     var overWrite := Types.OverWriteEncryptedHierarchicalKey(
       Item := active,
-      Old := oldActiveItem);
+      Old := oldActiveItem
+    );
 
     var _ :- storage.WriteNewEncryptedBranchKeyVersion(
       Types.WriteNewEncryptedBranchKeyVersionInput(

diff --git a/...graphicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy b/...graphicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy
@@ -49,17 +49,11 @@ module DefaultKeyStorageInterface {
   // in the case statement to evaluate a literal.
   const MUTATION_COMMITMENT_TYPE := "branch:MUTATION_COMMITMENT" // Structure.MUTATION_COMMITMENT_TYPE
   const MUTATION_INDEX_TYPE := "branch:MUTATION_INDEX" // Structure.MUTATION_INDEX_TYPE
-  // const BRANCH_KEY_ACTIVE_TYPE := "branch:ACTIVE" // Structure.BRANCH_KEY_ACTIVE_TYPE
-  // const BEACON_KEY_TYPE_VALUE :=  "beacon:ACTIVE" // Structure.BEACON_KEY_TYPE_VALUE
-  // const VERSION_TYPE_PREFIX := "branch:version:" // Structure.BRANCH_KEY_TYPE_PREFIX
 
   lemma TypesAreCorrect()
     ensures
       && MUTATION_COMMITMENT_TYPE == Structure.MUTATION_COMMITMENT_TYPE
       && MUTATION_INDEX_TYPE == Structure.MUTATION_INDEX_TYPE
-    // && BRANCH_KEY_ACTIVE_TYPE == Structure.BRANCH_KEY_ACTIVE_TYPE
-    // && BEACON_KEY_TYPE_VALUE == Structure.BEACON_KEY_TYPE_VALUE
-    // && VERSION_TYPE_PREFIX == Structure.BRANCH_KEY_TYPE_PREFIX
   {}
 
   class {:termination false} DynamoDBKeyStorageInterface
@@ -560,12 +554,12 @@ module DefaultKeyStorageInterface {
         return Failure(
             Types.KeyStorageException(
               message :=
-                "DDB request to Write Mutated Versions was failed by DDB with TransactionCanceledException. "
+                "DDB request to Write Mutated Versions failed with DynamoDB's TransactionCanceledException. "
                 + "This MAY be caused by a race between hosts mutating the same Branch Key ID. "
                 + "The Mutation has NOT completed. "
                 + "Table Name: "+ ddbTableName
                 + "\tBranch Key ID: " + input.MutationCommitment.Identifier
-                + "\tDDB Exception Message: \n" + ddbResponse?.error.Message.UnwrapOr("")));
+                + "\tDynamoDB Exception Message: \n" + ddbResponse?.error.Message.UnwrapOr("")));
       }
       var ddbResponse :- ddbResponse?
       .MapFailure(

diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy b/...ptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy
@@ -218,7 +218,7 @@ structure VersionKeyInput {
   Identifier: String
 
   @required
-  @documentation("Multi-Region or Single Region AWS KMS Key used to protect the Branch Key, but not aliases!")
+  @documentation("Multi-Region or Single Region AWS KMS Key ARN used to protect the Branch Key, but not aliases!")
   KmsArn: KmsAesIdentifier
 
   Strategy: KeyManagementStrategy