try something to help with default values

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy

@@ -22,7 +22,7 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
     nameonly MutationToken: MutationToken ,
     nameonly PageSize: Option<int32> := Option.None ,
     nameonly Strategy: Option<KeyManagementStrategy> := Option.None ,
-    nameonly SystemKey: SystemKey
+    nameonly SystemKey: Option<SystemKey> := Option.None
   )
   datatype ApplyMutationOutput = | ApplyMutationOutput (
     nameonly MutationResult: ApplyMutationResult ,
@@ -44,18 +44,18 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
     nameonly Identifier: string
   )
   datatype DescribeMutationOutput = | DescribeMutationOutput (
-    nameonly Original: Option<MutableBranchKeyProperities> := Option.None ,
-    nameonly Terminal: Option<MutableBranchKeyProperities> := Option.None
+    nameonly MutationInFlight: MutationInFlight
   )
   datatype InitializeMutationFlag =
-    | Created(Created: string)
-    | Resumed(Resumed: string)
-    | ResumedWithoutIndex(ResumedWithoutIndex: string)
+    | Created
+    | Resumed
+    | ResumedWithoutIndex
   datatype InitializeMutationInput = | InitializeMutationInput (
     nameonly Identifier: string ,
     nameonly Mutations: Mutations ,
     nameonly Strategy: Option<KeyManagementStrategy> := Option.None ,
-    nameonly SystemKey: SystemKey
+    nameonly SystemKey: Option<SystemKey> := Option.None ,
+    nameonly DoNotVersion: Option<bool> := Option.None
   )
   datatype InitializeMutationOutput = | InitializeMutationOutput (
     nameonly MutationToken: MutationToken ,
@@ -204,6 +204,15 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
   datatype MutationComplete = | MutationComplete (
 
                               )
+  datatype MutationDescription = | MutationDescription (
+    nameonly Original: MutableBranchKeyProperities ,
+    nameonly Terminal: MutableBranchKeyProperities ,
+    nameonly Input: Mutations ,
+    nameonly SystemKey: Option<string> := Option.None
+  )
+  datatype MutationInFlight =
+    | Yes(Yes: MutationDescription)
+    | No(No: string)
   datatype Mutations = | Mutations (
     nameonly TerminalKmsArn: Option<string> := Option.None ,
     nameonly TerminalEncryptionContext: Option<AwsCryptographyKeyStoreTypes.EncryptionContextString> := Option.None
@@ -253,6 +262,9 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
     | UnexpectedStateException (
         nameonly message: string
       )
+    | UnsupportedFeatureException (
+        nameonly message: string
+      )
       // Any dependent models are listed here
     | AwsCryptographyKeyStore(AwsCryptographyKeyStore: AwsCryptographyKeyStoreTypes.Error)
     | ComAmazonawsDynamodb(ComAmazonawsDynamodb: ComAmazonawsDynamodbTypes.Error)

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy

@@ -46,15 +46,17 @@ service KeyStoreAdmin {
     DescribeMutation
   ],
   errors: [
-    KeyStoreAdminException,
-    MutationConflictException,
-    MutationInvalidException,
+    KeyStoreAdminException
+    MutationConflictException
+    MutationInvalidException
+    aws.cryptography.keyStore#KeyStorageException
     aws.cryptography.keyStore#VersionRaceException
     MutationLockInvalidException
     UnexpectedStateException
     MutationFromException
     MutationToException
     MutationVerificationException
+    UnsupportedFeatureException
   ]
 }
 
@@ -120,9 +122,11 @@ structure KmsAes {
 for non-cryptographic items.")
 structure TrustStorage {}
 
+// TODO: verify version before release
 @documentation(
 "Key Store Admin protects any non-cryptographic
-items stored with this Key.")
+items stored with this Key.
+As of v1.8.0, TrustStorage is the default behavior.")
 union SystemKey {
   kmsAes: KmsAes
   trustStorage: TrustStorage
@@ -172,6 +176,10 @@ Additionally create a Beacon Key that is tied to this Branch Key.")
 operation CreateKey {
   input: CreateKeyInput,
   output: CreateKeyOutput
+  errors: [
+    aws.cryptography.keyStore#KeyStorageException
+    KeyStoreAdminException
+  ]
 }
 
 structure CreateKeyInput {
@@ -208,7 +216,11 @@ structure CreateKeyOutput {
 operation VersionKey {
   input: VersionKeyInput,
   output: VersionKeyOutput,
-  errors: [aws.cryptography.keyStore#VersionRaceException]
+  errors: [
+    aws.cryptography.keyStore#VersionRaceException
+    aws.cryptography.keyStore#KeyStorageException
+    KeyStoreAdminException    
+  ]
 }
 
 
@@ -243,9 +255,11 @@ operation InitializeMutation {
     MutationConflictException
     MutationInvalidException
     aws.cryptography.keyStore#VersionRaceException
+    aws.cryptography.keyStore#KeyStorageException
     MutationVerificationException
     MutationToException
     MutationFromException
+    UnsupportedFeatureException
   ]
 }
 
@@ -261,8 +275,11 @@ structure InitializeMutationInput {
   @documentation("Optional. Defaults to reEncrypt with a default KMS Client.")
   Strategy: KeyManagementStrategy
 
-  @required
+  @documentation("Optional. Defaults to TrustStorage. See System Key.")
   SystemKey: SystemKey
+
+  @documentation("Optional. Defaults to False. As of v1.8.0, setting this true throws an exception.")
+  DoNotVersion: Boolean
 }
 
 structure MutationToken {
@@ -278,14 +295,20 @@ structure MutationToken {
   CreateTime: String
 }
 
-union InitializeMutationFlag {
-  @documentation("This is a new mutation.")
-  Created: String
-  @documentation("A matching mutation already existed.")
-  Resumed: String
-  @documentation("A matching mutation already existed, but no Page Index was found.")
-  ResumedWithoutIndex: String
-}
+@enum([
+  { // "This is a new mutation."
+    name: "Created",
+    value: "Created"
+  },
+  { // "A matching mutation already existed."
+    name: "Resumed",
+    value: "Resumed"
+  },
+  { // "A matching mutation already existed, but no Page Index was found."
+    name: "ResumedWithoutIndex",
+    value: "ResumedWithoutIndex"
+  }])
+string InitializeMutationFlag
 
 structure MutatedBranchKeyItem {
   @required
@@ -343,11 +366,13 @@ operation ApplyMutation {
   input:  ApplyMutationInput
   output: ApplyMutationOutput
   errors: [
+    aws.cryptography.keyStore#KeyStorageException
     MutationLockInvalidException
     UnexpectedStateException
     MutationVerificationException
     MutationToException
     MutationFromException
+    KeyStoreAdminException
   ]
 }
 
@@ -366,7 +391,7 @@ structure ApplyMutationInput {
   @documentation("Optional. Defaults to reEncrypt with a default KMS Client.")
   Strategy: KeyManagementStrategy
 
-  @required
+  @documentation("Optional. Defaults to TrustStorage. See System Key.")
   SystemKey: SystemKey
 }
 
@@ -407,6 +432,11 @@ If one exists, return a description of the mutation.")
 operation DescribeMutation {
   input:  DescribeMutationInput
   output: DescribeMutationOutput
+  errors: [
+    KeyStoreAdminException
+    aws.cryptography.keyStore#KeyStorageException
+    UnsupportedFeatureException
+  ]
 }
 
 structure DescribeMutationInput {
@@ -415,12 +445,29 @@ structure DescribeMutationInput {
   Identifier: String
 }
 
-structure DescribeMutationOutput {
+structure MutationDescription {
+  @required
   @documentation("The original properities of the Branch Key.")
   Original: MutableBranchKeyProperities
-
+  @required
   @documentation("The terminal properities of the Branch Key.")
   Terminal: MutableBranchKeyProperities
+  @required
+  @documentation("The input for this mutation.")
+  Input: Mutations
+  @documentation("String descprition of the System Key.")
+  SystemKey: String
+}
+
+@documentation("If a Mutation is In Flight for this Branch Key.")
+union MutationInFlight {
+  Yes: MutationDescription
+  No: String
+}
+
+structure DescribeMutationOutput {
+  @required
+  MutationInFlight: MutationInFlight
 }
 
 // Errors
@@ -511,3 +558,10 @@ structure MutationFromException {
   @required
   message: String,
 }
+
+@error("client")
+@documentation("This feature is not yet implemented.")
+structure UnsupportedFeatureException {
+  @required
+  message: String,
+}

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/AwsCryptographyKeyStoreAdminOperations.dfy

@@ -36,6 +36,20 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
   function {:opaque} MutationLie(): set<object>
   {{}}
 
+  function method DefaultSystemKey(
+    input: Option<Types.SystemKey> := None
+  ): (output: Types.SystemKey)
+  {
+    if input.None? then Types.SystemKey.trustStorage(TrustStorage()) else input.value
+  }
+
+  function method DefaultInitializeMutationDoNotVersion(
+    input: Option<bool> := None
+  ): (output: bool)
+  {
+    if input.None? then false else input.value
+  }
+
   function ModifiesInternalConfig(config: InternalConfig) : set<object>
   {
     config.storage.Modifies + MutationLie()
@@ -280,8 +294,18 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
     // See Smithy-Dafny : https://github.com/smithy-lang/smithy-dafny/pull/543
     assume {:axiom} keyManagerStrat.reEncrypt.kmsClient.Modifies < MutationLie();
 
-    var _ :- Mutations.ValidateInitializeMutationInput(input, config.logicalKeyStoreName);
-    output := Mutations.InitializeMutation(input, config.logicalKeyStoreName, keyManagerStrat, config.storage);
+    var internalInput := Mutations.InternalInitializeMutationInput(
+      Identifier := input.Identifier,
+      Mutations := input.Mutations,
+      SystemKey := DefaultSystemKey(input.SystemKey),
+      DoNotVersion := DefaultInitializeMutationDoNotVersion(input.DoNotVersion),
+      logicalKeyStoreName := config.logicalKeyStoreName,
+      keyManagerStrategy := keyManagerStrat,
+      storage := config.storage
+    );
+
+    var _ :- Mutations.ValidateInitializeMutationInput(internalInput);
+    output := Mutations.InitializeMutation(internalInput);
     return output;
   }