Not self-accepting even though these are only comments; it would be cool if
someone double-checks that the proofs are correct.

1 patch for repository http://darcs.net/screened:

patch cd1d4ea4c5589c6f47d83b96e411ec51c1924d1f
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Jun  9 00:07:35 CEST 2023
  * add proofs of impossibility for all error cases in V3.Core

Attachments

• add-proofs-of-impossibility-for-all-error-cases-in-v3_core.dpatch
• patch-preview.txt

Reviewing these proofs slowly...

> (2) If v depends on u and p conflicts with u then it also conflicts
> with v.

I actually have trouble understanding what this means: my intuitive
definition of "p conflicts with u" is that `merge (p :\/: u) == Nothing`.
But in this scenario we can't even construct `p :\/: v`.

> merge (lhs@(Conflictor com_r x cp) :\/: rhs@(Conflictor com_s y cq)) =
>   case findCommonFL com_r com_s of
>     Fork _ r s ->
>       case cleanMerge (r :\/: s) of
>         Nothing ->
>           -- Proof that this is impossible:

I believe this one.

> -- similar to above case: a prim and a conflictor that conflicts with the prim
> -- but also conflicts with other patches
> -- [p] :> [p^ s, {s^:p} U Y, cq] <-> [s, Y, cq] :> [, {cq}, s^:p]
> commuteConflicting (Prim p :> Conflictor s y cq)
>   | ident p `S.member` S.map ctxId y =
>       case fastRemoveFL (invert p) s of
>         Nothing ->
>           -- Proof that this is impossible:
>           --
>           -- The case assumption (that p is in conflict with q) together
>           -- with the fact that the rhs is obviously the first patch that
>           -- conflicts with the lhs, imply that p^ is contained in s. It
>           -- remains to be shown that p^ does not depend on any prim contained
>           -- in s. Suppose there were such a prim, then p would be in conflict
>           -- with it, which means p would have to be a conflictor. QED

FWIW I found this slightly harder to read because of a notational inconsistency between
the code and the comment just above the code: in the comment p^ is not part of s,
but in the code p^ is part of s (as we have to remove it).

Coming back to the proof and expanding out the final bits of the argument a bit:

"It remains to be shown that p^ does not depend on any prim r^ contained in s.
Suppose there were such a prim, then p and r^ would be in conflict, as r^p^
wouldn't commute."

However r^ is the inverse of a prim r somewhere in the history of the repo, whereas
p is a prim directly in the history of the repo, so I can't quite get from the
statement that they are in conflict to "p would have to be a conflictor".

I can convince myself with the following slightly stronger statement about
invariants:

If we take the effect of a conflictor, then let rs = the inverse of that effect, i.e. the
patches the conflictor reverts. If we let cs = the the unconflicted prims in the context
of that conflictor, then we can commute cs so that rs is a suffix of it.

Given that statement, the appearance of r^p^ in s with p^ depending on r^ implies
that the unconflicted prims in the context contain pr where r depends on p. But then
the commute we are trying to do is impossible because r would be stuck inbetween p and
the conflictor.

