[Simple-Model] Combine CosmosDB!WriteInit and CosmosDB!WriteInitToken

[lemmy]

In the simple model, writing to the database looks like this:

SomeAction ==
   /\ CosmosDB!WriteInit("k", "v")
   /\ token' = CosmosDB!WriteInitToken
   /\ ...

To make it explicit that WriteInitToken is the result of WriteInit, the following "API" would be more intuitive:

SomeAction ==
   /\ CosmosDB!WriteInit("k", "v", LAMBDA t: token' = t)

\* Def of WriteInit in CosmosDB.tla

WriteInitToken == [
    epoch |-> epoch,
    checkpoint |-> Len(log) + 1 \* checkpoint |-> Len(log')
]

WriteInit(key, value, Op(_)) ==
    /\ log' = Append(log, [
            key |-> key,
            value |-> value
       ])
    /\ Op(WriteInitToken)

---

Additionally, I propose to include the key and value in WriteInitToken to free a client spec of ComosDB.tla from manually keeping track of the relationship:

WriteInitToken(key, value) == [
    epoch |-> epoch,
    checkpoint |-> Len(log) + 1,
    key |-> key,
    value |-> value
]

\* This operator initiates a write, adding it to the log.
\* It is only useful alongside other constructs, such as:
\* - WritesAccepted
\* - WriteInitToken
WriteInit(key, value, Op(_)) ==
    /\ log' = Append(log, [
            key |-> key,
            value |-> value
       ])
    /\ Op(WriteInitToken(key, value))

SessionTokenIsValid(token) ==
    SessionTokenLEQ(token, WriteInitToken(token.key, token.value))

Client:

12FrontendWrite ==
    /\ future = Nil
    /\ \E r \in requests: DB!WriteInit(r.key, r.val, LAMBDA t: future' = t)
    /\ UNCHANGED <<dbVarsLog, requests, queue, backend>>

34FrontendEnqueue ==
    /\ future # Nil /\ DB!WriteSucceed(future)
    \* Make use of the key and value kept in the write token.
    /\ requests' = requests \ { [key |-> future.key, val |-> future.value ]}
    /\ queue' = Append(queue, [ k |-> future.key, t |-> future ])
    /\ future' = Nil
    /\ UNCHANGED <<dbVars, backend>>

/cc @fhackett