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

Author: texastony

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/AwsCryptographyKeyStoreAdminOperations.dfy

@@ -204,7 +204,7 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
     return Success(internal);
   }
 
-  method ResolveHierarchyVersion(
+  method ResolveHierarchyVersionForCreateKey(
     hierarchyVersion?: Option<KeyStoreTypes.HierarchyVersion>,
     config: InternalConfig
   )
@@ -279,7 +279,7 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
     // See Smithy-Dafny : https://github.com/smithy-lang/smithy-dafny/pull/543
     assume {:axiom} legacyConfig.kmsClient.Modifies < MutationLie();
 
-    var hvInput :- ResolveHierarchyVersion(input.HierarchyVersion, config);
+    var hvInput :- ResolveHierarchyVersionForCreateKey(input.HierarchyVersion, config);
     :- Need(
       hvInput.v1?,
       Types.KeyStoreAdminException(message :="Only hierarchy-version-1 is supported at this time.")
@@ -349,11 +349,12 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
       Types.KeyStoreAdminException(message := "At this time, Mutations do not support KeyManagementStrategy#AwsKmsSimple.")
     );
 
-    var hvInput :- ResolveHierarchyVersion(input.Mutations.TerminalHierarchyVersion, config);
-    :- Need(
-      hvInput.v1?,
-      Types.KeyStoreAdminException(message :="Only hierarchy-version-1 is supported at this time.")
-    );
+    if (
+        && input.Mutations.TerminalHierarchyVersion.Some?
+        && input.Mutations.TerminalHierarchyVersion.value.v2?
+      ) {
+      return Failure(Types.KeyStoreAdminException(message :="At this time, Mutations do not support mutations to hierarchy-version-2."));
+    }
     var internalInput := KSAInitializeMutation.InternalInitializeMutationInput(
       Identifier := input.Identifier,
       Mutations := input.Mutations,

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/AdminFixtures.dfy

@@ -176,7 +176,7 @@ module {:options "/functionSyntax:4" } AdminFixtures {
     requires DDB.Types.IsValid_TableName(physicalName)
     requires UTF8.IsASCIIString(physicalName) && UTF8.IsASCIIString(logicalName)
     // Either the keyValue is NOT reserved, or this is violating a reserved attribute
-    requires !violateReservedAttribute || keyValue.key !in Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES
+    requires violateReservedAttribute || keyValue.key !in Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES
     requires DDB.Types.IsValid_AttributeName(keyValue.key)
     requires ddbClient?.Some? ==> ddbClient?.value.ValidState()
     modifies (if ddbClient?.Some? then ddbClient?.value.Modifies else {})
@@ -217,7 +217,7 @@ module {:options "/functionSyntax:4" } AdminFixtures {
     modifies kmsClient.Modifies
     ensures kmsClient.ValidState()
     // Either the keyValue is NOT reserved, or this is violating a reserved attribute
-    requires !violateReservedAttribute || keyValue.key !in Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES
+    requires violateReservedAttribute || keyValue.key !in Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES
     requires DDB.Types.IsValid_AttributeName(keyValue.key)
     requires DDB.Types.IsValid_TableName(physicalName)
   {