> -- if we have two conflictors where the rhs conflicts /only/ with the lhs,
> -- the latter becomes a prim patch
> -- [r, X, cp] [, {cp}, r^:q] <-> [q] [q^r, {r^:q} U X, cp]
> commuteConflicting (lhs@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
>   | y == S.singleton cp =
>       case ctxView (ctxAddFL r cq) of
>         Sealed (NilFL :> q') -> [...]
>         Sealed (c' :> _) ->
>           -- Proof that this is impossible:
>           --
>           -- First, it must be true that commutePastFL r cq = Just cq'. For if
>           -- not, then there would be a conflict between the rhs and one of the
>           -- prims that the lhs reverts, in contradiction to our case
>           -- assumption that the rhs conflicts only with the lhs.
>           --
>           -- Second, suppose that cq' has residual nonempty context. That means
>           -- there is a patch x in the history that the rhs depends on, and
>           -- which is in conflict with at least one other patch y in our
>           -- history (the history being the patches that precede the lhs);
>           -- because otherwise cq' appended to the history would be a sequence
>           -- that contains x twice without an intermediate revert. But then the
>           -- rhs would also have to conflict with the patch x, again in
>           -- contradiction to our case assumption. QED

I roughly get the argument here, but I'm having trouble following it precisely.

I think it'd help if you used the same functions in the proof as in the logic:
how does commutePastFL relate to ctxAddFL? And is that definitely what you meant,
don't we actually expect the inverse-cancellation logic of ctxAdd to kick in?

Also is it meaningful to talk both about the rhs depending on x and being in
conflict with it? (this partly goes back to my earlier comment about
what being in conflict really means)

>> (2) If v depends on u and p conflicts with u then it also conflicts
>> with v.
> 
> I actually have trouble understanding what this means: my intuitive
> definition of "p conflicts with u" is that `merge (p :\/: u) == Nothing`.

More precisely it means that `cleanMerge (p :\/: u) == Nothing`.

> But in this scenario we can't even construct `p :\/: v`.

True. In this formulation I (sloppily) identify nominally equal patches. Formally, we can

  merge (p :\/: u) = u' :/\: p'

and then

  cleanMerge (p' :\/: v)

should fail if

  cleanMerge (p :\/: u)

fails. The sloppy formulation can be excused on the ground that commutation (or merge) 
never changes whether patches commute, which is the identity law we discussed lately.

> FWIW I found this slightly harder to read because of a notational inconsistency between
> the code and the comment just above the code: in the comment p^ is not part of s,
> but in the code p^ is part of s (as we have to remove it).

Ah, yes. In the proofs I used the notation from the code, not the older comments above, 
which I had more or less copied from the paper (modulo some renamings) back when I wrote 
this code. Perhaps I should delete these older "pseudo-formal" comments, the more so since 
their notation is also borrowed from the paper and that notation is nowhere explained in 
the module.

> Coming back to the proof and expanding out the final bits of the argument a bit:
> 
> "It remains to be shown that p^ does not depend on any prim r^ contained in s.
> Suppose there were such a prim, then p and r^ would be in conflict, as r^p^
> wouldn't commute."

I like your formulation that gives an explicit name to the supposedly existing prim in s. 
My formulation is unclear because it doesn't clearly distinguish between r and r^.

> However r^ is the inverse of a prim r somewhere in the history of the repo, whereas
> p is a prim directly in the history of the repo, so I can't quite get from the
> statement that they are in conflict to "p would have to be a conflictor".

The fact that the lhs is a Prim (capital case i.e. not a Conflictor) means that p cannot be 
in conflict with any patch preceding it. I think that's plainly obvious, or isn't it?

>> commuteConflicting (lhs@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
>>    | y == S.singleton cp =
>>        case ctxView (ctxAddFL r cq) of
>>          Sealed (NilFL :> q') -> [...]
>>          Sealed (c' :> _) ->
>>            -- Proof that this is impossible:
>>            --
>>            -- First, it must be true that commutePastFL r cq = Just cq'. For if
>>            -- not, then there would be a conflict between the rhs and one of the
>>            -- prims that the lhs reverts, in contradiction to our case
>>            -- assumption that the rhs conflicts only with the lhs.
>>            --
>>            -- Second, suppose that cq' has residual nonempty context. That means
>>            -- there is a patch x in the history that the rhs depends on, and
>>            -- which is in conflict with at least one other patch y in our
>>            -- history (the history being the patches that precede the lhs);
>>            -- because otherwise cq' appended to the history would be a sequence
>>            -- that contains x twice without an intermediate revert. But then the
>>            -- rhs would also have to conflict with the patch x, again in
>>            -- contradiction to our case assumption. QED
> 
> I roughly get the argument here, but I'm having trouble following it precisely.

This is the most difficult proof and it's not easy to follow.

> I think it'd help if you used the same functions in the proof as in the logic:
> how does commutePastFL relate to ctxAddFL?

I used a fact about Contexted that is not explicitly stated anywhere, but obvious from the 
definition of ctxAdd, namely

 (*) commutePast r cq = Just cq' => ctxAdd r cq = cq'

We want to prove that the context in (ctxAddFL r cq) is empty. What I show is that 
(commutePast r cq) succeeds and its result has empty context. Together with (*) this implies 
that the context in (ctxAddFL r cq) is empty.

> And is that definitely what you meant,
> don't we actually expect the inverse-cancellation logic of ctxAdd to kick in?

No; if my argument in the first paragraph of the proof convinces you, then inverses of prims 
in r cannot be in the context of cq.

> Also is it meaningful to talk both about the rhs depending on x and being in
> conflict with it? (this partly goes back to my earlier comment about
> what being in conflict really means)

Thanks for pointing that out. Indeed I made two mistakes here. First I re-used the variables x 
and y for new things, which is bad. Let us use u and v instead. The second mistake was that in 
the last sentence I should have said "y" instead of "x".

The point is that something (say, u) can be in the context of cq only if it previously got 
reverted by a conflictor. That is, we must have a situation like this:

  u ... (conflictor (...u^...) _ (... : v)) ... lhs rhs@(Conflictor _ _ cq@(...u... : q))

Now, u being in the context of q means that q depends on u. So, by our invariant (2), v (which 
conflicts with u) must also conflict with q, in contradiction to the case assumption that q 
only conflicts with p.

The problem I have with your definition of "conflict" is that it
is based on some notion of repo patches rather than prim patches.
Granted, all valid implementations should behave in the way you
describe, but it's still quite circular. Plus the distinction
between merge and cleanMerge adds extra complexity.

In addition, the constituent parts of a RepoPatchV3 are all prim 
patches, so it's weird to be talking about properties that only
make sense when they are lifted into repo patches.

[mismatch between notation and code]
> Ah, yes. In the proofs I used the notation from the code, not
> the older comments above, which I had more or less copied from
> the paper (modulo some renamings) back when I wrote this code.
> Perhaps I should delete these older "pseudo-formal" comments,
> the more so since their notation is also borrowed from the paper
> and that notation is nowhere explained in the module.

I found that reading the comments helped quite a bit even with the
mismatches, so I'd like to keep them.

> > Suppose there were such a prim, then p and r^ would be in
> > conflict, [...]

> > However r^ is the inverse of a prim r somewhere in the
> > history of the repo, whereas p is a prim directly in the
> > history of the repo, so I can't quite get from the
> > statement that they are in conflict to "p would have to
> > be a conflictor".

> The fact that the lhs is a Prim (capital case i.e. not a
> Conflictor) means that p cannot be in conflict with any patch
> preceding it. I think that's plainly obvious, or isn't it?

But r^ isn't even in the repo so can't precede p in the repo.
My alternative argument doesn't talk about conflicts, it actually
talks about dependencies.

The problem I have with your formulation of the invariant (2) is that it is 
a "global" property of all patches in the context of a conflictor i.e. that 
they can be reordered in a certain way. That means it is hard to see that we 
actually maintain it when constructing new Conflictors, which makes it 
useless in practice.

Instead, let me re-phrase my invariant (2) to avoid any circularity:

First, generalize the definition(!) of "conflicts with" for (named) prims: 
if p conflicts with u, and v depends on u, then we say that p also conflicts 
with v. It follows from permutivity that this generalized definition is 
commutation invariant and is therefore a property that depends only on the identity of the prims involved.

The invariant now says: if both (Prim u) and (Prim v) are present in the 
history of (i.e. the context preceding) the conflictor representing p, then the latter must have a contexted prim (...u... : v') as a member of its "set 
of conflicts", where ident v' == indent v.

In other words, the "set of conflicts" in a Conflictor representing p 
/indeed/ contains all prims (in Contexted form) that are in its context and 
that p conflicts with. Formally: for every RepoPatch Q representing q in the 
context of a (Conflictor _ x _) representing p we have

  ident q `S.member` S.map ctxId x == "p conflicts with q"

in the generalized sense of "conflicts with" defined above.

It is now easy to systematically check that whenever we construct a new 
Conflictor we maintain this invariant.

I'll keep working through your comments, but if possible when you have a chance
could you turn your changes to the proofs into new draft patch? It'll make
it easier for me to re-read the updated argument in its entirety.

> The problem I have with your formulation of the invariant (2) is that it is 
> a "global" property of all patches in the context of a conflictor i.e. that 
> they can be reordered in a certain way. That means it is hard to see that we 
> actually maintain it when constructing new Conflictors, which makes it 
> useless in practice.

Here's a rough sketch of what I intuitively had in mind. Re-quoting the invariant:

> If we take the effect of a conflictor, then let rs = the inverse of that effect,
> i.e. the patches the conflictor reverts. If we let cs = the unconflicted 
> prims in the context of that conflictor, then we can commute cs so that rs
> is a suffix of it.

Let's assume that the invariant already holds for all Conflictors in a repo.
Essentially the idea is that whenever we do an operation that might touch cs
or rs for a particular Conflictor, the nature of the changes we make also
guarantee that the "can commute cs so that rs is a suffix" property is maintained.

When we first introduce a Conflictor from nothing, I think it always just
reverts a single prim? That prim is always going to be right before it in the
context so the property is obvious.

Let's suppose we permute the patches in the context of a Conflictor X, i.e.
we might be changing cs. If we just touch Prim patches, the property is maintained
for X because we can always undo do the commutes to get back to the previous cs.

If we touch Conflictors too, I think the logic guarantees that we
don't invert any new prims, just move around where it happens, so cs
should be unchanged.

When we commute conflictor X itself then rs is what might change. I think again
all we are doing is shuffling the prims we already inverted around, and any 
shuffling will involve commute on the prims. So we can also undo those
commutes to get back to the previous rs, which is equivalent to commuting cs so 
that the new rs is a suffix of it.

Following up as requested. I haven't screened them yet, so I can still amend
if I made a mistake or something is still unclear.

On a general note, this is not unlike writing a paper: one the one hand you
want to be as precise and clear as possible, on the other hand you have
limits on the length of the text. I think it is important to keep these
proofs inline with the code, so they should be concise and not too much
frought with formal detail. This is clearly a difficult balancing act!

I am using the re-formulated invariant (2) in the proofs by tacitly assuming
that the "set of conflicts" really coincides with the set of prims from the
context that (in the generalized sense) conflict with the prim represented
by the Conflictor in question.

Regarding your counter-proposal for invariant (2): you have made it clear
that it is not "useless", sorry for claiming that. I still prefer my version
because it more closely corresponds to (and explains) the concept underlying
the "set of conflicts" component of a Conflictor, and (I think) allows for
shorter proofs.

2 patches for repository http://darcs.net/screened:

patch a0fbff5012d0e8cc5402552fa3e384f5b3c8e81d
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed Jul 19 22:48:56 CEST 2023
  * RepoPatchV3: improve definition of invariant (2)

patch 47a8e3d7dea1de5da6cb4e75e4b15b7158fa73ff
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed Jul 19 23:41:06 CEST 2023
  * RepoPatchV3: reword one of the proofs

Attachments

• patch-preview.txt
• repopatchv3_-improve-definition-of-invariant-_2_.dpatch

One more follow-up, not yet screened.

1 patch for repository http://darcs.net/screened:

patch 9b5ed0d55de16416f0c86143b8c914481b0dc59f
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Jul 21 10:29:24 CEST 2023
  * RepoPatchV3: fix yet another proof

  I talked about "conflicts with" here which is completely wrong, it is purely
  about dependency.

Attachments

• patch-preview.txt
• repopatchv3_-fix-yet-another-proof.dpatch

One remark about the proof for

commuteConflicting (lhs@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
  | y == S.singleton cp =
      case ctxView (ctxAddFL r cq) of
        Sealed (NilFL :> q') ->
          Just $ Prim q' :> Conflictor (invert q' :>: r) (cq +| x) cp
        Sealed (c' :> _) ->
          -- Proof that this is impossible:

It relies on a property about sequences of patches in class Ident:

  In any sequence of patches identities must be unique.

Formally:

  forall u,v :: p, (u;ps;v) :: Fl p. ident u /= ident v

(Notation: (;) is concatenating, identifying single patches with singleton 
sequences)

This is, BTW, also needed in order for the instance Ident (FL p) to make 
sense.

Can we prove that from the class laws? Or do we have to add another axiom 
here? So far my attempts to prove it failed...

Ah, forget it: this is only true for "positive patches". If patches 
can be inverted (like for named prims), then this is clearly false.

The property we want is actually

  forall u,u' :: p, (u;ps;u') :: Fl p. ident u == ident u'
  => ps contains some p with ident p = ident u^

If all patches are not invertible then this implies that patch 
identities are unique, but not the other way around.

Coming back to invariant (2).

When I (again: sloppily) wrote that "v depends on u", I was implicitly including 
situations where u and v are not adjacent, i.e. we may have u;p_1;...;p_n;v. 
Formally, for u;v define "v directly depends on u" iff commute(u,v) fails, then 
"depends on" is the transitive closure of "directly depends on".

But that doesn't make sense. Suppose our universe of patches has x;u and x;v, which 
can be merged cleanly to x;u;v', that is, commute(u^;v)=Just(v',_). So v does not 
depend on u^. But we can also form the sequence u^;x^;x;v and now it would appear 
that v does depend (indirectly) on u^ since none of the adjacent pairs in that 
sequence commute!

(How is that possible? I guess the answer is that indeed the transitive closure here 
is trivial i.e. relates any two patches. And this is probably true for any non-
trivial universe of patches.)

So we need a better definition. One possibility is to define "depends on" only for 
the sub-universes of either positive or negative patches. The transitive closure is 
thus taken only over patches with the same polarity (given by the 'positiveId' method 
of class SignedId).

That means the extended definition of "conflicts with" is also valid only if 
restricted to positive patches. I think all the proofs will go through with that 
restriction. We may need an additional invariant (3) stating that all elements of a 
Contexted prim inside a Conflictor are positive. In fact, this is a stated property 
that we test with QC.

I think this also clarifies why we are allowed (and indeed required) to "cancel 
inverses" in Contexted prims, but not anywhere else. And the answer is that what we 
actually do here is removing (positive) prims from the context by "adding inverses". 
The definition of ctxAdd makes this quite clear: the first thing it tries is to 
fastRemoveFL (invert p). So to prove that we maintain invariant (3) we need to show 
that whenever we add a negative prim to a Contexted, it's inverse is already 
contained in it.

I deleted the unscreened follow-up patches in favour of a single patch 
(upcoming) that fixes a few errors, simplifies some of the proofs, and 
(most importantly) takes my latest considerations into account.

The two dependencies (which I would like to screen to get them out of the
way) make minor refactors to the code itself. The changes to the proofs and
definitions are all in the last patch (which is not for screened yet).

I find the theory of the newly introduced relations "positively depends on"
and "positively conflicts with", quite interesting insofar as they clarify
why we need contexted prims. Indeed, the contexts contained in them are
exactly what we need to constructively /calculate/ these relations, provided
they are positive throughout as stated by invariant (3). Perhaps we should
move the definitions to D.P.V3.Contexted?

Another point that became clear to me is that ctxNoConflicts really is a
misnomer. The relation it expresses (again, assuming contexteds contain only
positive prims) is exactly what I called "(positively) unrelated", i.e. they
don't conflict and neither patch depends on the other. A better name would
thus be ctxUnrelated.

One last remark: I am aware that my definition of "positively depends on /
conflicts with" has the disadvantage of not being constructive, because of
the existential quantifiers. Your variant may thus be better suited for full
formalisation. However, I find them quite elegant to use for the sort of
informal reasoning we are doing here.

3 patches for repository http://darcs.net/screened:

patch 6258469bb43380d5f73532d5a7d88a7867f6444e
Author: Ben Franksen <ben.franksen@online.de>
Date:   Sun Jul 23 09:19:35 CEST 2023
  * RepoPatchV3: rename a local variable in commuteConflicting

patch 5a1177c436d5cafe50337833e614c0e81201b0c2
Author: Ben Franksen <ben.franksen@online.de>
Date:   Mon Jul  3 23:02:52 CEST 2023
  * RepoPatchV3 refactor commuteNoConflicts case for two conflictors

  The code now mirrors the corresponding case in cleanMerge exactly.

patch 439bfa608121eb75932c4eb85c430367043a63d1
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Jul 21 21:31:58 CEST 2023
  * WIP RepoPatchV3: refine and fix proofs

Attachments

• patch-preview.txt
• repopatchv3_-rename-a-local-variable-in-commuteconflicting.dpatch

No problem to screen things as convenient.

Couple of initial questions from a first glance:

> It follows from permutivity that "(positively/negatively) depends on" and
> "positively conflicts with" are commutation invariant and therefore depend
> only on the identity of the prims involved.

I don't think this is true by your definitions: for example if p and q
conflict "directly", i.e. cleanMerge (p :\/: q) fails, and p commutes
to p' which lives in a different context, then none of the clauses
for "conflicts with" apply.

I think it's a simple fix though, just start by talking about being able
to commute them to an common context.

> Also, both relations are irreflexive, so any patch is unrelated to itself.

Given we work on NamedPrims, this is sort of true, except that
cleanMerge (p :\/: p) is an error case which confuses the formal definitions
a bit.

> The two dependencies (which I would like to screen to get them out of
> the way) make minor refactors to the code itself.

>     -  commuteNoConflicts _ = Nothing

Did you drop this by mistake? I'm now getting incomplete pattern-match 
warnings for several cases in commuteNoConflicts.

>>     -  commuteNoConflicts _ = Nothing
>
> Did you drop this by mistake? I'm now getting incomplete pattern-match 
> warnings for several cases in commuteNoConflicts.

Ah, yes, removing this line actually belongs to another patch. I'm glad I 
did in fact not yet screen those. Will fix and then send the amended 
refactors separately.

Your observations about my new definitions are both good points, thanks 
for noticing them! More details later.

Re-worked definitions, following up on your latest comments.

1 patch for repository http://darcs.net/screened:

patch 1c9efc791a220f6992895ddd7dea49d1852564d3
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Jul 21 21:31:58 CEST 2023
  * WIP RepoPatchV3: proofs and definitions

Attachments

• patch-preview.txt
• wip-repopatchv3_-proofs-and-definitions.dpatch

Forgot to record a minor change that clarifies invariant (3).

1 patch for repository http://darcs.net/screened:

patch 5d1f8104581b352f09a002bcb4b0c3f1d67f2cc8
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Jul 21 21:31:58 CEST 2023
  * WIP RepoPatchV3: proofs and definitions

Attachments

• patch-preview.txt
• wip-repopatchv3_-proofs-and-definitions.dpatch

> -- (ctxAddInvFL s) adds positive prims

I had to stop and think about this for a bit. I wonder if the code
in general would be easier to read if we made the first parameter to
Conflictor positive, so that all the contained patches are positive?

>> -- (ctxAddInvFL s) adds positive prims
> 
> I had to stop and think about this for a bit. I wonder if the code
> in general would be easier to read if we made the first parameter to
> Conflictor positive, so that all the contained patches are positive?

I have thought about this, too. This is how it was done for RepoPatchV2. In the 
end I decided against that for several reasons. First, I always found the 
witnesses somewhat confusing there. With the way Ian designed it, the prims in 
a conflictor always point rightwards. To me this is the picture that makes the 
most sense when thinking about e.g. how to define commute. Also, in many places 
we do need the effect (as negative prims) for commutation with prims in plain 
or in contexted form. So I think any clarity you may win for ctxAdd* would be 
offset by a loss of clarity when commuting them.

Going to accept this now as I haven't had time to think about it
further for ages, and I think even if the proofs are imperfect
it would be better than not having them.