[darcs-users] If AB and B' are repos, does that imply A and B commute?

[Ben Franksen]

Am 21.11.20 um 20:39 schrieb James Cook:
> I've been trying to put together a proof, and ran into a strange
> example: what if AB and B' are both repositories, but A and B don't
> commute? I.e. A can only be applied if B hasn't been applied yet, but B
> doesn't depend on A.
> 
> My questions: Is this situation disallowed by some existing patch
> theory formalization? Is there a good reason to rule it out? Is it
> actually possible in Darcs? (I doubt the last one.)

TL;DR:

I don't believe that any existing text on patch theory has ever fully
formalized this requirement, but I may be wrong e.g. the camp paper may
have. (It's been quite a while since I last looked at the paper.)

There are very good reasons to rule this out, indeed it is essential to
do so, otherwise there is no point in naming primitive patches.

It is possible in Darcs, but only if you manually craft patches and not
with darcs commands, unless you are exceptionally unlucky ;-)

> As far as I can tell, the example is consistent with the patch theory
> axioms in [0] and [1]: we can simply say that in our patch theory,
> nothing ever commutes, and then the axioms don't have much to say.
> 
> The Camp theory pdf [2] makes a claim that seems to rule out the
> example: in section 8.1, "Merge preparation", it's asserted that as a
> first step toward merging two repos, we can move the common patches to
> the beginning. In this case, that would imply B can be moved to the
> beginning of the repo AB. However, I'm not sure where that's proved,
> and I also can't see why the above situation is inconsistent with the
> axioms in that write-up. (Admittedly, I haven't read it completely ---
> if someone can point me to the right parts, I'd appreciate it.)

The property you need to rule this out is a global one: you must assume
that each newly recorded patch has a universally unique name. The patch
laws are all local properties, so they cannot give you that.

Darcs tries to ensure this by adding a random number (taken from system
entropy i.e. cryptographically secure, as far as that is possible) to
the patch name when a patch is recorded (or amended etc). But it is
clear that this is no guarantee, since it cannot prevent someone from
manually creating a patch that has the same identity as a completely
unrelated patch somewhere else. If you pull such a patch, you repo
invariants are broken and you may get crashes (or worse: inconsistent
behavior).

This is a great, perhaps the greatest, weakness of patch theories a la
Darcs. We have discussed this at great length during the past years on
darcs-devel in varying contexts. It crops up again and again.

The reason we need this property is that we use patch names to calculate
equality of patch sequences. We assume that two sequences are equal (in
the usual sense i.e. modulo permutations) if their patch name sets are
equal. Indeed this is the only reason why we bother to name (primitive)
patches in the first place: it allows us to distinguish between
duplicate prims. The camp paper explains how patch names are used in the
merge algorithm to compute the common trunk, and it is easy to see that
this completely breaks down unless we assume universal uniqueness.

Concretely, if B and B' have the same name, we want to be able to
conclude that they have originally been the same patch. Formally this
means that (a) we can commute them to the same context (set of preceding
patches) and (b) that they will then be /structurally/ equal in any such
common context. In your scenario there obviously doesn't exist a common
context for B and B', so they cannot have the same name.

> In practice, I suspect it can't happen in Darcs, but I could imagine
> maybe someone would want a patch theory where it's possible. For
> example, maybe A reverses the order of lines in a file, and B deletes
> that file.

It is easy to see that this can't work if you study the details. In fact
I suspect that any such scenario will eventually lead to a violation of
permutivity (I don't have a proof though).

The more interesting question (for me) is how to detect violations of
name uniqueness when exchanging patches, so that (1) the user is warned
and can make an informed choice (e.g. not to trust either the remote or
their own repo), and (2) we can containsuch inconsistencies from spreading.

Cheers
Ben