chore(Mutations): PageIndex vs. ExclusiveStartKey

PageIndex is what is serialized to Storage.
ExclusiveStartKey is what the Storage interface uses in queries.

PageIndex can be:
- "Not Started", no versions have been mutated
- "branch:version:uuid", down to here have been mutated
- "Done", all versions have been mutated

ExclusiveStartKey can be:
- Not Set, no versions have been mutated
- Set and not blank, down to here have been mutated
- Set and blank, all versions have been mutated

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy

@@ -845,12 +845,12 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
   )
   type OverWriteEncryptedHierarchicalKeys = seq<OverWriteEncryptedHierarchicalKey>
   datatype QueryForVersionsInput = | QueryForVersionsInput (
-    nameonly PageIndex: Option<seq<uint8>> := Option.None ,
+    nameonly ExclusiveStartKey: Option<seq<uint8>> := Option.None ,
     nameonly Identifier: string ,
     nameonly PageSize: int32
   )
   datatype QueryForVersionsOutput = | QueryForVersionsOutput (
-    nameonly PageIndex: seq<uint8> ,
+    nameonly ExclusiveStartKey: seq<uint8> ,
     nameonly Items: EncryptedHierarchicalKeys
   )
   type Secret = seq<uint8>

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/Storage.smithy

@@ -491,7 +491,7 @@ structure QueryForVersionsInput {
   see Amazon DynamoDB's defination of exclusiveStartKey for details.
   Note: While the Default Storage is DDB,
   the Key Store transforms the exclusiveStartKey into an opaque representation.")
-  PageIndex: Blob
+  ExclusiveStartKey: Blob
   @required
   @documentation("The Identifier of the Branch Key.")
   Identifier: String
@@ -509,7 +509,7 @@ structure QueryForVersionsOutput {
   Note: While the Default Storage is DDB,
   the Key Store transforms the exclusiveStartKey into an opaque representation.")
   @required
-  PageIndex: Blob
+  ExclusiveStartKey: Blob
   @documentation("Up to pageSize list of version (decrypt only) items of a Branch Key.")
   @required
   Items: EncryptedHierarchicalKeys

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy

@@ -1189,9 +1189,9 @@ module DefaultKeyStorageInterface {
     {
       /** Construct & Issue DDB Request */
       var exclusiveStartKey: Option<DDB.Key> := None;
-      if (input.PageIndex.Some?) {
+      if (input.ExclusiveStartKey.Some?) {
         var decodedLastKey :- BlobToExclusiveStartKey(
-          input.PageIndex.value,
+          input.ExclusiveStartKey.value,
           input.Identifier);
         exclusiveStartKey := Some(decodedLastKey);
       }
@@ -1232,7 +1232,7 @@ module DefaultKeyStorageInterface {
       }
       if (ddbResponse.Items.None? || ( |ddbResponse.Items.value| == 0) ) {
         return Success(Types.QueryForVersionsOutput(
-                         PageIndex := lastKeyBlob,
+                         ExclusiveStartKey := lastKeyBlob,
                          Items := []
                        ));
       }
@@ -1256,7 +1256,7 @@ module DefaultKeyStorageInterface {
 
       return Success(
           Types.QueryForVersionsOutput(
-            PageIndex := lastKeyBlob,
+            ExclusiveStartKey := lastKeyBlob,
             Items := branchKeys
           ));
     }

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationStateStructures.dfy

@@ -65,9 +65,27 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
     Terminal: MutableProperties,
     CreateTime: string,
     ExclusiveStartKey: Option<seq<uint8>> := Option.None ,
-    UUID: Option<string> := Option.None
+    UUID: string
   )
 
+  /** The Lock & Index are persisted to the storage by Initialize. **/
+  /** The Lock & Index are read by Apply. **/
+  /** The Index is updated by Apply. **/
+  /** Both are deleted when the Mutation is completed by Apply. **/
+  datatype LockAndIndex = LockAndIndex(
+    Lock: KeyStoreTypes.MutationLock,
+    Index: KeyStoreTypes.MutationIndex
+  )
+  {
+    /** The Lock & Index MUST always have the same Identifier & UUID. **/
+    /** They MAY NOT have the same CreateTime. **/
+    ghost predicate ValidState()
+    {
+      && Lock.Identifier == Index.Identifier
+      && Lock.UUID == Index.UUID
+    }
+  }
+
   predicate MutationToApply?(MutationToApply: MutationToApply)
   {
     && KmsArn.ValidKmsArn?(MutationToApply.Original.kmsArn)
@@ -142,7 +160,7 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
 
   function SerializeMutableBranchKeyProperties(
     MutationToApply: MutationToApply
-  ): (output: Result<Types.MutationToken, Types.Error>)
+  ): (output: Result<KeyStoreTypes.MutationLock, Types.Error>)
     requires MutationToApply?(MutationToApply)
   {
     var OriginalJson
@@ -165,20 +183,27 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
     var terminalBytes :- JSON.Serialize(TerminalJson).MapFailure(
                            (e: JSONErrors.SerializationError)
                            => Types.KeyStoreAdminException(
-                               message := "Could not JSON Serialize state: terminal properties. " + e.ToString()));
-    Success(
-      Types.MutationToken(
-        Identifier := MutationToApply.Identifier,
-        Original := originalBytes,
-        Terminal := terminalBytes,
-        ExclusiveStartKey := MutationToApply.ExclusiveStartKey,
-        UUID := MutationToApply.UUID,
-        CreateTime := MutationToApply.CreateTime
-      ))
+                           message := "Could not JSON Serialize state: terminal properties. " + e.ToString()));
+    var lock := KeyStoreTypes.MutationLock(
+      Identifier := MutationToApply.Identifier,
+      Original := originalBytes,
+      Terminal := terminalBytes,
+      UUID := MutationToApply.UUID,
+      CreateTime := MutationToApply.CreateTime,
+      CiphertextBlob := [0] //TODO-Mutations-GA Wire up System Key
+    );
+    var index := KeyStoreTypes.MutationIndex(
+      Identifier := MutationToApply.Identifier,
+      PageIndex := MutationToApply.ExclusiveStartKey, //TONY This probably needs to optional... fudge. 
+      UUID := MutationToApply.UUID,
+      CreateTime := MutationToApply.CreateTime,
+      CiphertextBlob := [0] //TODO-Mutations-GA Wire up System Key
+    );
+    Success(LockAndIndex(lock, index))
   }
 
   function DeserializeMutationToken(
-    Token: Types.MutationToken
+    Token: KeyStoreTypes.MutationLock
   )
     : (output: Result<MutationToApply, Types.Error>)
     ensures output.Success? ==> MutationToApply?(output.value)
@@ -207,7 +232,7 @@ module {:options "/functionSyntax:4" } MutationStateStructures {
           kmsArn := TerminalJson.obj[1].1.str,
           customEncryptionContext := JSONToEncryptionContextString(TerminalJson.obj[0].1)
         ),
-        ExclusiveStartKey := Token.ExclusiveStartKey,
+        // ExclusiveStartKey := Token.ExclusiveStartKey,
         UUID := Token.UUID,
         CreateTime := Token.CreateTime
       ))

AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java

@@ -950,13 +950,13 @@ public static OverWriteEncryptedHierarchicalKey OverWriteEncryptedHierarchicalKe
   public static QueryForVersionsInput QueryForVersionsInput(
     software.amazon.cryptography.keystore.model.QueryForVersionsInput nativeValue
   ) {
-    Option<DafnySequence<? extends Byte>> pageIndex;
-    pageIndex =
-      Objects.nonNull(nativeValue.PageIndex())
+    Option<DafnySequence<? extends Byte>> exclusiveStartKey;
+    exclusiveStartKey =
+      Objects.nonNull(nativeValue.ExclusiveStartKey())
         ? Option.create_Some(
           DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(
-            nativeValue.PageIndex()
+            nativeValue.ExclusiveStartKey()
           )
         )
         : Option.create_None(
@@ -969,20 +969,20 @@ public static QueryForVersionsInput QueryForVersionsInput(
       );
     Integer pageSize;
     pageSize = (nativeValue.PageSize());
-    return new QueryForVersionsInput(pageIndex, identifier, pageSize);
+    return new QueryForVersionsInput(exclusiveStartKey, identifier, pageSize);
   }
 
   public static QueryForVersionsOutput QueryForVersionsOutput(
     software.amazon.cryptography.keystore.model.QueryForVersionsOutput nativeValue
   ) {
-    DafnySequence<? extends Byte> pageIndex;
-    pageIndex =
+    DafnySequence<? extends Byte> exclusiveStartKey;
+    exclusiveStartKey =
       software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(
-        nativeValue.PageIndex()
+        nativeValue.ExclusiveStartKey()
       );
     DafnySequence<? extends EncryptedHierarchicalKey> items;
     items = ToDafny.EncryptedHierarchicalKeys(nativeValue.Items());
-    return new QueryForVersionsOutput(pageIndex, items);
+    return new QueryForVersionsOutput(exclusiveStartKey, items);
   }
 
   public static UpdateMutationIndexInput UpdateMutationIndexInput(

AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToNative.java

@@ -953,10 +953,10 @@ public static QueryForVersionsInput QueryForVersionsInput(
   ) {
     QueryForVersionsInput.Builder nativeBuilder =
       QueryForVersionsInput.builder();
-    if (dafnyValue.dtor_PageIndex().is_Some()) {
-      nativeBuilder.PageIndex(
+    if (dafnyValue.dtor_ExclusiveStartKey().is_Some()) {
+      nativeBuilder.ExclusiveStartKey(
         software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(
-          dafnyValue.dtor_PageIndex().dtor_value()
+          dafnyValue.dtor_ExclusiveStartKey().dtor_value()
         )
       );
     }
@@ -974,9 +974,9 @@ public static QueryForVersionsOutput QueryForVersionsOutput(
   ) {
     QueryForVersionsOutput.Builder nativeBuilder =
       QueryForVersionsOutput.builder();
-    nativeBuilder.PageIndex(
+    nativeBuilder.ExclusiveStartKey(
       software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(
-        dafnyValue.dtor_PageIndex()
+        dafnyValue.dtor_ExclusiveStartKey()
       )
     );
     nativeBuilder.Items(

AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/QueryForVersionsInput.java

@@ -17,7 +17,7 @@ public class QueryForVersionsInput {
    *   Note: While the Default Storage is DDB,
    *   the Key Store transforms the exclusiveStartKey into an opaque representation.
    */
-  private final ByteBuffer PageIndex;
+  private final ByteBuffer ExclusiveStartKey;
 
   /**
    * The Identifier of the Branch Key.
@@ -30,7 +30,7 @@ public class QueryForVersionsInput {
   private final Integer PageSize;
 
   protected QueryForVersionsInput(BuilderImpl builder) {
-    this.PageIndex = builder.PageIndex();
+    this.ExclusiveStartKey = builder.ExclusiveStartKey();
     this.Identifier = builder.Identifier();
     this.PageSize = builder.PageSize();
   }
@@ -44,8 +44,8 @@ protected QueryForVersionsInput(BuilderImpl builder) {
    *   Note: While the Default Storage is DDB,
    *   the Key Store transforms the exclusiveStartKey into an opaque representation.
    */
-  public ByteBuffer PageIndex() {
-    return this.PageIndex;
+  public ByteBuffer ExclusiveStartKey() {
+    return this.ExclusiveStartKey;
   }
 
   /**
@@ -72,15 +72,15 @@ public static Builder builder() {
 
   public interface Builder {
     /**
-     * @param PageIndex Optional.
+     * @param ExclusiveStartKey Optional.
      *   If set, Query will start at this index and read forward.
      *   Otherwise, Query will start at the indexes begining.
      *   The Default Storage is DDB;
      *   see Amazon DynamoDB's defination of exclusiveStartKey for details.
      *   Note: While the Default Storage is DDB,
      *   the Key Store transforms the exclusiveStartKey into an opaque representation.
      */
-    Builder PageIndex(ByteBuffer PageIndex);
+    Builder ExclusiveStartKey(ByteBuffer ExclusiveStartKey);
 
     /**
      * @return Optional.
@@ -91,7 +91,7 @@ public interface Builder {
      *   Note: While the Default Storage is DDB,
      *   the Key Store transforms the exclusiveStartKey into an opaque representation.
      */
-    ByteBuffer PageIndex();
+    ByteBuffer ExclusiveStartKey();
 
     /**
      * @param Identifier The Identifier of the Branch Key.
@@ -118,7 +118,7 @@ public interface Builder {
 
   static class BuilderImpl implements Builder {
 
-    protected ByteBuffer PageIndex;
+    protected ByteBuffer ExclusiveStartKey;
 
     protected String Identifier;
 
@@ -127,18 +127,18 @@ static class BuilderImpl implements Builder {
     protected BuilderImpl() {}
 
     protected BuilderImpl(QueryForVersionsInput model) {
-      this.PageIndex = model.PageIndex();
+      this.ExclusiveStartKey = model.ExclusiveStartKey();
       this.Identifier = model.Identifier();
       this.PageSize = model.PageSize();
     }
 
-    public Builder PageIndex(ByteBuffer PageIndex) {
-      this.PageIndex = PageIndex;
+    public Builder ExclusiveStartKey(ByteBuffer ExclusiveStartKey) {
+      this.ExclusiveStartKey = ExclusiveStartKey;
       return this;
     }
 
-    public ByteBuffer PageIndex() {
-      return this.PageIndex;
+    public ByteBuffer ExclusiveStartKey() {
+      return this.ExclusiveStartKey;
     }
 
     public Builder Identifier(String Identifier) {