Model ledgerBranches sparsely.

[lemmy]

Refactor modeling of ledgerBranch[i] from seq into function.

[eddyashton]

We have this pattern in multiple places, can we pull it out and name it?

SparseLen(s) == Max(DOMAIN s \cup {0})

SparseAppend(s, e) == s @@ (SparseLen(s) + 1 :> e)

For the others that don't have multiple callers its less clear-cut, but maybe still more readable to introduce SparseSelectSeq and SparseSubSeq?

[achamayou]

Let's hold off until we have the trace validation matching to make changes to the model that directly help the trace validate.

[achamayou]

So interestingly, making the branches sparse may not be a the clear simplicity win I expected, because although it means we can probably remove BackfillLedgerBranch(es), it means that we can no longer call RwTxExecuteAction and IsRoTxResponseAction directly from the spec, and must replace them with copies that choose the txid instead.

With the dense models, we have to add two backfill actions, but every action from the trace can directly call its namesake in the spec.

[lemmy]

it means that we can no longer call RwTxExecuteAction and IsRoTxResponseAction directly from the spec, and must replace them with copies that choose the txid instead.

I don't understand what you mean by "choose the txid"? RoTxResponseAction already chooses the maximum tx_id in the branch. What would be the new predicate that you want to choose on?

[achamayou]

I don't understand what you mean by "choose the txid"?

I forgot we could use conditions on future states to constrain the state, so perhaps we could do:

IsRwTxExecuteAction ==
    /\ IsEvent("RwTxExecuteAction")
    \* Model action
    /\ RwTxExecuteAction
    \* Match message contents
    /\ Last(history').tx = logline.tx
    \* RwTxExecuteAction can only take place if a branch exists for the view
    \* If there is no branch, BackfillLedgerBranches will create the right amount of branches
    /\ Len(ledgerBranches) >= logline.tx_id[1]
    /\ logline.tx_id[2] \in DOMAIN ledgerBranches'[logline.tx_id[1]]

But that does not seem work.

RoTxResponseAction already chooses the maximum tx_id in the branch. What would be the new predicate that you want to choose on?

The framework exposes the KV read version, which is dependent on all previous transactions, not just transactions to that key. To match that, we either need to insert a single Tx at read versions, where they don't match one of the model's Tx (because it's a signature, some governance, yadda yadda), or modify the application code to return an applicative read version that's really the version of last previous write.

[achamayou]

Summary of discussion with @lemmy yesterday:

1. Selection of sparse transactions does not work because Execute is constrained to seqno + 1. This would need to be opened up in the action, and bounded in the MC through an action constraint, which the TV would not be subject to.
2. The branches backfill needs to stay in some form, as an equivalent to the rollback.
3. Either the Ro response needs to backfill one other OtherTxn just before it, to get the right read version, or we need to change the app to return an app-specific version-of-last-write as the read version.

For the time being, because the validation passes, this is not urgent.