Open lemmy opened 4 weeks ago
Let's hold off until we have the trace validation matching to make changes to the model that directly help the trace validate.
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.
it means that we can no longer call
RwTxExecuteAction
andIsRoTxResponseAction
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?
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 maximumtx_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.
Summary of discussion with @lemmy yesterday:
For the time being, because the validation passes, this is not urgent.
Refactor modeling of ledgerBranch[i] from seq into function.