https://github.com/prismlab/certified-mrdts/blob/92570b7444e9f921b9a801e71727b85ba78f3906/icounter.fst#L50
Choosing the id as 0 will cause issues I think. But we can handle that later. I added the id because structural equality alone is not sufficient.
Without some id, the history on the left would be isomorphic to the history on the right. Merging the two 5s on the left does not preserve the intent. Choosing 0 all the time may cause problems later. We can come back to this later.
I’m assuming that every operation introduces a unique id. This is not enforced in the well-formedness condition. Essentially, you want to say in the well-formedness that every sub-history of a well-formed history has a unique id.
It would be easy to express this in a tree, but the history being a DAG introduces some trickiness. For example, we can’t just claim that all the sub-histories have unique id since we can have two different immediate children point to the same history due to merge. Not insurmountable, but a little more than what I could do the other day.
https://github.com/prismlab/certified-mrdts/blob/92570b7444e9f921b9a801e71727b85ba78f3906/icounter.fst#L50
Choosing the id as 0 will cause issues I think. But we can handle that later. I added the id because structural equality alone is not sufficient.
Without some id, the history on the left would be isomorphic to the history on the right. Merging the two 5s on the left does not preserve the intent. Choosing 0 all the time may cause problems later. We can come back to this later.
I’m assuming that every operation introduces a unique id. This is not enforced in the well-formedness condition. Essentially, you want to say in the well-formedness that every sub-history of a well-formed history has a unique id.
It would be easy to express this in a tree, but the history being a DAG introduces some trickiness. For example, we can’t just claim that all the sub-histories have unique id since we can have two different immediate children point to the same history due to merge. Not insurmountable, but a little more than what I could do the other day.