chiark / gitweb /
73217528caf6f8329960297c22fc687353e5fecf
[topbloke-formulae.git] / article.tex
1 \documentclass[a4paper,leqno]{strayman}
2 \errorcontextlines=50
3 \let\numberwithin=\notdef
4 \usepackage{amsmath}
5 \usepackage{mathabx}
6 \usepackage{txfonts}
7 \usepackage{amsfonts}
8 \usepackage{mdwlist}
9 %\usepackage{accents}
10
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
15
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
18
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
23
24         \newif\ifhidehack\hidehackfalse
25         \DeclareRobustCommand\hidefromedef[2]{%
26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
28
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
32
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
36
37 \newcommand{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
40
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
46
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\nequiv}{\nLeftrightarrow}
50 \renewcommand{\land}{\wedge}
51 \renewcommand{\lor}{\vee}
52
53 \newcommand{\pancs}{{\mathcal A}}
54 \newcommand{\pends}{{\mathcal E}}
55
56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
58
59 \newcommand{\merge}{{\mathcal M}}
60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
62
63 \newcommand{\patch}{{\mathcal P}}
64 \newcommand{\base}{{\mathcal B}}
65
66 \newcommand{\patchof}[1]{\patch ( #1 ) }
67 \newcommand{\baseof}[1]{\base ( #1 ) }
68
69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
71
72 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
73 \newcommand{\bigforall}{%
74   \mathop{\mathchoice%
75     {\hbox{\huge$\forall$}}%
76     {\hbox{\Large$\forall$}}%
77     {\hbox{\normalsize$\forall$}}%
78     {\hbox{\scriptsize$\forall$}}}%
79 }
80
81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
83
84 \newcommand{\qed}{\square}
85 \newcommand{\proofstarts}{{\it Proof:}}
86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
87
88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
89 \newcommand{\gathnext}{\\ \tag*{}}
90
91 \newcommand{\true}{t}
92 \newcommand{\false}{f}
93
94 \begin{document}
95
96 \section{Notation}
97
98 \begin{basedescript}{
99 \desclabelwidth{5em}
100 \desclabelstyle{\nextlinelabel}
101 }
102 \item[ $ C \hasparents \set X $ ]
103 The parents of commit $C$ are exactly the set
104 $\set X$.
105
106 \item[ $ C \ge D $ ]
107 $C$ is a descendant of $D$ in the git commit
108 graph.  This is a partial order, namely the transitive closure of 
109 $ D \in \set X $ where $ C \hasparents \set X $.
110
111 \item[ $ C \has D $ ]
112 Informally, the tree at commit $C$ contains the change
113 made in commit $D$.  Does not take account of deliberate reversions by
114 the user or reversion, rebasing or rewinding in
115 non-Topbloke-controlled branches.  For merges and Topbloke-generated
116 anticommits or re-commits, the ``change made'' is only to be thought
117 of as any conflict resolution.  This is not a partial order because it
118 is not transitive.
119
120 \item[ $ \p, \py, \pn $ ]
121 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
122 are respectively the base and tip git branches.  $\p$ may be used
123 where the context requires a set, in which case the statement
124 is to be taken as applying to both $\py$ and $\pn$.
125 None of these sets overlap.  Hence:
126
127 \item[ $ \patchof{ C } $ ]
128 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
129 A function from commits to patches' sets $\p$.
130
131 \item[ $ \pancsof{C}{\set P} $ ]
132 $ \{ A \; | \; A \le C \land A \in \set P \} $ 
133 i.e. all the ancestors of $C$
134 which are in $\set P$.
135
136 \item[ $ \pendsof{C}{\set P} $ ]
137 $ \{ E \; | \; E \in \pancsof{C}{\set P}
138   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
139   E \neq A \land E \le A \} $ 
140 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
141
142 \item[ $ \baseof{C} $ ]
143 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
144 A partial function from commits to commits.
145 See Unique Base, below.
146
147 \item[ $ C \haspatch \p $ ]
148 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
149 ~ Informally, $C$ has the contents of $\p$.
150
151 \item[ $ C \nothaspatch \p $ ]
152 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
153 ~ Informally, $C$ has none of the contents of $\p$.  
154
155 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
156 includes commits on plain git branches made by applying a Topbloke
157 patch.  If a Topbloke
158 patch is applied to a non-Topbloke branch and then bubbles back to
159 the relevant Topbloke branches, we hope that 
160 if the user still cares about the Topbloke patch,
161 git's merge algorithm will DTRT when trying to re-apply the changes.
162
163 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
164 The contents of a git merge result:
165
166 $\displaystyle D \isin C \equiv
167   \begin{cases}
168     (D \isin L \land D \isin R) \lor D = C : & \true \\
169     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
170     \text{otherwise} : & D \not\isin M
171   \end{cases}
172
173
174 \end{basedescript}
175 \newpage
176 \section{Invariants}
177
178 We maintain these each time we construct a new commit. \\
179 \[ \eqn{No Replay:}{
180   C \has D \implies C \ge D
181 }\]
182 \[\eqn{Unique Base:}{
183  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
184 }\]
185 \[\eqn{Tip Contents:}{
186   \bigforall_{C \in \py} D \isin C \equiv
187     { D \isin \baseof{C} \lor \atop
188       (D \in \py \land D \le C) }
189 }\]
190 \[\eqn{Base Acyclic:}{
191   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
192 }\]
193 \[\eqn{Coherence:}{
194   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
195 }\]
196 \[\eqn{Foreign Inclusion:}{
197   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
198 }\]
199
200 \section{Some lemmas}
201
202 \[ \eqn{Alternative (overlapping) formulations defining
203   $\mergeof{C}{L}{M}{R}$:}{
204  D \isin C \equiv
205   \begin{cases}
206     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
207     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
208     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
209     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
210     \text{as above with L and R exchanged}
211   \end{cases}
212 }\]
213 \proof{
214   Truth table xxx
215
216   Original definition is symmetrical in $L$ and $R$.
217 }
218
219 \[ \eqn{Exclusive Tip Contents:}{
220   \bigforall_{C \in \py} 
221     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
222       \Bigr]
223 }\]
224 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
225
226 \proof{
227 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
228 So by Base Acyclic $D \isin B \implies D \notin \py$.
229 }
230 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
231   \bigforall_{C \in \py} D \isin C \equiv
232   \begin{cases}
233     D \in \py : & D \le C \\
234     D \not\in \py : & D \isin \baseof{C}
235   \end{cases}
236 }\]
237
238 \[ \eqn{Tip Self Inpatch:}{
239   \bigforall_{C \in \py} C \haspatch \p
240 }\]
241 Ie, tip commits contain their own patch.
242
243 \proof{
244 Apply Exclusive Tip Contents to some $D \in \py$:
245 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
246   D \isin C \equiv D \le C $
247 }
248
249 \[ \eqn{Exact Ancestors:}{
250   \bigforall_{ C \hasparents \set{R} }
251   D \le C \equiv
252     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
253     \lor D = C
254 }\]
255 xxx proof tbd
256
257 \[ \eqn{Transitive Ancestors:}{
258   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
259   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
260 }\]
261
262 \proof{
263 The implication from right to left is trivial because
264 $ \pends() \subset \pancs() $.
265 For the implication from left to right: 
266 by the definition of $\mathcal E$,
267 for every such $A$, either $A \in \pends()$ which implies
268 $A \le M$ by the LHS directly,
269 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
270 in which case we repeat for $A'$.  Since there are finitely many
271 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
272 by the LHS.  And $A \le A''$.
273 }
274
275 \[ \eqn{Calculation Of Ends:}{
276   \bigforall_{C \hasparents \set A}
277     \pendsof{C}{\set P} =
278       \begin{cases}
279        C \in \p : & \{ C \}
280       \\
281        C \not\in \p : & \displaystyle
282        \left\{ E \Big|
283            \Bigl[ \Largeexists_{A \in \set A} 
284                        E \in \pendsof{A}{\set P} \Bigr] \land
285            \Bigl[ \Largenexists_{B \in \set A} 
286                        E \neq B \land E \le B \Bigr]
287        \right\}
288       \end{cases}
289 }\]
290 xxx proof tbd
291
292 \subsection{No Replay for Merge Results}
293
294 If we are constructing $C$, with,
295 \gathbegin
296   \mergeof{C}{L}{M}{R}
297 \gathnext
298   L \le C
299 \gathnext
300   R \le C
301 \end{gather}
302 No Replay is preserved.  \proofstarts
303
304 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
305
306 \subsubsection{For $D \isin L \land D \isin R$:}
307 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
308
309 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
310 $D \not\isin C$.  OK.
311
312 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
313  \land D \not\isin M$:}
314 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
315 R$ so $D \le C$.  OK.
316
317 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
318  \land D \isin M$:}
319 $D \not\isin C$.  OK.
320
321 $\qed$
322
323 \section{Commit annotation}
324
325 We annotate each Topbloke commit $C$ with:
326 \gathbegin
327  \patchof{C}
328 \gathnext
329  \baseof{C}, \text{ if } C \in \py
330 \gathnext
331  \bigforall_{\pa{Q}} 
332    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
333 \gathnext
334  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
335 \end{gather}
336
337 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
338 in the summary in the section for that kind of commit.
339
340 Whether $\baseof{C}$ is required, and if so what the value is, is
341 stated in the proof of Unique Base for each kind of commit.
342
343 $C \haspatch \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
344 set $\{ \pa{Q} | C \haspatch \pa{Q} \}$.  Whether $C \haspatch \pa{Q}$
345 is in stated
346 (in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
347 for the ingredients $I$),
348 in the proof of Coherence for each kind of commit.
349
350 $\pendsof{C}{\pa{Q}^+}$ is computed, for all Topbloke-generated commits,
351 using the lemma Calculation of Ends, above.
352 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
353 make it wrong to make plain commits with git because the recorded $\pends$
354 would have to be updated.  The annotation is not needed in that case
355 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
356
357 \section{Simple commit}
358
359 A simple single-parent forward commit $C$ as made by git-commit.
360 \begin{gather}
361 \tag*{} C \hasparents \{ A \} \\
362 \tag*{} \patchof{C} = \patchof{A} \\
363 \tag*{} D \isin C \equiv D \isin A \lor D = C
364 \end{gather}
365 This also covers Topbloke-generated commits on plain git branches:
366 Topbloke strips the metadata when exporting.
367
368 \subsection{No Replay}
369 Trivial.
370
371 \subsection{Unique Base}
372 If $A, C \in \py$ then by Calculation of Ends for
373 $C, \py, C \not\in \py$:
374 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
375 $\baseof{C} = \baseof{A}$. $\qed$
376
377 \subsection{Tip Contents}
378 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
379 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
380 Substitute into the contents of $C$:
381 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
382     \lor D = C \]
383 Since $D = C \implies D \in \py$, 
384 and substituting in $\baseof{C}$, this gives:
385 \[ D \isin C \equiv D \isin \baseof{C} \lor
386     (D \in \py \land D \le A) \lor
387     (D = C \land D \in \py) \]
388 \[ \equiv D \isin \baseof{C} \lor
389    [ D \in \py \land ( D \le A \lor D = C ) ] \]
390 So by Exact Ancestors:
391 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
392 ) \]
393 $\qed$
394
395 \subsection{Base Acyclic}
396
397 Need to consider only $A, C \in \pn$.  
398
399 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
400
401 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
402 $A$, $D \isin C \implies D \not\in \py$.
403
404 $\qed$
405
406 \subsection{Coherence and patch inclusion}
407
408 Need to consider $D \in \py$
409
410 \subsubsection{For $A \haspatch P, D = C$:}
411
412 Ancestors of $C$:
413 $ D \le C $.
414
415 Contents of $C$:
416 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
417
418 \subsubsection{For $A \haspatch P, D \neq C$:}
419 Ancestors: $ D \le C \equiv D \le A $.
420
421 Contents: $ D \isin C \equiv D \isin A \lor f $
422 so $ D \isin C \equiv D \isin A $.
423
424 So:
425 \[ A \haspatch P \implies C \haspatch P \]
426
427 \subsubsection{For $A \nothaspatch P$:}
428
429 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
430 Thus $D \neq C$.
431
432 Now by contents of $A$, $D \notin A$, so $D \notin C$.
433
434 So:
435 \[ A \nothaspatch P \implies C \nothaspatch P \]
436 $\qed$
437
438 \subsection{Foreign inclusion:}
439
440 If $D = C$, trivial.  For $D \neq C$:
441 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
442
443 \section{Create Base}
444
445 Given $L$, create a Topbloke base branch initial commit $B$.
446 \gathbegin
447  B \hasparents \{ L \}
448 \gathnext
449  \patchof{B} = \pa{B}
450 \gathnext
451  D \isin B \equiv D \isin L \lor D = B
452 \end{gather}
453
454 \subsection{Conditions}
455
456 \[ \eqn{ Ingredients }{
457  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
458 }\]
459 \[ \eqn{ Non-recursion }{
460  L \not\in \pa{B}
461 }\]
462
463 \subsection{No Replay}
464
465 If $\patchof{L} = \pa{L}$, trivial by Base Acyclic for $L$.
466
467 If $\patchof{L} = \bot$, xxx
468
469 Trivial from Base Acyclic for $L$.  $\qed$
470
471 \subsection{Unique Base}
472
473 Not applicable. $\qed$
474
475 \subsection{Tip Contents}
476
477 Not applicable. $\qed$
478
479 \subsection{Base Acyclic}
480
481 xxx
482
483 xxx unfinished
484
485 \section{Create Tip}
486
487 xxx tbd
488
489 \section{Anticommit}
490
491 Given $L$ and $\pr$ as represented by $R^+, R^-$.
492 Construct $C$ which has $\pr$ removed.
493 Used for removing a branch dependency.
494 \gathbegin
495  C \hasparents \{ L \}
496 \gathnext
497  \patchof{C} = \patchof{L}
498 \gathnext
499  \mergeof{C}{L}{R^+}{R^-}
500 \end{gather}
501
502 \subsection{Conditions}
503
504 \[ \eqn{ Ingredients }{
505 R^+ \in \pry \land R^- = \baseof{R^+}
506 }\]
507 \[ \eqn{ Into Base }{
508  L \in \pn
509 }\]
510 \[ \eqn{ Unique Tip }{
511  \pendsof{L}{\pry} = \{ R^+ \}
512 }\]
513 \[ \eqn{ Currently Included }{
514  L \haspatch \pry
515 }\]
516
517 \subsection{Ordering of ${L, R^+, R^-}$:}
518
519 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
520 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
521 $\qed$
522
523 (Note that $R^+ \not\le R^-$, i.e. the merge base
524 is a descendant, not an ancestor, of the 2nd parent.)
525
526 \subsection{No Replay}
527
528 No Replay for Merge Results applies.  $\qed$
529
530 \subsection{Desired Contents}
531
532 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
533 \proofstarts
534
535 \subsubsection{For $D = C$:}
536
537 Trivially $D \isin C$.  OK.
538
539 \subsubsection{For $D \neq C, D \not\le L$:}
540
541 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
542 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
543
544 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
545
546 By Currently Included, $D \isin L$.
547
548 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
549 by Unique Tip, $D \le R^+ \equiv D \le L$.  
550 So $D \isin R^+$.
551
552 By Base Acyclic, $D \not\isin R^-$.
553
554 Apply $\merge$: $D \not\isin C$.  OK.
555
556 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
557
558 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
559
560 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
561
562 $\qed$
563
564 \subsection{Unique Base}
565
566 Into Base means that $C \in \pn$, so Unique Base is not
567 applicable. $\qed$
568
569 \subsection{Tip Contents}
570
571 Again, not applicable. $\qed$
572
573 \subsection{Base Acyclic}
574
575 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
576 And by Into Base $C \not\in \py$.
577 Now from Desired Contents, above, $D \isin C
578 \implies D \isin L \lor D = C$, which thus
579 $\implies D \not\in \py$.  $\qed$.
580
581 \subsection{Coherence and Patch Inclusion}
582
583 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
584
585 \subsubsection{For $\p = \pr$:}
586 By Desired Contents, above, $D \not\isin C$.
587 So $C \nothaspatch \pr$.
588
589 \subsubsection{For $\p \neq \pr$:}
590 By Desired Contents, $D \isin C \equiv D \isin L$
591 (since $D \in \py$ so $D \not\in \pry$).
592
593 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
594 So $L \nothaspatch \p \implies C \nothaspatch \p$.
595
596 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
597 so $L \haspatch \p \implies C \haspatch \p$.
598
599 $\qed$
600
601 \subsection{Foreign Inclusion}
602
603 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
604 So by Desired Contents $D \isin C \equiv D \isin L$.
605 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
606
607 And $D \le C \equiv D \le L$.
608 Thus $D \isin C \equiv D \le C$.
609
610 $\qed$
611
612 \section{Merge}
613
614 Merge commits $L$ and $R$ using merge base $M$:
615 \gathbegin
616  C \hasparents \{ L, R \}
617 \gathnext
618  \patchof{C} = \patchof{L}
619 \gathnext
620  \mergeof{C}{L}{M}{R}
621 \end{gather}
622 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
623
624 \subsection{Conditions}
625 \[ \eqn{ Ingredients }{
626  M \le L, M \le R
627 }\]
628 \[ \eqn{ Tip Merge }{
629  L \in \py \implies
630    \begin{cases}
631       R \in \py : & \baseof{R} \ge \baseof{L}
632               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
633       R \in \pn : & M = \baseof{L} \\
634       \text{otherwise} : & \false
635    \end{cases}
636 }\]
637 \[ \eqn{ Merge Acyclic }{
638     L \in \pn
639    \implies
640     R \nothaspatch \p
641 }\]
642 \[ \eqn{ Removal Merge Ends }{
643     X \not\haspatch \p \land
644     Y \haspatch \p \land
645     M \haspatch \p
646   \implies
647     \pendsof{Y}{\py} = \pendsof{M}{\py}
648 }\]
649 \[ \eqn{ Addition Merge Ends }{
650     X \not\haspatch \p \land
651     Y \haspatch \p \land
652     M \nothaspatch \p
653    \implies \left[
654     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
655    \right]
656 }\]
657
658 \subsection{Non-Topbloke merges}
659
660 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
661 I.e. not only is it forbidden to merge into a Topbloke-controlled
662 branch without Topbloke's assistance, it is also forbidden to
663 merge any Topbloke-controlled branch into any plain git branch.
664
665 Given those conditions, Tip Merge and Merge Acyclic do not apply.
666 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
667 Merge Ends condition applies.  Good.
668
669 \subsection{No Replay}
670
671 No Replay for Merge Results applies.  $\qed$
672
673 \subsection{Unique Base}
674
675 Need to consider only $C \in \py$, ie $L \in \py$,
676 and calculate $\pendsof{C}{\pn}$.  So we will consider some
677 putative ancestor $A \in \pn$ and see whether $A \le C$.
678
679 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
680 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
681 Thus $A \le C \equiv A \le L \lor A \le R$.
682
683 By Unique Base of L and Transitive Ancestors,
684 $A \le L \equiv A \le \baseof{L}$.
685
686 \subsubsection{For $R \in \py$:}
687
688 By Unique Base of $R$ and Transitive Ancestors,
689 $A \le R \equiv A \le \baseof{R}$.
690
691 But by Tip Merge condition on $\baseof{R}$,
692 $A \le \baseof{L} \implies A \le \baseof{R}$, so
693 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
694 Thus $A \le C \equiv A \le \baseof{R}$.  
695 That is, $\baseof{C} = \baseof{R}$.
696
697 \subsubsection{For $R \in \pn$:}
698
699 By Tip Merge condition on $R$ and since $M \le R$,
700 $A \le \baseof{L} \implies A \le R$, so
701 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
702 Thus $A \le C \equiv A \le R$.  
703 That is, $\baseof{C} = R$.
704
705 $\qed$
706
707 \subsection{Coherence and Patch Inclusion}
708
709 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
710 This involves considering $D \in \py$.  
711
712 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
713 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
714 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
715 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
716
717 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
718 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
719 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
720
721 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
722
723 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
724  \equiv D \isin L \lor D \isin R$.  
725 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
726
727 Consider $D \neq C, D \isin X \land D \isin Y$:
728 By $\merge$, $D \isin C$.  Also $D \le X$ 
729 so $D \le C$.  OK for $C \haspatch \p$.
730
731 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
732 By $\merge$, $D \not\isin C$.  
733 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
734 OK for $C \haspatch \p$.
735
736 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
737 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
738 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
739 OK for $C \haspatch \p$.
740
741 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
742
743 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
744
745 $M \haspatch \p \implies C \nothaspatch \p$.
746 $M \nothaspatch \p \implies C \haspatch \p$.
747
748 \proofstarts
749
750 One of the Merge Ends conditions applies.  
751 Recall that we are considering $D \in \py$.
752 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
753 We will show for each of
754 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
755 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
756
757 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
758 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
759 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
760 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
761
762 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
763 $D \le Y$ so $D \le C$.  
764 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
765
766 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
767 $D \not\le Y$.  If $D \le X$ then
768 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
769 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
770 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
771
772 Consider $D \neq C, M \haspatch P, D \isin Y$:
773 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
774 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
775 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
776
777 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
778 By $\merge$, $D \not\isin C$.  OK.
779
780 $\qed$
781
782 \subsection{Base Acyclic}
783
784 This applies when $C \in \pn$.
785 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
786
787 Consider some $D \in \py$.
788
789 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
790 R$.  And $D \neq C$.  So $D \not\isin C$.
791
792 $\qed$
793
794 \subsection{Tip Contents}
795
796 We need worry only about $C \in \py$.  
797 And $\patchof{C} = \patchof{L}$
798 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
799 of $C$, and its Coherence and Patch Inclusion, as just proved.
800
801 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
802 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
803 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
804 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
805 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
806
807 We will consider an arbitrary commit $D$
808 and prove the Exclusive Tip Contents form.
809
810 \subsubsection{For $D \in \py$:}
811 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
812 \le C$.  OK.
813
814 \subsubsection{For $D \not\in \py, R \not\in \py$:}
815
816 $D \neq C$.  By Tip Contents of $L$,
817 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
818 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
819 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
820 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
821
822 \subsubsection{For $D \not\in \py, R \in \py$:}
823
824 $D \neq C$.
825
826 By Tip Contents
827 $D \isin L \equiv D \isin \baseof{L}$ and
828 $D \isin R \equiv D \isin \baseof{R}$.
829
830 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
831 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
832 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
833 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
834
835 So $D \isin M \equiv D \isin L$ and by $\merge$,
836 $D \isin C \equiv D \isin R$.  But from Unique Base,
837 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
838
839 $\qed$
840
841 \subsection{Foreign Inclusion}
842
843 Consider some $D$ s.t. $\patchof{D} = \bot$.
844 By Foreign Inclusion of $L, M, R$:
845 $D \isin L \equiv D \le L$;
846 $D \isin M \equiv D \le M$;
847 $D \isin R \equiv D \le R$.
848
849 \subsubsection{For $D = C$:}
850
851 $D \isin C$ and $D \le C$.  OK.
852
853 \subsubsection{For $D \neq C, D \isin M$:}
854
855 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
856 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
857
858 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
859
860 By $\merge$, $D \isin C$.
861 And $D \isin X$ means $D \le X$ so $D \le C$.
862 OK.
863
864 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
865
866 By $\merge$, $D \not\isin C$.
867 And $D \not\le L, D \not\le R$ so $D \not\le C$.
868 OK
869
870 $\qed$
871
872 \end{document}